Mathbox for Glauco Siliprandi < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  stoweidlem26 Structured version   Visualization version   GIF version

Theorem stoweidlem26 40561
 Description: This lemma is used to prove that there is a function 𝑔 as in the proof of [BrosowskiDeutsh] p. 92: this lemma proves that g(t) > ( j - 4 / 3 ) * ε. Here 𝐿 is used to represnt j in the paper, 𝐷 is used to represent A in the paper, 𝑆 is used to represent t, and 𝐸 is used to represent ε. (Contributed by Glauco Siliprandi, 20-Apr-2017.)
Hypotheses
Ref Expression
stoweidlem26.1 𝑡𝐹
stoweidlem26.2 𝑗𝜑
stoweidlem26.3 𝑡𝜑
stoweidlem26.4 𝐷 = (𝑗 ∈ (0...𝑁) ↦ {𝑡𝑇 ∣ (𝐹𝑡) ≤ ((𝑗 − (1 / 3)) · 𝐸)})
stoweidlem26.5 𝐵 = (𝑗 ∈ (0...𝑁) ↦ {𝑡𝑇 ∣ ((𝑗 + (1 / 3)) · 𝐸) ≤ (𝐹𝑡)})
stoweidlem26.6 (𝜑𝑁 ∈ ℕ)
stoweidlem26.7 (𝜑𝑇 ∈ V)
stoweidlem26.8 (𝜑𝐿 ∈ (1...𝑁))
stoweidlem26.9 (𝜑𝑆 ∈ ((𝐷𝐿) ∖ (𝐷‘(𝐿 − 1))))
stoweidlem26.10 (𝜑𝐹:𝑇⟶ℝ)
stoweidlem26.11 (𝜑𝐸 ∈ ℝ+)
stoweidlem26.12 (𝜑𝐸 < (1 / 3))
stoweidlem26.13 ((𝜑𝑖 ∈ (0...𝑁)) → (𝑋𝑖):𝑇⟶ℝ)
stoweidlem26.14 ((𝜑𝑖 ∈ (0...𝑁) ∧ 𝑡𝑇) → 0 ≤ ((𝑋𝑖)‘𝑡))
stoweidlem26.15 ((𝜑𝑖 ∈ (0...𝑁) ∧ 𝑡 ∈ (𝐵𝑖)) → (1 − (𝐸 / 𝑁)) < ((𝑋𝑖)‘𝑡))
Assertion
Ref Expression
stoweidlem26 (𝜑 → ((𝐿 − (4 / 3)) · 𝐸) < ((𝑡𝑇 ↦ Σ𝑖 ∈ (0...𝑁)(𝐸 · ((𝑋𝑖)‘𝑡)))‘𝑆))
Distinct variable groups:   𝑖,𝑗,𝑡,𝐸   𝑖,𝐿,𝑗,𝑡   𝑖,𝑁,𝑗,𝑡   𝑆,𝑖,𝑡   𝜑,𝑖   𝑗,𝐹   𝑇,𝑗,𝑡   𝑡,𝑋
Allowed substitution hints:   𝜑(𝑡,𝑗)   𝐵(𝑡,𝑖,𝑗)   𝐷(𝑡,𝑖,𝑗)   𝑆(𝑗)   𝑇(𝑖)   𝐹(𝑡,𝑖)   𝑋(𝑖,𝑗)

