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

Theorem stoweidlem26 46041
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 represent 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 11261 . . . . . . . 8 1 ∈ ℝ
2 eleq1 2829 . . . . . . . 8 (𝐿 = 1 → (𝐿 ∈ ℝ ↔ 1 ∈ ℝ))
31, 2mpbiri 258 . . . . . . 7 (𝐿 = 1 → 𝐿 ∈ ℝ)
43adantl 481 . . . . . 6 ((𝜑𝐿 = 1) → 𝐿 ∈ ℝ)
5 4re 12350 . . . . . . . 8 4 ∈ ℝ
65a1i 11 . . . . . . 7 ((𝜑𝐿 = 1) → 4 ∈ ℝ)
7 3re 12346 . . . . . . . 8 3 ∈ ℝ
87a1i 11 . . . . . . 7 ((𝜑𝐿 = 1) → 3 ∈ ℝ)
9 3ne0 12372 . . . . . . . 8 3 ≠ 0
109a1i 11 . . . . . . 7 ((𝜑𝐿 = 1) → 3 ≠ 0)
116, 8, 10redivcld 12095 . . . . . 6 ((𝜑𝐿 = 1) → (4 / 3) ∈ ℝ)
124, 11resubcld 11691 . . . . 5 ((𝜑𝐿 = 1) → (𝐿 − (4 / 3)) ∈ ℝ)
13 stoweidlem26.11 . . . . . . 7 (𝜑𝐸 ∈ ℝ+)
1413rpred 13077 . . . . . 6 (𝜑𝐸 ∈ ℝ)
1514adantr 480 . . . . 5 ((𝜑𝐿 = 1) → 𝐸 ∈ ℝ)
1612, 15remulcld 11291 . . . 4 ((𝜑𝐿 = 1) → ((𝐿 − (4 / 3)) · 𝐸) ∈ ℝ)
17 0red 11264 . . . 4 ((𝜑𝐿 = 1) → 0 ∈ ℝ)
18 fzfid 14014 . . . . . 6 (𝜑 → (0...𝑁) ∈ Fin)
1914adantr 480 . . . . . . 7 ((𝜑𝑖 ∈ (0...𝑁)) → 𝐸 ∈ ℝ)
20 stoweidlem26.13 . . . . . . . 8 ((𝜑𝑖 ∈ (0...𝑁)) → (𝑋𝑖):𝑇⟶ℝ)
21 stoweidlem26.9 . . . . . . . . . . . . . 14 (𝜑𝑆 ∈ ((𝐷𝐿) ∖ (𝐷‘(𝐿 − 1))))
22 eldif 3961 . . . . . . . . . . . . . 14 (𝑆 ∈ ((𝐷𝐿) ∖ (𝐷‘(𝐿 − 1))) ↔ (𝑆 ∈ (𝐷𝐿) ∧ ¬ 𝑆 ∈ (𝐷‘(𝐿 − 1))))
2321, 22sylib 218 . . . . . . . . . . . . 13 (𝜑 → (𝑆 ∈ (𝐷𝐿) ∧ ¬ 𝑆 ∈ (𝐷‘(𝐿 − 1))))
2423simpld 494 . . . . . . . . . . . 12 (𝜑𝑆 ∈ (𝐷𝐿))
25 stoweidlem26.4 . . . . . . . . . . . . 13 𝐷 = (𝑗 ∈ (0...𝑁) ↦ {𝑡𝑇 ∣ (𝐹𝑡) ≤ ((𝑗 − (1 / 3)) · 𝐸)})
26 oveq1 7438 . . . . . . . . . . . . . . . 16 (𝑗 = 𝐿 → (𝑗 − (1 / 3)) = (𝐿 − (1 / 3)))
2726oveq1d 7446 . . . . . . . . . . . . . . 15 (𝑗 = 𝐿 → ((𝑗 − (1 / 3)) · 𝐸) = ((𝐿 − (1 / 3)) · 𝐸))
2827breq2d 5155 . . . . . . . . . . . . . 14 (𝑗 = 𝐿 → ((𝐹𝑡) ≤ ((𝑗 − (1 / 3)) · 𝐸) ↔ (𝐹𝑡) ≤ ((𝐿 − (1 / 3)) · 𝐸)))
2928rabbidv 3444 . . . . . . . . . . . . 13 (𝑗 = 𝐿 → {𝑡𝑇 ∣ (𝐹𝑡) ≤ ((𝑗 − (1 / 3)) · 𝐸)} = {𝑡𝑇 ∣ (𝐹𝑡) ≤ ((𝐿 − (1 / 3)) · 𝐸)})
30 fz1ssfz0 13663 . . . . . . . . . . . . . 14 (1...𝑁) ⊆ (0...𝑁)
31 stoweidlem26.8 . . . . . . . . . . . . . 14 (𝜑𝐿 ∈ (1...𝑁))
3230, 31sselid 3981 . . . . . . . . . . . . 13 (𝜑𝐿 ∈ (0...𝑁))
33 stoweidlem26.7 . . . . . . . . . . . . . 14 (𝜑𝑇 ∈ V)
34 rabexg 5337 . . . . . . . . . . . . . 14 (𝑇 ∈ V → {𝑡𝑇 ∣ (𝐹𝑡) ≤ ((𝐿 − (1 / 3)) · 𝐸)} ∈ V)
3533, 34syl 17 . . . . . . . . . . . . 13 (𝜑 → {𝑡𝑇 ∣ (𝐹𝑡) ≤ ((𝐿 − (1 / 3)) · 𝐸)} ∈ V)
3625, 29, 32, 35fvmptd3 7039 . . . . . . . . . . . 12 (𝜑 → (𝐷𝐿) = {𝑡𝑇 ∣ (𝐹𝑡) ≤ ((𝐿 − (1 / 3)) · 𝐸)})
3724, 36eleqtrd 2843 . . . . . . . . . . 11 (𝜑𝑆 ∈ {𝑡𝑇 ∣ (𝐹𝑡) ≤ ((𝐿 − (1 / 3)) · 𝐸)})
38 nfcv 2905 . . . . . . . . . . . 12 𝑡𝑆
39 nfcv 2905 . . . . . . . . . . . 12 𝑡𝑇
40 stoweidlem26.1 . . . . . . . . . . . . . 14 𝑡𝐹
4140, 38nffv 6916 . . . . . . . . . . . . 13 𝑡(𝐹𝑆)
42 nfcv 2905 . . . . . . . . . . . . 13 𝑡
43 nfcv 2905 . . . . . . . . . . . . 13 𝑡((𝐿 − (1 / 3)) · 𝐸)
4441, 42, 43nfbr 5190 . . . . . . . . . . . 12 𝑡(𝐹𝑆) ≤ ((𝐿 − (1 / 3)) · 𝐸)
45 fveq2 6906 . . . . . . . . . . . . 13 (𝑡 = 𝑆 → (𝐹𝑡) = (𝐹𝑆))
4645breq1d 5153 . . . . . . . . . . . 12 (𝑡 = 𝑆 → ((𝐹𝑡) ≤ ((𝐿 − (1 / 3)) · 𝐸) ↔ (𝐹𝑆) ≤ ((𝐿 − (1 / 3)) · 𝐸)))
4738, 39, 44, 46elrabf 3688 . . . . . . . . . . 11 (𝑆 ∈ {𝑡𝑇 ∣ (𝐹𝑡) ≤ ((𝐿 − (1 / 3)) · 𝐸)} ↔ (𝑆𝑇 ∧ (𝐹𝑆) ≤ ((𝐿 − (1 / 3)) · 𝐸)))
4837, 47sylib 218 . . . . . . . . . 10 (𝜑 → (𝑆𝑇 ∧ (𝐹𝑆) ≤ ((𝐿 − (1 / 3)) · 𝐸)))
4948simpld 494 . . . . . . . . 9 (𝜑𝑆𝑇)
5049adantr 480 . . . . . . . 8 ((𝜑𝑖 ∈ (0...𝑁)) → 𝑆𝑇)
5120, 50ffvelcdmd 7105 . . . . . . 7 ((𝜑𝑖 ∈ (0...𝑁)) → ((𝑋𝑖)‘𝑆) ∈ ℝ)
5219, 51remulcld 11291 . . . . . 6 ((𝜑𝑖 ∈ (0...𝑁)) → (𝐸 · ((𝑋𝑖)‘𝑆)) ∈ ℝ)
5318, 52fsumrecl 15770 . . . . 5 (𝜑 → Σ𝑖 ∈ (0...𝑁)(𝐸 · ((𝑋𝑖)‘𝑆)) ∈ ℝ)
5453adantr 480 . . . 4 ((𝜑𝐿 = 1) → Σ𝑖 ∈ (0...𝑁)(𝐸 · ((𝑋𝑖)‘𝑆)) ∈ ℝ)
555, 7, 9redivcli 12034 . . . . . . 7 (4 / 3) ∈ ℝ
5655a1i 11 . . . . . 6 ((𝜑𝐿 = 1) → (4 / 3) ∈ ℝ)
574, 56resubcld 11691 . . . . 5 ((𝜑𝐿 = 1) → (𝐿 − (4 / 3)) ∈ ℝ)
584recnd 11289 . . . . . . . 8 ((𝜑𝐿 = 1) → 𝐿 ∈ ℂ)
5958subid1d 11609 . . . . . . 7 ((𝜑𝐿 = 1) → (𝐿 − 0) = 𝐿)
60 3cn 12347 . . . . . . . . . 10 3 ∈ ℂ
6160, 9dividi 12000 . . . . . . . . 9 (3 / 3) = 1
62 3lt4 12440 . . . . . . . . . 10 3 < 4
63 3pos 12371 . . . . . . . . . . 11 0 < 3
647, 5, 7, 63ltdiv1ii 12197 . . . . . . . . . 10 (3 < 4 ↔ (3 / 3) < (4 / 3))
6562, 64mpbi 230 . . . . . . . . 9 (3 / 3) < (4 / 3)
6661, 65eqbrtrri 5166 . . . . . . . 8 1 < (4 / 3)
67 breq1 5146 . . . . . . . . 9 (𝐿 = 1 → (𝐿 < (4 / 3) ↔ 1 < (4 / 3)))
6867adantl 481 . . . . . . . 8 ((𝜑𝐿 = 1) → (𝐿 < (4 / 3) ↔ 1 < (4 / 3)))
6966, 68mpbiri 258 . . . . . . 7 ((𝜑𝐿 = 1) → 𝐿 < (4 / 3))
7059, 69eqbrtrd 5165 . . . . . 6 ((𝜑𝐿 = 1) → (𝐿 − 0) < (4 / 3))
714, 17, 56, 70ltsub23d 11868 . . . . 5 ((𝜑𝐿 = 1) → (𝐿 − (4 / 3)) < 0)
7213rpgt0d 13080 . . . . . 6 (𝜑 → 0 < 𝐸)
7372adantr 480 . . . . 5 ((𝜑𝐿 = 1) → 0 < 𝐸)
74 mulltgt0 45027 . . . . 5 ((((𝐿 − (4 / 3)) ∈ ℝ ∧ (𝐿 − (4 / 3)) < 0) ∧ (𝐸 ∈ ℝ ∧ 0 < 𝐸)) → ((𝐿 − (4 / 3)) · 𝐸) < 0)
7557, 71, 15, 73, 74syl22anc 839 . . . 4 ((𝜑𝐿 = 1) → ((𝐿 − (4 / 3)) · 𝐸) < 0)
76 0cn 11253 . . . . . . . 8 0 ∈ ℂ
77 fsumconst 15826 . . . . . . . 8 (((0...𝑁) ∈ Fin ∧ 0 ∈ ℂ) → Σ𝑖 ∈ (0...𝑁)0 = ((♯‘(0...𝑁)) · 0))
7818, 76, 77sylancl 586 . . . . . . 7 (𝜑 → Σ𝑖 ∈ (0...𝑁)0 = ((♯‘(0...𝑁)) · 0))
79 hashcl 14395 . . . . . . . . 9 ((0...𝑁) ∈ Fin → (♯‘(0...𝑁)) ∈ ℕ0)
80 nn0cn 12536 . . . . . . . . 9 ((♯‘(0...𝑁)) ∈ ℕ0 → (♯‘(0...𝑁)) ∈ ℂ)
8118, 79, 803syl 18 . . . . . . . 8 (𝜑 → (♯‘(0...𝑁)) ∈ ℂ)
8281mul01d 11460 . . . . . . 7 (𝜑 → ((♯‘(0...𝑁)) · 0) = 0)
8378, 82eqtrd 2777 . . . . . 6 (𝜑 → Σ𝑖 ∈ (0...𝑁)0 = 0)
8483adantr 480 . . . . 5 ((𝜑𝐿 = 1) → Σ𝑖 ∈ (0...𝑁)0 = 0)
85 0red 11264 . . . . . . 7 ((𝜑𝑖 ∈ (0...𝑁)) → 0 ∈ ℝ)
8613rpge0d 13081 . . . . . . . . 9 (𝜑 → 0 ≤ 𝐸)
8786adantr 480 . . . . . . . 8 ((𝜑𝑖 ∈ (0...𝑁)) → 0 ≤ 𝐸)
88 stoweidlem26.3 . . . . . . . . . . . 12 𝑡𝜑
89 nfv 1914 . . . . . . . . . . . 12 𝑡 𝑖 ∈ (0...𝑁)
9088, 89nfan 1899 . . . . . . . . . . 11 𝑡(𝜑𝑖 ∈ (0...𝑁))
91 nfv 1914 . . . . . . . . . . 11 𝑡0 ≤ ((𝑋𝑖)‘𝑆)
9290, 91nfim 1896 . . . . . . . . . 10 𝑡((𝜑𝑖 ∈ (0...𝑁)) → 0 ≤ ((𝑋𝑖)‘𝑆))
93 fveq2 6906 . . . . . . . . . . . 12 (𝑡 = 𝑆 → ((𝑋𝑖)‘𝑡) = ((𝑋𝑖)‘𝑆))
9493breq2d 5155 . . . . . . . . . . 11 (𝑡 = 𝑆 → (0 ≤ ((𝑋𝑖)‘𝑡) ↔ 0 ≤ ((𝑋𝑖)‘𝑆)))
9594imbi2d 340 . . . . . . . . . 10 (𝑡 = 𝑆 → (((𝜑𝑖 ∈ (0...𝑁)) → 0 ≤ ((𝑋𝑖)‘𝑡)) ↔ ((𝜑𝑖 ∈ (0...𝑁)) → 0 ≤ ((𝑋𝑖)‘𝑆))))
96 stoweidlem26.14 . . . . . . . . . . . 12 ((𝜑𝑖 ∈ (0...𝑁) ∧ 𝑡𝑇) → 0 ≤ ((𝑋𝑖)‘𝑡))
97963expia 1122 . . . . . . . . . . 11 ((𝜑𝑖 ∈ (0...𝑁)) → (𝑡𝑇 → 0 ≤ ((𝑋𝑖)‘𝑡)))
9897com12 32 . . . . . . . . . 10 (𝑡𝑇 → ((𝜑𝑖 ∈ (0...𝑁)) → 0 ≤ ((𝑋𝑖)‘𝑡)))
9938, 92, 95, 98vtoclgaf 3576 . . . . . . . . 9 (𝑆𝑇 → ((𝜑𝑖 ∈ (0...𝑁)) → 0 ≤ ((𝑋𝑖)‘𝑆)))
10050, 99mpcom 38 . . . . . . . 8 ((𝜑𝑖 ∈ (0...𝑁)) → 0 ≤ ((𝑋𝑖)‘𝑆))
10119, 51, 87, 100mulge0d 11840 . . . . . . 7 ((𝜑𝑖 ∈ (0...𝑁)) → 0 ≤ (𝐸 · ((𝑋𝑖)‘𝑆)))
10218, 85, 52, 101fsumle 15835 . . . . . 6 (𝜑 → Σ𝑖 ∈ (0...𝑁)0 ≤ Σ𝑖 ∈ (0...𝑁)(𝐸 · ((𝑋𝑖)‘𝑆)))
103102adantr 480 . . . . 5 ((𝜑𝐿 = 1) → Σ𝑖 ∈ (0...𝑁)0 ≤ Σ𝑖 ∈ (0...𝑁)(𝐸 · ((𝑋𝑖)‘𝑆)))
10484, 103eqbrtrrd 5167 . . . 4 ((𝜑𝐿 = 1) → 0 ≤ Σ𝑖 ∈ (0...𝑁)(𝐸 · ((𝑋𝑖)‘𝑆)))
10516, 17, 54, 75, 104ltletrd 11421 . . 3 ((𝜑𝐿 = 1) → ((𝐿 − (4 / 3)) · 𝐸) < Σ𝑖 ∈ (0...𝑁)(𝐸 · ((𝑋𝑖)‘𝑆)))
106 elfzelz 13564 . . . . . . . . 9 (𝐿 ∈ (1...𝑁) → 𝐿 ∈ ℤ)
107 zre 12617 . . . . . . . . 9 (𝐿 ∈ ℤ → 𝐿 ∈ ℝ)
10831, 106, 1073syl 18 . . . . . . . 8 (𝜑𝐿 ∈ ℝ)
1095a1i 11 . . . . . . . . 9 (𝜑 → 4 ∈ ℝ)
1107a1i 11 . . . . . . . . 9 (𝜑 → 3 ∈ ℝ)
1119a1i 11 . . . . . . . . 9 (𝜑 → 3 ≠ 0)
112109, 110, 111redivcld 12095 . . . . . . . 8 (𝜑 → (4 / 3) ∈ ℝ)
113108, 112resubcld 11691 . . . . . . 7 (𝜑 → (𝐿 − (4 / 3)) ∈ ℝ)
114113, 14remulcld 11291 . . . . . 6 (𝜑 → ((𝐿 − (4 / 3)) · 𝐸) ∈ ℝ)
115114adantr 480 . . . . 5 ((𝜑 ∧ ¬ 𝐿 = 1) → ((𝐿 − (4 / 3)) · 𝐸) ∈ ℝ)
1161a1i 11 . . . . . . . . 9 (𝜑 → 1 ∈ ℝ)
117 stoweidlem26.6 . . . . . . . . . 10 (𝜑𝑁 ∈ ℕ)
11814, 117nndivred 12320 . . . . . . . . 9 (𝜑 → (𝐸 / 𝑁) ∈ ℝ)
119116, 118resubcld 11691 . . . . . . . 8 (𝜑 → (1 − (𝐸 / 𝑁)) ∈ ℝ)
120108, 116resubcld 11691 . . . . . . . 8 (𝜑 → (𝐿 − 1) ∈ ℝ)
121119, 120remulcld 11291 . . . . . . 7 (𝜑 → ((1 − (𝐸 / 𝑁)) · (𝐿 − 1)) ∈ ℝ)
12214, 121remulcld 11291 . . . . . 6 (𝜑 → (𝐸 · ((1 − (𝐸 / 𝑁)) · (𝐿 − 1))) ∈ ℝ)
123122adantr 480 . . . . 5 ((𝜑 ∧ ¬ 𝐿 = 1) → (𝐸 · ((1 − (𝐸 / 𝑁)) · (𝐿 − 1))) ∈ ℝ)
124 fzfid 14014 . . . . . . . 8 (𝜑 → (0...(𝐿 − 2)) ∈ Fin)
12531elfzelzd 13565 . . . . . . . . . . . . . 14 (𝜑𝐿 ∈ ℤ)
126 2z 12649 . . . . . . . . . . . . . . 15 2 ∈ ℤ
127126a1i 11 . . . . . . . . . . . . . 14 (𝜑 → 2 ∈ ℤ)
128125, 127zsubcld 12727 . . . . . . . . . . . . 13 (𝜑 → (𝐿 − 2) ∈ ℤ)
129117nnzd 12640 . . . . . . . . . . . . 13 (𝜑𝑁 ∈ ℤ)
130125zred 12722 . . . . . . . . . . . . . . 15 (𝜑𝐿 ∈ ℝ)
131 2re 12340 . . . . . . . . . . . . . . . 16 2 ∈ ℝ
132131a1i 11 . . . . . . . . . . . . . . 15 (𝜑 → 2 ∈ ℝ)
133130, 132resubcld 11691 . . . . . . . . . . . . . 14 (𝜑 → (𝐿 − 2) ∈ ℝ)
134117nnred 12281 . . . . . . . . . . . . . 14 (𝜑𝑁 ∈ ℝ)
135 0le2 12368 . . . . . . . . . . . . . . . 16 0 ≤ 2
136 0red 11264 . . . . . . . . . . . . . . . . 17 (𝜑 → 0 ∈ ℝ)
137136, 132, 130lesub2d 11871 . . . . . . . . . . . . . . . 16 (𝜑 → (0 ≤ 2 ↔ (𝐿 − 2) ≤ (𝐿 − 0)))
138135, 137mpbii 233 . . . . . . . . . . . . . . 15 (𝜑 → (𝐿 − 2) ≤ (𝐿 − 0))
139125zcnd 12723 . . . . . . . . . . . . . . . 16 (𝜑𝐿 ∈ ℂ)
140139subid1d 11609 . . . . . . . . . . . . . . 15 (𝜑 → (𝐿 − 0) = 𝐿)
141138, 140breqtrd 5169 . . . . . . . . . . . . . 14 (𝜑 → (𝐿 − 2) ≤ 𝐿)
142 elfzle2 13568 . . . . . . . . . . . . . . 15 (𝐿 ∈ (1...𝑁) → 𝐿𝑁)
14331, 142syl 17 . . . . . . . . . . . . . 14 (𝜑𝐿𝑁)
144133, 130, 134, 141, 143letrd 11418 . . . . . . . . . . . . 13 (𝜑 → (𝐿 − 2) ≤ 𝑁)
145128, 129, 1443jca 1129 . . . . . . . . . . . 12 (𝜑 → ((𝐿 − 2) ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ (𝐿 − 2) ≤ 𝑁))
146 eluz2 12884 . . . . . . . . . . . 12 (𝑁 ∈ (ℤ‘(𝐿 − 2)) ↔ ((𝐿 − 2) ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ (𝐿 − 2) ≤ 𝑁))
147145, 146sylibr 234 . . . . . . . . . . 11 (𝜑𝑁 ∈ (ℤ‘(𝐿 − 2)))
148 fzss2 13604 . . . . . . . . . . 11 (𝑁 ∈ (ℤ‘(𝐿 − 2)) → (0...(𝐿 − 2)) ⊆ (0...𝑁))
149147, 148syl 17 . . . . . . . . . 10 (𝜑 → (0...(𝐿 − 2)) ⊆ (0...𝑁))
150149sselda 3983 . . . . . . . . 9 ((𝜑𝑖 ∈ (0...(𝐿 − 2))) → 𝑖 ∈ (0...𝑁))
151150, 51syldan 591 . . . . . . . 8 ((𝜑𝑖 ∈ (0...(𝐿 − 2))) → ((𝑋𝑖)‘𝑆) ∈ ℝ)
152124, 151fsumrecl 15770 . . . . . . 7 (𝜑 → Σ𝑖 ∈ (0...(𝐿 − 2))((𝑋𝑖)‘𝑆) ∈ ℝ)
15314, 152remulcld 11291 . . . . . 6 (𝜑 → (𝐸 · Σ𝑖 ∈ (0...(𝐿 − 2))((𝑋𝑖)‘𝑆)) ∈ ℝ)
154153adantr 480 . . . . 5 ((𝜑 ∧ ¬ 𝐿 = 1) → (𝐸 · Σ𝑖 ∈ (0...(𝐿 − 2))((𝑋𝑖)‘𝑆)) ∈ ℝ)
15514, 120remulcld 11291 . . . . . . . . 9 (𝜑 → (𝐸 · (𝐿 − 1)) ∈ ℝ)
15614, 14remulcld 11291 . . . . . . . . 9 (𝜑 → (𝐸 · 𝐸) ∈ ℝ)
157155, 156resubcld 11691 . . . . . . . 8 (𝜑 → ((𝐸 · (𝐿 − 1)) − (𝐸 · 𝐸)) ∈ ℝ)
158120, 117nndivred 12320 . . . . . . . . . 10 (𝜑 → ((𝐿 − 1) / 𝑁) ∈ ℝ)
159156, 158remulcld 11291 . . . . . . . . 9 (𝜑 → ((𝐸 · 𝐸) · ((𝐿 − 1) / 𝑁)) ∈ ℝ)
160155, 159resubcld 11691 . . . . . . . 8 (𝜑 → ((𝐸 · (𝐿 − 1)) − ((𝐸 · 𝐸) · ((𝐿 − 1) / 𝑁))) ∈ ℝ)
161120, 14resubcld 11691 . . . . . . . . . 10 (𝜑 → ((𝐿 − 1) − 𝐸) ∈ ℝ)
162116, 14readdcld 11290 . . . . . . . . . . . 12 (𝜑 → (1 + 𝐸) ∈ ℝ)
1631, 7, 9redivcli 12034 . . . . . . . . . . . . . . 15 (1 / 3) ∈ ℝ
164163a1i 11 . . . . . . . . . . . . . 14 (𝜑 → (1 / 3) ∈ ℝ)
165 stoweidlem26.12 . . . . . . . . . . . . . 14 (𝜑𝐸 < (1 / 3))
16614, 164, 116, 165ltadd2dd 11420 . . . . . . . . . . . . 13 (𝜑 → (1 + 𝐸) < (1 + (1 / 3)))
167 ax-1cn 11213 . . . . . . . . . . . . . . 15 1 ∈ ℂ
16860, 167, 60, 9divdiri 12024 . . . . . . . . . . . . . 14 ((3 + 1) / 3) = ((3 / 3) + (1 / 3))
169 3p1e4 12411 . . . . . . . . . . . . . . 15 (3 + 1) = 4
170169oveq1i 7441 . . . . . . . . . . . . . 14 ((3 + 1) / 3) = (4 / 3)
17161oveq1i 7441 . . . . . . . . . . . . . 14 ((3 / 3) + (1 / 3)) = (1 + (1 / 3))
172168, 170, 1713eqtr3ri 2774 . . . . . . . . . . . . 13 (1 + (1 / 3)) = (4 / 3)
173166, 172breqtrdi 5184 . . . . . . . . . . . 12 (𝜑 → (1 + 𝐸) < (4 / 3))
174162, 112, 108, 173ltsub2dd 11876 . . . . . . . . . . 11 (𝜑 → (𝐿 − (4 / 3)) < (𝐿 − (1 + 𝐸)))
175167a1i 11 . . . . . . . . . . . 12 (𝜑 → 1 ∈ ℂ)
17613rpcnd 13079 . . . . . . . . . . . 12 (𝜑𝐸 ∈ ℂ)
177139, 175, 176subsub4d 11651 . . . . . . . . . . 11 (𝜑 → ((𝐿 − 1) − 𝐸) = (𝐿 − (1 + 𝐸)))
178174, 177breqtrrd 5171 . . . . . . . . . 10 (𝜑 → (𝐿 − (4 / 3)) < ((𝐿 − 1) − 𝐸))
179113, 161, 13, 178ltmul1dd 13132 . . . . . . . . 9 (𝜑 → ((𝐿 − (4 / 3)) · 𝐸) < (((𝐿 − 1) − 𝐸) · 𝐸))
180139, 175subcld 11620 . . . . . . . . . . . 12 (𝜑 → (𝐿 − 1) ∈ ℂ)
181180, 176subcld 11620 . . . . . . . . . . 11 (𝜑 → ((𝐿 − 1) − 𝐸) ∈ ℂ)
182176, 181mulcomd 11282 . . . . . . . . . 10 (𝜑 → (𝐸 · ((𝐿 − 1) − 𝐸)) = (((𝐿 − 1) − 𝐸) · 𝐸))
183176, 180, 176subdid 11719 . . . . . . . . . 10 (𝜑 → (𝐸 · ((𝐿 − 1) − 𝐸)) = ((𝐸 · (𝐿 − 1)) − (𝐸 · 𝐸)))
184182, 183eqtr3d 2779 . . . . . . . . 9 (𝜑 → (((𝐿 − 1) − 𝐸) · 𝐸) = ((𝐸 · (𝐿 − 1)) − (𝐸 · 𝐸)))
185179, 184breqtrd 5169 . . . . . . . 8 (𝜑 → ((𝐿 − (4 / 3)) · 𝐸) < ((𝐸 · (𝐿 − 1)) − (𝐸 · 𝐸)))
186 1zzd 12648 . . . . . . . . . . . . . . . . 17 (𝜑 → 1 ∈ ℤ)
187 elfz 13553 . . . . . . . . . . . . . . . . 17 ((𝐿 ∈ ℤ ∧ 1 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝐿 ∈ (1...𝑁) ↔ (1 ≤ 𝐿𝐿𝑁)))
188125, 186, 129, 187syl3anc 1373 . . . . . . . . . . . . . . . 16 (𝜑 → (𝐿 ∈ (1...𝑁) ↔ (1 ≤ 𝐿𝐿𝑁)))
18931, 188mpbid 232 . . . . . . . . . . . . . . 15 (𝜑 → (1 ≤ 𝐿𝐿𝑁))
190189simprd 495 . . . . . . . . . . . . . 14 (𝜑𝐿𝑁)
191 zlem1lt 12669 . . . . . . . . . . . . . . 15 ((𝐿 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝐿𝑁 ↔ (𝐿 − 1) < 𝑁))
192125, 129, 191syl2anc 584 . . . . . . . . . . . . . 14 (𝜑 → (𝐿𝑁 ↔ (𝐿 − 1) < 𝑁))
193190, 192mpbid 232 . . . . . . . . . . . . 13 (𝜑 → (𝐿 − 1) < 𝑁)
194117nngt0d 12315 . . . . . . . . . . . . . 14 (𝜑 → 0 < 𝑁)
195 ltdiv1 12132 . . . . . . . . . . . . . 14 (((𝐿 − 1) ∈ ℝ ∧ 𝑁 ∈ ℝ ∧ (𝑁 ∈ ℝ ∧ 0 < 𝑁)) → ((𝐿 − 1) < 𝑁 ↔ ((𝐿 − 1) / 𝑁) < (𝑁 / 𝑁)))
196120, 134, 134, 194, 195syl112anc 1376 . . . . . . . . . . . . 13 (𝜑 → ((𝐿 − 1) < 𝑁 ↔ ((𝐿 − 1) / 𝑁) < (𝑁 / 𝑁)))
197193, 196mpbid 232 . . . . . . . . . . . 12 (𝜑 → ((𝐿 − 1) / 𝑁) < (𝑁 / 𝑁))
198117nncnd 12282 . . . . . . . . . . . . 13 (𝜑𝑁 ∈ ℂ)
199117nnne0d 12316 . . . . . . . . . . . . 13 (𝜑𝑁 ≠ 0)
200198, 199dividd 12041 . . . . . . . . . . . 12 (𝜑 → (𝑁 / 𝑁) = 1)
201197, 200breqtrd 5169 . . . . . . . . . . 11 (𝜑 → ((𝐿 − 1) / 𝑁) < 1)
20214, 14, 72, 72mulgt0d 11416 . . . . . . . . . . . 12 (𝜑 → 0 < (𝐸 · 𝐸))
203 ltmul2 12118 . . . . . . . . . . . 12 ((((𝐿 − 1) / 𝑁) ∈ ℝ ∧ 1 ∈ ℝ ∧ ((𝐸 · 𝐸) ∈ ℝ ∧ 0 < (𝐸 · 𝐸))) → (((𝐿 − 1) / 𝑁) < 1 ↔ ((𝐸 · 𝐸) · ((𝐿 − 1) / 𝑁)) < ((𝐸 · 𝐸) · 1)))
204158, 116, 156, 202, 203syl112anc 1376 . . . . . . . . . . 11 (𝜑 → (((𝐿 − 1) / 𝑁) < 1 ↔ ((𝐸 · 𝐸) · ((𝐿 − 1) / 𝑁)) < ((𝐸 · 𝐸) · 1)))
205201, 204mpbid 232 . . . . . . . . . 10 (𝜑 → ((𝐸 · 𝐸) · ((𝐿 − 1) / 𝑁)) < ((𝐸 · 𝐸) · 1))
206176, 176mulcld 11281 . . . . . . . . . . 11 (𝜑 → (𝐸 · 𝐸) ∈ ℂ)
207206mulridd 11278 . . . . . . . . . 10 (𝜑 → ((𝐸 · 𝐸) · 1) = (𝐸 · 𝐸))
208205, 207breqtrd 5169 . . . . . . . . 9 (𝜑 → ((𝐸 · 𝐸) · ((𝐿 − 1) / 𝑁)) < (𝐸 · 𝐸))
209159, 156, 155, 208ltsub2dd 11876 . . . . . . . 8 (𝜑 → ((𝐸 · (𝐿 − 1)) − (𝐸 · 𝐸)) < ((𝐸 · (𝐿 − 1)) − ((𝐸 · 𝐸) · ((𝐿 − 1) / 𝑁))))
210114, 157, 160, 185, 209lttrd 11422 . . . . . . 7 (𝜑 → ((𝐿 − (4 / 3)) · 𝐸) < ((𝐸 · (𝐿 − 1)) − ((𝐸 · 𝐸) · ((𝐿 − 1) / 𝑁))))
211176, 198, 199divcld 12043 . . . . . . . . . . 11 (𝜑 → (𝐸 / 𝑁) ∈ ℂ)
212175, 211, 180subdird 11720 . . . . . . . . . 10 (𝜑 → ((1 − (𝐸 / 𝑁)) · (𝐿 − 1)) = ((1 · (𝐿 − 1)) − ((𝐸 / 𝑁) · (𝐿 − 1))))
213180mullidd 11279 . . . . . . . . . . 11 (𝜑 → (1 · (𝐿 − 1)) = (𝐿 − 1))
214213oveq1d 7446 . . . . . . . . . 10 (𝜑 → ((1 · (𝐿 − 1)) − ((𝐸 / 𝑁) · (𝐿 − 1))) = ((𝐿 − 1) − ((𝐸 / 𝑁) · (𝐿 − 1))))
215212, 214eqtrd 2777 . . . . . . . . 9 (𝜑 → ((1 − (𝐸 / 𝑁)) · (𝐿 − 1)) = ((𝐿 − 1) − ((𝐸 / 𝑁) · (𝐿 − 1))))
216215oveq2d 7447 . . . . . . . 8 (𝜑 → (𝐸 · ((1 − (𝐸 / 𝑁)) · (𝐿 − 1))) = (𝐸 · ((𝐿 − 1) − ((𝐸 / 𝑁) · (𝐿 − 1)))))
217211, 180mulcld 11281 . . . . . . . . 9 (𝜑 → ((𝐸 / 𝑁) · (𝐿 − 1)) ∈ ℂ)
218176, 180, 217subdid 11719 . . . . . . . 8 (𝜑 → (𝐸 · ((𝐿 − 1) − ((𝐸 / 𝑁) · (𝐿 − 1)))) = ((𝐸 · (𝐿 − 1)) − (𝐸 · ((𝐸 / 𝑁) · (𝐿 − 1)))))
219176, 198, 180, 199div32d 12066 . . . . . . . . . . 11 (𝜑 → ((𝐸 / 𝑁) · (𝐿 − 1)) = (𝐸 · ((𝐿 − 1) / 𝑁)))
220219oveq2d 7447 . . . . . . . . . 10 (𝜑 → (𝐸 · ((𝐸 / 𝑁) · (𝐿 − 1))) = (𝐸 · (𝐸 · ((𝐿 − 1) / 𝑁))))
221180, 198, 199divcld 12043 . . . . . . . . . . 11 (𝜑 → ((𝐿 − 1) / 𝑁) ∈ ℂ)
222176, 176, 221mulassd 11284 . . . . . . . . . 10 (𝜑 → ((𝐸 · 𝐸) · ((𝐿 − 1) / 𝑁)) = (𝐸 · (𝐸 · ((𝐿 − 1) / 𝑁))))
223220, 222eqtr4d 2780 . . . . . . . . 9 (𝜑 → (𝐸 · ((𝐸 / 𝑁) · (𝐿 − 1))) = ((𝐸 · 𝐸) · ((𝐿 − 1) / 𝑁)))
224223oveq2d 7447 . . . . . . . 8 (𝜑 → ((𝐸 · (𝐿 − 1)) − (𝐸 · ((𝐸 / 𝑁) · (𝐿 − 1)))) = ((𝐸 · (𝐿 − 1)) − ((𝐸 · 𝐸) · ((𝐿 − 1) / 𝑁))))
225216, 218, 2243eqtrd 2781 . . . . . . 7 (𝜑 → (𝐸 · ((1 − (𝐸 / 𝑁)) · (𝐿 − 1))) = ((𝐸 · (𝐿 − 1)) − ((𝐸 · 𝐸) · ((𝐿 − 1) / 𝑁))))
226210, 225breqtrrd 5171 . . . . . 6 (𝜑 → ((𝐿 − (4 / 3)) · 𝐸) < (𝐸 · ((1 − (𝐸 / 𝑁)) · (𝐿 − 1))))
227226adantr 480 . . . . 5 ((𝜑 ∧ ¬ 𝐿 = 1) → ((𝐿 − (4 / 3)) · 𝐸) < (𝐸 · ((1 − (𝐸 / 𝑁)) · (𝐿 − 1))))
228175, 211subcld 11620 . . . . . . . . . 10 (𝜑 → (1 − (𝐸 / 𝑁)) ∈ ℂ)
229 fsumconst 15826 . . . . . . . . . 10 (((0...(𝐿 − 2)) ∈ Fin ∧ (1 − (𝐸 / 𝑁)) ∈ ℂ) → Σ𝑖 ∈ (0...(𝐿 − 2))(1 − (𝐸 / 𝑁)) = ((♯‘(0...(𝐿 − 2))) · (1 − (𝐸 / 𝑁))))
230124, 228, 229syl2anc 584 . . . . . . . . 9 (𝜑 → Σ𝑖 ∈ (0...(𝐿 − 2))(1 − (𝐸 / 𝑁)) = ((♯‘(0...(𝐿 − 2))) · (1 − (𝐸 / 𝑁))))
231230adantr 480 . . . . . . . 8 ((𝜑 ∧ ¬ 𝐿 = 1) → Σ𝑖 ∈ (0...(𝐿 − 2))(1 − (𝐸 / 𝑁)) = ((♯‘(0...(𝐿 − 2))) · (1 − (𝐸 / 𝑁))))
232 0zd 12625 . . . . . . . . . . . . 13 ((𝜑 ∧ ¬ 𝐿 = 1) → 0 ∈ ℤ)
23331adantr 480 . . . . . . . . . . . . . . 15 ((𝜑 ∧ ¬ 𝐿 = 1) → 𝐿 ∈ (1...𝑁))
234233elfzelzd 13565 . . . . . . . . . . . . . 14 ((𝜑 ∧ ¬ 𝐿 = 1) → 𝐿 ∈ ℤ)
235126a1i 11 . . . . . . . . . . . . . 14 ((𝜑 ∧ ¬ 𝐿 = 1) → 2 ∈ ℤ)
236234, 235zsubcld 12727 . . . . . . . . . . . . 13 ((𝜑 ∧ ¬ 𝐿 = 1) → (𝐿 − 2) ∈ ℤ)
237 elnnuz 12922 . . . . . . . . . . . . . . . . . . . 20 (𝑁 ∈ ℕ ↔ 𝑁 ∈ (ℤ‘1))
238117, 237sylib 218 . . . . . . . . . . . . . . . . . . 19 (𝜑𝑁 ∈ (ℤ‘1))
239 elfzp12 13643 . . . . . . . . . . . . . . . . . . 19 (𝑁 ∈ (ℤ‘1) → (𝐿 ∈ (1...𝑁) ↔ (𝐿 = 1 ∨ 𝐿 ∈ ((1 + 1)...𝑁))))
240238, 239syl 17 . . . . . . . . . . . . . . . . . 18 (𝜑 → (𝐿 ∈ (1...𝑁) ↔ (𝐿 = 1 ∨ 𝐿 ∈ ((1 + 1)...𝑁))))
24131, 240mpbid 232 . . . . . . . . . . . . . . . . 17 (𝜑 → (𝐿 = 1 ∨ 𝐿 ∈ ((1 + 1)...𝑁)))
242241orcanai 1005 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ ¬ 𝐿 = 1) → 𝐿 ∈ ((1 + 1)...𝑁))
243 1p1e2 12391 . . . . . . . . . . . . . . . . . 18 (1 + 1) = 2
244243a1i 11 . . . . . . . . . . . . . . . . 17 ((𝜑 ∧ ¬ 𝐿 = 1) → (1 + 1) = 2)
245244oveq1d 7446 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ ¬ 𝐿 = 1) → ((1 + 1)...𝑁) = (2...𝑁))
246242, 245eleqtrd 2843 . . . . . . . . . . . . . . 15 ((𝜑 ∧ ¬ 𝐿 = 1) → 𝐿 ∈ (2...𝑁))
247 elfzle1 13567 . . . . . . . . . . . . . . 15 (𝐿 ∈ (2...𝑁) → 2 ≤ 𝐿)
248246, 247syl 17 . . . . . . . . . . . . . 14 ((𝜑 ∧ ¬ 𝐿 = 1) → 2 ≤ 𝐿)
249108adantr 480 . . . . . . . . . . . . . . 15 ((𝜑 ∧ ¬ 𝐿 = 1) → 𝐿 ∈ ℝ)
250131a1i 11 . . . . . . . . . . . . . . 15 ((𝜑 ∧ ¬ 𝐿 = 1) → 2 ∈ ℝ)
251249, 250subge0d 11853 . . . . . . . . . . . . . 14 ((𝜑 ∧ ¬ 𝐿 = 1) → (0 ≤ (𝐿 − 2) ↔ 2 ≤ 𝐿))
252248, 251mpbird 257 . . . . . . . . . . . . 13 ((𝜑 ∧ ¬ 𝐿 = 1) → 0 ≤ (𝐿 − 2))
253232, 236, 2523jca 1129 . . . . . . . . . . . 12 ((𝜑 ∧ ¬ 𝐿 = 1) → (0 ∈ ℤ ∧ (𝐿 − 2) ∈ ℤ ∧ 0 ≤ (𝐿 − 2)))
254 eluz2 12884 . . . . . . . . . . . 12 ((𝐿 − 2) ∈ (ℤ‘0) ↔ (0 ∈ ℤ ∧ (𝐿 − 2) ∈ ℤ ∧ 0 ≤ (𝐿 − 2)))
255253, 254sylibr 234 . . . . . . . . . . 11 ((𝜑 ∧ ¬ 𝐿 = 1) → (𝐿 − 2) ∈ (ℤ‘0))
256 hashfz 14466 . . . . . . . . . . 11 ((𝐿 − 2) ∈ (ℤ‘0) → (♯‘(0...(𝐿 − 2))) = (((𝐿 − 2) − 0) + 1))
257255, 256syl 17 . . . . . . . . . 10 ((𝜑 ∧ ¬ 𝐿 = 1) → (♯‘(0...(𝐿 − 2))) = (((𝐿 − 2) − 0) + 1))
258 2cn 12341 . . . . . . . . . . . . . . . 16 2 ∈ ℂ
259258a1i 11 . . . . . . . . . . . . . . 15 (𝜑 → 2 ∈ ℂ)
260139, 259subcld 11620 . . . . . . . . . . . . . 14 (𝜑 → (𝐿 − 2) ∈ ℂ)
261260subid1d 11609 . . . . . . . . . . . . 13 (𝜑 → ((𝐿 − 2) − 0) = (𝐿 − 2))
262261oveq1d 7446 . . . . . . . . . . . 12 (𝜑 → (((𝐿 − 2) − 0) + 1) = ((𝐿 − 2) + 1))
263139, 259, 175subadd23d 11642 . . . . . . . . . . . 12 (𝜑 → ((𝐿 − 2) + 1) = (𝐿 + (1 − 2)))
264258, 167negsubdi2i 11595 . . . . . . . . . . . . . . . 16 -(2 − 1) = (1 − 2)
265 2m1e1 12392 . . . . . . . . . . . . . . . . 17 (2 − 1) = 1
266265negeqi 11501 . . . . . . . . . . . . . . . 16 -(2 − 1) = -1
267264, 266eqtr3i 2767 . . . . . . . . . . . . . . 15 (1 − 2) = -1
268267a1i 11 . . . . . . . . . . . . . 14 (𝜑 → (1 − 2) = -1)
269268oveq2d 7447 . . . . . . . . . . . . 13 (𝜑 → (𝐿 + (1 − 2)) = (𝐿 + -1))
270139, 175negsubd 11626 . . . . . . . . . . . . 13 (𝜑 → (𝐿 + -1) = (𝐿 − 1))
271269, 270eqtrd 2777 . . . . . . . . . . . 12 (𝜑 → (𝐿 + (1 − 2)) = (𝐿 − 1))
272262, 263, 2713eqtrd 2781 . . . . . . . . . . 11 (𝜑 → (((𝐿 − 2) − 0) + 1) = (𝐿 − 1))
273272adantr 480 . . . . . . . . . 10 ((𝜑 ∧ ¬ 𝐿 = 1) → (((𝐿 − 2) − 0) + 1) = (𝐿 − 1))
274257, 273eqtrd 2777 . . . . . . . . 9 ((𝜑 ∧ ¬ 𝐿 = 1) → (♯‘(0...(𝐿 − 2))) = (𝐿 − 1))
275274oveq1d 7446 . . . . . . . 8 ((𝜑 ∧ ¬ 𝐿 = 1) → ((♯‘(0...(𝐿 − 2))) · (1 − (𝐸 / 𝑁))) = ((𝐿 − 1) · (1 − (𝐸 / 𝑁))))
276180, 228mulcomd 11282 . . . . . . . . 9 (𝜑 → ((𝐿 − 1) · (1 − (𝐸 / 𝑁))) = ((1 − (𝐸 / 𝑁)) · (𝐿 − 1)))
277276adantr 480 . . . . . . . 8 ((𝜑 ∧ ¬ 𝐿 = 1) → ((𝐿 − 1) · (1 − (𝐸 / 𝑁))) = ((1 − (𝐸 / 𝑁)) · (𝐿 − 1)))
278231, 275, 2773eqtrd 2781 . . . . . . 7 ((𝜑 ∧ ¬ 𝐿 = 1) → Σ𝑖 ∈ (0...(𝐿 − 2))(1 − (𝐸 / 𝑁)) = ((1 − (𝐸 / 𝑁)) · (𝐿 − 1)))
279 fzfid 14014 . . . . . . . 8 ((𝜑 ∧ ¬ 𝐿 = 1) → (0...(𝐿 − 2)) ∈ Fin)
280 fzn0 13578 . . . . . . . . 9 ((0...(𝐿 − 2)) ≠ ∅ ↔ (𝐿 − 2) ∈ (ℤ‘0))
281255, 280sylibr 234 . . . . . . . 8 ((𝜑 ∧ ¬ 𝐿 = 1) → (0...(𝐿 − 2)) ≠ ∅)
282119ad2antrr 726 . . . . . . . 8 (((𝜑 ∧ ¬ 𝐿 = 1) ∧ 𝑖 ∈ (0...(𝐿 − 2))) → (1 − (𝐸 / 𝑁)) ∈ ℝ)
283 simpll 767 . . . . . . . . 9 (((𝜑 ∧ ¬ 𝐿 = 1) ∧ 𝑖 ∈ (0...(𝐿 − 2))) → 𝜑)
284150adantlr 715 . . . . . . . . 9 (((𝜑 ∧ ¬ 𝐿 = 1) ∧ 𝑖 ∈ (0...(𝐿 − 2))) → 𝑖 ∈ (0...𝑁))
285283, 284, 51syl2anc 584 . . . . . . . 8 (((𝜑 ∧ ¬ 𝐿 = 1) ∧ 𝑖 ∈ (0...(𝐿 − 2))) → ((𝑋𝑖)‘𝑆) ∈ ℝ)
28649adantr 480 . . . . . . . . . . . 12 ((𝜑𝑖 ∈ (0...(𝐿 − 2))) → 𝑆𝑇)
287 elfzelz 13564 . . . . . . . . . . . . . . . . 17 (𝑖 ∈ (0...(𝐿 − 2)) → 𝑖 ∈ ℤ)
288287zred 12722 . . . . . . . . . . . . . . . 16 (𝑖 ∈ (0...(𝐿 − 2)) → 𝑖 ∈ ℝ)
289288adantl 481 . . . . . . . . . . . . . . 15 ((𝜑𝑖 ∈ (0...(𝐿 − 2))) → 𝑖 ∈ ℝ)
290163a1i 11 . . . . . . . . . . . . . . 15 ((𝜑𝑖 ∈ (0...(𝐿 − 2))) → (1 / 3) ∈ ℝ)
291289, 290readdcld 11290 . . . . . . . . . . . . . 14 ((𝜑𝑖 ∈ (0...(𝐿 − 2))) → (𝑖 + (1 / 3)) ∈ ℝ)
29214adantr 480 . . . . . . . . . . . . . 14 ((𝜑𝑖 ∈ (0...(𝐿 − 2))) → 𝐸 ∈ ℝ)
293291, 292remulcld 11291 . . . . . . . . . . . . 13 ((𝜑𝑖 ∈ (0...(𝐿 − 2))) → ((𝑖 + (1 / 3)) · 𝐸) ∈ ℝ)
294108adantr 480 . . . . . . . . . . . . . . . 16 ((𝜑𝑖 ∈ (0...(𝐿 − 2))) → 𝐿 ∈ ℝ)
295131a1i 11 . . . . . . . . . . . . . . . 16 ((𝜑𝑖 ∈ (0...(𝐿 − 2))) → 2 ∈ ℝ)
296294, 295resubcld 11691 . . . . . . . . . . . . . . 15 ((𝜑𝑖 ∈ (0...(𝐿 − 2))) → (𝐿 − 2) ∈ ℝ)
297296, 290readdcld 11290 . . . . . . . . . . . . . 14 ((𝜑𝑖 ∈ (0...(𝐿 − 2))) → ((𝐿 − 2) + (1 / 3)) ∈ ℝ)
298297, 292remulcld 11291 . . . . . . . . . . . . 13 ((𝜑𝑖 ∈ (0...(𝐿 − 2))) → (((𝐿 − 2) + (1 / 3)) · 𝐸) ∈ ℝ)
299 stoweidlem26.10 . . . . . . . . . . . . . . . 16 (𝜑𝐹:𝑇⟶ℝ)
300299, 49jca 511 . . . . . . . . . . . . . . 15 (𝜑 → (𝐹:𝑇⟶ℝ ∧ 𝑆𝑇))
301300adantr 480 . . . . . . . . . . . . . 14 ((𝜑𝑖 ∈ (0...(𝐿 − 2))) → (𝐹:𝑇⟶ℝ ∧ 𝑆𝑇))
302 ffvelcdm 7101 . . . . . . . . . . . . . 14 ((𝐹:𝑇⟶ℝ ∧ 𝑆𝑇) → (𝐹𝑆) ∈ ℝ)
303301, 302syl 17 . . . . . . . . . . . . 13 ((𝜑𝑖 ∈ (0...(𝐿 − 2))) → (𝐹𝑆) ∈ ℝ)
304 elfzle2 13568 . . . . . . . . . . . . . . . 16 (𝑖 ∈ (0...(𝐿 − 2)) → 𝑖 ≤ (𝐿 − 2))
305304adantl 481 . . . . . . . . . . . . . . 15 ((𝜑𝑖 ∈ (0...(𝐿 − 2))) → 𝑖 ≤ (𝐿 − 2))
306289, 296, 290, 305leadd1dd 11877 . . . . . . . . . . . . . 14 ((𝜑𝑖 ∈ (0...(𝐿 − 2))) → (𝑖 + (1 / 3)) ≤ ((𝐿 − 2) + (1 / 3)))
30714, 72jca 511 . . . . . . . . . . . . . . . 16 (𝜑 → (𝐸 ∈ ℝ ∧ 0 < 𝐸))
308307adantr 480 . . . . . . . . . . . . . . 15 ((𝜑𝑖 ∈ (0...(𝐿 − 2))) → (𝐸 ∈ ℝ ∧ 0 < 𝐸))
309 lemul1 12119 . . . . . . . . . . . . . . 15 (((𝑖 + (1 / 3)) ∈ ℝ ∧ ((𝐿 − 2) + (1 / 3)) ∈ ℝ ∧ (𝐸 ∈ ℝ ∧ 0 < 𝐸)) → ((𝑖 + (1 / 3)) ≤ ((𝐿 − 2) + (1 / 3)) ↔ ((𝑖 + (1 / 3)) · 𝐸) ≤ (((𝐿 − 2) + (1 / 3)) · 𝐸)))
310291, 297, 308, 309syl3anc 1373 . . . . . . . . . . . . . 14 ((𝜑𝑖 ∈ (0...(𝐿 − 2))) → ((𝑖 + (1 / 3)) ≤ ((𝐿 − 2) + (1 / 3)) ↔ ((𝑖 + (1 / 3)) · 𝐸) ≤ (((𝐿 − 2) + (1 / 3)) · 𝐸)))
311306, 310mpbid 232 . . . . . . . . . . . . 13 ((𝜑𝑖 ∈ (0...(𝐿 − 2))) → ((𝑖 + (1 / 3)) · 𝐸) ≤ (((𝐿 − 2) + (1 / 3)) · 𝐸))
312108, 132resubcld 11691 . . . . . . . . . . . . . . . . 17 (𝜑 → (𝐿 − 2) ∈ ℝ)
313312, 164readdcld 11290 . . . . . . . . . . . . . . . 16 (𝜑 → ((𝐿 − 2) + (1 / 3)) ∈ ℝ)
314313, 14remulcld 11291 . . . . . . . . . . . . . . 15 (𝜑 → (((𝐿 − 2) + (1 / 3)) · 𝐸) ∈ ℝ)
315299, 49ffvelcdmd 7105 . . . . . . . . . . . . . . 15 (𝜑 → (𝐹𝑆) ∈ ℝ)
316120, 164resubcld 11691 . . . . . . . . . . . . . . . . 17 (𝜑 → ((𝐿 − 1) − (1 / 3)) ∈ ℝ)
317316, 14remulcld 11291 . . . . . . . . . . . . . . . 16 (𝜑 → (((𝐿 − 1) − (1 / 3)) · 𝐸) ∈ ℝ)
318 addrid 11441 . . . . . . . . . . . . . . . . . . . . . . . . 25 (1 ∈ ℂ → (1 + 0) = 1)
319318eqcomd 2743 . . . . . . . . . . . . . . . . . . . . . . . 24 (1 ∈ ℂ → 1 = (1 + 0))
320167, 319mp1i 13 . . . . . . . . . . . . . . . . . . . . . . 23 (𝜑 → 1 = (1 + 0))
321175subidd 11608 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝜑 → (1 − 1) = 0)
322321eqcomd 2743 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝜑 → 0 = (1 − 1))
323322oveq2d 7447 . . . . . . . . . . . . . . . . . . . . . . 23 (𝜑 → (1 + 0) = (1 + (1 − 1)))
324 addsubass 11518 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((1 ∈ ℂ ∧ 1 ∈ ℂ ∧ 1 ∈ ℂ) → ((1 + 1) − 1) = (1 + (1 − 1)))
325324eqcomd 2743 . . . . . . . . . . . . . . . . . . . . . . . 24 ((1 ∈ ℂ ∧ 1 ∈ ℂ ∧ 1 ∈ ℂ) → (1 + (1 − 1)) = ((1 + 1) − 1))
326175, 175, 175, 325syl3anc 1373 . . . . . . . . . . . . . . . . . . . . . . 23 (𝜑 → (1 + (1 − 1)) = ((1 + 1) − 1))
327320, 323, 3263eqtrd 2781 . . . . . . . . . . . . . . . . . . . . . 22 (𝜑 → 1 = ((1 + 1) − 1))
328327oveq2d 7447 . . . . . . . . . . . . . . . . . . . . 21 (𝜑 → (𝐿 − 1) = (𝐿 − ((1 + 1) − 1)))
329243a1i 11 . . . . . . . . . . . . . . . . . . . . . . 23 (𝜑 → (1 + 1) = 2)
330329oveq1d 7446 . . . . . . . . . . . . . . . . . . . . . 22 (𝜑 → ((1 + 1) − 1) = (2 − 1))
331330oveq2d 7447 . . . . . . . . . . . . . . . . . . . . 21 (𝜑 → (𝐿 − ((1 + 1) − 1)) = (𝐿 − (2 − 1)))
332139, 259, 175subsubd 11648 . . . . . . . . . . . . . . . . . . . . 21 (𝜑 → (𝐿 − (2 − 1)) = ((𝐿 − 2) + 1))
333328, 331, 3323eqtrd 2781 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → (𝐿 − 1) = ((𝐿 − 2) + 1))
334333oveq1d 7446 . . . . . . . . . . . . . . . . . . 19 (𝜑 → ((𝐿 − 1) − (2 / 3)) = (((𝐿 − 2) + 1) − (2 / 3)))
335258, 60, 9divcli 12009 . . . . . . . . . . . . . . . . . . . . 21 (2 / 3) ∈ ℂ
336335a1i 11 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → (2 / 3) ∈ ℂ)
337260, 175, 336addsubassd 11640 . . . . . . . . . . . . . . . . . . 19 (𝜑 → (((𝐿 − 2) + 1) − (2 / 3)) = ((𝐿 − 2) + (1 − (2 / 3))))
338167, 60, 9divcli 12009 . . . . . . . . . . . . . . . . . . . . . 22 (1 / 3) ∈ ℂ
339 df-3 12330 . . . . . . . . . . . . . . . . . . . . . . . 24 3 = (2 + 1)
340339oveq1i 7441 . . . . . . . . . . . . . . . . . . . . . . 23 (3 / 3) = ((2 + 1) / 3)
341258, 167, 60, 9divdiri 12024 . . . . . . . . . . . . . . . . . . . . . . 23 ((2 + 1) / 3) = ((2 / 3) + (1 / 3))
342340, 61, 3413eqtr3ri 2774 . . . . . . . . . . . . . . . . . . . . . 22 ((2 / 3) + (1 / 3)) = 1
343167, 335, 338, 342subaddrii 11598 . . . . . . . . . . . . . . . . . . . . 21 (1 − (2 / 3)) = (1 / 3)
344343a1i 11 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → (1 − (2 / 3)) = (1 / 3))
345344oveq2d 7447 . . . . . . . . . . . . . . . . . . 19 (𝜑 → ((𝐿 − 2) + (1 − (2 / 3))) = ((𝐿 − 2) + (1 / 3)))
346334, 337, 3453eqtrd 2781 . . . . . . . . . . . . . . . . . 18 (𝜑 → ((𝐿 − 1) − (2 / 3)) = ((𝐿 − 2) + (1 / 3)))
347131, 7, 9redivcli 12034 . . . . . . . . . . . . . . . . . . . 20 (2 / 3) ∈ ℝ
348347a1i 11 . . . . . . . . . . . . . . . . . . 19 (𝜑 → (2 / 3) ∈ ℝ)
349 1lt2 12437 . . . . . . . . . . . . . . . . . . . 20 1 < 2
3507, 63pm3.2i 470 . . . . . . . . . . . . . . . . . . . . . 22 (3 ∈ ℝ ∧ 0 < 3)
3511, 131, 3503pm3.2i 1340 . . . . . . . . . . . . . . . . . . . . 21 (1 ∈ ℝ ∧ 2 ∈ ℝ ∧ (3 ∈ ℝ ∧ 0 < 3))
352 ltdiv1 12132 . . . . . . . . . . . . . . . . . . . . 21 ((1 ∈ ℝ ∧ 2 ∈ ℝ ∧ (3 ∈ ℝ ∧ 0 < 3)) → (1 < 2 ↔ (1 / 3) < (2 / 3)))
353351, 352mp1i 13 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → (1 < 2 ↔ (1 / 3) < (2 / 3)))
354349, 353mpbii 233 . . . . . . . . . . . . . . . . . . 19 (𝜑 → (1 / 3) < (2 / 3))
355164, 348, 120, 354ltsub2dd 11876 . . . . . . . . . . . . . . . . . 18 (𝜑 → ((𝐿 − 1) − (2 / 3)) < ((𝐿 − 1) − (1 / 3)))
356346, 355eqbrtrrd 5167 . . . . . . . . . . . . . . . . 17 (𝜑 → ((𝐿 − 2) + (1 / 3)) < ((𝐿 − 1) − (1 / 3)))
357313, 316, 13, 356ltmul1dd 13132 . . . . . . . . . . . . . . . 16 (𝜑 → (((𝐿 − 2) + (1 / 3)) · 𝐸) < (((𝐿 − 1) − (1 / 3)) · 𝐸))
35823simprd 495 . . . . . . . . . . . . . . . . . . . . . . 23 (𝜑 → ¬ 𝑆 ∈ (𝐷‘(𝐿 − 1)))
359 oveq1 7438 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑗 = (𝐿 − 1) → (𝑗 − (1 / 3)) = ((𝐿 − 1) − (1 / 3)))
360359oveq1d 7446 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑗 = (𝐿 − 1) → ((𝑗 − (1 / 3)) · 𝐸) = (((𝐿 − 1) − (1 / 3)) · 𝐸))
361360breq2d 5155 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑗 = (𝐿 − 1) → ((𝐹𝑡) ≤ ((𝑗 − (1 / 3)) · 𝐸) ↔ (𝐹𝑡) ≤ (((𝐿 − 1) − (1 / 3)) · 𝐸)))
362361rabbidv 3444 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑗 = (𝐿 − 1) → {𝑡𝑇 ∣ (𝐹𝑡) ≤ ((𝑗 − (1 / 3)) · 𝐸)} = {𝑡𝑇 ∣ (𝐹𝑡) ≤ (((𝐿 − 1) − (1 / 3)) · 𝐸)})
363129peano2zd 12725 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝜑 → (𝑁 + 1) ∈ ℤ)
364189simpld 494 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝜑 → 1 ≤ 𝐿)
365134, 116readdcld 11290 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝜑 → (𝑁 + 1) ∈ ℝ)
366134lep1d 12199 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝜑𝑁 ≤ (𝑁 + 1))
367108, 134, 365, 190, 366letrd 11418 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝜑𝐿 ≤ (𝑁 + 1))
368186, 363, 125, 364, 367elfzd 13555 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝜑𝐿 ∈ (1...(𝑁 + 1)))
369139, 175npcand 11624 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝜑 → ((𝐿 − 1) + 1) = 𝐿)
370 0p1e1 12388 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (0 + 1) = 1
371370a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝜑 → (0 + 1) = 1)
372371oveq1d 7446 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝜑 → ((0 + 1)...(𝑁 + 1)) = (1...(𝑁 + 1)))
373368, 369, 3723eltr4d 2856 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝜑 → ((𝐿 − 1) + 1) ∈ ((0 + 1)...(𝑁 + 1)))
374 0zd 12625 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝜑 → 0 ∈ ℤ)
375125, 186zsubcld 12727 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝜑 → (𝐿 − 1) ∈ ℤ)
376 fzaddel 13598 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((0 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ ((𝐿 − 1) ∈ ℤ ∧ 1 ∈ ℤ)) → ((𝐿 − 1) ∈ (0...𝑁) ↔ ((𝐿 − 1) + 1) ∈ ((0 + 1)...(𝑁 + 1))))
377374, 129, 375, 186, 376syl22anc 839 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝜑 → ((𝐿 − 1) ∈ (0...𝑁) ↔ ((𝐿 − 1) + 1) ∈ ((0 + 1)...(𝑁 + 1))))
378373, 377mpbird 257 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝜑 → (𝐿 − 1) ∈ (0...𝑁))
379 rabexg 5337 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑇 ∈ V → {𝑡𝑇 ∣ (𝐹𝑡) ≤ (((𝐿 − 1) − (1 / 3)) · 𝐸)} ∈ V)
38033, 379syl 17 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝜑 → {𝑡𝑇 ∣ (𝐹𝑡) ≤ (((𝐿 − 1) − (1 / 3)) · 𝐸)} ∈ V)
38125, 362, 378, 380fvmptd3 7039 . . . . . . . . . . . . . . . . . . . . . . 23 (𝜑 → (𝐷‘(𝐿 − 1)) = {𝑡𝑇 ∣ (𝐹𝑡) ≤ (((𝐿 − 1) − (1 / 3)) · 𝐸)})
382358, 381neleqtrd 2863 . . . . . . . . . . . . . . . . . . . . . 22 (𝜑 → ¬ 𝑆 ∈ {𝑡𝑇 ∣ (𝐹𝑡) ≤ (((𝐿 − 1) − (1 / 3)) · 𝐸)})
383 nfcv 2905 . . . . . . . . . . . . . . . . . . . . . . . 24 𝑡(((𝐿 − 1) − (1 / 3)) · 𝐸)
38441, 42, 383nfbr 5190 . . . . . . . . . . . . . . . . . . . . . . 23 𝑡(𝐹𝑆) ≤ (((𝐿 − 1) − (1 / 3)) · 𝐸)
38545breq1d 5153 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑡 = 𝑆 → ((𝐹𝑡) ≤ (((𝐿 − 1) − (1 / 3)) · 𝐸) ↔ (𝐹𝑆) ≤ (((𝐿 − 1) − (1 / 3)) · 𝐸)))
38638, 39, 384, 385elrabf 3688 . . . . . . . . . . . . . . . . . . . . . 22 (𝑆 ∈ {𝑡𝑇 ∣ (𝐹𝑡) ≤ (((𝐿 − 1) − (1 / 3)) · 𝐸)} ↔ (𝑆𝑇 ∧ (𝐹𝑆) ≤ (((𝐿 − 1) − (1 / 3)) · 𝐸)))
387382, 386sylnib 328 . . . . . . . . . . . . . . . . . . . . 21 (𝜑 → ¬ (𝑆𝑇 ∧ (𝐹𝑆) ≤ (((𝐿 − 1) − (1 / 3)) · 𝐸)))
388 ianor 984 . . . . . . . . . . . . . . . . . . . . 21 (¬ (𝑆𝑇 ∧ (𝐹𝑆) ≤ (((𝐿 − 1) − (1 / 3)) · 𝐸)) ↔ (¬ 𝑆𝑇 ∨ ¬ (𝐹𝑆) ≤ (((𝐿 − 1) − (1 / 3)) · 𝐸)))
389387, 388sylib 218 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → (¬ 𝑆𝑇 ∨ ¬ (𝐹𝑆) ≤ (((𝐿 − 1) − (1 / 3)) · 𝐸)))
390 olc 869 . . . . . . . . . . . . . . . . . . . . 21 (𝑆𝑇 → (¬ (𝐹𝑆) ≤ (((𝐿 − 1) − (1 / 3)) · 𝐸) ∨ 𝑆𝑇))
391390anim1i 615 . . . . . . . . . . . . . . . . . . . 20 ((𝑆𝑇 ∧ (¬ 𝑆𝑇 ∨ ¬ (𝐹𝑆) ≤ (((𝐿 − 1) − (1 / 3)) · 𝐸))) → ((¬ (𝐹𝑆) ≤ (((𝐿 − 1) − (1 / 3)) · 𝐸) ∨ 𝑆𝑇) ∧ (¬ 𝑆𝑇 ∨ ¬ (𝐹𝑆) ≤ (((𝐿 − 1) − (1 / 3)) · 𝐸))))
39249, 389, 391syl2anc 584 . . . . . . . . . . . . . . . . . . 19 (𝜑 → ((¬ (𝐹𝑆) ≤ (((𝐿 − 1) − (1 / 3)) · 𝐸) ∨ 𝑆𝑇) ∧ (¬ 𝑆𝑇 ∨ ¬ (𝐹𝑆) ≤ (((𝐿 − 1) − (1 / 3)) · 𝐸))))
393 orcom 871 . . . . . . . . . . . . . . . . . . . 20 ((¬ 𝑆𝑇 ∨ ¬ (𝐹𝑆) ≤ (((𝐿 − 1) − (1 / 3)) · 𝐸)) ↔ (¬ (𝐹𝑆) ≤ (((𝐿 − 1) − (1 / 3)) · 𝐸) ∨ ¬ 𝑆𝑇))
394393anbi2i 623 . . . . . . . . . . . . . . . . . . 19 (((¬ (𝐹𝑆) ≤ (((𝐿 − 1) − (1 / 3)) · 𝐸) ∨ 𝑆𝑇) ∧ (¬ 𝑆𝑇 ∨ ¬ (𝐹𝑆) ≤ (((𝐿 − 1) − (1 / 3)) · 𝐸))) ↔ ((¬ (𝐹𝑆) ≤ (((𝐿 − 1) − (1 / 3)) · 𝐸) ∨ 𝑆𝑇) ∧ (¬ (𝐹𝑆) ≤ (((𝐿 − 1) − (1 / 3)) · 𝐸) ∨ ¬ 𝑆𝑇)))
395392, 394sylib 218 . . . . . . . . . . . . . . . . . 18 (𝜑 → ((¬ (𝐹𝑆) ≤ (((𝐿 − 1) − (1 / 3)) · 𝐸) ∨ 𝑆𝑇) ∧ (¬ (𝐹𝑆) ≤ (((𝐿 − 1) − (1 / 3)) · 𝐸) ∨ ¬ 𝑆𝑇)))
396 pm4.43 1025 . . . . . . . . . . . . . . . . . 18 (¬ (𝐹𝑆) ≤ (((𝐿 − 1) − (1 / 3)) · 𝐸) ↔ ((¬ (𝐹𝑆) ≤ (((𝐿 − 1) − (1 / 3)) · 𝐸) ∨ 𝑆𝑇) ∧ (¬ (𝐹𝑆) ≤ (((𝐿 − 1) − (1 / 3)) · 𝐸) ∨ ¬ 𝑆𝑇)))
397395, 396sylibr 234 . . . . . . . . . . . . . . . . 17 (𝜑 → ¬ (𝐹𝑆) ≤ (((𝐿 − 1) − (1 / 3)) · 𝐸))
398317, 315ltnled 11408 . . . . . . . . . . . . . . . . 17 (𝜑 → ((((𝐿 − 1) − (1 / 3)) · 𝐸) < (𝐹𝑆) ↔ ¬ (𝐹𝑆) ≤ (((𝐿 − 1) − (1 / 3)) · 𝐸)))
399397, 398mpbird 257 . . . . . . . . . . . . . . . 16 (𝜑 → (((𝐿 − 1) − (1 / 3)) · 𝐸) < (𝐹𝑆))
400314, 317, 315, 357, 399lttrd 11422 . . . . . . . . . . . . . . 15 (𝜑 → (((𝐿 − 2) + (1 / 3)) · 𝐸) < (𝐹𝑆))
401314, 315, 400ltled 11409 . . . . . . . . . . . . . 14 (𝜑 → (((𝐿 − 2) + (1 / 3)) · 𝐸) ≤ (𝐹𝑆))
402401adantr 480 . . . . . . . . . . . . 13 ((𝜑𝑖 ∈ (0...(𝐿 − 2))) → (((𝐿 − 2) + (1 / 3)) · 𝐸) ≤ (𝐹𝑆))
403293, 298, 303, 311, 402letrd 11418 . . . . . . . . . . . 12 ((𝜑𝑖 ∈ (0...(𝐿 − 2))) → ((𝑖 + (1 / 3)) · 𝐸) ≤ (𝐹𝑆))
404 nfcv 2905 . . . . . . . . . . . . . 14 𝑡((𝑖 + (1 / 3)) · 𝐸)
405404, 42, 41nfbr 5190 . . . . . . . . . . . . 13 𝑡((𝑖 + (1 / 3)) · 𝐸) ≤ (𝐹𝑆)
40645breq2d 5155 . . . . . . . . . . . . 13 (𝑡 = 𝑆 → (((𝑖 + (1 / 3)) · 𝐸) ≤ (𝐹𝑡) ↔ ((𝑖 + (1 / 3)) · 𝐸) ≤ (𝐹𝑆)))
40738, 39, 405, 406elrabf 3688 . . . . . . . . . . . 12 (𝑆 ∈ {𝑡𝑇 ∣ ((𝑖 + (1 / 3)) · 𝐸) ≤ (𝐹𝑡)} ↔ (𝑆𝑇 ∧ ((𝑖 + (1 / 3)) · 𝐸) ≤ (𝐹𝑆)))
408286, 403, 407sylanbrc 583 . . . . . . . . . . 11 ((𝜑𝑖 ∈ (0...(𝐿 − 2))) → 𝑆 ∈ {𝑡𝑇 ∣ ((𝑖 + (1 / 3)) · 𝐸) ≤ (𝐹𝑡)})
409 stoweidlem26.5 . . . . . . . . . . . 12 𝐵 = (𝑗 ∈ (0...𝑁) ↦ {𝑡𝑇 ∣ ((𝑗 + (1 / 3)) · 𝐸) ≤ (𝐹𝑡)})
410 oveq1 7438 . . . . . . . . . . . . . . 15 (𝑗 = 𝑖 → (𝑗 + (1 / 3)) = (𝑖 + (1 / 3)))
411410oveq1d 7446 . . . . . . . . . . . . . 14 (𝑗 = 𝑖 → ((𝑗 + (1 / 3)) · 𝐸) = ((𝑖 + (1 / 3)) · 𝐸))
412411breq1d 5153 . . . . . . . . . . . . 13 (𝑗 = 𝑖 → (((𝑗 + (1 / 3)) · 𝐸) ≤ (𝐹𝑡) ↔ ((𝑖 + (1 / 3)) · 𝐸) ≤ (𝐹𝑡)))
413412rabbidv 3444 . . . . . . . . . . . 12 (𝑗 = 𝑖 → {𝑡𝑇 ∣ ((𝑗 + (1 / 3)) · 𝐸) ≤ (𝐹𝑡)} = {𝑡𝑇 ∣ ((𝑖 + (1 / 3)) · 𝐸) ≤ (𝐹𝑡)})
414 rabexg 5337 . . . . . . . . . . . . . 14 (𝑇 ∈ V → {𝑡𝑇 ∣ ((𝑖 + (1 / 3)) · 𝐸) ≤ (𝐹𝑡)} ∈ V)
41533, 414syl 17 . . . . . . . . . . . . 13 (𝜑 → {𝑡𝑇 ∣ ((𝑖 + (1 / 3)) · 𝐸) ≤ (𝐹𝑡)} ∈ V)
416415adantr 480 . . . . . . . . . . . 12 ((𝜑𝑖 ∈ (0...(𝐿 − 2))) → {𝑡𝑇 ∣ ((𝑖 + (1 / 3)) · 𝐸) ≤ (𝐹𝑡)} ∈ V)
417409, 413, 150, 416fvmptd3 7039 . . . . . . . . . . 11 ((𝜑𝑖 ∈ (0...(𝐿 − 2))) → (𝐵𝑖) = {𝑡𝑇 ∣ ((𝑖 + (1 / 3)) · 𝐸) ≤ (𝐹𝑡)})
418408, 417eleqtrrd 2844 . . . . . . . . . 10 ((𝜑𝑖 ∈ (0...(𝐿 − 2))) → 𝑆 ∈ (𝐵𝑖))
4191453ad2ant1 1134 . . . . . . . . . . . . . 14 ((𝜑𝑖 ∈ (0...(𝐿 − 2)) ∧ 𝑆 ∈ (𝐵𝑖)) → ((𝐿 − 2) ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ (𝐿 − 2) ≤ 𝑁))
420419, 146sylibr 234 . . . . . . . . . . . . 13 ((𝜑𝑖 ∈ (0...(𝐿 − 2)) ∧ 𝑆 ∈ (𝐵𝑖)) → 𝑁 ∈ (ℤ‘(𝐿 − 2)))
421420, 148syl 17 . . . . . . . . . . . 12 ((𝜑𝑖 ∈ (0...(𝐿 − 2)) ∧ 𝑆 ∈ (𝐵𝑖)) → (0...(𝐿 − 2)) ⊆ (0...𝑁))
422 simp2 1138 . . . . . . . . . . . 12 ((𝜑𝑖 ∈ (0...(𝐿 − 2)) ∧ 𝑆 ∈ (𝐵𝑖)) → 𝑖 ∈ (0...(𝐿 − 2)))
423421, 422sseldd 3984 . . . . . . . . . . 11 ((𝜑𝑖 ∈ (0...(𝐿 − 2)) ∧ 𝑆 ∈ (𝐵𝑖)) → 𝑖 ∈ (0...𝑁))
424 elex 3501 . . . . . . . . . . . . 13 (𝑆 ∈ (𝐵𝑖) → 𝑆 ∈ V)
4254243ad2ant3 1136 . . . . . . . . . . . 12 ((𝜑𝑖 ∈ (0...𝑁) ∧ 𝑆 ∈ (𝐵𝑖)) → 𝑆 ∈ V)
426 nfcv 2905 . . . . . . . . . . . . . . . . . . 19 𝑡(0...𝑁)
427 nfrab1 3457 . . . . . . . . . . . . . . . . . . 19 𝑡{𝑡𝑇 ∣ ((𝑗 + (1 / 3)) · 𝐸) ≤ (𝐹𝑡)}
428426, 427nfmpt 5249 . . . . . . . . . . . . . . . . . 18 𝑡(𝑗 ∈ (0...𝑁) ↦ {𝑡𝑇 ∣ ((𝑗 + (1 / 3)) · 𝐸) ≤ (𝐹𝑡)})
429409, 428nfcxfr 2903 . . . . . . . . . . . . . . . . 17 𝑡𝐵
430 nfcv 2905 . . . . . . . . . . . . . . . . 17 𝑡𝑖
431429, 430nffv 6916 . . . . . . . . . . . . . . . 16 𝑡(𝐵𝑖)
432431nfel2 2924 . . . . . . . . . . . . . . 15 𝑡 𝑆 ∈ (𝐵𝑖)
43388, 89, 432nf3an 1901 . . . . . . . . . . . . . 14 𝑡(𝜑𝑖 ∈ (0...𝑁) ∧ 𝑆 ∈ (𝐵𝑖))
434 nfv 1914 . . . . . . . . . . . . . 14 𝑡(1 − (𝐸 / 𝑁)) < ((𝑋𝑖)‘𝑆)
435433, 434nfim 1896 . . . . . . . . . . . . 13 𝑡((𝜑𝑖 ∈ (0...𝑁) ∧ 𝑆 ∈ (𝐵𝑖)) → (1 − (𝐸 / 𝑁)) < ((𝑋𝑖)‘𝑆))
436 eleq1 2829 . . . . . . . . . . . . . . 15 (𝑡 = 𝑆 → (𝑡 ∈ (𝐵𝑖) ↔ 𝑆 ∈ (𝐵𝑖)))
4374363anbi3d 1444 . . . . . . . . . . . . . 14 (𝑡 = 𝑆 → ((𝜑𝑖 ∈ (0...𝑁) ∧ 𝑡 ∈ (𝐵𝑖)) ↔ (𝜑𝑖 ∈ (0...𝑁) ∧ 𝑆 ∈ (𝐵𝑖))))
43893breq2d 5155 . . . . . . . . . . . . . 14 (𝑡 = 𝑆 → ((1 − (𝐸 / 𝑁)) < ((𝑋𝑖)‘𝑡) ↔ (1 − (𝐸 / 𝑁)) < ((𝑋𝑖)‘𝑆)))
439437, 438imbi12d 344 . . . . . . . . . . . . 13 (𝑡 = 𝑆 → (((𝜑𝑖 ∈ (0...𝑁) ∧ 𝑡 ∈ (𝐵𝑖)) → (1 − (𝐸 / 𝑁)) < ((𝑋𝑖)‘𝑡)) ↔ ((𝜑𝑖 ∈ (0...𝑁) ∧ 𝑆 ∈ (𝐵𝑖)) → (1 − (𝐸 / 𝑁)) < ((𝑋𝑖)‘𝑆))))
440 stoweidlem26.15 . . . . . . . . . . . . 13 ((𝜑𝑖 ∈ (0...𝑁) ∧ 𝑡 ∈ (𝐵𝑖)) → (1 − (𝐸 / 𝑁)) < ((𝑋𝑖)‘𝑡))
441435, 439, 440vtoclg1f 3570 . . . . . . . . . . . 12 (𝑆 ∈ V → ((𝜑𝑖 ∈ (0...𝑁) ∧ 𝑆 ∈ (𝐵𝑖)) → (1 − (𝐸 / 𝑁)) < ((𝑋𝑖)‘𝑆)))
442425, 441mpcom 38 . . . . . . . . . . 11 ((𝜑𝑖 ∈ (0...𝑁) ∧ 𝑆 ∈ (𝐵𝑖)) → (1 − (𝐸 / 𝑁)) < ((𝑋𝑖)‘𝑆))
443423, 442syld3an2 1413 . . . . . . . . . 10 ((𝜑𝑖 ∈ (0...(𝐿 − 2)) ∧ 𝑆 ∈ (𝐵𝑖)) → (1 − (𝐸 / 𝑁)) < ((𝑋𝑖)‘𝑆))
444418, 443mpd3an3 1464 . . . . . . . . 9 ((𝜑𝑖 ∈ (0...(𝐿 − 2))) → (1 − (𝐸 / 𝑁)) < ((𝑋𝑖)‘𝑆))
445444adantlr 715 . . . . . . . 8 (((𝜑 ∧ ¬ 𝐿 = 1) ∧ 𝑖 ∈ (0...(𝐿 − 2))) → (1 − (𝐸 / 𝑁)) < ((𝑋𝑖)‘𝑆))
446279, 281, 282, 285, 445fsumlt 15836 . . . . . . 7 ((𝜑 ∧ ¬ 𝐿 = 1) → Σ𝑖 ∈ (0...(𝐿 − 2))(1 − (𝐸 / 𝑁)) < Σ𝑖 ∈ (0...(𝐿 − 2))((𝑋𝑖)‘𝑆))
447278, 446eqbrtrrd 5167 . . . . . 6 ((𝜑 ∧ ¬ 𝐿 = 1) → ((1 − (𝐸 / 𝑁)) · (𝐿 − 1)) < Σ𝑖 ∈ (0...(𝐿 − 2))((𝑋𝑖)‘𝑆))
448121adantr 480 . . . . . . 7 ((𝜑 ∧ ¬ 𝐿 = 1) → ((1 − (𝐸 / 𝑁)) · (𝐿 − 1)) ∈ ℝ)
449152adantr 480 . . . . . . 7 ((𝜑 ∧ ¬ 𝐿 = 1) → Σ𝑖 ∈ (0...(𝐿 − 2))((𝑋𝑖)‘𝑆) ∈ ℝ)
450307adantr 480 . . . . . . 7 ((𝜑 ∧ ¬ 𝐿 = 1) → (𝐸 ∈ ℝ ∧ 0 < 𝐸))
451 ltmul2 12118 . . . . . . 7 ((((1 − (𝐸 / 𝑁)) · (𝐿 − 1)) ∈ ℝ ∧ Σ𝑖 ∈ (0...(𝐿 − 2))((𝑋𝑖)‘𝑆) ∈ ℝ ∧ (𝐸 ∈ ℝ ∧ 0 < 𝐸)) → (((1 − (𝐸 / 𝑁)) · (𝐿 − 1)) < Σ𝑖 ∈ (0...(𝐿 − 2))((𝑋𝑖)‘𝑆) ↔ (𝐸 · ((1 − (𝐸 / 𝑁)) · (𝐿 − 1))) < (𝐸 · Σ𝑖 ∈ (0...(𝐿 − 2))((𝑋𝑖)‘𝑆))))
452448, 449, 450, 451syl3anc 1373 . . . . . 6 ((𝜑 ∧ ¬ 𝐿 = 1) → (((1 − (𝐸 / 𝑁)) · (𝐿 − 1)) < Σ𝑖 ∈ (0...(𝐿 − 2))((𝑋𝑖)‘𝑆) ↔ (𝐸 · ((1 − (𝐸 / 𝑁)) · (𝐿 − 1))) < (𝐸 · Σ𝑖 ∈ (0...(𝐿 − 2))((𝑋𝑖)‘𝑆))))
453447, 452mpbid 232 . . . . 5 ((𝜑 ∧ ¬ 𝐿 = 1) → (𝐸 · ((1 − (𝐸 / 𝑁)) · (𝐿 − 1))) < (𝐸 · Σ𝑖 ∈ (0...(𝐿 − 2))((𝑋𝑖)‘𝑆)))
454115, 123, 154, 227, 453lttrd 11422 . . . 4 ((𝜑 ∧ ¬ 𝐿 = 1) → ((𝐿 − (4 / 3)) · 𝐸) < (𝐸 · Σ𝑖 ∈ (0...(𝐿 − 2))((𝑋𝑖)‘𝑆)))
455150, 52syldan 591 . . . . . . . . . 10 ((𝜑𝑖 ∈ (0...(𝐿 − 2))) → (𝐸 · ((𝑋𝑖)‘𝑆)) ∈ ℝ)
456455adantlr 715 . . . . . . . . 9 (((𝜑 ∧ ¬ 𝐿 = 1) ∧ 𝑖 ∈ (0...(𝐿 − 2))) → (𝐸 · ((𝑋𝑖)‘𝑆)) ∈ ℝ)
457456recnd 11289 . . . . . . . 8 (((𝜑 ∧ ¬ 𝐿 = 1) ∧ 𝑖 ∈ (0...(𝐿 − 2))) → (𝐸 · ((𝑋𝑖)‘𝑆)) ∈ ℂ)
458279, 457fsumcl 15769 . . . . . . 7 ((𝜑 ∧ ¬ 𝐿 = 1) → Σ𝑖 ∈ (0...(𝐿 − 2))(𝐸 · ((𝑋𝑖)‘𝑆)) ∈ ℂ)
459458addridd 11461 . . . . . 6 ((𝜑 ∧ ¬ 𝐿 = 1) → (Σ𝑖 ∈ (0...(𝐿 − 2))(𝐸 · ((𝑋𝑖)‘𝑆)) + 0) = Σ𝑖 ∈ (0...(𝐿 − 2))(𝐸 · ((𝑋𝑖)‘𝑆)))
460 0red 11264 . . . . . . 7 ((𝜑 ∧ ¬ 𝐿 = 1) → 0 ∈ ℝ)
461 fzfid 14014 . . . . . . . 8 ((𝜑 ∧ ¬ 𝐿 = 1) → ((𝐿 − 1)...𝑁) ∈ Fin)
46214adantr 480 . . . . . . . . . 10 ((𝜑𝑖 ∈ ((𝐿 − 1)...𝑁)) → 𝐸 ∈ ℝ)
463 0zd 12625 . . . . . . . . . . . 12 ((𝜑𝑖 ∈ ((𝐿 − 1)...𝑁)) → 0 ∈ ℤ)
464129adantr 480 . . . . . . . . . . . 12 ((𝜑𝑖 ∈ ((𝐿 − 1)...𝑁)) → 𝑁 ∈ ℤ)
465 elfzelz 13564 . . . . . . . . . . . . 13 (𝑖 ∈ ((𝐿 − 1)...𝑁) → 𝑖 ∈ ℤ)
466465adantl 481 . . . . . . . . . . . 12 ((𝜑𝑖 ∈ ((𝐿 − 1)...𝑁)) → 𝑖 ∈ ℤ)
467 0red 11264 . . . . . . . . . . . . 13 ((𝜑𝑖 ∈ ((𝐿 − 1)...𝑁)) → 0 ∈ ℝ)
468120adantr 480 . . . . . . . . . . . . 13 ((𝜑𝑖 ∈ ((𝐿 − 1)...𝑁)) → (𝐿 − 1) ∈ ℝ)
469465zred 12722 . . . . . . . . . . . . . 14 (𝑖 ∈ ((𝐿 − 1)...𝑁) → 𝑖 ∈ ℝ)
470469adantl 481 . . . . . . . . . . . . 13 ((𝜑𝑖 ∈ ((𝐿 − 1)...𝑁)) → 𝑖 ∈ ℝ)
471 1m1e0 12338 . . . . . . . . . . . . . . 15 (1 − 1) = 0
472116, 108, 116, 364lesub1dd 11879 . . . . . . . . . . . . . . 15 (𝜑 → (1 − 1) ≤ (𝐿 − 1))
473471, 472eqbrtrrid 5179 . . . . . . . . . . . . . 14 (𝜑 → 0 ≤ (𝐿 − 1))
474473adantr 480 . . . . . . . . . . . . 13 ((𝜑𝑖 ∈ ((𝐿 − 1)...𝑁)) → 0 ≤ (𝐿 − 1))
475 simpr 484 . . . . . . . . . . . . . . 15 ((𝜑𝑖 ∈ ((𝐿 − 1)...𝑁)) → 𝑖 ∈ ((𝐿 − 1)...𝑁))
476375adantr 480 . . . . . . . . . . . . . . . 16 ((𝜑𝑖 ∈ ((𝐿 − 1)...𝑁)) → (𝐿 − 1) ∈ ℤ)
477 elfz 13553 . . . . . . . . . . . . . . . 16 ((𝑖 ∈ ℤ ∧ (𝐿 − 1) ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑖 ∈ ((𝐿 − 1)...𝑁) ↔ ((𝐿 − 1) ≤ 𝑖𝑖𝑁)))
478466, 476, 464, 477syl3anc 1373 . . . . . . . . . . . . . . 15 ((𝜑𝑖 ∈ ((𝐿 − 1)...𝑁)) → (𝑖 ∈ ((𝐿 − 1)...𝑁) ↔ ((𝐿 − 1) ≤ 𝑖𝑖𝑁)))
479475, 478mpbid 232 . . . . . . . . . . . . . 14 ((𝜑𝑖 ∈ ((𝐿 − 1)...𝑁)) → ((𝐿 − 1) ≤ 𝑖𝑖𝑁))
480479simpld 494 . . . . . . . . . . . . 13 ((𝜑𝑖 ∈ ((𝐿 − 1)...𝑁)) → (𝐿 − 1) ≤ 𝑖)
481467, 468, 470, 474, 480letrd 11418 . . . . . . . . . . . 12 ((𝜑𝑖 ∈ ((𝐿 − 1)...𝑁)) → 0 ≤ 𝑖)
482 elfzle2 13568 . . . . . . . . . . . . 13 (𝑖 ∈ ((𝐿 − 1)...𝑁) → 𝑖𝑁)
483482adantl 481 . . . . . . . . . . . 12 ((𝜑𝑖 ∈ ((𝐿 − 1)...𝑁)) → 𝑖𝑁)
484463, 464, 466, 481, 483elfzd 13555 . . . . . . . . . . 11 ((𝜑𝑖 ∈ ((𝐿 − 1)...𝑁)) → 𝑖 ∈ (0...𝑁))
485484, 51syldan 591 . . . . . . . . . 10 ((𝜑𝑖 ∈ ((𝐿 − 1)...𝑁)) → ((𝑋𝑖)‘𝑆) ∈ ℝ)
486462, 485remulcld 11291 . . . . . . . . 9 ((𝜑𝑖 ∈ ((𝐿 − 1)...𝑁)) → (𝐸 · ((𝑋𝑖)‘𝑆)) ∈ ℝ)
487486adantlr 715 . . . . . . . 8 (((𝜑 ∧ ¬ 𝐿 = 1) ∧ 𝑖 ∈ ((𝐿 − 1)...𝑁)) → (𝐸 · ((𝑋𝑖)‘𝑆)) ∈ ℝ)
488461, 487fsumrecl 15770 . . . . . . 7 ((𝜑 ∧ ¬ 𝐿 = 1) → Σ𝑖 ∈ ((𝐿 − 1)...𝑁)(𝐸 · ((𝑋𝑖)‘𝑆)) ∈ ℝ)
489279, 456fsumrecl 15770 . . . . . . 7 ((𝜑 ∧ ¬ 𝐿 = 1) → Σ𝑖 ∈ (0...(𝐿 − 2))(𝐸 · ((𝑋𝑖)‘𝑆)) ∈ ℝ)
490 fzfid 14014 . . . . . . . . 9 (𝜑 → ((𝐿 − 1)...𝑁) ∈ Fin)
491176adantr 480 . . . . . . . . . . 11 ((𝜑𝑖 ∈ ((𝐿 − 1)...𝑁)) → 𝐸 ∈ ℂ)
492491mul01d 11460 . . . . . . . . . 10 ((𝜑𝑖 ∈ ((𝐿 − 1)...𝑁)) → (𝐸 · 0) = 0)
493484, 100syldan 591 . . . . . . . . . . 11 ((𝜑𝑖 ∈ ((𝐿 − 1)...𝑁)) → 0 ≤ ((𝑋𝑖)‘𝑆))
494307adantr 480 . . . . . . . . . . . 12 ((𝜑𝑖 ∈ ((𝐿 − 1)...𝑁)) → (𝐸 ∈ ℝ ∧ 0 < 𝐸))
495 lemul2 12120 . . . . . . . . . . . 12 ((0 ∈ ℝ ∧ ((𝑋𝑖)‘𝑆) ∈ ℝ ∧ (𝐸 ∈ ℝ ∧ 0 < 𝐸)) → (0 ≤ ((𝑋𝑖)‘𝑆) ↔ (𝐸 · 0) ≤ (𝐸 · ((𝑋𝑖)‘𝑆))))
496467, 485, 494, 495syl3anc 1373 . . . . . . . . . . 11 ((𝜑𝑖 ∈ ((𝐿 − 1)...𝑁)) → (0 ≤ ((𝑋𝑖)‘𝑆) ↔ (𝐸 · 0) ≤ (𝐸 · ((𝑋𝑖)‘𝑆))))
497493, 496mpbid 232 . . . . . . . . . 10 ((𝜑𝑖 ∈ ((𝐿 − 1)...𝑁)) → (𝐸 · 0) ≤ (𝐸 · ((𝑋𝑖)‘𝑆)))
498492, 497eqbrtrrd 5167 . . . . . . . . 9 ((𝜑𝑖 ∈ ((𝐿 − 1)...𝑁)) → 0 ≤ (𝐸 · ((𝑋𝑖)‘𝑆)))
499490, 486, 498fsumge0 15831 . . . . . . . 8 (𝜑 → 0 ≤ Σ𝑖 ∈ ((𝐿 − 1)...𝑁)(𝐸 · ((𝑋𝑖)‘𝑆)))
500499adantr 480 . . . . . . 7 ((𝜑 ∧ ¬ 𝐿 = 1) → 0 ≤ Σ𝑖 ∈ ((𝐿 − 1)...𝑁)(𝐸 · ((𝑋𝑖)‘𝑆)))
501460, 488, 489, 500leadd2dd 11878 . . . . . 6 ((𝜑 ∧ ¬ 𝐿 = 1) → (Σ𝑖 ∈ (0...(𝐿 − 2))(𝐸 · ((𝑋𝑖)‘𝑆)) + 0) ≤ (Σ𝑖 ∈ (0...(𝐿 − 2))(𝐸 · ((𝑋𝑖)‘𝑆)) + Σ𝑖 ∈ ((𝐿 − 1)...𝑁)(𝐸 · ((𝑋𝑖)‘𝑆))))
502459, 501eqbrtrrd 5167 . . . . 5 ((𝜑 ∧ ¬ 𝐿 = 1) → Σ𝑖 ∈ (0...(𝐿 − 2))(𝐸 · ((𝑋𝑖)‘𝑆)) ≤ (Σ𝑖 ∈ (0...(𝐿 − 2))(𝐸 · ((𝑋𝑖)‘𝑆)) + Σ𝑖 ∈ ((𝐿 − 1)...𝑁)(𝐸 · ((𝑋𝑖)‘𝑆))))
503151recnd 11289 . . . . . . 7 ((𝜑𝑖 ∈ (0...(𝐿 − 2))) → ((𝑋𝑖)‘𝑆) ∈ ℂ)
504124, 176, 503fsummulc2 15820 . . . . . 6 (𝜑 → (𝐸 · Σ𝑖 ∈ (0...(𝐿 − 2))((𝑋𝑖)‘𝑆)) = Σ𝑖 ∈ (0...(𝐿 − 2))(𝐸 · ((𝑋𝑖)‘𝑆)))
505504adantr 480 . . . . 5 ((𝜑 ∧ ¬ 𝐿 = 1) → (𝐸 · Σ𝑖 ∈ (0...(𝐿 − 2))((𝑋𝑖)‘𝑆)) = Σ𝑖 ∈ (0...(𝐿 − 2))(𝐸 · ((𝑋𝑖)‘𝑆)))
506 stoweidlem26.2 . . . . . . . . 9 𝑗𝜑
507 elfzelz 13564 . . . . . . . . . . . . . . . 16 (𝑗 ∈ (0...(𝐿 − 2)) → 𝑗 ∈ ℤ)
508507adantl 481 . . . . . . . . . . . . . . 15 ((𝜑𝑗 ∈ (0...(𝐿 − 2))) → 𝑗 ∈ ℤ)
509508zred 12722 . . . . . . . . . . . . . 14 ((𝜑𝑗 ∈ (0...(𝐿 − 2))) → 𝑗 ∈ ℝ)
510312adantr 480 . . . . . . . . . . . . . 14 ((𝜑𝑗 ∈ (0...(𝐿 − 2))) → (𝐿 − 2) ∈ ℝ)
511120adantr 480 . . . . . . . . . . . . . 14 ((𝜑𝑗 ∈ (0...(𝐿 − 2))) → (𝐿 − 1) ∈ ℝ)
512 simpr 484 . . . . . . . . . . . . . . . 16 ((𝜑𝑗 ∈ (0...(𝐿 − 2))) → 𝑗 ∈ (0...(𝐿 − 2)))
513 0zd 12625 . . . . . . . . . . . . . . . . 17 ((𝜑𝑗 ∈ (0...(𝐿 − 2))) → 0 ∈ ℤ)
514128adantr 480 . . . . . . . . . . . . . . . . 17 ((𝜑𝑗 ∈ (0...(𝐿 − 2))) → (𝐿 − 2) ∈ ℤ)
515 elfz 13553 . . . . . . . . . . . . . . . . 17 ((𝑗 ∈ ℤ ∧ 0 ∈ ℤ ∧ (𝐿 − 2) ∈ ℤ) → (𝑗 ∈ (0...(𝐿 − 2)) ↔ (0 ≤ 𝑗𝑗 ≤ (𝐿 − 2))))
516508, 513, 514, 515syl3anc 1373 . . . . . . . . . . . . . . . 16 ((𝜑𝑗 ∈ (0...(𝐿 − 2))) → (𝑗 ∈ (0...(𝐿 − 2)) ↔ (0 ≤ 𝑗𝑗 ≤ (𝐿 − 2))))
517512, 516mpbid 232 . . . . . . . . . . . . . . 15 ((𝜑𝑗 ∈ (0...(𝐿 − 2))) → (0 ≤ 𝑗𝑗 ≤ (𝐿 − 2)))
518517simprd 495 . . . . . . . . . . . . . 14 ((𝜑𝑗 ∈ (0...(𝐿 − 2))) → 𝑗 ≤ (𝐿 − 2))
519116, 132, 108ltsub2d 11873 . . . . . . . . . . . . . . . 16 (𝜑 → (1 < 2 ↔ (𝐿 − 2) < (𝐿 − 1)))
520349, 519mpbii 233 . . . . . . . . . . . . . . 15 (𝜑 → (𝐿 − 2) < (𝐿 − 1))
521520adantr 480 . . . . . . . . . . . . . 14 ((𝜑𝑗 ∈ (0...(𝐿 − 2))) → (𝐿 − 2) < (𝐿 − 1))
522509, 510, 511, 518, 521lelttrd 11419 . . . . . . . . . . . . 13 ((𝜑𝑗 ∈ (0...(𝐿 − 2))) → 𝑗 < (𝐿 − 1))
523509, 511ltnled 11408 . . . . . . . . . . . . 13 ((𝜑𝑗 ∈ (0...(𝐿 − 2))) → (𝑗 < (𝐿 − 1) ↔ ¬ (𝐿 − 1) ≤ 𝑗))
524522, 523mpbid 232 . . . . . . . . . . . 12 ((𝜑𝑗 ∈ (0...(𝐿 − 2))) → ¬ (𝐿 − 1) ≤ 𝑗)
525524intnanrd 489 . . . . . . . . . . 11 ((𝜑𝑗 ∈ (0...(𝐿 − 2))) → ¬ ((𝐿 − 1) ≤ 𝑗𝑗𝑁))
526375adantr 480 . . . . . . . . . . . 12 ((𝜑𝑗 ∈ (0...(𝐿 − 2))) → (𝐿 − 1) ∈ ℤ)
527129adantr 480 . . . . . . . . . . . 12 ((𝜑𝑗 ∈ (0...(𝐿 − 2))) → 𝑁 ∈ ℤ)
528 elfz 13553 . . . . . . . . . . . 12 ((𝑗 ∈ ℤ ∧ (𝐿 − 1) ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑗 ∈ ((𝐿 − 1)...𝑁) ↔ ((𝐿 − 1) ≤ 𝑗𝑗𝑁)))
529508, 526, 527, 528syl3anc 1373 . . . . . . . . . . 11 ((𝜑𝑗 ∈ (0...(𝐿 − 2))) → (𝑗 ∈ ((𝐿 − 1)...𝑁) ↔ ((𝐿 − 1) ≤ 𝑗𝑗𝑁)))
530525, 529mtbird 325 . . . . . . . . . 10 ((𝜑𝑗 ∈ (0...(𝐿 − 2))) → ¬ 𝑗 ∈ ((𝐿 − 1)...𝑁))
531530ex 412 . . . . . . . . 9 (𝜑 → (𝑗 ∈ (0...(𝐿 − 2)) → ¬ 𝑗 ∈ ((𝐿 − 1)...𝑁)))
532506, 531ralrimi 3257 . . . . . . . 8 (𝜑 → ∀𝑗 ∈ (0...(𝐿 − 2)) ¬ 𝑗 ∈ ((𝐿 − 1)...𝑁))
533 disj 4450 . . . . . . . 8 (((0...(𝐿 − 2)) ∩ ((𝐿 − 1)...𝑁)) = ∅ ↔ ∀𝑗 ∈ (0...(𝐿 − 2)) ¬ 𝑗 ∈ ((𝐿 − 1)...𝑁))
534532, 533sylibr 234 . . . . . . 7 (𝜑 → ((0...(𝐿 − 2)) ∩ ((𝐿 − 1)...𝑁)) = ∅)
535534adantr 480 . . . . . 6 ((𝜑 ∧ ¬ 𝐿 = 1) → ((0...(𝐿 − 2)) ∩ ((𝐿 − 1)...𝑁)) = ∅)
536144adantr 480 . . . . . . . . 9 ((𝜑 ∧ ¬ 𝐿 = 1) → (𝐿 − 2) ≤ 𝑁)
537128, 374, 1293jca 1129 . . . . . . . . . . 11 (𝜑 → ((𝐿 − 2) ∈ ℤ ∧ 0 ∈ ℤ ∧ 𝑁 ∈ ℤ))
538537adantr 480 . . . . . . . . . 10 ((𝜑 ∧ ¬ 𝐿 = 1) → ((𝐿 − 2) ∈ ℤ ∧ 0 ∈ ℤ ∧ 𝑁 ∈ ℤ))
539 elfz 13553 . . . . . . . . . 10 (((𝐿 − 2) ∈ ℤ ∧ 0 ∈ ℤ ∧ 𝑁 ∈ ℤ) → ((𝐿 − 2) ∈ (0...𝑁) ↔ (0 ≤ (𝐿 − 2) ∧ (𝐿 − 2) ≤ 𝑁)))
540538, 539syl 17 . . . . . . . . 9 ((𝜑 ∧ ¬ 𝐿 = 1) → ((𝐿 − 2) ∈ (0...𝑁) ↔ (0 ≤ (𝐿 − 2) ∧ (𝐿 − 2) ≤ 𝑁)))
541252, 536, 540mpbir2and 713 . . . . . . . 8 ((𝜑 ∧ ¬ 𝐿 = 1) → (𝐿 − 2) ∈ (0...𝑁))
542 fzsplit 13590 . . . . . . . 8 ((𝐿 − 2) ∈ (0...𝑁) → (0...𝑁) = ((0...(𝐿 − 2)) ∪ (((𝐿 − 2) + 1)...𝑁)))
543541, 542syl 17 . . . . . . 7 ((𝜑 ∧ ¬ 𝐿 = 1) → (0...𝑁) = ((0...(𝐿 − 2)) ∪ (((𝐿 − 2) + 1)...𝑁)))
544263, 269, 2703eqtrd 2781 . . . . . . . . . 10 (𝜑 → ((𝐿 − 2) + 1) = (𝐿 − 1))
545544oveq1d 7446 . . . . . . . . 9 (𝜑 → (((𝐿 − 2) + 1)...𝑁) = ((𝐿 − 1)...𝑁))
546545uneq2d 4168 . . . . . . . 8 (𝜑 → ((0...(𝐿 − 2)) ∪ (((𝐿 − 2) + 1)...𝑁)) = ((0...(𝐿 − 2)) ∪ ((𝐿 − 1)...𝑁)))
547546adantr 480 . . . . . . 7 ((𝜑 ∧ ¬ 𝐿 = 1) → ((0...(𝐿 − 2)) ∪ (((𝐿 − 2) + 1)...𝑁)) = ((0...(𝐿 − 2)) ∪ ((𝐿 − 1)...𝑁)))
548543, 547eqtrd 2777 . . . . . 6 ((𝜑 ∧ ¬ 𝐿 = 1) → (0...𝑁) = ((0...(𝐿 − 2)) ∪ ((𝐿 − 1)...𝑁)))
549 fzfid 14014 . . . . . 6 ((𝜑 ∧ ¬ 𝐿 = 1) → (0...𝑁) ∈ Fin)
550176adantr 480 . . . . . . . 8 ((𝜑𝑖 ∈ (0...𝑁)) → 𝐸 ∈ ℂ)
55151recnd 11289 . . . . . . . 8 ((𝜑𝑖 ∈ (0...𝑁)) → ((𝑋𝑖)‘𝑆) ∈ ℂ)
552550, 551mulcld 11281 . . . . . . 7 ((𝜑𝑖 ∈ (0...𝑁)) → (𝐸 · ((𝑋𝑖)‘𝑆)) ∈ ℂ)
553552adantlr 715 . . . . . 6 (((𝜑 ∧ ¬ 𝐿 = 1) ∧ 𝑖 ∈ (0...𝑁)) → (𝐸 · ((𝑋𝑖)‘𝑆)) ∈ ℂ)
554535, 548, 549, 553fsumsplit 15777 . . . . 5 ((𝜑 ∧ ¬ 𝐿 = 1) → Σ𝑖 ∈ (0...𝑁)(𝐸 · ((𝑋𝑖)‘𝑆)) = (Σ𝑖 ∈ (0...(𝐿 − 2))(𝐸 · ((𝑋𝑖)‘𝑆)) + Σ𝑖 ∈ ((𝐿 − 1)...𝑁)(𝐸 · ((𝑋𝑖)‘𝑆))))
555502, 505, 5543brtr4d 5175 . . . 4 ((𝜑 ∧ ¬ 𝐿 = 1) → (𝐸 · Σ𝑖 ∈ (0...(𝐿 − 2))((𝑋𝑖)‘𝑆)) ≤ Σ𝑖 ∈ (0...𝑁)(𝐸 · ((𝑋𝑖)‘𝑆)))
556114, 153, 533jca 1129 . . . . . 6 (𝜑 → (((𝐿 − (4 / 3)) · 𝐸) ∈ ℝ ∧ (𝐸 · Σ𝑖 ∈ (0...(𝐿 − 2))((𝑋𝑖)‘𝑆)) ∈ ℝ ∧ Σ𝑖 ∈ (0...𝑁)(𝐸 · ((𝑋𝑖)‘𝑆)) ∈ ℝ))
557556adantr 480 . . . . 5 ((𝜑 ∧ ¬ 𝐿 = 1) → (((𝐿 − (4 / 3)) · 𝐸) ∈ ℝ ∧ (𝐸 · Σ𝑖 ∈ (0...(𝐿 − 2))((𝑋𝑖)‘𝑆)) ∈ ℝ ∧ Σ𝑖 ∈ (0...𝑁)(𝐸 · ((𝑋𝑖)‘𝑆)) ∈ ℝ))
558 ltletr 11353 . . . . 5 ((((𝐿 − (4 / 3)) · 𝐸) ∈ ℝ ∧ (𝐸 · Σ𝑖 ∈ (0...(𝐿 − 2))((𝑋𝑖)‘𝑆)) ∈ ℝ ∧ Σ𝑖 ∈ (0...𝑁)(𝐸 · ((𝑋𝑖)‘𝑆)) ∈ ℝ) → ((((𝐿 − (4 / 3)) · 𝐸) < (𝐸 · Σ𝑖 ∈ (0...(𝐿 − 2))((𝑋𝑖)‘𝑆)) ∧ (𝐸 · Σ𝑖 ∈ (0...(𝐿 − 2))((𝑋𝑖)‘𝑆)) ≤ Σ𝑖 ∈ (0...𝑁)(𝐸 · ((𝑋𝑖)‘𝑆))) → ((𝐿 − (4 / 3)) · 𝐸) < Σ𝑖 ∈ (0...𝑁)(𝐸 · ((𝑋𝑖)‘𝑆))))
559557, 558syl 17 . . . 4 ((𝜑 ∧ ¬ 𝐿 = 1) → ((((𝐿 − (4 / 3)) · 𝐸) < (𝐸 · Σ𝑖 ∈ (0...(𝐿 − 2))((𝑋𝑖)‘𝑆)) ∧ (𝐸 · Σ𝑖 ∈ (0...(𝐿 − 2))((𝑋𝑖)‘𝑆)) ≤ Σ𝑖 ∈ (0...𝑁)(𝐸 · ((𝑋𝑖)‘𝑆))) → ((𝐿 − (4 / 3)) · 𝐸) < Σ𝑖 ∈ (0...𝑁)(𝐸 · ((𝑋𝑖)‘𝑆))))
560454, 555, 559mp2and 699 . . 3 ((𝜑 ∧ ¬ 𝐿 = 1) → ((𝐿 − (4 / 3)) · 𝐸) < Σ𝑖 ∈ (0...𝑁)(𝐸 · ((𝑋𝑖)‘𝑆)))
561105, 560pm2.61dan 813 . 2 (𝜑 → ((𝐿 − (4 / 3)) · 𝐸) < Σ𝑖 ∈ (0...𝑁)(𝐸 · ((𝑋𝑖)‘𝑆)))
562 sumex 15724 . . 3 Σ𝑖 ∈ (0...𝑁)(𝐸 · ((𝑋𝑖)‘𝑆)) ∈ V
56393oveq2d 7447 . . . . 5 (𝑡 = 𝑆 → (𝐸 · ((𝑋𝑖)‘𝑡)) = (𝐸 · ((𝑋𝑖)‘𝑆)))
564563sumeq2sdv 15739 . . . 4 (𝑡 = 𝑆 → Σ𝑖 ∈ (0...𝑁)(𝐸 · ((𝑋𝑖)‘𝑡)) = Σ𝑖 ∈ (0...𝑁)(𝐸 · ((𝑋𝑖)‘𝑆)))
565 eqid 2737 . . . 4 (𝑡𝑇 ↦ Σ𝑖 ∈ (0...𝑁)(𝐸 · ((𝑋𝑖)‘𝑡))) = (𝑡𝑇 ↦ Σ𝑖 ∈ (0...𝑁)(𝐸 · ((𝑋𝑖)‘𝑡)))
566564, 565fvmptg 7014 . . 3 ((𝑆𝑇 ∧ Σ𝑖 ∈ (0...𝑁)(𝐸 · ((𝑋𝑖)‘𝑆)) ∈ V) → ((𝑡𝑇 ↦ Σ𝑖 ∈ (0...𝑁)(𝐸 · ((𝑋𝑖)‘𝑡)))‘𝑆) = Σ𝑖 ∈ (0...𝑁)(𝐸 · ((𝑋𝑖)‘𝑆)))
56749, 562, 566sylancl 586 . 2 (𝜑 → ((𝑡𝑇 ↦ Σ𝑖 ∈ (0...𝑁)(𝐸 · ((𝑋𝑖)‘𝑡)))‘𝑆) = Σ𝑖 ∈ (0...𝑁)(𝐸 · ((𝑋𝑖)‘𝑆)))
568561, 567breqtrrd 5171 1 (𝜑 → ((𝐿 − (4 / 3)) · 𝐸) < ((𝑡𝑇 ↦ Σ𝑖 ∈ (0...𝑁)(𝐸 · ((𝑋𝑖)‘𝑡)))‘𝑆))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 206  wa 395  wo 848  w3a 1087   = wceq 1540  wnf 1783  wcel 2108  wnfc 2890  wne 2940  wral 3061  {crab 3436  Vcvv 3480  cdif 3948  cun 3949  cin 3950  wss 3951  c0 4333   class class class wbr 5143  cmpt 5225  wf 6557  cfv 6561  (class class class)co 7431  Fincfn 8985  cc 11153  cr 11154  0cc0 11155  1c1 11156   + caddc 11158   · cmul 11160   < clt 11295  cle 11296  cmin 11492  -cneg 11493   / cdiv 11920  cn 12266  2c2 12321  3c3 12322  4c4 12323  0cn0 12526  cz 12613  cuz 12878  +crp 13034  ...cfz 13547  chash 14369  Σcsu 15722
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-10 2141  ax-11 2157  ax-12 2177  ax-ext 2708  ax-rep 5279  ax-sep 5296  ax-nul 5306  ax-pow 5365  ax-pr 5432  ax-un 7755  ax-inf2 9681  ax-cnex 11211  ax-resscn 11212  ax-1cn 11213  ax-icn 11214  ax-addcl 11215  ax-addrcl 11216  ax-mulcl 11217  ax-mulrcl 11218  ax-mulcom 11219  ax-addass 11220  ax-mulass 11221  ax-distr 11222  ax-i2m1 11223  ax-1ne0 11224  ax-1rid 11225  ax-rnegex 11226  ax-rrecex 11227  ax-cnre 11228  ax-pre-lttri 11229  ax-pre-lttrn 11230  ax-pre-ltadd 11231  ax-pre-mulgt0 11232  ax-pre-sup 11233
This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3or 1088  df-3an 1089  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2065  df-mo 2540  df-eu 2569  df-clab 2715  df-cleq 2729  df-clel 2816  df-nfc 2892  df-ne 2941  df-nel 3047  df-ral 3062  df-rex 3071  df-rmo 3380  df-reu 3381  df-rab 3437  df-v 3482  df-sbc 3789  df-csb 3900  df-dif 3954  df-un 3956  df-in 3958  df-ss 3968  df-pss 3971  df-nul 4334  df-if 4526  df-pw 4602  df-sn 4627  df-pr 4629  df-op 4633  df-uni 4908  df-int 4947  df-iun 4993  df-br 5144  df-opab 5206  df-mpt 5226  df-tr 5260  df-id 5578  df-eprel 5584  df-po 5592  df-so 5593  df-fr 5637  df-se 5638  df-we 5639  df-xp 5691  df-rel 5692  df-cnv 5693  df-co 5694  df-dm 5695  df-rn 5696  df-res 5697  df-ima 5698  df-pred 6321  df-ord 6387  df-on 6388  df-lim 6389  df-suc 6390  df-iota 6514  df-fun 6563  df-fn 6564  df-f 6565  df-f1 6566  df-fo 6567  df-f1o 6568  df-fv 6569  df-isom 6570  df-riota 7388  df-ov 7434  df-oprab 7435  df-mpo 7436  df-om 7888  df-1st 8014  df-2nd 8015  df-frecs 8306  df-wrecs 8337  df-recs 8411  df-rdg 8450  df-1o 8506  df-er 8745  df-en 8986  df-dom 8987  df-sdom 8988  df-fin 8989  df-sup 9482  df-oi 9550  df-card 9979  df-pnf 11297  df-mnf 11298  df-xr 11299  df-ltxr 11300  df-le 11301  df-sub 11494  df-neg 11495  df-div 11921  df-nn 12267  df-2 12329  df-3 12330  df-4 12331  df-n0 12527  df-z 12614  df-uz 12879  df-rp 13035  df-ico 13393  df-fz 13548  df-fzo 13695  df-seq 14043  df-exp 14103  df-hash 14370  df-cj 15138  df-re 15139  df-im 15140  df-sqrt 15274  df-abs 15275  df-clim 15524  df-sum 15723
This theorem is referenced by:  stoweidlem34  46049
  Copyright terms: Public domain W3C validator