Proof of Theorem stoweidlem26
StepHypRef Expression
1 1re 10077 . . . . . . . 8 1 ∈ ℝ
2 eleq1 2718 . . . . . . . 8 (𝐿 = 1 → (𝐿 ∈ ℝ ↔ 1 ∈ ℝ))
31, 2mpbiri 248 . . . . . . 7 (𝐿 = 1 → 𝐿 ∈ ℝ)
43adantl 481 . . . . . 6 ((𝜑𝐿 = 1) → 𝐿 ∈ ℝ)
5 4re 11135 . . . . . . . 8 4 ∈ ℝ
65a1i 11 . . . . . . 7 ((𝜑𝐿 = 1) → 4 ∈ ℝ)
7 3re 11132 . . . . . . . 8 3 ∈ ℝ
87a1i 11 . . . . . . 7 ((𝜑𝐿 = 1) → 3 ∈ ℝ)
9 3ne0 11153 . . . . . . . 8 3 ≠ 0
109a1i 11 . . . . . . 7 ((𝜑𝐿 = 1) → 3 ≠ 0)
116, 8, 10redivcld 10891 . . . . . 6 ((𝜑𝐿 = 1) → (4 / 3) ∈ ℝ)
124, 11resubcld 10496 . . . . 5 ((𝜑𝐿 = 1) → (𝐿 − (4 / 3)) ∈ ℝ)
13 stoweidlem26.11 . . . . . . 7 (𝜑𝐸 ∈ ℝ+)
1413rpred 11910 . . . . . 6 (𝜑𝐸 ∈ ℝ)
1514adantr 480 . . . . 5 ((𝜑𝐿 = 1) → 𝐸 ∈ ℝ)
1612, 15remulcld 10108 . . . 4 ((𝜑𝐿 = 1) → ((𝐿 − (4 / 3)) · 𝐸) ∈ ℝ)
17 0red 10079 . . . 4 ((𝜑𝐿 = 1) → 0 ∈ ℝ)
18 fzfid 12812 . . . . . 6 (𝜑 → (0...𝑁) ∈ Fin)
1914adantr 480 . . . . . . 7 ((𝜑𝑖 ∈ (0...𝑁)) → 𝐸 ∈ ℝ)
20 stoweidlem26.13 . . . . . . . 8 ((𝜑𝑖 ∈ (0...𝑁)) → (𝑋𝑖):𝑇⟶ℝ)
21 stoweidlem26.9 . . . . . . . . . . . . . 14 (𝜑𝑆 ∈ ((𝐷𝐿) ∖ (𝐷‘(𝐿 − 1))))
22 eldif 3617 . . . . . . . . . . . . . 14 (𝑆 ∈ ((𝐷𝐿) ∖ (𝐷‘(𝐿 − 1))) ↔ (𝑆 ∈ (𝐷𝐿) ∧ ¬ 𝑆 ∈ (𝐷‘(𝐿 − 1))))
2321, 22sylib 208 . . . . . . . . . . . . 13 (𝜑 → (𝑆 ∈ (𝐷𝐿) ∧ ¬ 𝑆 ∈ (𝐷‘(𝐿 − 1))))
2423simpld 474 . . . . . . . . . . . 12 (𝜑𝑆 ∈ (𝐷𝐿))
25 fz1ssfz0 12474 . . . . . . . . . . . . . 14 (1...𝑁) ⊆ (0...𝑁)
26 stoweidlem26.8 . . . . . . . . . . . . . 14 (𝜑𝐿 ∈ (1...𝑁))
2725, 26sseldi 3634 . . . . . . . . . . . . 13 (𝜑𝐿 ∈ (0...𝑁))
28 stoweidlem26.7 . . . . . . . . . . . . . 14 (𝜑𝑇 ∈ V)
29 rabexg 4844 . . . . . . . . . . . . . 14 (𝑇 ∈ V → {𝑡𝑇 ∣ (𝐹𝑡) ≤ ((𝐿 − (1 / 3)) · 𝐸)} ∈ V)
3028, 29syl 17 . . . . . . . . . . . . 13 (𝜑 → {𝑡𝑇 ∣ (𝐹𝑡) ≤ ((𝐿 − (1 / 3)) · 𝐸)} ∈ V)
31 oveq1 6697 . . . . . . . . . . . . . . . . 17 (𝑗 = 𝐿 → (𝑗 − (1 / 3)) = (𝐿 − (1 / 3)))
3231oveq1d 6705 . . . . . . . . . . . . . . . 16 (𝑗 = 𝐿 → ((𝑗 − (1 / 3)) · 𝐸) = ((𝐿 − (1 / 3)) · 𝐸))
3332breq2d 4697 . . . . . . . . . . . . . . 15 (𝑗 = 𝐿 → ((𝐹𝑡) ≤ ((𝑗 − (1 / 3)) · 𝐸) ↔ (𝐹𝑡) ≤ ((𝐿 − (1 / 3)) · 𝐸)))
3433rabbidv 3220 . . . . . . . . . . . . . 14 (𝑗 = 𝐿 → {𝑡𝑇 ∣ (𝐹𝑡) ≤ ((𝑗 − (1 / 3)) · 𝐸)} = {𝑡𝑇 ∣ (𝐹𝑡) ≤ ((𝐿 − (1 / 3)) · 𝐸)})
35 stoweidlem26.4 . . . . . . . . . . . . . 14 𝐷 = (𝑗 ∈ (0...𝑁) ↦ {𝑡𝑇 ∣ (𝐹𝑡) ≤ ((𝑗 − (1 / 3)) · 𝐸)})
3634, 35fvmptg 6319 . . . . . . . . . . . . 13 ((𝐿 ∈ (0...𝑁) ∧ {𝑡𝑇 ∣ (𝐹𝑡) ≤ ((𝐿 − (1 / 3)) · 𝐸)} ∈ V) → (𝐷𝐿) = {𝑡𝑇 ∣ (𝐹𝑡) ≤ ((𝐿 − (1 / 3)) · 𝐸)})
3727, 30, 36syl2anc 694 . . . . . . . . . . . 12 (𝜑 → (𝐷𝐿) = {𝑡𝑇 ∣ (𝐹𝑡) ≤ ((𝐿 − (1 / 3)) · 𝐸)})
3824, 37eleqtrd 2732 . . . . . . . . . . 11 (𝜑𝑆 ∈ {𝑡𝑇 ∣ (𝐹𝑡) ≤ ((𝐿 − (1 / 3)) · 𝐸)})
39 nfcv 2793 . . . . . . . . . . . 12 𝑡𝑆
40 nfcv 2793 . . . . . . . . . . . 12 𝑡𝑇
41 stoweidlem26.1 . . . . . . . . . . . . . 14 𝑡𝐹
4241, 39nffv 6236 . . . . . . . . . . . . 13 𝑡(𝐹𝑆)
43 nfcv 2793 . . . . . . . . . . . . 13 𝑡
44 nfcv 2793 . . . . . . . . . . . . 13 𝑡((𝐿 − (1 / 3)) · 𝐸)
4542, 43, 44nfbr 4732 . . . . . . . . . . . 12 𝑡(𝐹𝑆) ≤ ((𝐿 − (1 / 3)) · 𝐸)
46 fveq2 6229 . . . . . . . . . . . . 13 (𝑡 = 𝑆 → (𝐹𝑡) = (𝐹𝑆))
4746breq1d 4695 . . . . . . . . . . . 12 (𝑡 = 𝑆 → ((𝐹𝑡) ≤ ((𝐿 − (1 / 3)) · 𝐸) ↔ (𝐹𝑆) ≤ ((𝐿 − (1 / 3)) · 𝐸)))
4839, 40, 45, 47elrabf 3392 . . . . . . . . . . 11 (𝑆 ∈ {𝑡𝑇 ∣ (𝐹𝑡) ≤ ((𝐿 − (1 / 3)) · 𝐸)} ↔ (𝑆𝑇 ∧ (𝐹𝑆) ≤ ((𝐿 − (1 / 3)) · 𝐸)))
4938, 48sylib 208 . . . . . . . . . 10 (𝜑 → (𝑆𝑇 ∧ (𝐹𝑆) ≤ ((𝐿 − (1 / 3)) · 𝐸)))
5049simpld 474 . . . . . . . . 9 (𝜑𝑆𝑇)
5150adantr 480 . . . . . . . 8 ((𝜑𝑖 ∈ (0...𝑁)) → 𝑆𝑇)
5220, 51ffvelrnd 6400 . . . . . . 7 ((𝜑𝑖 ∈ (0...𝑁)) → ((𝑋𝑖)‘𝑆) ∈ ℝ)
5319, 52remulcld 10108 . . . . . 6 ((𝜑𝑖 ∈ (0...𝑁)) → (𝐸 · ((𝑋𝑖)‘𝑆)) ∈ ℝ)
5418, 53fsumrecl 14509 . . . . 5 (𝜑 → Σ𝑖 ∈ (0...𝑁)(𝐸 · ((𝑋𝑖)‘𝑆)) ∈ ℝ)
5554adantr 480 . . . 4 ((𝜑𝐿 = 1) → Σ𝑖 ∈ (0...𝑁)(𝐸 · ((𝑋𝑖)‘𝑆)) ∈ ℝ)
565, 7, 9redivcli 10830 . . . . . . 7 (4 / 3) ∈ ℝ
5756a1i 11 . . . . . 6 ((𝜑𝐿 = 1) → (4 / 3) ∈ ℝ)
584, 57resubcld 10496 . . . . 5 ((𝜑𝐿 = 1) → (𝐿 − (4 / 3)) ∈ ℝ)
594recnd 10106 . . . . . . . 8 ((𝜑𝐿 = 1) → 𝐿 ∈ ℂ)
6059subid1d 10419 . . . . . . 7 ((𝜑𝐿 = 1) → (𝐿 − 0) = 𝐿)
61 3cn 11133 . . . . . . . . . 10 3 ∈ ℂ
6261, 9dividi 10796 . . . . . . . . 9 (3 / 3) = 1
63 3lt4 11235 . . . . . . . . . 10 3 < 4
64 3pos 11152 . . . . . . . . . . 11 0 < 3
657, 5, 7, 64ltdiv1ii 10991 . . . . . . . . . 10 (3 < 4 ↔ (3 / 3) < (4 / 3))
6663, 65mpbi 220 . . . . . . . . 9 (3 / 3) < (4 / 3)
6762, 66eqbrtrri 4708 . . . . . . . 8 1 < (4 / 3)
68 breq1 4688 . . . . . . . . 9 (𝐿 = 1 → (𝐿 < (4 / 3) ↔ 1 < (4 / 3)))
6968adantl 481 . . . . . . . 8 ((𝜑𝐿 = 1) → (𝐿 < (4 / 3) ↔ 1 < (4 / 3)))
7067, 69mpbiri 248 . . . . . . 7 ((𝜑𝐿 = 1) → 𝐿 < (4 / 3))
7160, 70eqbrtrd 4707 . . . . . 6 ((𝜑𝐿 = 1) → (𝐿 − 0) < (4 / 3))
724, 17, 57, 71ltsub23d 10670 . . . . 5 ((𝜑𝐿 = 1) → (𝐿 − (4 / 3)) < 0)
7313rpgt0d 11913 . . . . . 6 (𝜑 → 0 < 𝐸)
7473adantr 480 . . . . 5 ((𝜑𝐿 = 1) → 0 < 𝐸)
75 mulltgt0 39495 . . . . 5 ((((𝐿 − (4 / 3)) ∈ ℝ ∧ (𝐿 − (4 / 3)) < 0) ∧ (𝐸 ∈ ℝ ∧ 0 < 𝐸)) → ((𝐿 − (4 / 3)) · 𝐸) < 0)
7658, 72, 15, 74, 75syl22anc 1367 . . . 4 ((𝜑𝐿 = 1) → ((𝐿 − (4 / 3)) · 𝐸) < 0)
77 0cn 10070 . . . . . . . 8 0 ∈ ℂ
78 fsumconst 14566 . . . . . . . 8 (((0...𝑁) ∈ Fin ∧ 0 ∈ ℂ) → Σ𝑖 ∈ (0...𝑁)0 = ((#‘(0...𝑁)) · 0))
7918, 77, 78sylancl 695 . . . . . . 7 (𝜑 → Σ𝑖 ∈ (0...𝑁)0 = ((#‘(0...𝑁)) · 0))
80 hashcl 13185 . . . . . . . . 9 ((0...𝑁) ∈ Fin → (#‘(0...𝑁)) ∈ ℕ0)
81 nn0cn 11340 . . . . . . . . 9 ((#‘(0...𝑁)) ∈ ℕ0 → (#‘(0...𝑁)) ∈ ℂ)
8218, 80, 813syl 18 . . . . . . . 8 (𝜑 → (#‘(0...𝑁)) ∈ ℂ)
8382mul01d 10273 . . . . . . 7 (𝜑 → ((#‘(0...𝑁)) · 0) = 0)
8479, 83eqtrd 2685 . . . . . 6 (𝜑 → Σ𝑖 ∈ (0...𝑁)0 = 0)
8584adantr 480 . . . . 5 ((𝜑𝐿 = 1) → Σ𝑖 ∈ (0...𝑁)0 = 0)
86 0red 10079 . . . . . . 7 ((𝜑𝑖 ∈ (0...𝑁)) → 0 ∈ ℝ)
8713rpge0d 11914 . . . . . . . . 9 (𝜑 → 0 ≤ 𝐸)
8887adantr 480 . . . . . . . 8 ((𝜑𝑖 ∈ (0...𝑁)) → 0 ≤ 𝐸)
89 stoweidlem26.3 . . . . . . . . . . . 12 𝑡𝜑
90 nfv 1883 . . . . . . . . . . . 12 𝑡 𝑖 ∈ (0...𝑁)
9189, 90nfan 1868 . . . . . . . . . . 11 𝑡(𝜑𝑖 ∈ (0...𝑁))
92 nfv 1883 . . . . . . . . . . 11 𝑡0 ≤ ((𝑋𝑖)‘𝑆)
9391, 92nfim 1865 . . . . . . . . . 10 𝑡((𝜑𝑖 ∈ (0...𝑁)) → 0 ≤ ((𝑋𝑖)‘𝑆))
94 fveq2 6229 . . . . . . . . . . . 12 (𝑡 = 𝑆 → ((𝑋𝑖)‘𝑡) = ((𝑋𝑖)‘𝑆))
9594breq2d 4697 . . . . . . . . . . 11 (𝑡 = 𝑆 → (0 ≤ ((𝑋𝑖)‘𝑡) ↔ 0 ≤ ((𝑋𝑖)‘𝑆)))
9695imbi2d 329 . . . . . . . . . 10 (𝑡 = 𝑆 → (((𝜑𝑖 ∈ (0...𝑁)) → 0 ≤ ((𝑋𝑖)‘𝑡)) ↔ ((𝜑𝑖 ∈ (0...𝑁)) → 0 ≤ ((𝑋𝑖)‘𝑆))))
97 stoweidlem26.14 . . . . . . . . . . . 12 ((𝜑𝑖 ∈ (0...𝑁) ∧ 𝑡𝑇) → 0 ≤ ((𝑋𝑖)‘𝑡))
98973expia 1286 . . . . . . . . . . 11 ((𝜑𝑖 ∈ (0...𝑁)) → (𝑡𝑇 → 0 ≤ ((𝑋𝑖)‘𝑡)))
9998com12 32 . . . . . . . . . 10 (𝑡𝑇 → ((𝜑𝑖 ∈ (0...𝑁)) → 0 ≤ ((𝑋𝑖)‘𝑡)))
10039, 93, 96, 99vtoclgaf 3302 . . . . . . . . 9 (𝑆𝑇 → ((𝜑𝑖 ∈ (0...𝑁)) → 0 ≤ ((𝑋𝑖)‘𝑆)))
10151, 100mpcom 38 . . . . . . . 8 ((𝜑𝑖 ∈ (0...𝑁)) → 0 ≤ ((𝑋𝑖)‘𝑆))
10219, 52, 88, 101mulge0d 10642 . . . . . . 7 ((𝜑𝑖 ∈ (0...𝑁)) → 0 ≤ (𝐸 · ((𝑋𝑖)‘𝑆)))
10318, 86, 53, 102fsumle 14575 . . . . . 6 (𝜑 → Σ𝑖 ∈ (0...𝑁)0 ≤ Σ𝑖 ∈ (0...𝑁)(𝐸 · ((𝑋𝑖)‘𝑆)))
104103adantr 480 . . . . 5 ((𝜑𝐿 = 1) → Σ𝑖 ∈ (0...𝑁)0 ≤ Σ𝑖 ∈ (0...𝑁)(𝐸 · ((𝑋𝑖)‘𝑆)))
10585, 104eqbrtrrd 4709 . . . 4 ((𝜑𝐿 = 1) → 0 ≤ Σ𝑖 ∈ (0...𝑁)(𝐸 · ((𝑋𝑖)‘𝑆)))
10616, 17, 55, 76, 105ltletrd 10235 . . 3 ((𝜑𝐿 = 1) → ((𝐿 − (4 / 3)) · 𝐸) < Σ𝑖 ∈ (0...𝑁)(𝐸 · ((𝑋𝑖)‘𝑆)))
107 elfzelz 12380 . . . . . . . . 9 (𝐿 ∈ (1...𝑁) → 𝐿 ∈ ℤ)
108 zre 11419 . . . . . . . . 9 (𝐿 ∈ ℤ → 𝐿 ∈ ℝ)
10926, 107, 1083syl 18 . . . . . . . 8 (𝜑𝐿 ∈ ℝ)
1105a1i 11 . . . . . . . . 9 (𝜑 → 4 ∈ ℝ)
1117a1i 11 . . . . . . . . 9 (𝜑 → 3 ∈ ℝ)
1129a1i 11 . . . . . . . . 9 (𝜑 → 3 ≠ 0)
113110, 111, 112redivcld 10891 . . . . . . . 8 (𝜑 → (4 / 3) ∈ ℝ)
114109, 113resubcld 10496 . . . . . . 7 (𝜑 → (𝐿 − (4 / 3)) ∈ ℝ)
115114, 14remulcld 10108 . . . . . 6 (𝜑 → ((𝐿 − (4 / 3)) · 𝐸) ∈ ℝ)
116115adantr 480 . . . . 5 ((𝜑 ∧ ¬ 𝐿 = 1) → ((𝐿 − (4 / 3)) · 𝐸) ∈ ℝ)
1171a1i 11 . . . . . . . . 9 (𝜑 → 1 ∈ ℝ)
118 stoweidlem26.6 . . . . . . . . . 10 (𝜑𝑁 ∈ ℕ)
11914, 118nndivred 11107 . . . . . . . . 9 (𝜑 → (𝐸 / 𝑁) ∈ ℝ)
120117, 119resubcld 10496 . . . . . . . 8 (𝜑 → (1 − (𝐸 / 𝑁)) ∈ ℝ)
121109, 117resubcld 10496 . . . . . . . 8 (𝜑 → (𝐿 − 1) ∈ ℝ)
122120, 121remulcld 10108 . . . . . . 7 (𝜑 → ((1 − (𝐸 / 𝑁)) · (𝐿 − 1)) ∈ ℝ)
12314, 122remulcld 10108 . . . . . 6 (𝜑 → (𝐸 · ((1 − (𝐸 / 𝑁)) · (𝐿 − 1))) ∈ ℝ)
124123adantr 480 . . . . 5 ((𝜑 ∧ ¬ 𝐿 = 1) → (𝐸 · ((1 − (𝐸 / 𝑁)) · (𝐿 − 1))) ∈ ℝ)
125 fzfid 12812 . . . . . . . 8 (𝜑 → (0...(𝐿 − 2)) ∈ Fin)
12626, 107syl 17 . . . . . . . . . . . . . 14 (𝜑𝐿 ∈ ℤ)
127 2z 11447 . . . . . . . . . . . . . . 15 2 ∈ ℤ
128127a1i 11 . . . . . . . . . . . . . 14 (𝜑 → 2 ∈ ℤ)
129126, 128zsubcld 11525 . . . . . . . . . . . . 13 (𝜑 → (𝐿 − 2) ∈ ℤ)
130118nnzd 11519 . . . . . . . . . . . . 13 (𝜑𝑁 ∈ ℤ)
131126zred 11520 . . . . . . . . . . . . . . 15 (𝜑𝐿 ∈ ℝ)
132 2re 11128 . . . . . . . . . . . . . . . 16 2 ∈ ℝ
133132a1i 11 . . . . . . . . . . . . . . 15 (𝜑 → 2 ∈ ℝ)
134131, 133resubcld 10496 . . . . . . . . . . . . . 14 (𝜑 → (𝐿 − 2) ∈ ℝ)
135118nnred 11073 . . . . . . . . . . . . . 14 (𝜑𝑁 ∈ ℝ)
136 0le2 11149 . . . . . . . . . . . . . . . 16 0 ≤ 2
137 0red 10079 . . . . . . . . . . . . . . . . 17 (𝜑 → 0 ∈ ℝ)
138137, 133, 131lesub2d 10673 . . . . . . . . . . . . . . . 16 (𝜑 → (0 ≤ 2 ↔ (𝐿 − 2) ≤ (𝐿 − 0)))
139136, 138mpbii 223 . . . . . . . . . . . . . . 15 (𝜑 → (𝐿 − 2) ≤ (𝐿 − 0))
140126zcnd 11521 . . . . . . . . . . . . . . . 16 (𝜑𝐿 ∈ ℂ)
141140subid1d 10419 . . . . . . . . . . . . . . 15 (𝜑 → (𝐿 − 0) = 𝐿)
142139, 141breqtrd 4711 . . . . . . . . . . . . . 14 (𝜑 → (𝐿 − 2) ≤ 𝐿)
143 elfzle2 12383 . . . . . . . . . . . . . . 15 (𝐿 ∈ (1...𝑁) → 𝐿𝑁)
14426, 143syl 17 . . . . . . . . . . . . . 14 (𝜑𝐿𝑁)
145134, 131, 135, 142, 144letrd 10232 . . . . . . . . . . . . 13 (𝜑 → (𝐿 − 2) ≤ 𝑁)
146129, 130, 1453jca 1261 . . . . . . . . . . . 12 (𝜑 → ((𝐿 − 2) ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ (𝐿 − 2) ≤ 𝑁))
147 eluz2 11731 . . . . . . . . . . . 12 (𝑁 ∈ (ℤ‘(𝐿 − 2)) ↔ ((𝐿 − 2) ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ (𝐿 − 2) ≤ 𝑁))
148146, 147sylibr 224 . . . . . . . . . . 11 (𝜑𝑁 ∈ (ℤ‘(𝐿 − 2)))
149 fzss2 12419 . . . . . . . . . . 11 (𝑁 ∈ (ℤ‘(𝐿 − 2)) → (0...(𝐿 − 2)) ⊆ (0...𝑁))
150148, 149syl 17 . . . . . . . . . 10 (𝜑 → (0...(𝐿 − 2)) ⊆ (0...𝑁))
151150sselda 3636 . . . . . . . . 9 ((𝜑𝑖 ∈ (0...(𝐿 − 2))) → 𝑖 ∈ (0...𝑁))
152151, 52syldan 486 . . . . . . . 8 ((𝜑𝑖 ∈ (0...(𝐿 − 2))) → ((𝑋𝑖)‘𝑆) ∈ ℝ)
153125, 152fsumrecl 14509 . . . . . . 7 (𝜑 → Σ𝑖 ∈ (0...(𝐿 − 2))((𝑋𝑖)‘𝑆) ∈ ℝ)
15414, 153remulcld 10108 . . . . . 6 (𝜑 → (𝐸 · Σ𝑖 ∈ (0...(𝐿 − 2))((𝑋𝑖)‘𝑆)) ∈ ℝ)
155154adantr 480 . . . . 5 ((𝜑 ∧ ¬ 𝐿 = 1) → (𝐸 · Σ𝑖 ∈ (0...(𝐿 − 2))((𝑋𝑖)‘𝑆)) ∈ ℝ)
15614, 121remulcld 10108 . . . . . . . . 9 (𝜑 → (𝐸 · (𝐿 − 1)) ∈ ℝ)
15714, 14remulcld 10108 . . . . . . . . 9 (𝜑 → (𝐸 · 𝐸) ∈ ℝ)
158156, 157resubcld 10496 . . . . . . . 8 (𝜑 → ((𝐸 · (𝐿 − 1)) − (𝐸 · 𝐸)) ∈ ℝ)
159121, 118nndivred 11107 . . . . . . . . . 10 (𝜑 → ((𝐿 − 1) / 𝑁) ∈ ℝ)
160157, 159remulcld 10108 . . . . . . . . 9 (𝜑 → ((𝐸 · 𝐸) · ((𝐿 − 1) / 𝑁)) ∈ ℝ)
161156, 160resubcld 10496 . . . . . . . 8 (𝜑 → ((𝐸 · (𝐿 − 1)) − ((𝐸 · 𝐸) · ((𝐿 − 1) / 𝑁))) ∈ ℝ)
162121, 14resubcld 10496 . . . . . . . . . 10 (𝜑 → ((𝐿 − 1) − 𝐸) ∈ ℝ)
163117, 14readdcld 10107 . . . . . . . . . . . 12 (𝜑 → (1 + 𝐸) ∈ ℝ)
1641, 7, 9redivcli 10830 . . . . . . . . . . . . . . 15 (1 / 3) ∈ ℝ
165164a1i 11 . . . . . . . . . . . . . 14 (𝜑 → (1 / 3) ∈ ℝ)
166 stoweidlem26.12 . . . . . . . . . . . . . 14 (𝜑𝐸 < (1 / 3))
16714, 165, 117, 166ltadd2dd 10234 . . . . . . . . . . . . 13 (𝜑 → (1 + 𝐸) < (1 + (1 / 3)))
168 ax-1cn 10032 . . . . . . . . . . . . . . 15 1 ∈ ℂ
16961, 168, 61, 9divdiri 10820 . . . . . . . . . . . . . 14 ((3 + 1) / 3) = ((3 / 3) + (1 / 3))
170 3p1e4 11191 . . . . . . . . . . . . . . 15 (3 + 1) = 4
171170oveq1i 6700 . . . . . . . . . . . . . 14 ((3 + 1) / 3) = (4 / 3)
17262oveq1i 6700 . . . . . . . . . . . . . 14 ((3 / 3) + (1 / 3)) = (1 + (1 / 3))
173169, 171, 1723eqtr3ri 2682 . . . . . . . . . . . . 13 (1 + (1 / 3)) = (4 / 3)
174167, 173syl6breq 4726 . . . . . . . . . . . 12 (𝜑 → (1 + 𝐸) < (4 / 3))
175163, 113, 109, 174ltsub2dd 10678 . . . . . . . . . . 11 (𝜑 → (𝐿 − (4 / 3)) < (𝐿 − (1 + 𝐸)))
176168a1i 11 . . . . . . . . . . . 12 (𝜑 → 1 ∈ ℂ)
17713rpcnd 11912 . . . . . . . . . . . 12 (𝜑𝐸 ∈ ℂ)
178140, 176, 177subsub4d 10461 . . . . . . . . . . 11 (𝜑 → ((𝐿 − 1) − 𝐸) = (𝐿 − (1 + 𝐸)))
179175, 178breqtrrd 4713 . . . . . . . . . 10 (𝜑 → (𝐿 − (4 / 3)) < ((𝐿 − 1) − 𝐸))
180114, 162, 13, 179ltmul1dd 11965 . . . . . . . . 9 (𝜑 → ((𝐿 − (4 / 3)) · 𝐸) < (((𝐿 − 1) − 𝐸) · 𝐸))
181140, 176subcld 10430 . . . . . . . . . . . 12 (𝜑 → (𝐿 − 1) ∈ ℂ)
182181, 177subcld 10430 . . . . . . . . . . 11 (𝜑 → ((𝐿 − 1) − 𝐸) ∈ ℂ)
183177, 182mulcomd 10099 . . . . . . . . . 10 (𝜑 → (𝐸 · ((𝐿 − 1) − 𝐸)) = (((𝐿 − 1) − 𝐸) · 𝐸))
184177, 181, 177subdid 10524 . . . . . . . . . 10 (𝜑 → (𝐸 · ((𝐿 − 1) − 𝐸)) = ((𝐸 · (𝐿 − 1)) − (𝐸 · 𝐸)))
185183, 184eqtr3d 2687 . . . . . . . . 9 (𝜑 → (((𝐿 − 1) − 𝐸) · 𝐸) = ((𝐸 · (𝐿 − 1)) − (𝐸 · 𝐸)))
186180, 185breqtrd 4711 . . . . . . . 8 (𝜑 → ((𝐿 − (4 / 3)) · 𝐸) < ((𝐸 · (𝐿 − 1)) − (𝐸 · 𝐸)))
187 1zzd 11446 . . . . . . . . . . . . . . . . 17 (𝜑 → 1 ∈ ℤ)
188 elfz 12370 . . . . . . . . . . . . . . . . 17 ((𝐿 ∈ ℤ ∧ 1 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝐿 ∈ (1...𝑁) ↔ (1 ≤ 𝐿𝐿𝑁)))
189126, 187, 130, 188syl3anc 1366 . . . . . . . . . . . . . . . 16 (𝜑 → (𝐿 ∈ (1...𝑁) ↔ (1 ≤ 𝐿𝐿𝑁)))
19026, 189mpbid 222 . . . . . . . . . . . . . . 15 (𝜑 → (1 ≤ 𝐿𝐿𝑁))
191190simprd 478 . . . . . . . . . . . . . 14 (𝜑𝐿𝑁)
192 zlem1lt 11467 . . . . . . . . . . . . . . 15 ((𝐿 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝐿𝑁 ↔ (𝐿 − 1) < 𝑁))
193126, 130, 192syl2anc 694 . . . . . . . . . . . . . 14 (𝜑 → (𝐿𝑁 ↔ (𝐿 − 1) < 𝑁))
194191, 193mpbid 222 . . . . . . . . . . . . 13 (𝜑 → (𝐿 − 1) < 𝑁)
195118nngt0d 11102 . . . . . . . . . . . . . 14 (𝜑 → 0 < 𝑁)
196 ltdiv1 10925 . . . . . . . . . . . . . 14 (((𝐿 − 1) ∈ ℝ ∧ 𝑁 ∈ ℝ ∧ (𝑁 ∈ ℝ ∧ 0 < 𝑁)) → ((𝐿 − 1) < 𝑁 ↔ ((𝐿 − 1) / 𝑁) < (𝑁 / 𝑁)))
197121, 135, 135, 195, 196syl112anc 1370 . . . . . . . . . . . . 13 (𝜑 → ((𝐿 − 1) < 𝑁 ↔ ((𝐿 − 1) / 𝑁) < (𝑁 / 𝑁)))
198194, 197mpbid 222 . . . . . . . . . . . 12 (𝜑 → ((𝐿 − 1) / 𝑁) < (𝑁 / 𝑁))
199118nncnd 11074 . . . . . . . . . . . . 13 (𝜑𝑁 ∈ ℂ)
200118nnne0d 11103 . . . . . . . . . . . . 13 (𝜑𝑁 ≠ 0)
201199, 200dividd 10837 . . . . . . . . . . . 12 (𝜑 → (𝑁 / 𝑁) = 1)
202198, 201breqtrd 4711 . . . . . . . . . . 11 (𝜑 → ((𝐿 − 1) / 𝑁) < 1)
20314, 14, 73, 73mulgt0d 10230 . . . . . . . . . . . 12 (𝜑 → 0 < (𝐸 · 𝐸))
204 ltmul2 10912 . . . . . . . . . . . 12 ((((𝐿 − 1) / 𝑁) ∈ ℝ ∧ 1 ∈ ℝ ∧ ((𝐸 · 𝐸) ∈ ℝ ∧ 0 < (𝐸 · 𝐸))) → (((𝐿 − 1) / 𝑁) < 1 ↔ ((𝐸 · 𝐸) · ((𝐿 − 1) / 𝑁)) < ((𝐸 · 𝐸) · 1)))
205159, 117, 157, 203, 204syl112anc 1370 . . . . . . . . . . 11 (𝜑 → (((𝐿 − 1) / 𝑁) < 1 ↔ ((𝐸 · 𝐸) · ((𝐿 − 1) / 𝑁)) < ((𝐸 · 𝐸) · 1)))
206202, 205mpbid 222 . . . . . . . . . 10 (𝜑 → ((𝐸 · 𝐸) · ((𝐿 − 1) / 𝑁)) < ((𝐸 · 𝐸) · 1))
207177, 177mulcld 10098 . . . . . . . . . . 11 (𝜑 → (𝐸 · 𝐸) ∈ ℂ)
208207mulid1d 10095 . . . . . . . . . 10 (𝜑 → ((𝐸 · 𝐸) · 1) = (𝐸 · 𝐸))
209206, 208breqtrd 4711 . . . . . . . . 9 (𝜑 → ((𝐸 · 𝐸) · ((𝐿 − 1) / 𝑁)) < (𝐸 · 𝐸))
210160, 157, 156, 209ltsub2dd 10678 . . . . . . . 8 (𝜑 → ((𝐸 · (𝐿 − 1)) − (𝐸 · 𝐸)) < ((𝐸 · (𝐿 − 1)) − ((𝐸 · 𝐸) · ((𝐿 − 1) / 𝑁))))
211115, 158, 161, 186, 210lttrd 10236 . . . . . . 7 (𝜑 → ((𝐿 − (4 / 3)) · 𝐸) < ((𝐸 · (𝐿 − 1)) − ((𝐸 · 𝐸) · ((𝐿 − 1) / 𝑁))))
212177, 199, 200divcld 10839 . . . . . . . . . . 11 (𝜑 → (𝐸 / 𝑁) ∈ ℂ)
213176, 212, 181subdird 10525 . . . . . . . . . 10 (𝜑 → ((1 − (𝐸 / 𝑁)) · (𝐿 − 1)) = ((1 · (𝐿 − 1)) − ((𝐸 / 𝑁) · (𝐿 − 1))))
214181mulid2d 10096 . . . . . . . . . . 11 (𝜑 → (1 · (𝐿 − 1)) = (𝐿 − 1))
215214oveq1d 6705 . . . . . . . . . 10 (𝜑 → ((1 · (𝐿 − 1)) − ((𝐸 / 𝑁) · (𝐿 − 1))) = ((𝐿 − 1) − ((𝐸 / 𝑁) · (𝐿 − 1))))
216213, 215eqtrd 2685 . . . . . . . . 9 (𝜑 → ((1 − (𝐸 / 𝑁)) · (𝐿 − 1)) = ((𝐿 − 1) − ((𝐸 / 𝑁) · (𝐿 − 1))))
217216oveq2d 6706 . . . . . . . 8 (𝜑 → (𝐸 · ((1 − (𝐸 / 𝑁)) · (𝐿 − 1))) = (𝐸 · ((𝐿 − 1) − ((𝐸 / 𝑁) · (𝐿 − 1)))))
218212, 181mulcld 10098 . . . . . . . . 9 (𝜑 → ((𝐸 / 𝑁) · (𝐿 − 1)) ∈ ℂ)
219177, 181, 218subdid 10524 . . . . . . . 8 (𝜑 → (𝐸 · ((𝐿 − 1) − ((𝐸 / 𝑁) · (𝐿 − 1)))) = ((𝐸 · (𝐿 − 1)) − (𝐸 · ((𝐸 / 𝑁) · (𝐿 − 1)))))
220177, 199, 181, 200div32d 10862 . . . . . . . . . . 11 (𝜑 → ((𝐸 / 𝑁) · (𝐿 − 1)) = (𝐸 · ((𝐿 − 1) / 𝑁)))
221220oveq2d 6706 . . . . . . . . . 10 (𝜑 → (𝐸 · ((𝐸 / 𝑁) · (𝐿 − 1))) = (𝐸 · (𝐸 · ((𝐿 − 1) / 𝑁))))
222181, 199, 200divcld 10839 . . . . . . . . . . 11 (𝜑 → ((𝐿 − 1) / 𝑁) ∈ ℂ)
223177, 177, 222mulassd 10101 . . . . . . . . . 10 (𝜑 → ((𝐸 · 𝐸) · ((𝐿 − 1) / 𝑁)) = (𝐸 · (𝐸 · ((𝐿 − 1) / 𝑁))))
224221, 223eqtr4d 2688 . . . . . . . . 9 (𝜑 → (𝐸 · ((𝐸 / 𝑁) · (𝐿 − 1))) = ((𝐸 · 𝐸) · ((𝐿 − 1) / 𝑁)))
225224oveq2d 6706 . . . . . . . 8 (𝜑 → ((𝐸 · (𝐿 − 1)) − (𝐸 · ((𝐸 / 𝑁) · (𝐿 − 1)))) = ((𝐸 · (𝐿 − 1)) − ((𝐸 · 𝐸) · ((𝐿 − 1) / 𝑁))))
226217, 219, 2253eqtrd 2689 . . . . . . 7 (𝜑 → (𝐸 · ((1 − (𝐸 / 𝑁)) · (𝐿 − 1))) = ((𝐸 · (𝐿 − 1)) − ((𝐸 · 𝐸) · ((𝐿 − 1) / 𝑁))))
227211, 226breqtrrd 4713 . . . . . 6 (𝜑 → ((𝐿 − (4 / 3)) · 𝐸) < (𝐸 · ((1 − (𝐸 / 𝑁)) · (𝐿 − 1))))
228227adantr 480 . . . . 5 ((𝜑 ∧ ¬ 𝐿 = 1) → ((𝐿 − (4 / 3)) · 𝐸) < (𝐸 · ((1 − (𝐸 / 𝑁)) · (𝐿 − 1))))
229176, 212subcld 10430 . . . . . . . . . 10 (𝜑 → (1 − (𝐸 / 𝑁)) ∈ ℂ)
230 fsumconst 14566 . . . . . . . . . 10 (((0...(𝐿 − 2)) ∈ Fin ∧ (1 − (𝐸 / 𝑁)) ∈ ℂ) → Σ𝑖 ∈ (0...(𝐿 − 2))(1 − (𝐸 / 𝑁)) = ((#‘(0...(𝐿 − 2))) · (1 − (𝐸 / 𝑁))))
231125, 229, 230syl2anc 694 . . . . . . . . 9 (𝜑 → Σ𝑖 ∈ (0...(𝐿 − 2))(1 − (𝐸 / 𝑁)) = ((#‘(0...(𝐿 − 2))) · (1 − (𝐸 / 𝑁))))
232231adantr 480 . . . . . . . 8 ((𝜑 ∧ ¬ 𝐿 = 1) → Σ𝑖 ∈ (0...(𝐿 − 2))(1 − (𝐸 / 𝑁)) = ((#‘(0...(𝐿 − 2))) · (1 − (𝐸 / 𝑁))))
233 0zd 11427 . . . . . . . . . . . . 13 ((𝜑 ∧ ¬ 𝐿 = 1) → 0 ∈ ℤ)
23426adantr 480 . . . . . . . . . . . . . . 15 ((𝜑 ∧ ¬ 𝐿 = 1) → 𝐿 ∈ (1...𝑁))
235234, 107syl 17 . . . . . . . . . . . . . 14 ((𝜑 ∧ ¬ 𝐿 = 1) → 𝐿 ∈ ℤ)
236127a1i 11 . . . . . . . . . . . . . 14 ((𝜑 ∧ ¬ 𝐿 = 1) → 2 ∈ ℤ)
237235, 236zsubcld 11525 . . . . . . . . . . . . 13 ((𝜑 ∧ ¬ 𝐿 = 1) → (𝐿 − 2) ∈ ℤ)
238 elnnuz 11762 . . . . . . . . . . . . . . . . . . . 20 (𝑁 ∈ ℕ ↔ 𝑁 ∈ (ℤ‘1))
239118, 238sylib 208 . . . . . . . . . . . . . . . . . . 19 (𝜑𝑁 ∈ (ℤ‘1))
240 elfzp12 12457 . . . . . . . . . . . . . . . . . . 19 (𝑁 ∈ (ℤ‘1) → (𝐿 ∈ (1...𝑁) ↔ (𝐿 = 1 ∨ 𝐿 ∈ ((1 + 1)...𝑁))))
241239, 240syl 17 . . . . . . . . . . . . . . . . . 18 (𝜑 → (𝐿 ∈ (1...𝑁) ↔ (𝐿 = 1 ∨ 𝐿 ∈ ((1 + 1)...𝑁))))
24226, 241mpbid 222 . . . . . . . . . . . . . . . . 17 (𝜑 → (𝐿 = 1 ∨ 𝐿 ∈ ((1 + 1)...𝑁)))
243242orcanai 972 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ ¬ 𝐿 = 1) → 𝐿 ∈ ((1 + 1)...𝑁))
244 1p1e2 11172 . . . . . . . . . . . . . . . . . 18 (1 + 1) = 2
245244a1i 11 . . . . . . . . . . . . . . . . 17 ((𝜑 ∧ ¬ 𝐿 = 1) → (1 + 1) = 2)
246245oveq1d 6705 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ ¬ 𝐿 = 1) → ((1 + 1)...𝑁) = (2...𝑁))
247243, 246eleqtrd 2732 . . . . . . . . . . . . . . 15 ((𝜑 ∧ ¬ 𝐿 = 1) → 𝐿 ∈ (2...𝑁))
248 elfzle1 12382 . . . . . . . . . . . . . . 15 (𝐿 ∈ (2...𝑁) → 2 ≤ 𝐿)
249247, 248syl 17 . . . . . . . . . . . . . 14 ((𝜑 ∧ ¬ 𝐿 = 1) → 2 ≤ 𝐿)
250109adantr 480 . . . . . . . . . . . . . . 15 ((𝜑 ∧ ¬ 𝐿 = 1) → 𝐿 ∈ ℝ)
251132a1i 11 . . . . . . . . . . . . . . 15 ((𝜑 ∧ ¬ 𝐿 = 1) → 2 ∈ ℝ)
252250, 251subge0d 10655 . . . . . . . . . . . . . 14 ((𝜑 ∧ ¬ 𝐿 = 1) → (0 ≤ (𝐿 − 2) ↔ 2 ≤ 𝐿))
253249, 252mpbird 247 . . . . . . . . . . . . 13 ((𝜑 ∧ ¬ 𝐿 = 1) → 0 ≤ (𝐿 − 2))
254233, 237, 2533jca 1261 . . . . . . . . . . . 12 ((𝜑 ∧ ¬ 𝐿 = 1) → (0 ∈ ℤ ∧ (𝐿 − 2) ∈ ℤ ∧ 0 ≤ (𝐿 − 2)))
255 eluz2 11731 . . . . . . . . . . . 12 ((𝐿 − 2) ∈ (ℤ‘0) ↔ (0 ∈ ℤ ∧ (𝐿 − 2) ∈ ℤ ∧ 0 ≤ (𝐿 − 2)))
256254, 255sylibr 224 . . . . . . . . . . 11 ((𝜑 ∧ ¬ 𝐿 = 1) → (𝐿 − 2) ∈ (ℤ‘0))
257 hashfz 13252 . . . . . . . . . . 11 ((𝐿 − 2) ∈ (ℤ‘0) → (#‘(0...(𝐿 − 2))) = (((𝐿 − 2) − 0) + 1))
258256, 257syl 17 . . . . . . . . . 10 ((𝜑 ∧ ¬ 𝐿 = 1) → (#‘(0...(𝐿 − 2))) = (((𝐿 − 2) − 0) + 1))
259 2cn 11129 . . . . . . . . . . . . . . . 16 2 ∈ ℂ
260259a1i 11 . . . . . . . . . . . . . . 15 (𝜑 → 2 ∈ ℂ)
261140, 260subcld 10430 . . . . . . . . . . . . . 14 (𝜑 → (𝐿 − 2) ∈ ℂ)
262261subid1d 10419 . . . . . . . . . . . . 13 (𝜑 → ((𝐿 − 2) − 0) = (𝐿 − 2))
263262oveq1d 6705 . . . . . . . . . . . 12 (𝜑 → (((𝐿 − 2) − 0) + 1) = ((𝐿 − 2) + 1))
264140, 260, 176subadd23d 10452 . . . . . . . . . . . 12 (𝜑 → ((𝐿 − 2) + 1) = (𝐿 + (1 − 2)))
265259, 168negsubdi2i 10405 . . . . . . . . . . . . . . . 16 -(2 − 1) = (1 − 2)
266 2m1e1 11173 . . . . . . . . . . . . . . . . 17 (2 − 1) = 1
267266negeqi 10312 . . . . . . . . . . . . . . . 16 -(2 − 1) = -1
268265, 267eqtr3i 2675 . . . . . . . . . . . . . . 15 (1 − 2) = -1
269268a1i 11 . . . . . . . . . . . . . 14 (𝜑 → (1 − 2) = -1)
270269oveq2d 6706 . . . . . . . . . . . . 13 (𝜑 → (𝐿 + (1 − 2)) = (𝐿 + -1))
271140, 176negsubd 10436 . . . . . . . . . . . . 13 (𝜑 → (𝐿 + -1) = (𝐿 − 1))
272270, 271eqtrd 2685 . . . . . . . . . . . 12 (𝜑 → (𝐿 + (1 − 2)) = (𝐿 − 1))
273263, 264, 2723eqtrd 2689 . . . . . . . . . . 11 (𝜑 → (((𝐿 − 2) − 0) + 1) = (𝐿 − 1))
274273adantr 480 . . . . . . . . . 10 ((𝜑 ∧ ¬ 𝐿 = 1) → (((𝐿 − 2) − 0) + 1) = (𝐿 − 1))
275258, 274eqtrd 2685 . . . . . . . . 9 ((𝜑 ∧ ¬ 𝐿 = 1) → (#‘(0...(𝐿 − 2))) = (𝐿 − 1))
276275oveq1d 6705 . . . . . . . 8 ((𝜑 ∧ ¬ 𝐿 = 1) → ((#‘(0...(𝐿 − 2))) · (1 − (𝐸 / 𝑁))) = ((𝐿 − 1) · (1 − (𝐸 / 𝑁))))
277181, 229mulcomd 10099 . . . . . . . . 9 (𝜑 → ((𝐿 − 1) · (1 − (𝐸 / 𝑁))) = ((1 − (𝐸 / 𝑁)) · (𝐿 − 1)))
278277adantr 480 . . . . . . . 8 ((𝜑 ∧ ¬ 𝐿 = 1) → ((𝐿 − 1) · (1 − (𝐸 / 𝑁))) = ((1 − (𝐸 / 𝑁)) · (𝐿 − 1)))
279232, 276, 2783eqtrd 2689 . . . . . . 7 ((𝜑 ∧ ¬ 𝐿 = 1) → Σ𝑖 ∈ (0...(𝐿 − 2))(1 − (𝐸 / 𝑁)) = ((1 − (𝐸 / 𝑁)) · (𝐿 − 1)))
280 fzfid 12812 . . . . . . . 8 ((𝜑 ∧ ¬ 𝐿 = 1) → (0...(𝐿 − 2)) ∈ Fin)
281 fzn0 12393 . . . . . . . . 9 ((0...(𝐿 − 2)) ≠ ∅ ↔ (𝐿 − 2) ∈ (ℤ‘0))
282256, 281sylibr 224 . . . . . . . 8 ((𝜑 ∧ ¬ 𝐿 = 1) → (0...(𝐿 − 2)) ≠ ∅)
283120ad2antrr 762 . . . . . . . 8 (((𝜑 ∧ ¬ 𝐿 = 1) ∧ 𝑖 ∈ (0...(𝐿 − 2))) → (1 − (𝐸 / 𝑁)) ∈ ℝ)
284 simpll 805 . . . . . . . . 9 (((𝜑 ∧ ¬ 𝐿 = 1) ∧ 𝑖 ∈ (0...(𝐿 − 2))) → 𝜑)
285151adantlr 751 . . . . . . . . 9 (((𝜑 ∧ ¬ 𝐿 = 1) ∧ 𝑖 ∈ (0...(𝐿 − 2))) → 𝑖 ∈ (0...𝑁))
286284, 285, 52syl2anc 694 . . . . . . . 8 (((𝜑 ∧ ¬ 𝐿 = 1) ∧ 𝑖 ∈ (0...(𝐿 − 2))) → ((𝑋𝑖)‘𝑆) ∈ ℝ)
28750adantr 480 . . . . . . . . . . . 12 ((𝜑𝑖 ∈ (0...(𝐿 − 2))) → 𝑆𝑇)
288 elfzelz 12380 . . . . . . . . . . . . . . . . 17 (𝑖 ∈ (0...(𝐿 − 2)) → 𝑖 ∈ ℤ)
289288zred 11520 . . . . . . . . . . . . . . . 16 (𝑖 ∈ (0...(𝐿 − 2)) → 𝑖 ∈ ℝ)
290289adantl 481 . . . . . . . . . . . . . . 15 ((𝜑𝑖 ∈ (0...(𝐿 − 2))) → 𝑖 ∈ ℝ)
291164a1i 11 . . . . . . . . . . . . . . 15 ((𝜑𝑖 ∈ (0...(𝐿 − 2))) → (1 / 3) ∈ ℝ)
292290, 291readdcld 10107 . . . . . . . . . . . . . 14 ((𝜑𝑖 ∈ (0...(𝐿 − 2))) → (𝑖 + (1 / 3)) ∈ ℝ)
29314adantr 480 . . . . . . . . . . . . . 14 ((𝜑𝑖 ∈ (0...(𝐿 − 2))) → 𝐸 ∈ ℝ)
294292, 293remulcld 10108 . . . . . . . . . . . . 13 ((𝜑𝑖 ∈ (0...(𝐿 − 2))) → ((𝑖 + (1 / 3)) · 𝐸) ∈ ℝ)
295109adantr 480 . . . . . . . . . . . . . . . 16 ((𝜑𝑖 ∈ (0...(𝐿 − 2))) → 𝐿 ∈ ℝ)
296132a1i 11 . . . . . . . . . . . . . . . 16 ((𝜑𝑖 ∈ (0...(𝐿 − 2))) → 2 ∈ ℝ)
297295, 296resubcld 10496 . . . . . . . . . . . . . . 15 ((𝜑𝑖 ∈ (0...(𝐿 − 2))) → (𝐿 − 2) ∈ ℝ)
298297, 291readdcld 10107 . . . . . . . . . . . . . 14 ((𝜑𝑖 ∈ (0...(𝐿 − 2))) → ((𝐿 − 2) + (1 / 3)) ∈ ℝ)
299298, 293remulcld 10108 . . . . . . . . . . . . 13 ((𝜑𝑖 ∈ (0...(𝐿 − 2))) → (((𝐿 − 2) + (1 / 3)) · 𝐸) ∈ ℝ)
300 stoweidlem26.10 . . . . . . . . . . . . . . . 16 (𝜑𝐹:𝑇⟶ℝ)
301300, 50jca 553 . . . . . . . . . . . . . . 15 (𝜑 → (𝐹:𝑇⟶ℝ ∧ 𝑆𝑇))
302301adantr 480 . . . . . . . . . . . . . 14 ((𝜑𝑖 ∈ (0...(𝐿 − 2))) → (𝐹:𝑇⟶ℝ ∧ 𝑆𝑇))
303 ffvelrn 6397 . . . . . . . . . . . . . 14 ((𝐹:𝑇⟶ℝ ∧ 𝑆𝑇) → (𝐹𝑆) ∈ ℝ)
304302, 303syl 17 . . . . . . . . . . . . 13 ((𝜑𝑖 ∈ (0...(𝐿 − 2))) → (𝐹𝑆) ∈ ℝ)
305 elfzle2 12383 . . . . . . . . . . . . . . . 16 (𝑖 ∈ (0...(𝐿 − 2)) → 𝑖 ≤ (𝐿 − 2))
306305adantl 481 . . . . . . . . . . . . . . 15 ((𝜑𝑖 ∈ (0...(𝐿 − 2))) → 𝑖 ≤ (𝐿 − 2))
307290, 297, 291, 306leadd1dd 10679 . . . . . . . . . . . . . 14 ((𝜑𝑖 ∈ (0...(𝐿 − 2))) → (𝑖 + (1 / 3)) ≤ ((𝐿 − 2) + (1 / 3)))
30814, 73jca 553 . . . . . . . . . . . . . . . 16 (𝜑 → (𝐸 ∈ ℝ ∧ 0 < 𝐸))
309308adantr 480 . . . . . . . . . . . . . . 15 ((𝜑𝑖 ∈ (0...(𝐿 − 2))) → (𝐸 ∈ ℝ ∧ 0 < 𝐸))
310 lemul1 10913 . . . . . . . . . . . . . . 15 (((𝑖 + (1 / 3)) ∈ ℝ ∧ ((𝐿 − 2) + (1 / 3)) ∈ ℝ ∧ (𝐸 ∈ ℝ ∧ 0 < 𝐸)) → ((𝑖 + (1 / 3)) ≤ ((𝐿 − 2) + (1 / 3)) ↔ ((𝑖 + (1 / 3)) · 𝐸) ≤ (((𝐿 − 2) + (1 / 3)) · 𝐸)))
311292, 298, 309, 310syl3anc 1366 . . . . . . . . . . . . . 14 ((𝜑𝑖 ∈ (0...(𝐿 − 2))) → ((𝑖 + (1 / 3)) ≤ ((𝐿 − 2) + (1 / 3)) ↔ ((𝑖 + (1 / 3)) · 𝐸) ≤ (((𝐿 − 2) + (1 / 3)) · 𝐸)))
312307, 311mpbid 222 . . . . . . . . . . . . 13 ((𝜑𝑖 ∈ (0...(𝐿 − 2))) → ((𝑖 + (1 / 3)) · 𝐸) ≤ (((𝐿 − 2) + (1 / 3)) · 𝐸))
313109, 133resubcld 10496 . . . . . . . . . . . . . . . . 17 (𝜑 → (𝐿 − 2) ∈ ℝ)
314313, 165readdcld 10107 . . . . . . . . . . . . . . . 16 (𝜑 → ((𝐿 − 2) + (1 / 3)) ∈ ℝ)
315314, 14remulcld 10108 . . . . . . . . . . . . . . 15 (𝜑 → (((𝐿 − 2) + (1 / 3)) · 𝐸) ∈ ℝ)
316300, 50ffvelrnd 6400 . . . . . . . . . . . . . . 15 (𝜑 → (𝐹𝑆) ∈ ℝ)
317121, 165resubcld 10496 . . . . . . . . . . . . . . . . 17 (𝜑 → ((𝐿 − 1) − (1 / 3)) ∈ ℝ)
318317, 14remulcld 10108 . . . . . . . . . . . . . . . 16 (𝜑 → (((𝐿 − 1) − (1 / 3)) · 𝐸) ∈ ℝ)
319 addid1 10254 . . . . . . . . . . . . . . . . . . . . . . . . 25 (1 ∈ ℂ → (1 + 0) = 1)
320319eqcomd 2657 . . . . . . . . . . . . . . . . . . . . . . . 24 (1 ∈ ℂ → 1 = (1 + 0))
321168, 320mp1i 13 . . . . . . . . . . . . . . . . . . . . . . 23 (𝜑 → 1 = (1 + 0))
322176subidd 10418 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝜑 → (1 − 1) = 0)
323322eqcomd 2657 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝜑 → 0 = (1 − 1))
324323oveq2d 6706 . . . . . . . . . . . . . . . . . . . . . . 23 (𝜑 → (1 + 0) = (1 + (1 − 1)))
325 addsubass 10329 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((1 ∈ ℂ ∧ 1 ∈ ℂ ∧ 1 ∈ ℂ) → ((1 + 1) − 1) = (1 + (1 − 1)))
326325eqcomd 2657 . . . . . . . . . . . . . . . . . . . . . . . 24 ((1 ∈ ℂ ∧ 1 ∈ ℂ ∧ 1 ∈ ℂ) → (1 + (1 − 1)) = ((1 + 1) − 1))
327176, 176, 176, 326syl3anc 1366 . . . . . . . . . . . . . . . . . . . . . . 23 (𝜑 → (1 + (1 − 1)) = ((1 + 1) − 1))
328321, 324, 3273eqtrd 2689 . . . . . . . . . . . . . . . . . . . . . 22 (𝜑 → 1 = ((1 + 1) − 1))
329328oveq2d 6706 . . . . . . . . . . . . . . . . . . . . 21 (𝜑 → (𝐿 − 1) = (𝐿 − ((1 + 1) − 1)))
330244a1i 11 . . . . . . . . . . . . . . . . . . . . . . 23 (𝜑 → (1 + 1) = 2)
331330oveq1d 6705 . . . . . . . . . . . . . . . . . . . . . 22 (𝜑 → ((1 + 1) − 1) = (2 − 1))
332331oveq2d 6706 . . . . . . . . . . . . . . . . . . . . 21 (𝜑 → (𝐿 − ((1 + 1) − 1)) = (𝐿 − (2 − 1)))
333140, 260, 176subsubd 10458 . . . . . . . . . . . . . . . . . . . . 21 (𝜑 → (𝐿 − (2 − 1)) = ((𝐿 − 2) + 1))
334329, 332, 3333eqtrd 2689 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → (𝐿 − 1) = ((𝐿 − 2) + 1))
335334oveq1d 6705 . . . . . . . . . . . . . . . . . . 19 (𝜑 → ((𝐿 − 1) − (2 / 3)) = (((𝐿 − 2) + 1) − (2 / 3)))
336259, 61, 9divcli 10805 . . . . . . . . . . . . . . . . . . . . 21 (2 / 3) ∈ ℂ
337336a1i 11 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → (2 / 3) ∈ ℂ)
338261, 176, 337addsubassd 10450 . . . . . . . . . . . . . . . . . . 19 (𝜑 → (((𝐿 − 2) + 1) − (2 / 3)) = ((𝐿 − 2) + (1 − (2 / 3))))
339168, 61, 9divcli 10805 . . . . . . . . . . . . . . . . . . . . . 22 (1 / 3) ∈ ℂ
340 df-3 11118 . . . . . . . . . . . . . . . . . . . . . . . 24 3 = (2 + 1)
341340oveq1i 6700 . . . . . . . . . . . . . . . . . . . . . . 23 (3 / 3) = ((2 + 1) / 3)
342259, 168, 61, 9divdiri 10820 . . . . . . . . . . . . . . . . . . . . . . 23 ((2 + 1) / 3) = ((2 / 3) + (1 / 3))
343341, 62, 3423eqtr3ri 2682 . . . . . . . . . . . . . . . . . . . . . 22 ((2 / 3) + (1 / 3)) = 1
344168, 336, 339, 343subaddrii 10408 . . . . . . . . . . . . . . . . . . . . 21 (1 − (2 / 3)) = (1 / 3)
345344a1i 11 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → (1 − (2 / 3)) = (1 / 3))
346345oveq2d 6706 . . . . . . . . . . . . . . . . . . 19 (𝜑 → ((𝐿 − 2) + (1 − (2 / 3))) = ((𝐿 − 2) + (1 / 3)))
347335, 338, 3463eqtrd 2689 . . . . . . . . . . . . . . . . . 18 (𝜑 → ((𝐿 − 1) − (2 / 3)) = ((𝐿 − 2) + (1 / 3)))
348132, 7, 9redivcli 10830 . . . . . . . . . . . . . . . . . . . 20 (2 / 3) ∈ ℝ
349348a1i 11 . . . . . . . . . . . . . . . . . . 19 (𝜑 → (2 / 3) ∈ ℝ)
350 1lt2 11232 . . . . . . . . . . . . . . . . . . . 20 1 < 2
3517, 64pm3.2i 470 . . . . . . . . . . . . . . . . . . . . . 22 (3 ∈ ℝ ∧ 0 < 3)
3521, 132, 3513pm3.2i 1259 . . . . . . . . . . . . . . . . . . . . 21 (1 ∈ ℝ ∧ 2 ∈ ℝ ∧ (3 ∈ ℝ ∧ 0 < 3))
353 ltdiv1 10925 . . . . . . . . . . . . . . . . . . . . 21 ((1 ∈ ℝ ∧ 2 ∈ ℝ ∧ (3 ∈ ℝ ∧ 0 < 3)) → (1 < 2 ↔ (1 / 3) < (2 / 3)))
354352, 353mp1i 13 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → (1 < 2 ↔ (1 / 3) < (2 / 3)))
355350, 354mpbii 223 . . . . . . . . . . . . . . . . . . 19 (𝜑 → (1 / 3) < (2 / 3))
356165, 349, 121, 355ltsub2dd 10678 . . . . . . . . . . . . . . . . . 18 (𝜑 → ((𝐿 − 1) − (2 / 3)) < ((𝐿 − 1) − (1 / 3)))
357347, 356eqbrtrrd 4709 . . . . . . . . . . . . . . . . 17 (𝜑 → ((𝐿 − 2) + (1 / 3)) < ((𝐿 − 1) − (1 / 3)))
358314, 317, 13, 357ltmul1dd 11965 . . . . . . . . . . . . . . . 16 (𝜑 → (((𝐿 − 2) + (1 / 3)) · 𝐸) < (((𝐿 − 1) − (1 / 3)) · 𝐸))
35923simprd 478 . . . . . . . . . . . . . . . . . . . . . . 23 (𝜑 → ¬ 𝑆 ∈ (𝐷‘(𝐿 − 1)))
360190simpld 474 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝜑 → 1 ≤ 𝐿)
361135, 117readdcld 10107 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝜑 → (𝑁 + 1) ∈ ℝ)
362135lep1d 10993 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝜑𝑁 ≤ (𝑁 + 1))
363109, 135, 361, 191, 362letrd 10232 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝜑𝐿 ≤ (𝑁 + 1))
364130peano2zd 11523 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝜑 → (𝑁 + 1) ∈ ℤ)
365 elfz 12370 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝐿 ∈ ℤ ∧ 1 ∈ ℤ ∧ (𝑁 + 1) ∈ ℤ) → (𝐿 ∈ (1...(𝑁 + 1)) ↔ (1 ≤ 𝐿𝐿 ≤ (𝑁 + 1))))
366126, 187, 364, 365syl3anc 1366 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝜑 → (𝐿 ∈ (1...(𝑁 + 1)) ↔ (1 ≤ 𝐿𝐿 ≤ (𝑁 + 1))))
367360, 363, 366mpbir2and 977 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝜑𝐿 ∈ (1...(𝑁 + 1)))
368140, 176npcand 10434 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝜑 → ((𝐿 − 1) + 1) = 𝐿)
369 0p1e1 11170 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (0 + 1) = 1
370369a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝜑 → (0 + 1) = 1)
371370oveq1d 6705 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝜑 → ((0 + 1)...(𝑁 + 1)) = (1...(𝑁 + 1)))
372367, 368, 3713eltr4d 2745 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝜑 → ((𝐿 − 1) + 1) ∈ ((0 + 1)...(𝑁 + 1)))
373 0zd 11427 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝜑 → 0 ∈ ℤ)
374126, 187zsubcld 11525 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝜑 → (𝐿 − 1) ∈ ℤ)
375 fzaddel 12413 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((0 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ ((𝐿 − 1) ∈ ℤ ∧ 1 ∈ ℤ)) → ((𝐿 − 1) ∈ (0...𝑁) ↔ ((𝐿 − 1) + 1) ∈ ((0 + 1)...(𝑁 + 1))))
376373, 130, 374, 187, 375syl22anc 1367 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝜑 → ((𝐿 − 1) ∈ (0...𝑁) ↔ ((𝐿 − 1) + 1) ∈ ((0 + 1)...(𝑁 + 1))))
377372, 376mpbird 247 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝜑 → (𝐿 − 1) ∈ (0...𝑁))
378 rabexg 4844 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑇 ∈ V → {𝑡𝑇 ∣ (𝐹𝑡) ≤ (((𝐿 − 1) − (1 / 3)) · 𝐸)} ∈ V)
37928, 378syl 17 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝜑 → {𝑡𝑇 ∣ (𝐹𝑡) ≤ (((𝐿 − 1) − (1 / 3)) · 𝐸)} ∈ V)
380 oveq1 6697 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑗 = (𝐿 − 1) → (𝑗 − (1 / 3)) = ((𝐿 − 1) − (1 / 3)))
381380oveq1d 6705 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑗 = (𝐿 − 1) → ((𝑗 − (1 / 3)) · 𝐸) = (((𝐿 − 1) − (1 / 3)) · 𝐸))
382381breq2d 4697 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑗 = (𝐿 − 1) → ((𝐹𝑡) ≤ ((𝑗 − (1 / 3)) · 𝐸) ↔ (𝐹𝑡) ≤ (((𝐿 − 1) − (1 / 3)) · 𝐸)))
383382rabbidv 3220 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑗 = (𝐿 − 1) → {𝑡𝑇 ∣ (𝐹𝑡) ≤ ((𝑗 − (1 / 3)) · 𝐸)} = {𝑡𝑇 ∣ (𝐹𝑡) ≤ (((𝐿 − 1) − (1 / 3)) · 𝐸)})
384383, 35fvmptg 6319 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝐿 − 1) ∈ (0...𝑁) ∧ {𝑡𝑇 ∣ (𝐹𝑡) ≤ (((𝐿 − 1) − (1 / 3)) · 𝐸)} ∈ V) → (𝐷‘(𝐿 − 1)) = {𝑡𝑇 ∣ (𝐹𝑡) ≤ (((𝐿 − 1) − (1 / 3)) · 𝐸)})
385377, 379, 384syl2anc 694 . . . . . . . . . . . . . . . . . . . . . . 23 (𝜑 → (𝐷‘(𝐿 − 1)) = {𝑡𝑇 ∣ (𝐹𝑡) ≤ (((𝐿 − 1) − (1 / 3)) · 𝐸)})
386359, 385neleqtrd 2751 . . . . . . . . . . . . . . . . . . . . . 22 (𝜑 → ¬ 𝑆 ∈ {𝑡𝑇 ∣ (𝐹𝑡) ≤ (((𝐿 − 1) − (1 / 3)) · 𝐸)})
387 nfcv 2793 . . . . . . . . . . . . . . . . . . . . . . . 24 𝑡(((𝐿 − 1) − (1 / 3)) · 𝐸)
38842, 43, 387nfbr 4732 . . . . . . . . . . . . . . . . . . . . . . 23 𝑡(𝐹𝑆) ≤ (((𝐿 − 1) − (1 / 3)) · 𝐸)
38946breq1d 4695 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑡 = 𝑆 → ((𝐹𝑡) ≤ (((𝐿 − 1) − (1 / 3)) · 𝐸) ↔ (𝐹𝑆) ≤ (((𝐿 − 1) − (1 / 3)) · 𝐸)))
39039, 40, 388, 389elrabf 3392 . . . . . . . . . . . . . . . . . . . . . 22 (𝑆 ∈ {𝑡𝑇 ∣ (𝐹𝑡) ≤ (((𝐿 − 1) − (1 / 3)) · 𝐸)} ↔ (𝑆𝑇 ∧ (𝐹𝑆) ≤ (((𝐿 − 1) − (1 / 3)) · 𝐸)))
391386, 390sylnib 317 . . . . . . . . . . . . . . . . . . . . 21 (𝜑 → ¬ (𝑆𝑇 ∧ (𝐹𝑆) ≤ (((𝐿 − 1) − (1 / 3)) · 𝐸)))
392 ianor 508 . . . . . . . . . . . . . . . . . . . . 21 (¬ (𝑆𝑇 ∧ (𝐹𝑆) ≤ (((𝐿 − 1) − (1 / 3)) · 𝐸)) ↔ (¬ 𝑆𝑇 ∨ ¬ (𝐹𝑆) ≤ (((𝐿 − 1) − (1 / 3)) · 𝐸)))
393391, 392sylib 208 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → (¬ 𝑆𝑇 ∨ ¬ (𝐹𝑆) ≤ (((𝐿 − 1) − (1 / 3)) · 𝐸)))
394 olc 398 . . . . . . . . . . . . . . . . . . . . 21 (𝑆𝑇 → (¬ (𝐹𝑆) ≤ (((𝐿 − 1) − (1 / 3)) · 𝐸) ∨ 𝑆𝑇))
395394anim1i 591 . . . . . . . . . . . . . . . . . . . 20 ((𝑆𝑇 ∧ (¬ 𝑆𝑇 ∨ ¬ (𝐹𝑆) ≤ (((𝐿 − 1) − (1 / 3)) · 𝐸))) → ((¬ (𝐹𝑆) ≤ (((𝐿 − 1) − (1 / 3)) · 𝐸) ∨ 𝑆𝑇) ∧ (¬ 𝑆𝑇 ∨ ¬ (𝐹𝑆) ≤ (((𝐿 − 1) − (1 / 3)) · 𝐸))))
39650, 393, 395syl2anc 694 . . . . . . . . . . . . . . . . . . 19 (𝜑 → ((¬ (𝐹𝑆) ≤ (((𝐿 − 1) − (1 / 3)) · 𝐸) ∨ 𝑆𝑇) ∧ (¬ 𝑆𝑇 ∨ ¬ (𝐹𝑆) ≤ (((𝐿 − 1) − (1 / 3)) · 𝐸))))
397 orcom 401 . . . . . . . . . . . . . . . . . . . 20 ((¬ 𝑆𝑇 ∨ ¬ (𝐹𝑆) ≤ (((𝐿 − 1) − (1 / 3)) · 𝐸)) ↔ (¬ (𝐹𝑆) ≤ (((𝐿 − 1) − (1 / 3)) · 𝐸) ∨ ¬ 𝑆𝑇))
398397anbi2i 730 . . . . . . . . . . . . . . . . . . 19 (((¬ (𝐹𝑆) ≤ (((𝐿 − 1) − (1 / 3)) · 𝐸) ∨ 𝑆𝑇) ∧ (¬ 𝑆𝑇 ∨ ¬ (𝐹𝑆) ≤ (((𝐿 − 1) − (1 / 3)) · 𝐸))) ↔ ((¬ (𝐹𝑆) ≤ (((𝐿 − 1) − (1 / 3)) · 𝐸) ∨ 𝑆𝑇) ∧ (¬ (𝐹𝑆) ≤ (((𝐿 − 1) − (1 / 3)) · 𝐸) ∨ ¬ 𝑆𝑇)))
399396, 398sylib 208 . . . . . . . . . . . . . . . . . 18 (𝜑 → ((¬ (𝐹𝑆) ≤ (((𝐿 − 1) − (1 / 3)) · 𝐸) ∨ 𝑆𝑇) ∧ (¬ (𝐹𝑆) ≤ (((𝐿 − 1) − (1 / 3)) · 𝐸) ∨ ¬ 𝑆𝑇)))
400 pm4.43 988 . . . . . . . . . . . . . . . . . 18 (¬ (𝐹𝑆) ≤ (((𝐿 − 1) − (1 / 3)) · 𝐸) ↔ ((¬ (𝐹𝑆) ≤ (((𝐿 − 1) − (1 / 3)) · 𝐸) ∨ 𝑆𝑇) ∧ (¬ (𝐹𝑆) ≤ (((𝐿 − 1) − (1 / 3)) · 𝐸) ∨ ¬ 𝑆𝑇)))
401399, 400sylibr 224 . . . . . . . . . . . . . . . . 17 (𝜑 → ¬ (𝐹𝑆) ≤ (((𝐿 − 1) − (1 / 3)) · 𝐸))
402318, 316ltnled 10222 . . . . . . . . . . . . . . . . 17 (𝜑 → ((((𝐿 − 1) − (1 / 3)) · 𝐸) < (𝐹𝑆) ↔ ¬ (𝐹𝑆) ≤ (((𝐿 − 1) − (1 / 3)) · 𝐸)))
403401, 402mpbird 247 . . . . . . . . . . . . . . . 16 (𝜑 → (((𝐿 − 1) − (1 / 3)) · 𝐸) < (𝐹𝑆))
404315, 318, 316, 358, 403lttrd 10236 . . . . . . . . . . . . . . 15 (𝜑 → (((𝐿 − 2) + (1 / 3)) · 𝐸) < (𝐹𝑆))
405315, 316, 404ltled 10223 . . . . . . . . . . . . . 14 (𝜑 → (((𝐿 − 2) + (1 / 3)) · 𝐸) ≤ (𝐹𝑆))
406405adantr 480 . . . . . . . . . . . . 13 ((𝜑𝑖 ∈ (0...(𝐿 − 2))) → (((𝐿 − 2) + (1 / 3)) · 𝐸) ≤ (𝐹𝑆))
407294, 299, 304, 312, 406letrd 10232 . . . . . . . . . . . 12 ((𝜑𝑖 ∈ (0...(𝐿 − 2))) → ((𝑖 + (1 / 3)) · 𝐸) ≤ (𝐹𝑆))
408 nfcv 2793 . . . . . . . . . . . . . 14 𝑡((𝑖 + (1 / 3)) · 𝐸)
409408, 43, 42nfbr 4732 . . . . . . . . . . . . 13 𝑡((𝑖 + (1 / 3)) · 𝐸) ≤ (𝐹𝑆)
41046breq2d 4697 . . . . . . . . . . . . 13 (𝑡 = 𝑆 → (((𝑖 + (1 / 3)) · 𝐸) ≤ (𝐹𝑡) ↔ ((𝑖 + (1 / 3)) · 𝐸) ≤ (𝐹𝑆)))
41139, 40, 409, 410elrabf 3392 . . . . . . . . . . . 12 (𝑆 ∈ {𝑡𝑇 ∣ ((𝑖 + (1 / 3)) · 𝐸) ≤ (𝐹𝑡)} ↔ (𝑆𝑇 ∧ ((𝑖 + (1 / 3)) · 𝐸) ≤ (𝐹𝑆)))
412287, 407, 411sylanbrc 699 . . . . . . . . . . 11 ((𝜑𝑖 ∈ (0...(𝐿 − 2))) → 𝑆 ∈ {𝑡𝑇 ∣ ((𝑖 + (1 / 3)) · 𝐸) ≤ (𝐹𝑡)})
413 rabexg 4844 . . . . . . . . . . . . . 14 (𝑇 ∈ V → {𝑡𝑇 ∣ ((𝑖 + (1 / 3)) · 𝐸) ≤ (𝐹𝑡)} ∈ V)
41428, 413syl 17 . . . . . . . . . . . . 13 (𝜑 → {𝑡𝑇 ∣ ((𝑖 + (1 / 3)) · 𝐸) ≤ (𝐹𝑡)} ∈ V)
415414adantr 480 . . . . . . . . . . . 12 ((𝜑𝑖 ∈ (0...(𝐿 − 2))) → {𝑡𝑇 ∣ ((𝑖 + (1 / 3)) · 𝐸) ≤ (𝐹𝑡)} ∈ V)
416 oveq1 6697 . . . . . . . . . . . . . . . 16 (𝑗 = 𝑖 → (𝑗 + (1 / 3)) = (𝑖 + (1 / 3)))
417416oveq1d 6705 . . . . . . . . . . . . . . 15 (𝑗 = 𝑖 → ((𝑗 + (1 / 3)) · 𝐸) = ((𝑖 + (1 / 3)) · 𝐸))
418417breq1d 4695 . . . . . . . . . . . . . 14 (𝑗 = 𝑖 → (((𝑗 + (1 / 3)) · 𝐸) ≤ (𝐹𝑡) ↔ ((𝑖 + (1 / 3)) · 𝐸) ≤ (𝐹𝑡)))
419418rabbidv 3220 . . . . . . . . . . . . 13 (𝑗 = 𝑖 → {𝑡𝑇 ∣ ((𝑗 + (1 / 3)) · 𝐸) ≤ (𝐹𝑡)} = {𝑡𝑇 ∣ ((𝑖 + (1 / 3)) · 𝐸) ≤ (𝐹𝑡)})
420 stoweidlem26.5 . . . . . . . . . . . . 13 𝐵 = (𝑗 ∈ (0...𝑁) ↦ {𝑡𝑇 ∣ ((𝑗 + (1 / 3)) · 𝐸) ≤ (𝐹𝑡)})
421419, 420fvmptg 6319 . . . . . . . . . . . 12 ((𝑖 ∈ (0...𝑁) ∧ {𝑡𝑇 ∣ ((𝑖 + (1 / 3)) · 𝐸) ≤ (𝐹𝑡)} ∈ V) → (𝐵𝑖) = {𝑡𝑇 ∣ ((𝑖 + (1 / 3)) · 𝐸) ≤ (𝐹𝑡)})
422151, 415, 421syl2anc 694 . . . . . . . . . . 11 ((𝜑𝑖 ∈ (0...(𝐿 − 2))) → (𝐵𝑖) = {𝑡𝑇 ∣ ((𝑖 + (1 / 3)) · 𝐸) ≤ (𝐹𝑡)})
423412, 422eleqtrrd 2733 . . . . . . . . . 10 ((𝜑𝑖 ∈ (0...(𝐿 − 2))) → 𝑆 ∈ (𝐵𝑖))
4241463ad2ant1 1102 . . . . . . . . . . . . . 14 ((𝜑𝑖 ∈ (0...(𝐿 − 2)) ∧ 𝑆 ∈ (𝐵𝑖)) → ((𝐿 − 2) ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ (𝐿 − 2) ≤ 𝑁))
425424, 147sylibr 224 . . . . . . . . . . . . 13 ((𝜑𝑖 ∈ (0...(𝐿 − 2)) ∧ 𝑆 ∈ (𝐵𝑖)) → 𝑁 ∈ (ℤ‘(𝐿 − 2)))
426425, 149syl 17 . . . . . . . . . . . 12 ((𝜑𝑖 ∈ (0...(𝐿 − 2)) ∧ 𝑆 ∈ (𝐵𝑖)) → (0...(𝐿 − 2)) ⊆ (0...𝑁))
427 simp2 1082 . . . . . . . . . . . 12 ((𝜑𝑖 ∈ (0...(𝐿 − 2)) ∧ 𝑆 ∈ (𝐵𝑖)) → 𝑖 ∈ (0...(𝐿 − 2)))
428426, 427sseldd 3637 . . . . . . . . . . 11 ((𝜑𝑖 ∈ (0...(𝐿 − 2)) ∧ 𝑆 ∈ (𝐵𝑖)) → 𝑖 ∈ (0...𝑁))
429 elex 3243 . . . . . . . . . . . . 13 (𝑆 ∈ (𝐵𝑖) → 𝑆 ∈ V)
4304293ad2ant3 1104 . . . . . . . . . . . 12 ((𝜑𝑖 ∈ (0...𝑁) ∧ 𝑆 ∈ (𝐵𝑖)) → 𝑆 ∈ V)
431 nfcv 2793 . . . . . . . . . . . . . . . . . . 19 𝑡(0...𝑁)
432 nfrab1 3152 . . . . . . . . . . . . . . . . . . 19 𝑡{𝑡𝑇 ∣ ((𝑗 + (1 / 3)) · 𝐸) ≤ (𝐹𝑡)}
433431, 432nfmpt 4779 . . . . . . . . . . . . . . . . . 18 𝑡(𝑗 ∈ (0...𝑁) ↦ {𝑡𝑇 ∣ ((𝑗 + (1 / 3)) · 𝐸) ≤ (𝐹𝑡)})
434420, 433nfcxfr 2791 . . . . . . . . . . . . . . . . 17 𝑡𝐵
435 nfcv 2793 . . . . . . . . . . . . . . . . 17 𝑡𝑖
436434, 435nffv 6236 . . . . . . . . . . . . . . . 16 𝑡(𝐵𝑖)
437436nfel2 2810 . . . . . . . . . . . . . . 15 𝑡 𝑆 ∈ (𝐵𝑖)
43889, 90, 437nf3an 1871 . . . . . . . . . . . . . 14 𝑡(𝜑𝑖 ∈ (0...𝑁) ∧ 𝑆 ∈ (𝐵𝑖))
439 nfv 1883 . . . . . . . . . . . . . 14 𝑡(1 − (𝐸 / 𝑁)) < ((𝑋𝑖)‘𝑆)
440438, 439nfim 1865 . . . . . . . . . . . . 13 𝑡((𝜑𝑖 ∈ (0...𝑁) ∧ 𝑆 ∈ (𝐵𝑖)) → (1 − (𝐸 / 𝑁)) < ((𝑋𝑖)‘𝑆))
441 eleq1 2718 . . . . . . . . . . . . . . 15 (𝑡 = 𝑆 → (𝑡 ∈ (𝐵𝑖) ↔ 𝑆 ∈ (𝐵𝑖)))
4424413anbi3d 1445 . . . . . . . . . . . . . 14 (𝑡 = 𝑆 → ((𝜑𝑖 ∈ (0...𝑁) ∧ 𝑡 ∈ (𝐵𝑖)) ↔ (𝜑𝑖 ∈ (0...𝑁) ∧ 𝑆 ∈ (𝐵𝑖))))
44394breq2d 4697 . . . . . . . . . . . . . 14 (𝑡 = 𝑆 → ((1 − (𝐸 / 𝑁)) < ((𝑋𝑖)‘𝑡) ↔ (1 − (𝐸 / 𝑁)) < ((𝑋𝑖)‘𝑆)))
444442, 443imbi12d 333 . . . . . . . . . . . . 13 (𝑡 = 𝑆 → (((𝜑𝑖 ∈ (0...𝑁) ∧ 𝑡 ∈ (𝐵𝑖)) → (1 − (𝐸 / 𝑁)) < ((𝑋𝑖)‘𝑡)) ↔ ((𝜑𝑖 ∈ (0...𝑁) ∧ 𝑆 ∈ (𝐵𝑖)) → (1 − (𝐸 / 𝑁)) < ((𝑋𝑖)‘𝑆))))
445 stoweidlem26.15 . . . . . . . . . . . . 13 ((𝜑𝑖 ∈ (0...𝑁) ∧ 𝑡 ∈ (𝐵𝑖)) → (1 − (𝐸 / 𝑁)) < ((𝑋𝑖)‘𝑡))
446440, 444, 445vtoclg1f 3296 . . . . . . . . . . . 12 (𝑆 ∈ V → ((𝜑𝑖 ∈ (0...𝑁) ∧ 𝑆 ∈ (𝐵𝑖)) → (1 − (𝐸 / 𝑁)) < ((𝑋𝑖)‘𝑆)))
447430, 446mpcom 38 . . . . . . . . . . 11 ((𝜑𝑖 ∈ (0...𝑁) ∧ 𝑆 ∈ (𝐵𝑖)) → (1 − (𝐸 / 𝑁)) < ((𝑋𝑖)‘𝑆))
448428, 447syld3an2 1413 . . . . . . . . . 10 ((𝜑𝑖 ∈ (0...(𝐿 − 2)) ∧ 𝑆 ∈ (𝐵𝑖)) → (1 − (𝐸 / 𝑁)) < ((𝑋𝑖)‘𝑆))
449423, 448mpd3an3 1465 . . . . . . . . 9 ((𝜑𝑖 ∈ (0...(𝐿 − 2))) → (1 − (𝐸 / 𝑁)) < ((𝑋𝑖)‘𝑆))
450449adantlr 751 . . . . . . . 8 (((𝜑 ∧ ¬ 𝐿 = 1) ∧ 𝑖 ∈ (0...(𝐿 − 2))) → (1 − (𝐸 / 𝑁)) < ((𝑋𝑖)‘𝑆))
451280, 282, 283, 286, 450fsumlt 14576 . . . . . . 7 ((𝜑 ∧ ¬ 𝐿 = 1) → Σ𝑖 ∈ (0...(𝐿 − 2))(1 − (𝐸 / 𝑁)) < Σ𝑖 ∈ (0...(𝐿 − 2))((𝑋𝑖)‘𝑆))
452279, 451eqbrtrrd 4709 . . . . . 6 ((𝜑 ∧ ¬ 𝐿 = 1) → ((1 − (𝐸 / 𝑁)) · (𝐿 − 1)) < Σ𝑖 ∈ (0...(𝐿 − 2))((𝑋𝑖)‘𝑆))
453122adantr 480 . . . . . . 7 ((𝜑 ∧ ¬ 𝐿 = 1) → ((1 − (𝐸 / 𝑁)) · (𝐿 − 1)) ∈ ℝ)
454153adantr 480 . . . . . . 7 ((𝜑 ∧ ¬ 𝐿 = 1) → Σ𝑖 ∈ (0...(𝐿 − 2))((𝑋𝑖)‘𝑆) ∈ ℝ)
455308adantr 480 . . . . . . 7 ((𝜑 ∧ ¬ 𝐿 = 1) → (𝐸 ∈ ℝ ∧ 0 < 𝐸))
456 ltmul2 10912 . . . . . . 7 ((((1 − (𝐸 / 𝑁)) · (𝐿 − 1)) ∈ ℝ ∧ Σ𝑖 ∈ (0...(𝐿 − 2))((𝑋𝑖)‘𝑆) ∈ ℝ ∧ (𝐸 ∈ ℝ ∧ 0 < 𝐸)) → (((1 − (𝐸 / 𝑁)) · (𝐿 − 1)) < Σ𝑖 ∈ (0...(𝐿 − 2))((𝑋𝑖)‘𝑆) ↔ (𝐸 · ((1 − (𝐸 / 𝑁)) · (𝐿 − 1))) < (𝐸 · Σ𝑖 ∈ (0...(𝐿 − 2))((𝑋𝑖)‘𝑆))))
457453, 454, 455, 456syl3anc 1366 . . . . . 6 ((𝜑 ∧ ¬ 𝐿 = 1) → (((1 − (𝐸 / 𝑁)) · (𝐿 − 1)) < Σ𝑖 ∈ (0...(𝐿 − 2))((𝑋𝑖)‘𝑆) ↔ (𝐸 · ((1 − (𝐸 / 𝑁)) · (𝐿 − 1))) < (𝐸 · Σ𝑖 ∈ (0...(𝐿 − 2))((𝑋𝑖)‘𝑆))))
458452, 457mpbid 222 . . . . 5 ((𝜑 ∧ ¬ 𝐿 = 1) → (𝐸 · ((1 − (𝐸 / 𝑁)) · (𝐿 − 1))) < (𝐸 · Σ𝑖 ∈ (0...(𝐿 − 2))((𝑋𝑖)‘𝑆)))
459116, 124, 155, 228, 458lttrd 10236 . . . 4 ((𝜑 ∧ ¬ 𝐿 = 1) → ((𝐿 − (4 / 3)) · 𝐸) < (𝐸 · Σ𝑖 ∈ (0...(𝐿 − 2))((𝑋𝑖)‘𝑆)))
460151, 53syldan 486 . . . . . . . . . 10 ((𝜑𝑖 ∈ (0...(𝐿 − 2))) → (𝐸 · ((𝑋𝑖)‘𝑆)) ∈ ℝ)
461460adantlr 751 . . . . . . . . 9 (((𝜑 ∧ ¬ 𝐿 = 1) ∧ 𝑖 ∈ (0...(𝐿 − 2))) → (𝐸 · ((𝑋𝑖)‘𝑆)) ∈ ℝ)
462461recnd 10106 . . . . . . . 8 (((𝜑 ∧ ¬ 𝐿 = 1) ∧ 𝑖 ∈ (0...(𝐿 − 2))) → (𝐸 · ((𝑋𝑖)‘𝑆)) ∈ ℂ)
463280, 462fsumcl 14508 . . . . . . 7 ((𝜑 ∧ ¬ 𝐿 = 1) → Σ𝑖 ∈ (0...(𝐿 − 2))(𝐸 · ((𝑋𝑖)‘𝑆)) ∈ ℂ)
464463addid1d 10274 . . . . . 6 ((𝜑 ∧ ¬ 𝐿 = 1) → (Σ𝑖 ∈ (0...(𝐿 − 2))(𝐸 · ((𝑋𝑖)‘𝑆)) + 0) = Σ𝑖 ∈ (0...(𝐿 − 2))(𝐸 · ((𝑋𝑖)‘𝑆)))
465 0red 10079 . . . . . . 7 ((𝜑 ∧ ¬ 𝐿 = 1) → 0 ∈ ℝ)
466 fzfid 12812 . . . . . . . 8 ((𝜑 ∧ ¬ 𝐿 = 1) → ((𝐿 − 1)...𝑁) ∈ Fin)
46714adantr 480 . . . . . . . . . 10 ((𝜑𝑖 ∈ ((𝐿 − 1)...𝑁)) → 𝐸 ∈ ℝ)
468 0red 10079 . . . . . . . . . . . . 13 ((𝜑𝑖 ∈ ((𝐿 − 1)...𝑁)) → 0 ∈ ℝ)
469121adantr 480 . . . . . . . . . . . . 13 ((𝜑𝑖 ∈ ((𝐿 − 1)...𝑁)) → (𝐿 − 1) ∈ ℝ)
470 elfzelz 12380 . . . . . . . . . . . . . . 15 (𝑖 ∈ ((𝐿 − 1)...𝑁) → 𝑖 ∈ ℤ)
471470zred 11520 . . . . . . . . . . . . . 14 (𝑖 ∈ ((𝐿 − 1)...𝑁) → 𝑖 ∈ ℝ)
472471adantl 481 . . . . . . . . . . . . 13 ((𝜑𝑖 ∈ ((𝐿 − 1)...𝑁)) → 𝑖 ∈ ℝ)
473 1m1e0 11127 . . . . . . . . . . . . . . 15 (1 − 1) = 0
474117, 109, 117, 360lesub1dd 10681 . . . . . . . . . . . . . . 15 (𝜑 → (1 − 1) ≤ (𝐿 − 1))
475473, 474syl5eqbrr 4721 . . . . . . . . . . . . . 14 (𝜑 → 0 ≤ (𝐿 − 1))
476475adantr 480 . . . . . . . . . . . . 13 ((𝜑𝑖 ∈ ((𝐿 − 1)...𝑁)) → 0 ≤ (𝐿 − 1))
477 simpr 476 . . . . . . . . . . . . . . 15 ((𝜑𝑖 ∈ ((𝐿 − 1)...𝑁)) → 𝑖 ∈ ((𝐿 − 1)...𝑁))
478470adantl 481 . . . . . . . . . . . . . . . 16 ((𝜑𝑖 ∈ ((𝐿 − 1)...𝑁)) → 𝑖 ∈ ℤ)
479374adantr 480 . . . . . . . . . . . . . . . 16 ((𝜑𝑖 ∈ ((𝐿 − 1)...𝑁)) → (𝐿 − 1) ∈ ℤ)
480130adantr 480 . . . . . . . . . . . . . . . 16 ((𝜑𝑖 ∈ ((𝐿 − 1)...𝑁)) → 𝑁 ∈ ℤ)
481 elfz 12370 . . . . . . . . . . . . . . . 16 ((𝑖 ∈ ℤ ∧ (𝐿 − 1) ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑖 ∈ ((𝐿 − 1)...𝑁) ↔ ((𝐿 − 1) ≤ 𝑖𝑖𝑁)))
482478, 479, 480, 481syl3anc 1366 . . . . . . . . . . . . . . 15 ((𝜑𝑖 ∈ ((𝐿 − 1)...𝑁)) → (𝑖 ∈ ((𝐿 − 1)...𝑁) ↔ ((𝐿 − 1) ≤ 𝑖𝑖𝑁)))
483477, 482mpbid 222 . . . . . . . . . . . . . 14 ((𝜑𝑖 ∈ ((𝐿 − 1)...𝑁)) → ((𝐿 − 1) ≤ 𝑖𝑖𝑁))
484483simpld 474 . . . . . . . . . . . . 13 ((𝜑𝑖 ∈ ((𝐿 − 1)...𝑁)) → (𝐿 − 1) ≤ 𝑖)
485468, 469, 472, 476, 484letrd 10232 . . . . . . . . . . . 12 ((𝜑𝑖 ∈ ((𝐿 − 1)...𝑁)) → 0 ≤ 𝑖)
486 elfzle2 12383 . . . . . . . . . . . . 13 (𝑖 ∈ ((𝐿 − 1)...𝑁) → 𝑖𝑁)
487486adantl 481 . . . . . . . . . . . 12 ((𝜑𝑖 ∈ ((𝐿 − 1)...𝑁)) → 𝑖𝑁)
488 0zd 11427 . . . . . . . . . . . . 13 ((𝜑𝑖 ∈ ((𝐿 − 1)...𝑁)) → 0 ∈ ℤ)
489 elfz 12370 . . . . . . . . . . . . 13 ((𝑖 ∈ ℤ ∧ 0 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑖 ∈ (0...𝑁) ↔ (0 ≤ 𝑖𝑖𝑁)))
490478, 488, 480, 489syl3anc 1366 . . . . . . . . . . . 12 ((𝜑𝑖 ∈ ((𝐿 − 1)...𝑁)) → (𝑖 ∈ (0...𝑁) ↔ (0 ≤ 𝑖𝑖𝑁)))
491485, 487, 490mpbir2and 977 . . . . . . . . . . 11 ((𝜑𝑖 ∈ ((𝐿 − 1)...𝑁)) → 𝑖 ∈ (0...𝑁))
492491, 52syldan 486 . . . . . . . . . 10 ((𝜑𝑖 ∈ ((𝐿 − 1)...𝑁)) → ((𝑋𝑖)‘𝑆) ∈ ℝ)
493467, 492remulcld 10108 . . . . . . . . 9 ((𝜑𝑖 ∈ ((𝐿 − 1)...𝑁)) → (𝐸 · ((𝑋𝑖)‘𝑆)) ∈ ℝ)
494493adantlr 751 . . . . . . . 8 (((𝜑 ∧ ¬ 𝐿 = 1) ∧ 𝑖 ∈ ((𝐿 − 1)...𝑁)) → (𝐸 · ((𝑋𝑖)‘𝑆)) ∈ ℝ)
495466, 494fsumrecl 14509 . . . . . . 7 ((𝜑 ∧ ¬ 𝐿 = 1) → Σ𝑖 ∈ ((𝐿 − 1)...𝑁)(𝐸 · ((𝑋𝑖)‘𝑆)) ∈ ℝ)
496280, 461fsumrecl 14509 . . . . . . 7 ((𝜑 ∧ ¬ 𝐿 = 1) → Σ𝑖 ∈ (0...(𝐿 − 2))(𝐸 · ((𝑋𝑖)‘𝑆)) ∈ ℝ)
497 fzfid 12812 . . . . . . . . 9 (𝜑 → ((𝐿 − 1)...𝑁) ∈ Fin)
498177adantr 480 . . . . . . . . . . 11 ((𝜑𝑖 ∈ ((𝐿 − 1)...𝑁)) → 𝐸 ∈ ℂ)
499498mul01d 10273 . . . . . . . . . 10 ((𝜑𝑖 ∈ ((𝐿 − 1)...𝑁)) → (𝐸 · 0) = 0)
500491, 101syldan 486 . . . . . . . . . . 11 ((𝜑𝑖 ∈ ((𝐿 − 1)...𝑁)) → 0 ≤ ((𝑋𝑖)‘𝑆))
501308adantr 480 . . . . . . . . . . . 12 ((𝜑𝑖 ∈ ((𝐿 − 1)...𝑁)) → (𝐸 ∈ ℝ ∧ 0 < 𝐸))
502 lemul2 10914 . . . . . . . . . . . 12 ((0 ∈ ℝ ∧ ((𝑋𝑖)‘𝑆) ∈ ℝ ∧ (𝐸 ∈ ℝ ∧ 0 < 𝐸)) → (0 ≤ ((𝑋𝑖)‘𝑆) ↔ (𝐸 · 0) ≤ (𝐸 · ((𝑋𝑖)‘𝑆))))
503468, 492, 501, 502syl3anc 1366 . . . . . . . . . . 11 ((𝜑𝑖 ∈ ((𝐿 − 1)...𝑁)) → (0 ≤ ((𝑋𝑖)‘𝑆) ↔ (𝐸 · 0) ≤ (𝐸 · ((𝑋𝑖)‘𝑆))))
504500, 503mpbid 222 . . . . . . . . . 10 ((𝜑𝑖 ∈ ((𝐿 − 1)...𝑁)) → (𝐸 · 0) ≤ (𝐸 · ((𝑋𝑖)‘𝑆)))
505499, 504eqbrtrrd 4709 . . . . . . . . 9 ((𝜑𝑖 ∈ ((𝐿 − 1)...𝑁)) → 0 ≤ (𝐸 · ((𝑋𝑖)‘𝑆)))
506497, 493, 505fsumge0 14571 . . . . . . . 8 (𝜑 → 0 ≤ Σ𝑖 ∈ ((𝐿 − 1)...𝑁)(𝐸 · ((𝑋𝑖)‘𝑆)))
507506adantr 480 . . . . . . 7 ((𝜑 ∧ ¬ 𝐿 = 1) → 0 ≤ Σ𝑖 ∈ ((𝐿 − 1)...𝑁)(𝐸 · ((𝑋𝑖)‘𝑆)))
508465, 495, 496, 507leadd2dd 10680 . . . . . 6 ((𝜑 ∧ ¬ 𝐿 = 1) → (Σ𝑖 ∈ (0...(𝐿 − 2))(𝐸 · ((𝑋𝑖)‘𝑆)) + 0) ≤ (Σ𝑖 ∈ (0...(𝐿 − 2))(𝐸 · ((𝑋𝑖)‘𝑆)) + Σ𝑖 ∈ ((𝐿 − 1)...𝑁)(𝐸 · ((𝑋𝑖)‘𝑆))))
509464, 508eqbrtrrd 4709 . . . . 5 ((𝜑 ∧ ¬ 𝐿 = 1) → Σ𝑖 ∈ (0...(𝐿 − 2))(𝐸 · ((𝑋𝑖)‘𝑆)) ≤ (Σ𝑖 ∈ (0...(𝐿 − 2))(𝐸 · ((𝑋𝑖)‘𝑆)) + Σ𝑖 ∈ ((𝐿 − 1)...𝑁)(𝐸 · ((𝑋𝑖)‘𝑆))))
510152recnd 10106 . . . . . . 7 ((𝜑𝑖 ∈ (0...(𝐿 − 2))) → ((𝑋𝑖)‘𝑆) ∈ ℂ)
511125, 177, 510fsummulc2 14560 . . . . . 6 (𝜑 → (𝐸 · Σ𝑖 ∈ (0...(𝐿 − 2))((𝑋𝑖)‘𝑆)) = Σ𝑖 ∈ (0...(𝐿 − 2))(𝐸 · ((𝑋𝑖)‘𝑆)))
512511adantr 480 . . . . 5 ((𝜑 ∧ ¬ 𝐿 = 1) → (𝐸 · Σ𝑖 ∈ (0...(𝐿 − 2))((𝑋𝑖)‘𝑆)) = Σ𝑖 ∈ (0...(𝐿 − 2))(𝐸 · ((𝑋𝑖)‘𝑆)))
513 stoweidlem26.2 . . . . . . . . 9 𝑗𝜑
514 elfzelz 12380 . . . . . . . . . . . . . . . 16 (𝑗 ∈ (0...(𝐿 − 2)) → 𝑗 ∈ ℤ)
515514adantl 481 . . . . . . . . . . . . . . 15 ((𝜑𝑗 ∈ (0...(𝐿 − 2))) → 𝑗 ∈ ℤ)
516515zred 11520 . . . . . . . . . . . . . 14 ((𝜑𝑗 ∈ (0...(𝐿 − 2))) → 𝑗 ∈ ℝ)
517313adantr 480 . . . . . . . . . . . . . 14 ((𝜑𝑗 ∈ (0...(𝐿 − 2))) → (𝐿 − 2) ∈ ℝ)
518121adantr 480 . . . . . . . . . . . . . 14 ((𝜑𝑗 ∈ (0...(𝐿 − 2))) → (𝐿 − 1) ∈ ℝ)
519 simpr 476 . . . . . . . . . . . . . . . 16 ((𝜑𝑗 ∈ (0...(𝐿 − 2))) → 𝑗 ∈ (0...(𝐿 − 2)))
520 0zd 11427 . . . . . . . . . . . . . . . . 17 ((𝜑𝑗 ∈ (0...(𝐿 − 2))) → 0 ∈ ℤ)
521129adantr 480 . . . . . . . . . . . . . . . . 17 ((𝜑𝑗 ∈ (0...(𝐿 − 2))) → (𝐿 − 2) ∈ ℤ)
522 elfz 12370 . . . . . . . . . . . . . . . . 17 ((𝑗 ∈ ℤ ∧ 0 ∈ ℤ ∧ (𝐿 − 2) ∈ ℤ) → (𝑗 ∈ (0...(𝐿 − 2)) ↔ (0 ≤ 𝑗𝑗 ≤ (𝐿 − 2))))
523515, 520, 521, 522syl3anc 1366 . . . . . . . . . . . . . . . 16 ((𝜑𝑗 ∈ (0...(𝐿 − 2))) → (𝑗 ∈ (0...(𝐿 − 2)) ↔ (0 ≤ 𝑗𝑗 ≤ (𝐿 − 2))))
524519, 523mpbid 222 . . . . . . . . . . . . . . 15 ((𝜑𝑗 ∈ (0...(𝐿 − 2))) → (0 ≤ 𝑗𝑗 ≤ (𝐿 − 2)))
525524simprd 478 . . . . . . . . . . . . . 14 ((𝜑𝑗 ∈ (0...(𝐿 − 2))) → 𝑗 ≤ (𝐿 − 2))
526117, 133, 109ltsub2d 10675 . . . . . . . . . . . . . . . 16 (𝜑 → (1 < 2 ↔ (𝐿 − 2) < (𝐿 − 1)))
527350, 526mpbii 223 . . . . . . . . . . . . . . 15 (𝜑 → (𝐿 − 2) < (𝐿 − 1))
528527adantr 480 . . . . . . . . . . . . . 14 ((𝜑𝑗 ∈ (0...(𝐿 − 2))) → (𝐿 − 2) < (𝐿 − 1))
529516, 517, 518, 525, 528lelttrd 10233 . . . . . . . . . . . . 13 ((𝜑𝑗 ∈ (0...(𝐿 − 2))) → 𝑗 < (𝐿 − 1))
530516, 518ltnled 10222 . . . . . . . . . . . . 13 ((𝜑𝑗 ∈ (0...(𝐿 − 2))) → (𝑗 < (𝐿 − 1) ↔ ¬ (𝐿 − 1) ≤ 𝑗))
531529, 530mpbid 222 . . . . . . . . . . . 12 ((𝜑𝑗 ∈ (0...(𝐿 − 2))) → ¬ (𝐿 − 1) ≤ 𝑗)
532531intnanrd 983 . . . . . . . . . . 11 ((𝜑𝑗 ∈ (0...(𝐿 − 2))) → ¬ ((𝐿 − 1) ≤ 𝑗𝑗𝑁))
533374adantr 480 . . . . . . . . . . . 12 ((𝜑𝑗 ∈ (0...(𝐿 − 2))) → (𝐿 − 1) ∈ ℤ)
534130adantr 480 . . . . . . . . . . . 12 ((𝜑𝑗 ∈ (0...(𝐿 − 2))) → 𝑁 ∈ ℤ)
535 elfz 12370 . . . . . . . . . . . 12 ((𝑗 ∈ ℤ ∧ (𝐿 − 1) ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑗 ∈ ((𝐿 − 1)...𝑁) ↔ ((𝐿 − 1) ≤ 𝑗𝑗𝑁)))
536515, 533, 534, 535syl3anc 1366 . . . . . . . . . . 11 ((𝜑𝑗 ∈ (0...(𝐿 − 2))) → (𝑗 ∈ ((𝐿 − 1)...𝑁) ↔ ((𝐿 − 1) ≤ 𝑗𝑗𝑁)))
537532, 536mtbird 314 . . . . . . . . . 10 ((𝜑𝑗 ∈ (0...(𝐿 − 2))) → ¬ 𝑗 ∈ ((𝐿 − 1)...𝑁))
538537ex 449 . . . . . . . . 9 (𝜑 → (𝑗 ∈ (0...(𝐿 − 2)) → ¬ 𝑗 ∈ ((𝐿 − 1)...𝑁)))
539513, 538ralrimi 2986 . . . . . . . 8 (𝜑 → ∀𝑗 ∈ (0...(𝐿 − 2)) ¬ 𝑗 ∈ ((𝐿 − 1)...𝑁))
540 disj 4050 . . . . . . . 8 (((0...(𝐿 − 2)) ∩ ((𝐿 − 1)...𝑁)) = ∅ ↔ ∀𝑗 ∈ (0...(𝐿 − 2)) ¬ 𝑗 ∈ ((𝐿 − 1)...𝑁))
541539, 540sylibr 224 . . . . . . 7 (𝜑 → ((0...(𝐿 − 2)) ∩ ((𝐿 − 1)...𝑁)) = ∅)
542541adantr 480 . . . . . 6 ((𝜑 ∧ ¬ 𝐿 = 1) → ((0...(𝐿 − 2)) ∩ ((𝐿 − 1)...𝑁)) = ∅)
543145adantr 480 . . . . . . . . 9 ((𝜑 ∧ ¬ 𝐿 = 1) → (𝐿 − 2) ≤ 𝑁)
544129, 373, 1303jca 1261 . . . . . . . . . . 11 (𝜑 → ((𝐿 − 2) ∈ ℤ ∧ 0 ∈ ℤ ∧ 𝑁 ∈ ℤ))
545544adantr 480 . . . . . . . . . 10 ((𝜑 ∧ ¬ 𝐿 = 1) → ((𝐿 − 2) ∈ ℤ ∧ 0 ∈ ℤ ∧ 𝑁 ∈ ℤ))
546 elfz 12370 . . . . . . . . . 10 (((𝐿 − 2) ∈ ℤ ∧ 0 ∈ ℤ ∧ 𝑁 ∈ ℤ) → ((𝐿 − 2) ∈ (0...𝑁) ↔ (0 ≤ (𝐿 − 2) ∧ (𝐿 − 2) ≤ 𝑁)))
547545, 546syl 17 . . . . . . . . 9 ((𝜑 ∧ ¬ 𝐿 = 1) → ((𝐿 − 2) ∈ (0...𝑁) ↔ (0 ≤ (𝐿 − 2) ∧ (𝐿 − 2) ≤ 𝑁)))
548253, 543, 547mpbir2and 977 . . . . . . . 8 ((𝜑 ∧ ¬ 𝐿 = 1) → (𝐿 − 2) ∈ (0...𝑁))
549 fzsplit 12405 . . . . . . . 8 ((𝐿 − 2) ∈ (0...𝑁) → (0...𝑁) = ((0...(𝐿 − 2)) ∪ (((𝐿 − 2) + 1)...𝑁)))
550548, 549syl 17 . . . . . . 7 ((𝜑 ∧ ¬ 𝐿 = 1) → (0...𝑁) = ((0...(𝐿 − 2)) ∪ (((𝐿 − 2) + 1)...𝑁)))
551264, 270, 2713eqtrd 2689 . . . . . . . . . 10 (𝜑 → ((𝐿 − 2) + 1) = (𝐿 − 1))
552551oveq1d 6705 . . . . . . . . 9 (𝜑 → (((𝐿 − 2) + 1)...𝑁) = ((𝐿 − 1)...𝑁))
553552uneq2d 3800 . . . . . . . 8 (𝜑 → ((0...(𝐿 − 2)) ∪ (((𝐿 − 2) + 1)...𝑁)) = ((0...(𝐿 − 2)) ∪ ((𝐿 − 1)...𝑁)))
554553adantr 480 . . . . . . 7 ((𝜑 ∧ ¬ 𝐿 = 1) → ((0...(𝐿 − 2)) ∪ (((𝐿 − 2) + 1)...𝑁)) = ((0...(𝐿 − 2)) ∪ ((𝐿 − 1)...𝑁)))
555550, 554eqtrd 2685 . . . . . 6 ((𝜑 ∧ ¬ 𝐿 = 1) → (0...𝑁) = ((0...(𝐿 − 2)) ∪ ((𝐿 − 1)...𝑁)))
556 fzfid 12812 . . . . . 6 ((𝜑 ∧ ¬ 𝐿 = 1) → (0...𝑁) ∈ Fin)
557177adantr 480 . . . . . . . 8 ((𝜑𝑖 ∈ (0...𝑁)) → 𝐸 ∈ ℂ)
55852recnd 10106 . . . . . . . 8 ((𝜑𝑖 ∈ (0...𝑁)) → ((𝑋𝑖)‘𝑆) ∈ ℂ)
559557, 558mulcld 10098 . . . . . . 7 ((𝜑𝑖 ∈ (0...𝑁)) → (𝐸 · ((𝑋𝑖)‘𝑆)) ∈ ℂ)
560559adantlr 751 . . . . . 6 (((𝜑 ∧ ¬ 𝐿 = 1) ∧ 𝑖 ∈ (0...𝑁)) → (𝐸 · ((𝑋𝑖)‘𝑆)) ∈ ℂ)
561542, 555, 556, 560fsumsplit 14515 . . . . 5 ((𝜑 ∧ ¬ 𝐿 = 1) → Σ𝑖 ∈ (0...𝑁)(𝐸 · ((𝑋𝑖)‘𝑆)) = (Σ𝑖 ∈ (0...(𝐿 − 2))(𝐸 · ((𝑋𝑖)‘𝑆)) + Σ𝑖 ∈ ((𝐿 − 1)...𝑁)(𝐸 · ((𝑋𝑖)‘𝑆))))
562509, 512, 5613brtr4d 4717 . . . 4 ((𝜑 ∧ ¬ 𝐿 = 1) → (𝐸 · Σ𝑖 ∈ (0...(𝐿 − 2))((𝑋𝑖)‘𝑆)) ≤ Σ𝑖 ∈ (0...𝑁)(𝐸 · ((𝑋𝑖)‘𝑆)))
563115, 154, 543jca 1261 . . . . . 6 (𝜑 → (((𝐿 − (4 / 3)) · 𝐸) ∈ ℝ ∧ (𝐸 · Σ𝑖 ∈ (0...(𝐿 − 2))((𝑋𝑖)‘𝑆)) ∈ ℝ ∧ Σ𝑖 ∈ (0...𝑁)(𝐸 · ((𝑋𝑖)‘𝑆)) ∈ ℝ))
564563adantr 480 . . . . 5 ((𝜑 ∧ ¬ 𝐿 = 1) → (((𝐿 − (4 / 3)) · 𝐸) ∈ ℝ ∧ (𝐸 · Σ𝑖 ∈ (0...(𝐿 − 2))((𝑋𝑖)‘𝑆)) ∈ ℝ ∧ Σ𝑖 ∈ (0...𝑁)(𝐸 · ((𝑋𝑖)‘𝑆)) ∈ ℝ))
565 ltletr 10167 . . . . 5 ((((𝐿 − (4 / 3)) · 𝐸) ∈ ℝ ∧ (𝐸 · Σ𝑖 ∈ (0...(𝐿 − 2))((𝑋𝑖)‘𝑆)) ∈ ℝ ∧ Σ𝑖 ∈ (0...𝑁)(𝐸 · ((𝑋𝑖)‘𝑆)) ∈ ℝ) → ((((𝐿 − (4 / 3)) · 𝐸) < (𝐸 · Σ𝑖 ∈ (0...(𝐿 − 2))((𝑋𝑖)‘𝑆)) ∧ (𝐸 · Σ𝑖 ∈ (0...(𝐿 − 2))((𝑋𝑖)‘𝑆)) ≤ Σ𝑖 ∈ (0...𝑁)(𝐸 · ((𝑋𝑖)‘𝑆))) → ((𝐿 − (4 / 3)) · 𝐸) < Σ𝑖 ∈ (0...𝑁)(𝐸 · ((𝑋𝑖)‘𝑆))))
566564, 565syl 17 . . . 4 ((𝜑 ∧ ¬ 𝐿 = 1) → ((((𝐿 − (4 / 3)) · 𝐸) < (𝐸 · Σ𝑖 ∈ (0...(𝐿 − 2))((𝑋𝑖)‘𝑆)) ∧ (𝐸 · Σ𝑖 ∈ (0...(𝐿 − 2))((𝑋𝑖)‘𝑆)) ≤ Σ𝑖 ∈ (0...𝑁)(𝐸 · ((𝑋𝑖)‘𝑆))) → ((𝐿 − (4 / 3)) · 𝐸) < Σ𝑖 ∈ (0...𝑁)(𝐸 · ((𝑋𝑖)‘𝑆))))
567459, 562, 566mp2and 715 . . 3 ((𝜑 ∧ ¬ 𝐿 = 1) → ((𝐿 − (4 / 3)) · 𝐸) < Σ𝑖 ∈ (0...𝑁)(𝐸 · ((𝑋𝑖)‘𝑆)))
568106, 567pm2.61dan 849 . 2 (𝜑 → ((𝐿 − (4 / 3)) · 𝐸) < Σ𝑖 ∈ (0...𝑁)(𝐸 · ((𝑋𝑖)‘𝑆)))
569 sumex 14462 . . 3 Σ𝑖 ∈ (0...𝑁)(𝐸 · ((𝑋𝑖)‘𝑆)) ∈ V
57094oveq2d 6706 . . . . 5 (𝑡 = 𝑆 → (𝐸 · ((𝑋𝑖)‘𝑡)) = (𝐸 · ((𝑋𝑖)‘𝑆)))
571570sumeq2sdv 14479 . . . 4 (𝑡 = 𝑆 → Σ𝑖 ∈ (0...𝑁)(𝐸 · ((𝑋𝑖)‘𝑡)) = Σ𝑖 ∈ (0...𝑁)(𝐸 · ((𝑋𝑖)‘𝑆)))
572 eqid 2651 . . . 4 (𝑡𝑇 ↦ Σ𝑖 ∈ (0...𝑁)(𝐸 · ((𝑋𝑖)‘𝑡))) = (𝑡𝑇 ↦ Σ𝑖 ∈ (0...𝑁)(𝐸 · ((𝑋𝑖)‘𝑡)))
573571, 572fvmptg 6319 . . 3 ((𝑆𝑇 ∧ Σ𝑖 ∈ (0...𝑁)(𝐸 · ((𝑋𝑖)‘𝑆)) ∈ V) → ((𝑡𝑇 ↦ Σ𝑖 ∈ (0...𝑁)(𝐸 · ((𝑋𝑖)‘𝑡)))‘𝑆) = Σ𝑖 ∈ (0...𝑁)(𝐸 · ((𝑋𝑖)‘𝑆)))
57450, 569, 573sylancl 695 . 2 (𝜑 → ((𝑡𝑇 ↦ Σ𝑖 ∈ (0...𝑁)(𝐸 · ((𝑋𝑖)‘𝑡)))‘𝑆) = Σ𝑖 ∈ (0...𝑁)(𝐸 · ((𝑋𝑖)‘𝑆)))
575568, 574breqtrrd 4713 1 (𝜑 → ((𝐿 − (4 / 3)) · 𝐸) < ((𝑡𝑇 ↦ Σ𝑖 ∈ (0...𝑁)(𝐸 · ((𝑋𝑖)‘𝑡)))‘𝑆))
 Colors of variables: wff setvar class Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 196   ∨ wo 382   ∧ wa 383   ∧ w3a 1054   = wceq 1523  Ⅎwnf 1748   ∈ wcel 2030  Ⅎwnfc 2780   ≠ wne 2823  ∀wral 2941  {crab 2945  Vcvv 3231   ∖ cdif 3604   ∪ cun 3605   ∩ cin 3606   ⊆ wss 3607  ∅c0 3948   class class class wbr 4685   ↦ cmpt 4762  ⟶wf 5922  ‘cfv 5926  (class class class)co 6690  Fincfn 7997  ℂcc 9972  ℝcr 9973  0cc0 9974  1c1 9975   + caddc 9977   · cmul 9979   < clt 10112   ≤ cle 10113   − cmin 10304  -cneg 10305   / cdiv 10722  ℕcn 11058  2c2 11108  3c3 11109  4c4 11110  ℕ0cn0 11330  ℤcz 11415  ℤ≥cuz 11725  ℝ+crp 11870  ...cfz 12364  #chash 13157  Σcsu 14460 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-8 2032  ax-9 2039  ax-10 2059  ax-11 2074  ax-12 2087  ax-13 2282  ax-ext 2631  ax-rep 4804  ax-sep 4814  ax-nul 4822  ax-pow 4873  ax-pr 4936  ax-un 6991  ax-inf2 8576  ax-cnex 10030  ax-resscn 10031  ax-1cn 10032  ax-icn 10033  ax-addcl 10034  ax-addrcl 10035  ax-mulcl 10036  ax-mulrcl 10037  ax-mulcom 10038  ax-addass 10039  ax-mulass 10040  ax-distr 10041  ax-i2m1 10042  ax-1ne0 10043  ax-1rid 10044  ax-rnegex 10045  ax-rrecex 10046  ax-cnre 10047  ax-pre-lttri 10048  ax-pre-lttrn 10049  ax-pre-ltadd 10050  ax-pre-mulgt0 10051  ax-pre-sup 10052 This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3or 1055  df-3an 1056  df-tru 1526  df-fal 1529  df-ex 1745  df-nf 1750  df-sb 1938  df-eu 2502  df-mo 2503  df-clab 2638  df-cleq 2644  df-clel 2647  df-nfc 2782  df-ne 2824  df-nel 2927  df-ral 2946  df-rex 2947  df-reu 2948  df-rmo 2949  df-rab 2950  df-v 3233  df-sbc 3469  df-csb 3567  df-dif 3610  df-un 3612  df-in 3614  df-ss 3621  df-pss 3623  df-nul 3949  df-if 4120  df-pw 4193  df-sn 4211  df-pr 4213  df-tp 4215  df-op 4217  df-uni 4469  df-int 4508  df-iun 4554  df-br 4686  df-opab 4746  df-mpt 4763  df-tr 4786  df-id 5053  df-eprel 5058  df-po 5064  df-so 5065  df-fr 5102  df-se 5103  df-we 5104  df-xp 5149  df-rel 5150  df-cnv 5151  df-co 5152  df-dm 5153  df-rn 5154  df-res 5155  df-ima 5156  df-pred 5718  df-ord 5764  df-on 5765  df-lim 5766  df-suc 5767  df-iota 5889  df-fun 5928  df-fn 5929  df-f 5930  df-f1 5931  df-fo 5932  df-f1o 5933  df-fv 5934  df-isom 5935  df-riota 6651  df-ov 6693  df-oprab 6694  df-mpt2 6695  df-om 7108  df-1st 7210  df-2nd 7211  df-wrecs 7452  df-recs 7513  df-rdg 7551  df-1o 7605  df-oadd 7609  df-er 7787  df-en 7998  df-dom 7999  df-sdom 8000  df-fin 8001  df-sup 8389  df-oi 8456  df-card 8803  df-pnf 10114  df-mnf 10115  df-xr 10116  df-ltxr 10117  df-le 10118  df-sub 10306  df-neg 10307  df-div 10723  df-nn 11059  df-2 11117  df-3 11118  df-4 11119  df-n0 11331  df-z 11416  df-uz 11726  df-rp 11871  df-ico 12219  df-fz 12365  df-fzo 12505  df-seq 12842  df-exp 12901  df-hash 13158  df-cj 13883  df-re 13884  df-im 13885  df-sqrt 14019  df-abs 14020  df-clim 14263  df-sum 14461 This theorem is referenced by:  stoweidlem34  40569
 Copyright terms: Public domain W3C validator