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 43567
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 10975 . . . . . . . 8 1 ∈ ℝ
2 eleq1 2826 . . . . . . . 8 (𝐿 = 1 → (𝐿 ∈ ℝ ↔ 1 ∈ ℝ))
31, 2mpbiri 257 . . . . . . 7 (𝐿 = 1 → 𝐿 ∈ ℝ)
43adantl 482 . . . . . 6 ((𝜑𝐿 = 1) → 𝐿 ∈ ℝ)
5 4re 12057 . . . . . . . 8 4 ∈ ℝ
65a1i 11 . . . . . . 7 ((𝜑𝐿 = 1) → 4 ∈ ℝ)
7 3re 12053 . . . . . . . 8 3 ∈ ℝ
87a1i 11 . . . . . . 7 ((𝜑𝐿 = 1) → 3 ∈ ℝ)
9 3ne0 12079 . . . . . . . 8 3 ≠ 0
109a1i 11 . . . . . . 7 ((𝜑𝐿 = 1) → 3 ≠ 0)
116, 8, 10redivcld 11803 . . . . . 6 ((𝜑𝐿 = 1) → (4 / 3) ∈ ℝ)
124, 11resubcld 11403 . . . . 5 ((𝜑𝐿 = 1) → (𝐿 − (4 / 3)) ∈ ℝ)
13 stoweidlem26.11 . . . . . . 7 (𝜑𝐸 ∈ ℝ+)
1413rpred 12772 . . . . . 6 (𝜑𝐸 ∈ ℝ)
1514adantr 481 . . . . 5 ((𝜑𝐿 = 1) → 𝐸 ∈ ℝ)
1612, 15remulcld 11005 . . . 4 ((𝜑𝐿 = 1) → ((𝐿 − (4 / 3)) · 𝐸) ∈ ℝ)
17 0red 10978 . . . 4 ((𝜑𝐿 = 1) → 0 ∈ ℝ)
18 fzfid 13693 . . . . . 6 (𝜑 → (0...𝑁) ∈ Fin)
1914adantr 481 . . . . . . 7 ((𝜑𝑖 ∈ (0...𝑁)) → 𝐸 ∈ ℝ)
20 stoweidlem26.13 . . . . . . . 8 ((𝜑𝑖 ∈ (0...𝑁)) → (𝑋𝑖):𝑇⟶ℝ)
21 stoweidlem26.9 . . . . . . . . . . . . . 14 (𝜑𝑆 ∈ ((𝐷𝐿) ∖ (𝐷‘(𝐿 − 1))))
22 eldif 3897 . . . . . . . . . . . . . 14 (𝑆 ∈ ((𝐷𝐿) ∖ (𝐷‘(𝐿 − 1))) ↔ (𝑆 ∈ (𝐷𝐿) ∧ ¬ 𝑆 ∈ (𝐷‘(𝐿 − 1))))
2321, 22sylib 217 . . . . . . . . . . . . 13 (𝜑 → (𝑆 ∈ (𝐷𝐿) ∧ ¬ 𝑆 ∈ (𝐷‘(𝐿 − 1))))
2423simpld 495 . . . . . . . . . . . 12 (𝜑𝑆 ∈ (𝐷𝐿))
25 stoweidlem26.4 . . . . . . . . . . . . 13 𝐷 = (𝑗 ∈ (0...𝑁) ↦ {𝑡𝑇 ∣ (𝐹𝑡) ≤ ((𝑗 − (1 / 3)) · 𝐸)})
26 oveq1 7282 . . . . . . . . . . . . . . . 16 (𝑗 = 𝐿 → (𝑗 − (1 / 3)) = (𝐿 − (1 / 3)))
2726oveq1d 7290 . . . . . . . . . . . . . . 15 (𝑗 = 𝐿 → ((𝑗 − (1 / 3)) · 𝐸) = ((𝐿 − (1 / 3)) · 𝐸))
2827breq2d 5086 . . . . . . . . . . . . . 14 (𝑗 = 𝐿 → ((𝐹𝑡) ≤ ((𝑗 − (1 / 3)) · 𝐸) ↔ (𝐹𝑡) ≤ ((𝐿 − (1 / 3)) · 𝐸)))
2928rabbidv 3414 . . . . . . . . . . . . 13 (𝑗 = 𝐿 → {𝑡𝑇 ∣ (𝐹𝑡) ≤ ((𝑗 − (1 / 3)) · 𝐸)} = {𝑡𝑇 ∣ (𝐹𝑡) ≤ ((𝐿 − (1 / 3)) · 𝐸)})
30 fz1ssfz0 13352 . . . . . . . . . . . . . 14 (1...𝑁) ⊆ (0...𝑁)
31 stoweidlem26.8 . . . . . . . . . . . . . 14 (𝜑𝐿 ∈ (1...𝑁))
3230, 31sselid 3919 . . . . . . . . . . . . 13 (𝜑𝐿 ∈ (0...𝑁))
33 stoweidlem26.7 . . . . . . . . . . . . . 14 (𝜑𝑇 ∈ V)
34 rabexg 5255 . . . . . . . . . . . . . 14 (𝑇 ∈ V → {𝑡𝑇 ∣ (𝐹𝑡) ≤ ((𝐿 − (1 / 3)) · 𝐸)} ∈ V)
3533, 34syl 17 . . . . . . . . . . . . 13 (𝜑 → {𝑡𝑇 ∣ (𝐹𝑡) ≤ ((𝐿 − (1 / 3)) · 𝐸)} ∈ V)
3625, 29, 32, 35fvmptd3 6898 . . . . . . . . . . . 12 (𝜑 → (𝐷𝐿) = {𝑡𝑇 ∣ (𝐹𝑡) ≤ ((𝐿 − (1 / 3)) · 𝐸)})
3724, 36eleqtrd 2841 . . . . . . . . . . 11 (𝜑𝑆 ∈ {𝑡𝑇 ∣ (𝐹𝑡) ≤ ((𝐿 − (1 / 3)) · 𝐸)})
38 nfcv 2907 . . . . . . . . . . . 12 𝑡𝑆
39 nfcv 2907 . . . . . . . . . . . 12 𝑡𝑇
40 stoweidlem26.1 . . . . . . . . . . . . . 14 𝑡𝐹
4140, 38nffv 6784 . . . . . . . . . . . . 13 𝑡(𝐹𝑆)
42 nfcv 2907 . . . . . . . . . . . . 13 𝑡
43 nfcv 2907 . . . . . . . . . . . . 13 𝑡((𝐿 − (1 / 3)) · 𝐸)
4441, 42, 43nfbr 5121 . . . . . . . . . . . 12 𝑡(𝐹𝑆) ≤ ((𝐿 − (1 / 3)) · 𝐸)
45 fveq2 6774 . . . . . . . . . . . . 13 (𝑡 = 𝑆 → (𝐹𝑡) = (𝐹𝑆))
4645breq1d 5084 . . . . . . . . . . . 12 (𝑡 = 𝑆 → ((𝐹𝑡) ≤ ((𝐿 − (1 / 3)) · 𝐸) ↔ (𝐹𝑆) ≤ ((𝐿 − (1 / 3)) · 𝐸)))
4738, 39, 44, 46elrabf 3620 . . . . . . . . . . 11 (𝑆 ∈ {𝑡𝑇 ∣ (𝐹𝑡) ≤ ((𝐿 − (1 / 3)) · 𝐸)} ↔ (𝑆𝑇 ∧ (𝐹𝑆) ≤ ((𝐿 − (1 / 3)) · 𝐸)))
4837, 47sylib 217 . . . . . . . . . 10 (𝜑 → (𝑆𝑇 ∧ (𝐹𝑆) ≤ ((𝐿 − (1 / 3)) · 𝐸)))
4948simpld 495 . . . . . . . . 9 (𝜑𝑆𝑇)
5049adantr 481 . . . . . . . 8 ((𝜑𝑖 ∈ (0...𝑁)) → 𝑆𝑇)
5120, 50ffvelrnd 6962 . . . . . . 7 ((𝜑𝑖 ∈ (0...𝑁)) → ((𝑋𝑖)‘𝑆) ∈ ℝ)
5219, 51remulcld 11005 . . . . . 6 ((𝜑𝑖 ∈ (0...𝑁)) → (𝐸 · ((𝑋𝑖)‘𝑆)) ∈ ℝ)
5318, 52fsumrecl 15446 . . . . 5 (𝜑 → Σ𝑖 ∈ (0...𝑁)(𝐸 · ((𝑋𝑖)‘𝑆)) ∈ ℝ)
5453adantr 481 . . . 4 ((𝜑𝐿 = 1) → Σ𝑖 ∈ (0...𝑁)(𝐸 · ((𝑋𝑖)‘𝑆)) ∈ ℝ)
555, 7, 9redivcli 11742 . . . . . . 7 (4 / 3) ∈ ℝ
5655a1i 11 . . . . . 6 ((𝜑𝐿 = 1) → (4 / 3) ∈ ℝ)
574, 56resubcld 11403 . . . . 5 ((𝜑𝐿 = 1) → (𝐿 − (4 / 3)) ∈ ℝ)
584recnd 11003 . . . . . . . 8 ((𝜑𝐿 = 1) → 𝐿 ∈ ℂ)
5958subid1d 11321 . . . . . . 7 ((𝜑𝐿 = 1) → (𝐿 − 0) = 𝐿)
60 3cn 12054 . . . . . . . . . 10 3 ∈ ℂ
6160, 9dividi 11708 . . . . . . . . 9 (3 / 3) = 1
62 3lt4 12147 . . . . . . . . . 10 3 < 4
63 3pos 12078 . . . . . . . . . . 11 0 < 3
647, 5, 7, 63ltdiv1ii 11904 . . . . . . . . . 10 (3 < 4 ↔ (3 / 3) < (4 / 3))
6562, 64mpbi 229 . . . . . . . . 9 (3 / 3) < (4 / 3)
6661, 65eqbrtrri 5097 . . . . . . . 8 1 < (4 / 3)
67 breq1 5077 . . . . . . . . 9 (𝐿 = 1 → (𝐿 < (4 / 3) ↔ 1 < (4 / 3)))
6867adantl 482 . . . . . . . 8 ((𝜑𝐿 = 1) → (𝐿 < (4 / 3) ↔ 1 < (4 / 3)))
6966, 68mpbiri 257 . . . . . . 7 ((𝜑𝐿 = 1) → 𝐿 < (4 / 3))
7059, 69eqbrtrd 5096 . . . . . 6 ((𝜑𝐿 = 1) → (𝐿 − 0) < (4 / 3))
714, 17, 56, 70ltsub23d 11580 . . . . 5 ((𝜑𝐿 = 1) → (𝐿 − (4 / 3)) < 0)
7213rpgt0d 12775 . . . . . 6 (𝜑 → 0 < 𝐸)
7372adantr 481 . . . . 5 ((𝜑𝐿 = 1) → 0 < 𝐸)
74 mulltgt0 42565 . . . . 5 ((((𝐿 − (4 / 3)) ∈ ℝ ∧ (𝐿 − (4 / 3)) < 0) ∧ (𝐸 ∈ ℝ ∧ 0 < 𝐸)) → ((𝐿 − (4 / 3)) · 𝐸) < 0)
7557, 71, 15, 73, 74syl22anc 836 . . . 4 ((𝜑𝐿 = 1) → ((𝐿 − (4 / 3)) · 𝐸) < 0)
76 0cn 10967 . . . . . . . 8 0 ∈ ℂ
77 fsumconst 15502 . . . . . . . 8 (((0...𝑁) ∈ Fin ∧ 0 ∈ ℂ) → Σ𝑖 ∈ (0...𝑁)0 = ((♯‘(0...𝑁)) · 0))
7818, 76, 77sylancl 586 . . . . . . 7 (𝜑 → Σ𝑖 ∈ (0...𝑁)0 = ((♯‘(0...𝑁)) · 0))
79 hashcl 14071 . . . . . . . . 9 ((0...𝑁) ∈ Fin → (♯‘(0...𝑁)) ∈ ℕ0)
80 nn0cn 12243 . . . . . . . . 9 ((♯‘(0...𝑁)) ∈ ℕ0 → (♯‘(0...𝑁)) ∈ ℂ)
8118, 79, 803syl 18 . . . . . . . 8 (𝜑 → (♯‘(0...𝑁)) ∈ ℂ)
8281mul01d 11174 . . . . . . 7 (𝜑 → ((♯‘(0...𝑁)) · 0) = 0)
8378, 82eqtrd 2778 . . . . . 6 (𝜑 → Σ𝑖 ∈ (0...𝑁)0 = 0)
8483adantr 481 . . . . 5 ((𝜑𝐿 = 1) → Σ𝑖 ∈ (0...𝑁)0 = 0)
85 0red 10978 . . . . . . 7 ((𝜑𝑖 ∈ (0...𝑁)) → 0 ∈ ℝ)
8613rpge0d 12776 . . . . . . . . 9 (𝜑 → 0 ≤ 𝐸)
8786adantr 481 . . . . . . . 8 ((𝜑𝑖 ∈ (0...𝑁)) → 0 ≤ 𝐸)
88 stoweidlem26.3 . . . . . . . . . . . 12 𝑡𝜑
89 nfv 1917 . . . . . . . . . . . 12 𝑡 𝑖 ∈ (0...𝑁)
9088, 89nfan 1902 . . . . . . . . . . 11 𝑡(𝜑𝑖 ∈ (0...𝑁))
91 nfv 1917 . . . . . . . . . . 11 𝑡0 ≤ ((𝑋𝑖)‘𝑆)
9290, 91nfim 1899 . . . . . . . . . 10 𝑡((𝜑𝑖 ∈ (0...𝑁)) → 0 ≤ ((𝑋𝑖)‘𝑆))
93 fveq2 6774 . . . . . . . . . . . 12 (𝑡 = 𝑆 → ((𝑋𝑖)‘𝑡) = ((𝑋𝑖)‘𝑆))
9493breq2d 5086 . . . . . . . . . . 11 (𝑡 = 𝑆 → (0 ≤ ((𝑋𝑖)‘𝑡) ↔ 0 ≤ ((𝑋𝑖)‘𝑆)))
9594imbi2d 341 . . . . . . . . . 10 (𝑡 = 𝑆 → (((𝜑𝑖 ∈ (0...𝑁)) → 0 ≤ ((𝑋𝑖)‘𝑡)) ↔ ((𝜑𝑖 ∈ (0...𝑁)) → 0 ≤ ((𝑋𝑖)‘𝑆))))
96 stoweidlem26.14 . . . . . . . . . . . 12 ((𝜑𝑖 ∈ (0...𝑁) ∧ 𝑡𝑇) → 0 ≤ ((𝑋𝑖)‘𝑡))
97963expia 1120 . . . . . . . . . . 11 ((𝜑𝑖 ∈ (0...𝑁)) → (𝑡𝑇 → 0 ≤ ((𝑋𝑖)‘𝑡)))
9897com12 32 . . . . . . . . . 10 (𝑡𝑇 → ((𝜑𝑖 ∈ (0...𝑁)) → 0 ≤ ((𝑋𝑖)‘𝑡)))
9938, 92, 95, 98vtoclgaf 3512 . . . . . . . . 9 (𝑆𝑇 → ((𝜑𝑖 ∈ (0...𝑁)) → 0 ≤ ((𝑋𝑖)‘𝑆)))
10050, 99mpcom 38 . . . . . . . 8 ((𝜑𝑖 ∈ (0...𝑁)) → 0 ≤ ((𝑋𝑖)‘𝑆))
10119, 51, 87, 100mulge0d 11552 . . . . . . 7 ((𝜑𝑖 ∈ (0...𝑁)) → 0 ≤ (𝐸 · ((𝑋𝑖)‘𝑆)))
10218, 85, 52, 101fsumle 15511 . . . . . 6 (𝜑 → Σ𝑖 ∈ (0...𝑁)0 ≤ Σ𝑖 ∈ (0...𝑁)(𝐸 · ((𝑋𝑖)‘𝑆)))
103102adantr 481 . . . . 5 ((𝜑𝐿 = 1) → Σ𝑖 ∈ (0...𝑁)0 ≤ Σ𝑖 ∈ (0...𝑁)(𝐸 · ((𝑋𝑖)‘𝑆)))
10484, 103eqbrtrrd 5098 . . . 4 ((𝜑𝐿 = 1) → 0 ≤ Σ𝑖 ∈ (0...𝑁)(𝐸 · ((𝑋𝑖)‘𝑆)))
10516, 17, 54, 75, 104ltletrd 11135 . . 3 ((𝜑𝐿 = 1) → ((𝐿 − (4 / 3)) · 𝐸) < Σ𝑖 ∈ (0...𝑁)(𝐸 · ((𝑋𝑖)‘𝑆)))
106 elfzelz 13256 . . . . . . . . 9 (𝐿 ∈ (1...𝑁) → 𝐿 ∈ ℤ)
107 zre 12323 . . . . . . . . 9 (𝐿 ∈ ℤ → 𝐿 ∈ ℝ)
10831, 106, 1073syl 18 . . . . . . . 8 (𝜑𝐿 ∈ ℝ)
1095a1i 11 . . . . . . . . 9 (𝜑 → 4 ∈ ℝ)
1107a1i 11 . . . . . . . . 9 (𝜑 → 3 ∈ ℝ)
1119a1i 11 . . . . . . . . 9 (𝜑 → 3 ≠ 0)
112109, 110, 111redivcld 11803 . . . . . . . 8 (𝜑 → (4 / 3) ∈ ℝ)
113108, 112resubcld 11403 . . . . . . 7 (𝜑 → (𝐿 − (4 / 3)) ∈ ℝ)
114113, 14remulcld 11005 . . . . . 6 (𝜑 → ((𝐿 − (4 / 3)) · 𝐸) ∈ ℝ)
115114adantr 481 . . . . 5 ((𝜑 ∧ ¬ 𝐿 = 1) → ((𝐿 − (4 / 3)) · 𝐸) ∈ ℝ)
1161a1i 11 . . . . . . . . 9 (𝜑 → 1 ∈ ℝ)
117 stoweidlem26.6 . . . . . . . . . 10 (𝜑𝑁 ∈ ℕ)
11814, 117nndivred 12027 . . . . . . . . 9 (𝜑 → (𝐸 / 𝑁) ∈ ℝ)
119116, 118resubcld 11403 . . . . . . . 8 (𝜑 → (1 − (𝐸 / 𝑁)) ∈ ℝ)
120108, 116resubcld 11403 . . . . . . . 8 (𝜑 → (𝐿 − 1) ∈ ℝ)
121119, 120remulcld 11005 . . . . . . 7 (𝜑 → ((1 − (𝐸 / 𝑁)) · (𝐿 − 1)) ∈ ℝ)
12214, 121remulcld 11005 . . . . . 6 (𝜑 → (𝐸 · ((1 − (𝐸 / 𝑁)) · (𝐿 − 1))) ∈ ℝ)
123122adantr 481 . . . . 5 ((𝜑 ∧ ¬ 𝐿 = 1) → (𝐸 · ((1 − (𝐸 / 𝑁)) · (𝐿 − 1))) ∈ ℝ)
124 fzfid 13693 . . . . . . . 8 (𝜑 → (0...(𝐿 − 2)) ∈ Fin)
12531elfzelzd 13257 . . . . . . . . . . . . . 14 (𝜑𝐿 ∈ ℤ)
126 2z 12352 . . . . . . . . . . . . . . 15 2 ∈ ℤ
127126a1i 11 . . . . . . . . . . . . . 14 (𝜑 → 2 ∈ ℤ)
128125, 127zsubcld 12431 . . . . . . . . . . . . 13 (𝜑 → (𝐿 − 2) ∈ ℤ)
129117nnzd 12425 . . . . . . . . . . . . 13 (𝜑𝑁 ∈ ℤ)
130125zred 12426 . . . . . . . . . . . . . . 15 (𝜑𝐿 ∈ ℝ)
131 2re 12047 . . . . . . . . . . . . . . . 16 2 ∈ ℝ
132131a1i 11 . . . . . . . . . . . . . . 15 (𝜑 → 2 ∈ ℝ)
133130, 132resubcld 11403 . . . . . . . . . . . . . 14 (𝜑 → (𝐿 − 2) ∈ ℝ)
134117nnred 11988 . . . . . . . . . . . . . 14 (𝜑𝑁 ∈ ℝ)
135 0le2 12075 . . . . . . . . . . . . . . . 16 0 ≤ 2
136 0red 10978 . . . . . . . . . . . . . . . . 17 (𝜑 → 0 ∈ ℝ)
137136, 132, 130lesub2d 11583 . . . . . . . . . . . . . . . 16 (𝜑 → (0 ≤ 2 ↔ (𝐿 − 2) ≤ (𝐿 − 0)))
138135, 137mpbii 232 . . . . . . . . . . . . . . 15 (𝜑 → (𝐿 − 2) ≤ (𝐿 − 0))
139125zcnd 12427 . . . . . . . . . . . . . . . 16 (𝜑𝐿 ∈ ℂ)
140139subid1d 11321 . . . . . . . . . . . . . . 15 (𝜑 → (𝐿 − 0) = 𝐿)
141138, 140breqtrd 5100 . . . . . . . . . . . . . 14 (𝜑 → (𝐿 − 2) ≤ 𝐿)
142 elfzle2 13260 . . . . . . . . . . . . . . 15 (𝐿 ∈ (1...𝑁) → 𝐿𝑁)
14331, 142syl 17 . . . . . . . . . . . . . 14 (𝜑𝐿𝑁)
144133, 130, 134, 141, 143letrd 11132 . . . . . . . . . . . . 13 (𝜑 → (𝐿 − 2) ≤ 𝑁)
145128, 129, 1443jca 1127 . . . . . . . . . . . 12 (𝜑 → ((𝐿 − 2) ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ (𝐿 − 2) ≤ 𝑁))
146 eluz2 12588 . . . . . . . . . . . 12 (𝑁 ∈ (ℤ‘(𝐿 − 2)) ↔ ((𝐿 − 2) ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ (𝐿 − 2) ≤ 𝑁))
147145, 146sylibr 233 . . . . . . . . . . 11 (𝜑𝑁 ∈ (ℤ‘(𝐿 − 2)))
148 fzss2 13296 . . . . . . . . . . 11 (𝑁 ∈ (ℤ‘(𝐿 − 2)) → (0...(𝐿 − 2)) ⊆ (0...𝑁))
149147, 148syl 17 . . . . . . . . . 10 (𝜑 → (0...(𝐿 − 2)) ⊆ (0...𝑁))
150149sselda 3921 . . . . . . . . 9 ((𝜑𝑖 ∈ (0...(𝐿 − 2))) → 𝑖 ∈ (0...𝑁))
151150, 51syldan 591 . . . . . . . 8 ((𝜑𝑖 ∈ (0...(𝐿 − 2))) → ((𝑋𝑖)‘𝑆) ∈ ℝ)
152124, 151fsumrecl 15446 . . . . . . 7 (𝜑 → Σ𝑖 ∈ (0...(𝐿 − 2))((𝑋𝑖)‘𝑆) ∈ ℝ)
15314, 152remulcld 11005 . . . . . 6 (𝜑 → (𝐸 · Σ𝑖 ∈ (0...(𝐿 − 2))((𝑋𝑖)‘𝑆)) ∈ ℝ)
154153adantr 481 . . . . 5 ((𝜑 ∧ ¬ 𝐿 = 1) → (𝐸 · Σ𝑖 ∈ (0...(𝐿 − 2))((𝑋𝑖)‘𝑆)) ∈ ℝ)
15514, 120remulcld 11005 . . . . . . . . 9 (𝜑 → (𝐸 · (𝐿 − 1)) ∈ ℝ)
15614, 14remulcld 11005 . . . . . . . . 9 (𝜑 → (𝐸 · 𝐸) ∈ ℝ)
157155, 156resubcld 11403 . . . . . . . 8 (𝜑 → ((𝐸 · (𝐿 − 1)) − (𝐸 · 𝐸)) ∈ ℝ)
158120, 117nndivred 12027 . . . . . . . . . 10 (𝜑 → ((𝐿 − 1) / 𝑁) ∈ ℝ)
159156, 158remulcld 11005 . . . . . . . . 9 (𝜑 → ((𝐸 · 𝐸) · ((𝐿 − 1) / 𝑁)) ∈ ℝ)
160155, 159resubcld 11403 . . . . . . . 8 (𝜑 → ((𝐸 · (𝐿 − 1)) − ((𝐸 · 𝐸) · ((𝐿 − 1) / 𝑁))) ∈ ℝ)
161120, 14resubcld 11403 . . . . . . . . . 10 (𝜑 → ((𝐿 − 1) − 𝐸) ∈ ℝ)
162116, 14readdcld 11004 . . . . . . . . . . . 12 (𝜑 → (1 + 𝐸) ∈ ℝ)
1631, 7, 9redivcli 11742 . . . . . . . . . . . . . . 15 (1 / 3) ∈ ℝ
164163a1i 11 . . . . . . . . . . . . . 14 (𝜑 → (1 / 3) ∈ ℝ)
165 stoweidlem26.12 . . . . . . . . . . . . . 14 (𝜑𝐸 < (1 / 3))
16614, 164, 116, 165ltadd2dd 11134 . . . . . . . . . . . . 13 (𝜑 → (1 + 𝐸) < (1 + (1 / 3)))
167 ax-1cn 10929 . . . . . . . . . . . . . . 15 1 ∈ ℂ
16860, 167, 60, 9divdiri 11732 . . . . . . . . . . . . . 14 ((3 + 1) / 3) = ((3 / 3) + (1 / 3))
169 3p1e4 12118 . . . . . . . . . . . . . . 15 (3 + 1) = 4
170169oveq1i 7285 . . . . . . . . . . . . . 14 ((3 + 1) / 3) = (4 / 3)
17161oveq1i 7285 . . . . . . . . . . . . . 14 ((3 / 3) + (1 / 3)) = (1 + (1 / 3))
172168, 170, 1713eqtr3ri 2775 . . . . . . . . . . . . 13 (1 + (1 / 3)) = (4 / 3)
173166, 172breqtrdi 5115 . . . . . . . . . . . 12 (𝜑 → (1 + 𝐸) < (4 / 3))
174162, 112, 108, 173ltsub2dd 11588 . . . . . . . . . . 11 (𝜑 → (𝐿 − (4 / 3)) < (𝐿 − (1 + 𝐸)))
175167a1i 11 . . . . . . . . . . . 12 (𝜑 → 1 ∈ ℂ)
17613rpcnd 12774 . . . . . . . . . . . 12 (𝜑𝐸 ∈ ℂ)
177139, 175, 176subsub4d 11363 . . . . . . . . . . 11 (𝜑 → ((𝐿 − 1) − 𝐸) = (𝐿 − (1 + 𝐸)))
178174, 177breqtrrd 5102 . . . . . . . . . 10 (𝜑 → (𝐿 − (4 / 3)) < ((𝐿 − 1) − 𝐸))
179113, 161, 13, 178ltmul1dd 12827 . . . . . . . . 9 (𝜑 → ((𝐿 − (4 / 3)) · 𝐸) < (((𝐿 − 1) − 𝐸) · 𝐸))
180139, 175subcld 11332 . . . . . . . . . . . 12 (𝜑 → (𝐿 − 1) ∈ ℂ)
181180, 176subcld 11332 . . . . . . . . . . 11 (𝜑 → ((𝐿 − 1) − 𝐸) ∈ ℂ)
182176, 181mulcomd 10996 . . . . . . . . . 10 (𝜑 → (𝐸 · ((𝐿 − 1) − 𝐸)) = (((𝐿 − 1) − 𝐸) · 𝐸))
183176, 180, 176subdid 11431 . . . . . . . . . 10 (𝜑 → (𝐸 · ((𝐿 − 1) − 𝐸)) = ((𝐸 · (𝐿 − 1)) − (𝐸 · 𝐸)))
184182, 183eqtr3d 2780 . . . . . . . . 9 (𝜑 → (((𝐿 − 1) − 𝐸) · 𝐸) = ((𝐸 · (𝐿 − 1)) − (𝐸 · 𝐸)))
185179, 184breqtrd 5100 . . . . . . . 8 (𝜑 → ((𝐿 − (4 / 3)) · 𝐸) < ((𝐸 · (𝐿 − 1)) − (𝐸 · 𝐸)))
186 1zzd 12351 . . . . . . . . . . . . . . . . 17 (𝜑 → 1 ∈ ℤ)
187 elfz 13245 . . . . . . . . . . . . . . . . 17 ((𝐿 ∈ ℤ ∧ 1 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝐿 ∈ (1...𝑁) ↔ (1 ≤ 𝐿𝐿𝑁)))
188125, 186, 129, 187syl3anc 1370 . . . . . . . . . . . . . . . 16 (𝜑 → (𝐿 ∈ (1...𝑁) ↔ (1 ≤ 𝐿𝐿𝑁)))
18931, 188mpbid 231 . . . . . . . . . . . . . . 15 (𝜑 → (1 ≤ 𝐿𝐿𝑁))
190189simprd 496 . . . . . . . . . . . . . 14 (𝜑𝐿𝑁)
191 zlem1lt 12372 . . . . . . . . . . . . . . 15 ((𝐿 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝐿𝑁 ↔ (𝐿 − 1) < 𝑁))
192125, 129, 191syl2anc 584 . . . . . . . . . . . . . 14 (𝜑 → (𝐿𝑁 ↔ (𝐿 − 1) < 𝑁))
193190, 192mpbid 231 . . . . . . . . . . . . 13 (𝜑 → (𝐿 − 1) < 𝑁)
194117nngt0d 12022 . . . . . . . . . . . . . 14 (𝜑 → 0 < 𝑁)
195 ltdiv1 11839 . . . . . . . . . . . . . 14 (((𝐿 − 1) ∈ ℝ ∧ 𝑁 ∈ ℝ ∧ (𝑁 ∈ ℝ ∧ 0 < 𝑁)) → ((𝐿 − 1) < 𝑁 ↔ ((𝐿 − 1) / 𝑁) < (𝑁 / 𝑁)))
196120, 134, 134, 194, 195syl112anc 1373 . . . . . . . . . . . . 13 (𝜑 → ((𝐿 − 1) < 𝑁 ↔ ((𝐿 − 1) / 𝑁) < (𝑁 / 𝑁)))
197193, 196mpbid 231 . . . . . . . . . . . 12 (𝜑 → ((𝐿 − 1) / 𝑁) < (𝑁 / 𝑁))
198117nncnd 11989 . . . . . . . . . . . . 13 (𝜑𝑁 ∈ ℂ)
199117nnne0d 12023 . . . . . . . . . . . . 13 (𝜑𝑁 ≠ 0)
200198, 199dividd 11749 . . . . . . . . . . . 12 (𝜑 → (𝑁 / 𝑁) = 1)
201197, 200breqtrd 5100 . . . . . . . . . . 11 (𝜑 → ((𝐿 − 1) / 𝑁) < 1)
20214, 14, 72, 72mulgt0d 11130 . . . . . . . . . . . 12 (𝜑 → 0 < (𝐸 · 𝐸))
203 ltmul2 11826 . . . . . . . . . . . 12 ((((𝐿 − 1) / 𝑁) ∈ ℝ ∧ 1 ∈ ℝ ∧ ((𝐸 · 𝐸) ∈ ℝ ∧ 0 < (𝐸 · 𝐸))) → (((𝐿 − 1) / 𝑁) < 1 ↔ ((𝐸 · 𝐸) · ((𝐿 − 1) / 𝑁)) < ((𝐸 · 𝐸) · 1)))
204158, 116, 156, 202, 203syl112anc 1373 . . . . . . . . . . 11 (𝜑 → (((𝐿 − 1) / 𝑁) < 1 ↔ ((𝐸 · 𝐸) · ((𝐿 − 1) / 𝑁)) < ((𝐸 · 𝐸) · 1)))
205201, 204mpbid 231 . . . . . . . . . 10 (𝜑 → ((𝐸 · 𝐸) · ((𝐿 − 1) / 𝑁)) < ((𝐸 · 𝐸) · 1))
206176, 176mulcld 10995 . . . . . . . . . . 11 (𝜑 → (𝐸 · 𝐸) ∈ ℂ)
207206mulid1d 10992 . . . . . . . . . 10 (𝜑 → ((𝐸 · 𝐸) · 1) = (𝐸 · 𝐸))
208205, 207breqtrd 5100 . . . . . . . . 9 (𝜑 → ((𝐸 · 𝐸) · ((𝐿 − 1) / 𝑁)) < (𝐸 · 𝐸))
209159, 156, 155, 208ltsub2dd 11588 . . . . . . . 8 (𝜑 → ((𝐸 · (𝐿 − 1)) − (𝐸 · 𝐸)) < ((𝐸 · (𝐿 − 1)) − ((𝐸 · 𝐸) · ((𝐿 − 1) / 𝑁))))
210114, 157, 160, 185, 209lttrd 11136 . . . . . . 7 (𝜑 → ((𝐿 − (4 / 3)) · 𝐸) < ((𝐸 · (𝐿 − 1)) − ((𝐸 · 𝐸) · ((𝐿 − 1) / 𝑁))))
211176, 198, 199divcld 11751 . . . . . . . . . . 11 (𝜑 → (𝐸 / 𝑁) ∈ ℂ)
212175, 211, 180subdird 11432 . . . . . . . . . 10 (𝜑 → ((1 − (𝐸 / 𝑁)) · (𝐿 − 1)) = ((1 · (𝐿 − 1)) − ((𝐸 / 𝑁) · (𝐿 − 1))))
213180mulid2d 10993 . . . . . . . . . . 11 (𝜑 → (1 · (𝐿 − 1)) = (𝐿 − 1))
214213oveq1d 7290 . . . . . . . . . 10 (𝜑 → ((1 · (𝐿 − 1)) − ((𝐸 / 𝑁) · (𝐿 − 1))) = ((𝐿 − 1) − ((𝐸 / 𝑁) · (𝐿 − 1))))
215212, 214eqtrd 2778 . . . . . . . . 9 (𝜑 → ((1 − (𝐸 / 𝑁)) · (𝐿 − 1)) = ((𝐿 − 1) − ((𝐸 / 𝑁) · (𝐿 − 1))))
216215oveq2d 7291 . . . . . . . 8 (𝜑 → (𝐸 · ((1 − (𝐸 / 𝑁)) · (𝐿 − 1))) = (𝐸 · ((𝐿 − 1) − ((𝐸 / 𝑁) · (𝐿 − 1)))))
217211, 180mulcld 10995 . . . . . . . . 9 (𝜑 → ((𝐸 / 𝑁) · (𝐿 − 1)) ∈ ℂ)
218176, 180, 217subdid 11431 . . . . . . . 8 (𝜑 → (𝐸 · ((𝐿 − 1) − ((𝐸 / 𝑁) · (𝐿 − 1)))) = ((𝐸 · (𝐿 − 1)) − (𝐸 · ((𝐸 / 𝑁) · (𝐿 − 1)))))
219176, 198, 180, 199div32d 11774 . . . . . . . . . . 11 (𝜑 → ((𝐸 / 𝑁) · (𝐿 − 1)) = (𝐸 · ((𝐿 − 1) / 𝑁)))
220219oveq2d 7291 . . . . . . . . . 10 (𝜑 → (𝐸 · ((𝐸 / 𝑁) · (𝐿 − 1))) = (𝐸 · (𝐸 · ((𝐿 − 1) / 𝑁))))
221180, 198, 199divcld 11751 . . . . . . . . . . 11 (𝜑 → ((𝐿 − 1) / 𝑁) ∈ ℂ)
222176, 176, 221mulassd 10998 . . . . . . . . . 10 (𝜑 → ((𝐸 · 𝐸) · ((𝐿 − 1) / 𝑁)) = (𝐸 · (𝐸 · ((𝐿 − 1) / 𝑁))))
223220, 222eqtr4d 2781 . . . . . . . . 9 (𝜑 → (𝐸 · ((𝐸 / 𝑁) · (𝐿 − 1))) = ((𝐸 · 𝐸) · ((𝐿 − 1) / 𝑁)))
224223oveq2d 7291 . . . . . . . 8 (𝜑 → ((𝐸 · (𝐿 − 1)) − (𝐸 · ((𝐸 / 𝑁) · (𝐿 − 1)))) = ((𝐸 · (𝐿 − 1)) − ((𝐸 · 𝐸) · ((𝐿 − 1) / 𝑁))))
225216, 218, 2243eqtrd 2782 . . . . . . 7 (𝜑 → (𝐸 · ((1 − (𝐸 / 𝑁)) · (𝐿 − 1))) = ((𝐸 · (𝐿 − 1)) − ((𝐸 · 𝐸) · ((𝐿 − 1) / 𝑁))))
226210, 225breqtrrd 5102 . . . . . 6 (𝜑 → ((𝐿 − (4 / 3)) · 𝐸) < (𝐸 · ((1 − (𝐸 / 𝑁)) · (𝐿 − 1))))
227226adantr 481 . . . . 5 ((𝜑 ∧ ¬ 𝐿 = 1) → ((𝐿 − (4 / 3)) · 𝐸) < (𝐸 · ((1 − (𝐸 / 𝑁)) · (𝐿 − 1))))
228175, 211subcld 11332 . . . . . . . . . 10 (𝜑 → (1 − (𝐸 / 𝑁)) ∈ ℂ)
229 fsumconst 15502 . . . . . . . . . 10 (((0...(𝐿 − 2)) ∈ Fin ∧ (1 − (𝐸 / 𝑁)) ∈ ℂ) → Σ𝑖 ∈ (0...(𝐿 − 2))(1 − (𝐸 / 𝑁)) = ((♯‘(0...(𝐿 − 2))) · (1 − (𝐸 / 𝑁))))
230124, 228, 229syl2anc 584 . . . . . . . . 9 (𝜑 → Σ𝑖 ∈ (0...(𝐿 − 2))(1 − (𝐸 / 𝑁)) = ((♯‘(0...(𝐿 − 2))) · (1 − (𝐸 / 𝑁))))
231230adantr 481 . . . . . . . 8 ((𝜑 ∧ ¬ 𝐿 = 1) → Σ𝑖 ∈ (0...(𝐿 − 2))(1 − (𝐸 / 𝑁)) = ((♯‘(0...(𝐿 − 2))) · (1 − (𝐸 / 𝑁))))
232 0zd 12331 . . . . . . . . . . . . 13 ((𝜑 ∧ ¬ 𝐿 = 1) → 0 ∈ ℤ)
23331adantr 481 . . . . . . . . . . . . . . 15 ((𝜑 ∧ ¬ 𝐿 = 1) → 𝐿 ∈ (1...𝑁))
234233elfzelzd 13257 . . . . . . . . . . . . . 14 ((𝜑 ∧ ¬ 𝐿 = 1) → 𝐿 ∈ ℤ)
235126a1i 11 . . . . . . . . . . . . . 14 ((𝜑 ∧ ¬ 𝐿 = 1) → 2 ∈ ℤ)
236234, 235zsubcld 12431 . . . . . . . . . . . . 13 ((𝜑 ∧ ¬ 𝐿 = 1) → (𝐿 − 2) ∈ ℤ)
237 elnnuz 12622 . . . . . . . . . . . . . . . . . . . 20 (𝑁 ∈ ℕ ↔ 𝑁 ∈ (ℤ‘1))
238117, 237sylib 217 . . . . . . . . . . . . . . . . . . 19 (𝜑𝑁 ∈ (ℤ‘1))
239 elfzp12 13335 . . . . . . . . . . . . . . . . . . 19 (𝑁 ∈ (ℤ‘1) → (𝐿 ∈ (1...𝑁) ↔ (𝐿 = 1 ∨ 𝐿 ∈ ((1 + 1)...𝑁))))
240238, 239syl 17 . . . . . . . . . . . . . . . . . 18 (𝜑 → (𝐿 ∈ (1...𝑁) ↔ (𝐿 = 1 ∨ 𝐿 ∈ ((1 + 1)...𝑁))))
24131, 240mpbid 231 . . . . . . . . . . . . . . . . 17 (𝜑 → (𝐿 = 1 ∨ 𝐿 ∈ ((1 + 1)...𝑁)))
242241orcanai 1000 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ ¬ 𝐿 = 1) → 𝐿 ∈ ((1 + 1)...𝑁))
243 1p1e2 12098 . . . . . . . . . . . . . . . . . 18 (1 + 1) = 2
244243a1i 11 . . . . . . . . . . . . . . . . 17 ((𝜑 ∧ ¬ 𝐿 = 1) → (1 + 1) = 2)
245244oveq1d 7290 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ ¬ 𝐿 = 1) → ((1 + 1)...𝑁) = (2...𝑁))
246242, 245eleqtrd 2841 . . . . . . . . . . . . . . 15 ((𝜑 ∧ ¬ 𝐿 = 1) → 𝐿 ∈ (2...𝑁))
247 elfzle1 13259 . . . . . . . . . . . . . . 15 (𝐿 ∈ (2...𝑁) → 2 ≤ 𝐿)
248246, 247syl 17 . . . . . . . . . . . . . 14 ((𝜑 ∧ ¬ 𝐿 = 1) → 2 ≤ 𝐿)
249108adantr 481 . . . . . . . . . . . . . . 15 ((𝜑 ∧ ¬ 𝐿 = 1) → 𝐿 ∈ ℝ)
250131a1i 11 . . . . . . . . . . . . . . 15 ((𝜑 ∧ ¬ 𝐿 = 1) → 2 ∈ ℝ)
251249, 250subge0d 11565 . . . . . . . . . . . . . 14 ((𝜑 ∧ ¬ 𝐿 = 1) → (0 ≤ (𝐿 − 2) ↔ 2 ≤ 𝐿))
252248, 251mpbird 256 . . . . . . . . . . . . 13 ((𝜑 ∧ ¬ 𝐿 = 1) → 0 ≤ (𝐿 − 2))
253232, 236, 2523jca 1127 . . . . . . . . . . . 12 ((𝜑 ∧ ¬ 𝐿 = 1) → (0 ∈ ℤ ∧ (𝐿 − 2) ∈ ℤ ∧ 0 ≤ (𝐿 − 2)))
254 eluz2 12588 . . . . . . . . . . . 12 ((𝐿 − 2) ∈ (ℤ‘0) ↔ (0 ∈ ℤ ∧ (𝐿 − 2) ∈ ℤ ∧ 0 ≤ (𝐿 − 2)))
255253, 254sylibr 233 . . . . . . . . . . 11 ((𝜑 ∧ ¬ 𝐿 = 1) → (𝐿 − 2) ∈ (ℤ‘0))
256 hashfz 14142 . . . . . . . . . . 11 ((𝐿 − 2) ∈ (ℤ‘0) → (♯‘(0...(𝐿 − 2))) = (((𝐿 − 2) − 0) + 1))
257255, 256syl 17 . . . . . . . . . 10 ((𝜑 ∧ ¬ 𝐿 = 1) → (♯‘(0...(𝐿 − 2))) = (((𝐿 − 2) − 0) + 1))
258 2cn 12048 . . . . . . . . . . . . . . . 16 2 ∈ ℂ
259258a1i 11 . . . . . . . . . . . . . . 15 (𝜑 → 2 ∈ ℂ)
260139, 259subcld 11332 . . . . . . . . . . . . . 14 (𝜑 → (𝐿 − 2) ∈ ℂ)
261260subid1d 11321 . . . . . . . . . . . . 13 (𝜑 → ((𝐿 − 2) − 0) = (𝐿 − 2))
262261oveq1d 7290 . . . . . . . . . . . 12 (𝜑 → (((𝐿 − 2) − 0) + 1) = ((𝐿 − 2) + 1))
263139, 259, 175subadd23d 11354 . . . . . . . . . . . 12 (𝜑 → ((𝐿 − 2) + 1) = (𝐿 + (1 − 2)))
264258, 167negsubdi2i 11307 . . . . . . . . . . . . . . . 16 -(2 − 1) = (1 − 2)
265 2m1e1 12099 . . . . . . . . . . . . . . . . 17 (2 − 1) = 1
266265negeqi 11214 . . . . . . . . . . . . . . . 16 -(2 − 1) = -1
267264, 266eqtr3i 2768 . . . . . . . . . . . . . . 15 (1 − 2) = -1
268267a1i 11 . . . . . . . . . . . . . 14 (𝜑 → (1 − 2) = -1)
269268oveq2d 7291 . . . . . . . . . . . . 13 (𝜑 → (𝐿 + (1 − 2)) = (𝐿 + -1))
270139, 175negsubd 11338 . . . . . . . . . . . . 13 (𝜑 → (𝐿 + -1) = (𝐿 − 1))
271269, 270eqtrd 2778 . . . . . . . . . . . 12 (𝜑 → (𝐿 + (1 − 2)) = (𝐿 − 1))
272262, 263, 2713eqtrd 2782 . . . . . . . . . . 11 (𝜑 → (((𝐿 − 2) − 0) + 1) = (𝐿 − 1))
273272adantr 481 . . . . . . . . . 10 ((𝜑 ∧ ¬ 𝐿 = 1) → (((𝐿 − 2) − 0) + 1) = (𝐿 − 1))
274257, 273eqtrd 2778 . . . . . . . . 9 ((𝜑 ∧ ¬ 𝐿 = 1) → (♯‘(0...(𝐿 − 2))) = (𝐿 − 1))
275274oveq1d 7290 . . . . . . . 8 ((𝜑 ∧ ¬ 𝐿 = 1) → ((♯‘(0...(𝐿 − 2))) · (1 − (𝐸 / 𝑁))) = ((𝐿 − 1) · (1 − (𝐸 / 𝑁))))
276180, 228mulcomd 10996 . . . . . . . . 9 (𝜑 → ((𝐿 − 1) · (1 − (𝐸 / 𝑁))) = ((1 − (𝐸 / 𝑁)) · (𝐿 − 1)))
277276adantr 481 . . . . . . . 8 ((𝜑 ∧ ¬ 𝐿 = 1) → ((𝐿 − 1) · (1 − (𝐸 / 𝑁))) = ((1 − (𝐸 / 𝑁)) · (𝐿 − 1)))
278231, 275, 2773eqtrd 2782 . . . . . . 7 ((𝜑 ∧ ¬ 𝐿 = 1) → Σ𝑖 ∈ (0...(𝐿 − 2))(1 − (𝐸 / 𝑁)) = ((1 − (𝐸 / 𝑁)) · (𝐿 − 1)))
279 fzfid 13693 . . . . . . . 8 ((𝜑 ∧ ¬ 𝐿 = 1) → (0...(𝐿 − 2)) ∈ Fin)
280 fzn0 13270 . . . . . . . . 9 ((0...(𝐿 − 2)) ≠ ∅ ↔ (𝐿 − 2) ∈ (ℤ‘0))
281255, 280sylibr 233 . . . . . . . 8 ((𝜑 ∧ ¬ 𝐿 = 1) → (0...(𝐿 − 2)) ≠ ∅)
282119ad2antrr 723 . . . . . . . 8 (((𝜑 ∧ ¬ 𝐿 = 1) ∧ 𝑖 ∈ (0...(𝐿 − 2))) → (1 − (𝐸 / 𝑁)) ∈ ℝ)
283 simpll 764 . . . . . . . . 9 (((𝜑 ∧ ¬ 𝐿 = 1) ∧ 𝑖 ∈ (0...(𝐿 − 2))) → 𝜑)
284150adantlr 712 . . . . . . . . 9 (((𝜑 ∧ ¬ 𝐿 = 1) ∧ 𝑖 ∈ (0...(𝐿 − 2))) → 𝑖 ∈ (0...𝑁))
285283, 284, 51syl2anc 584 . . . . . . . 8 (((𝜑 ∧ ¬ 𝐿 = 1) ∧ 𝑖 ∈ (0...(𝐿 − 2))) → ((𝑋𝑖)‘𝑆) ∈ ℝ)
28649adantr 481 . . . . . . . . . . . 12 ((𝜑𝑖 ∈ (0...(𝐿 − 2))) → 𝑆𝑇)
287 elfzelz 13256 . . . . . . . . . . . . . . . . 17 (𝑖 ∈ (0...(𝐿 − 2)) → 𝑖 ∈ ℤ)
288287zred 12426 . . . . . . . . . . . . . . . 16 (𝑖 ∈ (0...(𝐿 − 2)) → 𝑖 ∈ ℝ)
289288adantl 482 . . . . . . . . . . . . . . 15 ((𝜑𝑖 ∈ (0...(𝐿 − 2))) → 𝑖 ∈ ℝ)
290163a1i 11 . . . . . . . . . . . . . . 15 ((𝜑𝑖 ∈ (0...(𝐿 − 2))) → (1 / 3) ∈ ℝ)
291289, 290readdcld 11004 . . . . . . . . . . . . . 14 ((𝜑𝑖 ∈ (0...(𝐿 − 2))) → (𝑖 + (1 / 3)) ∈ ℝ)
29214adantr 481 . . . . . . . . . . . . . 14 ((𝜑𝑖 ∈ (0...(𝐿 − 2))) → 𝐸 ∈ ℝ)
293291, 292remulcld 11005 . . . . . . . . . . . . 13 ((𝜑𝑖 ∈ (0...(𝐿 − 2))) → ((𝑖 + (1 / 3)) · 𝐸) ∈ ℝ)
294108adantr 481 . . . . . . . . . . . . . . . 16 ((𝜑𝑖 ∈ (0...(𝐿 − 2))) → 𝐿 ∈ ℝ)
295131a1i 11 . . . . . . . . . . . . . . . 16 ((𝜑𝑖 ∈ (0...(𝐿 − 2))) → 2 ∈ ℝ)
296294, 295resubcld 11403 . . . . . . . . . . . . . . 15 ((𝜑𝑖 ∈ (0...(𝐿 − 2))) → (𝐿 − 2) ∈ ℝ)
297296, 290readdcld 11004 . . . . . . . . . . . . . 14 ((𝜑𝑖 ∈ (0...(𝐿 − 2))) → ((𝐿 − 2) + (1 / 3)) ∈ ℝ)
298297, 292remulcld 11005 . . . . . . . . . . . . 13 ((𝜑𝑖 ∈ (0...(𝐿 − 2))) → (((𝐿 − 2) + (1 / 3)) · 𝐸) ∈ ℝ)
299 stoweidlem26.10 . . . . . . . . . . . . . . . 16 (𝜑𝐹:𝑇⟶ℝ)
300299, 49jca 512 . . . . . . . . . . . . . . 15 (𝜑 → (𝐹:𝑇⟶ℝ ∧ 𝑆𝑇))
301300adantr 481 . . . . . . . . . . . . . 14 ((𝜑𝑖 ∈ (0...(𝐿 − 2))) → (𝐹:𝑇⟶ℝ ∧ 𝑆𝑇))
302 ffvelrn 6959 . . . . . . . . . . . . . 14 ((𝐹:𝑇⟶ℝ ∧ 𝑆𝑇) → (𝐹𝑆) ∈ ℝ)
303301, 302syl 17 . . . . . . . . . . . . 13 ((𝜑𝑖 ∈ (0...(𝐿 − 2))) → (𝐹𝑆) ∈ ℝ)
304 elfzle2 13260 . . . . . . . . . . . . . . . 16 (𝑖 ∈ (0...(𝐿 − 2)) → 𝑖 ≤ (𝐿 − 2))
305304adantl 482 . . . . . . . . . . . . . . 15 ((𝜑𝑖 ∈ (0...(𝐿 − 2))) → 𝑖 ≤ (𝐿 − 2))
306289, 296, 290, 305leadd1dd 11589 . . . . . . . . . . . . . 14 ((𝜑𝑖 ∈ (0...(𝐿 − 2))) → (𝑖 + (1 / 3)) ≤ ((𝐿 − 2) + (1 / 3)))
30714, 72jca 512 . . . . . . . . . . . . . . . 16 (𝜑 → (𝐸 ∈ ℝ ∧ 0 < 𝐸))
308307adantr 481 . . . . . . . . . . . . . . 15 ((𝜑𝑖 ∈ (0...(𝐿 − 2))) → (𝐸 ∈ ℝ ∧ 0 < 𝐸))
309 lemul1 11827 . . . . . . . . . . . . . . 15 (((𝑖 + (1 / 3)) ∈ ℝ ∧ ((𝐿 − 2) + (1 / 3)) ∈ ℝ ∧ (𝐸 ∈ ℝ ∧ 0 < 𝐸)) → ((𝑖 + (1 / 3)) ≤ ((𝐿 − 2) + (1 / 3)) ↔ ((𝑖 + (1 / 3)) · 𝐸) ≤ (((𝐿 − 2) + (1 / 3)) · 𝐸)))
310291, 297, 308, 309syl3anc 1370 . . . . . . . . . . . . . 14 ((𝜑𝑖 ∈ (0...(𝐿 − 2))) → ((𝑖 + (1 / 3)) ≤ ((𝐿 − 2) + (1 / 3)) ↔ ((𝑖 + (1 / 3)) · 𝐸) ≤ (((𝐿 − 2) + (1 / 3)) · 𝐸)))
311306, 310mpbid 231 . . . . . . . . . . . . 13 ((𝜑𝑖 ∈ (0...(𝐿 − 2))) → ((𝑖 + (1 / 3)) · 𝐸) ≤ (((𝐿 − 2) + (1 / 3)) · 𝐸))
312108, 132resubcld 11403 . . . . . . . . . . . . . . . . 17 (𝜑 → (𝐿 − 2) ∈ ℝ)
313312, 164readdcld 11004 . . . . . . . . . . . . . . . 16 (𝜑 → ((𝐿 − 2) + (1 / 3)) ∈ ℝ)
314313, 14remulcld 11005 . . . . . . . . . . . . . . 15 (𝜑 → (((𝐿 − 2) + (1 / 3)) · 𝐸) ∈ ℝ)
315299, 49ffvelrnd 6962 . . . . . . . . . . . . . . 15 (𝜑 → (𝐹𝑆) ∈ ℝ)
316120, 164resubcld 11403 . . . . . . . . . . . . . . . . 17 (𝜑 → ((𝐿 − 1) − (1 / 3)) ∈ ℝ)
317316, 14remulcld 11005 . . . . . . . . . . . . . . . 16 (𝜑 → (((𝐿 − 1) − (1 / 3)) · 𝐸) ∈ ℝ)
318 addid1 11155 . . . . . . . . . . . . . . . . . . . . . . . . 25 (1 ∈ ℂ → (1 + 0) = 1)
319318eqcomd 2744 . . . . . . . . . . . . . . . . . . . . . . . 24 (1 ∈ ℂ → 1 = (1 + 0))
320167, 319mp1i 13 . . . . . . . . . . . . . . . . . . . . . . 23 (𝜑 → 1 = (1 + 0))
321175subidd 11320 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝜑 → (1 − 1) = 0)
322321eqcomd 2744 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝜑 → 0 = (1 − 1))
323322oveq2d 7291 . . . . . . . . . . . . . . . . . . . . . . 23 (𝜑 → (1 + 0) = (1 + (1 − 1)))
324 addsubass 11231 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((1 ∈ ℂ ∧ 1 ∈ ℂ ∧ 1 ∈ ℂ) → ((1 + 1) − 1) = (1 + (1 − 1)))
325324eqcomd 2744 . . . . . . . . . . . . . . . . . . . . . . . 24 ((1 ∈ ℂ ∧ 1 ∈ ℂ ∧ 1 ∈ ℂ) → (1 + (1 − 1)) = ((1 + 1) − 1))
326175, 175, 175, 325syl3anc 1370 . . . . . . . . . . . . . . . . . . . . . . 23 (𝜑 → (1 + (1 − 1)) = ((1 + 1) − 1))
327320, 323, 3263eqtrd 2782 . . . . . . . . . . . . . . . . . . . . . 22 (𝜑 → 1 = ((1 + 1) − 1))
328327oveq2d 7291 . . . . . . . . . . . . . . . . . . . . 21 (𝜑 → (𝐿 − 1) = (𝐿 − ((1 + 1) − 1)))
329243a1i 11 . . . . . . . . . . . . . . . . . . . . . . 23 (𝜑 → (1 + 1) = 2)
330329oveq1d 7290 . . . . . . . . . . . . . . . . . . . . . 22 (𝜑 → ((1 + 1) − 1) = (2 − 1))
331330oveq2d 7291 . . . . . . . . . . . . . . . . . . . . 21 (𝜑 → (𝐿 − ((1 + 1) − 1)) = (𝐿 − (2 − 1)))
332139, 259, 175subsubd 11360 . . . . . . . . . . . . . . . . . . . . 21 (𝜑 → (𝐿 − (2 − 1)) = ((𝐿 − 2) + 1))
333328, 331, 3323eqtrd 2782 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → (𝐿 − 1) = ((𝐿 − 2) + 1))
334333oveq1d 7290 . . . . . . . . . . . . . . . . . . 19 (𝜑 → ((𝐿 − 1) − (2 / 3)) = (((𝐿 − 2) + 1) − (2 / 3)))
335258, 60, 9divcli 11717 . . . . . . . . . . . . . . . . . . . . 21 (2 / 3) ∈ ℂ
336335a1i 11 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → (2 / 3) ∈ ℂ)
337260, 175, 336addsubassd 11352 . . . . . . . . . . . . . . . . . . 19 (𝜑 → (((𝐿 − 2) + 1) − (2 / 3)) = ((𝐿 − 2) + (1 − (2 / 3))))
338167, 60, 9divcli 11717 . . . . . . . . . . . . . . . . . . . . . 22 (1 / 3) ∈ ℂ
339 df-3 12037 . . . . . . . . . . . . . . . . . . . . . . . 24 3 = (2 + 1)
340339oveq1i 7285 . . . . . . . . . . . . . . . . . . . . . . 23 (3 / 3) = ((2 + 1) / 3)
341258, 167, 60, 9divdiri 11732 . . . . . . . . . . . . . . . . . . . . . . 23 ((2 + 1) / 3) = ((2 / 3) + (1 / 3))
342340, 61, 3413eqtr3ri 2775 . . . . . . . . . . . . . . . . . . . . . 22 ((2 / 3) + (1 / 3)) = 1
343167, 335, 338, 342subaddrii 11310 . . . . . . . . . . . . . . . . . . . . 21 (1 − (2 / 3)) = (1 / 3)
344343a1i 11 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → (1 − (2 / 3)) = (1 / 3))
345344oveq2d 7291 . . . . . . . . . . . . . . . . . . 19 (𝜑 → ((𝐿 − 2) + (1 − (2 / 3))) = ((𝐿 − 2) + (1 / 3)))
346334, 337, 3453eqtrd 2782 . . . . . . . . . . . . . . . . . 18 (𝜑 → ((𝐿 − 1) − (2 / 3)) = ((𝐿 − 2) + (1 / 3)))
347131, 7, 9redivcli 11742 . . . . . . . . . . . . . . . . . . . 20 (2 / 3) ∈ ℝ
348347a1i 11 . . . . . . . . . . . . . . . . . . 19 (𝜑 → (2 / 3) ∈ ℝ)
349 1lt2 12144 . . . . . . . . . . . . . . . . . . . 20 1 < 2
3507, 63pm3.2i 471 . . . . . . . . . . . . . . . . . . . . . 22 (3 ∈ ℝ ∧ 0 < 3)
3511, 131, 3503pm3.2i 1338 . . . . . . . . . . . . . . . . . . . . 21 (1 ∈ ℝ ∧ 2 ∈ ℝ ∧ (3 ∈ ℝ ∧ 0 < 3))
352 ltdiv1 11839 . . . . . . . . . . . . . . . . . . . . 21 ((1 ∈ ℝ ∧ 2 ∈ ℝ ∧ (3 ∈ ℝ ∧ 0 < 3)) → (1 < 2 ↔ (1 / 3) < (2 / 3)))
353351, 352mp1i 13 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → (1 < 2 ↔ (1 / 3) < (2 / 3)))
354349, 353mpbii 232 . . . . . . . . . . . . . . . . . . 19 (𝜑 → (1 / 3) < (2 / 3))
355164, 348, 120, 354ltsub2dd 11588 . . . . . . . . . . . . . . . . . 18 (𝜑 → ((𝐿 − 1) − (2 / 3)) < ((𝐿 − 1) − (1 / 3)))
356346, 355eqbrtrrd 5098 . . . . . . . . . . . . . . . . 17 (𝜑 → ((𝐿 − 2) + (1 / 3)) < ((𝐿 − 1) − (1 / 3)))
357313, 316, 13, 356ltmul1dd 12827 . . . . . . . . . . . . . . . 16 (𝜑 → (((𝐿 − 2) + (1 / 3)) · 𝐸) < (((𝐿 − 1) − (1 / 3)) · 𝐸))
35823simprd 496 . . . . . . . . . . . . . . . . . . . . . . 23 (𝜑 → ¬ 𝑆 ∈ (𝐷‘(𝐿 − 1)))
359 oveq1 7282 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑗 = (𝐿 − 1) → (𝑗 − (1 / 3)) = ((𝐿 − 1) − (1 / 3)))
360359oveq1d 7290 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑗 = (𝐿 − 1) → ((𝑗 − (1 / 3)) · 𝐸) = (((𝐿 − 1) − (1 / 3)) · 𝐸))
361360breq2d 5086 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑗 = (𝐿 − 1) → ((𝐹𝑡) ≤ ((𝑗 − (1 / 3)) · 𝐸) ↔ (𝐹𝑡) ≤ (((𝐿 − 1) − (1 / 3)) · 𝐸)))
362361rabbidv 3414 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑗 = (𝐿 − 1) → {𝑡𝑇 ∣ (𝐹𝑡) ≤ ((𝑗 − (1 / 3)) · 𝐸)} = {𝑡𝑇 ∣ (𝐹𝑡) ≤ (((𝐿 − 1) − (1 / 3)) · 𝐸)})
363129peano2zd 12429 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝜑 → (𝑁 + 1) ∈ ℤ)
364189simpld 495 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝜑 → 1 ≤ 𝐿)
365134, 116readdcld 11004 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝜑 → (𝑁 + 1) ∈ ℝ)
366134lep1d 11906 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝜑𝑁 ≤ (𝑁 + 1))
367108, 134, 365, 190, 366letrd 11132 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝜑𝐿 ≤ (𝑁 + 1))
368186, 363, 125, 364, 367elfzd 13247 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝜑𝐿 ∈ (1...(𝑁 + 1)))
369139, 175npcand 11336 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝜑 → ((𝐿 − 1) + 1) = 𝐿)
370 0p1e1 12095 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (0 + 1) = 1
371370a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝜑 → (0 + 1) = 1)
372371oveq1d 7290 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝜑 → ((0 + 1)...(𝑁 + 1)) = (1...(𝑁 + 1)))
373368, 369, 3723eltr4d 2854 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝜑 → ((𝐿 − 1) + 1) ∈ ((0 + 1)...(𝑁 + 1)))
374 0zd 12331 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝜑 → 0 ∈ ℤ)
375125, 186zsubcld 12431 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝜑 → (𝐿 − 1) ∈ ℤ)
376 fzaddel 13290 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((0 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ ((𝐿 − 1) ∈ ℤ ∧ 1 ∈ ℤ)) → ((𝐿 − 1) ∈ (0...𝑁) ↔ ((𝐿 − 1) + 1) ∈ ((0 + 1)...(𝑁 + 1))))
377374, 129, 375, 186, 376syl22anc 836 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝜑 → ((𝐿 − 1) ∈ (0...𝑁) ↔ ((𝐿 − 1) + 1) ∈ ((0 + 1)...(𝑁 + 1))))
378373, 377mpbird 256 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝜑 → (𝐿 − 1) ∈ (0...𝑁))
379 rabexg 5255 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑇 ∈ V → {𝑡𝑇 ∣ (𝐹𝑡) ≤ (((𝐿 − 1) − (1 / 3)) · 𝐸)} ∈ V)
38033, 379syl 17 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝜑 → {𝑡𝑇 ∣ (𝐹𝑡) ≤ (((𝐿 − 1) − (1 / 3)) · 𝐸)} ∈ V)
38125, 362, 378, 380fvmptd3 6898 . . . . . . . . . . . . . . . . . . . . . . 23 (𝜑 → (𝐷‘(𝐿 − 1)) = {𝑡𝑇 ∣ (𝐹𝑡) ≤ (((𝐿 − 1) − (1 / 3)) · 𝐸)})
382358, 381neleqtrd 2860 . . . . . . . . . . . . . . . . . . . . . 22 (𝜑 → ¬ 𝑆 ∈ {𝑡𝑇 ∣ (𝐹𝑡) ≤ (((𝐿 − 1) − (1 / 3)) · 𝐸)})
383 nfcv 2907 . . . . . . . . . . . . . . . . . . . . . . . 24 𝑡(((𝐿 − 1) − (1 / 3)) · 𝐸)
38441, 42, 383nfbr 5121 . . . . . . . . . . . . . . . . . . . . . . 23 𝑡(𝐹𝑆) ≤ (((𝐿 − 1) − (1 / 3)) · 𝐸)
38545breq1d 5084 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑡 = 𝑆 → ((𝐹𝑡) ≤ (((𝐿 − 1) − (1 / 3)) · 𝐸) ↔ (𝐹𝑆) ≤ (((𝐿 − 1) − (1 / 3)) · 𝐸)))
38638, 39, 384, 385elrabf 3620 . . . . . . . . . . . . . . . . . . . . . 22 (𝑆 ∈ {𝑡𝑇 ∣ (𝐹𝑡) ≤ (((𝐿 − 1) − (1 / 3)) · 𝐸)} ↔ (𝑆𝑇 ∧ (𝐹𝑆) ≤ (((𝐿 − 1) − (1 / 3)) · 𝐸)))
387382, 386sylnib 328 . . . . . . . . . . . . . . . . . . . . 21 (𝜑 → ¬ (𝑆𝑇 ∧ (𝐹𝑆) ≤ (((𝐿 − 1) − (1 / 3)) · 𝐸)))
388 ianor 979 . . . . . . . . . . . . . . . . . . . . 21 (¬ (𝑆𝑇 ∧ (𝐹𝑆) ≤ (((𝐿 − 1) − (1 / 3)) · 𝐸)) ↔ (¬ 𝑆𝑇 ∨ ¬ (𝐹𝑆) ≤ (((𝐿 − 1) − (1 / 3)) · 𝐸)))
389387, 388sylib 217 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → (¬ 𝑆𝑇 ∨ ¬ (𝐹𝑆) ≤ (((𝐿 − 1) − (1 / 3)) · 𝐸)))
390 olc 865 . . . . . . . . . . . . . . . . . . . . 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 867 . . . . . . . . . . . . . . . . . . . 20 ((¬ 𝑆𝑇 ∨ ¬ (𝐹𝑆) ≤ (((𝐿 − 1) − (1 / 3)) · 𝐸)) ↔ (¬ (𝐹𝑆) ≤ (((𝐿 − 1) − (1 / 3)) · 𝐸) ∨ ¬ 𝑆𝑇))
394393anbi2i 623 . . . . . . . . . . . . . . . . . . 19 (((¬ (𝐹𝑆) ≤ (((𝐿 − 1) − (1 / 3)) · 𝐸) ∨ 𝑆𝑇) ∧ (¬ 𝑆𝑇 ∨ ¬ (𝐹𝑆) ≤ (((𝐿 − 1) − (1 / 3)) · 𝐸))) ↔ ((¬ (𝐹𝑆) ≤ (((𝐿 − 1) − (1 / 3)) · 𝐸) ∨ 𝑆𝑇) ∧ (¬ (𝐹𝑆) ≤ (((𝐿 − 1) − (1 / 3)) · 𝐸) ∨ ¬ 𝑆𝑇)))
395392, 394sylib 217 . . . . . . . . . . . . . . . . . 18 (𝜑 → ((¬ (𝐹𝑆) ≤ (((𝐿 − 1) − (1 / 3)) · 𝐸) ∨ 𝑆𝑇) ∧ (¬ (𝐹𝑆) ≤ (((𝐿 − 1) − (1 / 3)) · 𝐸) ∨ ¬ 𝑆𝑇)))
396 pm4.43 1020 . . . . . . . . . . . . . . . . . 18 (¬ (𝐹𝑆) ≤ (((𝐿 − 1) − (1 / 3)) · 𝐸) ↔ ((¬ (𝐹𝑆) ≤ (((𝐿 − 1) − (1 / 3)) · 𝐸) ∨ 𝑆𝑇) ∧ (¬ (𝐹𝑆) ≤ (((𝐿 − 1) − (1 / 3)) · 𝐸) ∨ ¬ 𝑆𝑇)))
397395, 396sylibr 233 . . . . . . . . . . . . . . . . 17 (𝜑 → ¬ (𝐹𝑆) ≤ (((𝐿 − 1) − (1 / 3)) · 𝐸))
398317, 315ltnled 11122 . . . . . . . . . . . . . . . . 17 (𝜑 → ((((𝐿 − 1) − (1 / 3)) · 𝐸) < (𝐹𝑆) ↔ ¬ (𝐹𝑆) ≤ (((𝐿 − 1) − (1 / 3)) · 𝐸)))
399397, 398mpbird 256 . . . . . . . . . . . . . . . 16 (𝜑 → (((𝐿 − 1) − (1 / 3)) · 𝐸) < (𝐹𝑆))
400314, 317, 315, 357, 399lttrd 11136 . . . . . . . . . . . . . . 15 (𝜑 → (((𝐿 − 2) + (1 / 3)) · 𝐸) < (𝐹𝑆))
401314, 315, 400ltled 11123 . . . . . . . . . . . . . 14 (𝜑 → (((𝐿 − 2) + (1 / 3)) · 𝐸) ≤ (𝐹𝑆))
402401adantr 481 . . . . . . . . . . . . 13 ((𝜑𝑖 ∈ (0...(𝐿 − 2))) → (((𝐿 − 2) + (1 / 3)) · 𝐸) ≤ (𝐹𝑆))
403293, 298, 303, 311, 402letrd 11132 . . . . . . . . . . . 12 ((𝜑𝑖 ∈ (0...(𝐿 − 2))) → ((𝑖 + (1 / 3)) · 𝐸) ≤ (𝐹𝑆))
404 nfcv 2907 . . . . . . . . . . . . . 14 𝑡((𝑖 + (1 / 3)) · 𝐸)
405404, 42, 41nfbr 5121 . . . . . . . . . . . . 13 𝑡((𝑖 + (1 / 3)) · 𝐸) ≤ (𝐹𝑆)
40645breq2d 5086 . . . . . . . . . . . . 13 (𝑡 = 𝑆 → (((𝑖 + (1 / 3)) · 𝐸) ≤ (𝐹𝑡) ↔ ((𝑖 + (1 / 3)) · 𝐸) ≤ (𝐹𝑆)))
40738, 39, 405, 406elrabf 3620 . . . . . . . . . . . 12 (𝑆 ∈ {𝑡𝑇 ∣ ((𝑖 + (1 / 3)) · 𝐸) ≤ (𝐹𝑡)} ↔ (𝑆𝑇 ∧ ((𝑖 + (1 / 3)) · 𝐸) ≤ (𝐹𝑆)))
408286, 403, 407sylanbrc 583 . . . . . . . . . . 11 ((𝜑𝑖 ∈ (0...(𝐿 − 2))) → 𝑆 ∈ {𝑡𝑇 ∣ ((𝑖 + (1 / 3)) · 𝐸) ≤ (𝐹𝑡)})
409 stoweidlem26.5 . . . . . . . . . . . 12 𝐵 = (𝑗 ∈ (0...𝑁) ↦ {𝑡𝑇 ∣ ((𝑗 + (1 / 3)) · 𝐸) ≤ (𝐹𝑡)})
410 oveq1 7282 . . . . . . . . . . . . . . 15 (𝑗 = 𝑖 → (𝑗 + (1 / 3)) = (𝑖 + (1 / 3)))
411410oveq1d 7290 . . . . . . . . . . . . . 14 (𝑗 = 𝑖 → ((𝑗 + (1 / 3)) · 𝐸) = ((𝑖 + (1 / 3)) · 𝐸))
412411breq1d 5084 . . . . . . . . . . . . 13 (𝑗 = 𝑖 → (((𝑗 + (1 / 3)) · 𝐸) ≤ (𝐹𝑡) ↔ ((𝑖 + (1 / 3)) · 𝐸) ≤ (𝐹𝑡)))
413412rabbidv 3414 . . . . . . . . . . . 12 (𝑗 = 𝑖 → {𝑡𝑇 ∣ ((𝑗 + (1 / 3)) · 𝐸) ≤ (𝐹𝑡)} = {𝑡𝑇 ∣ ((𝑖 + (1 / 3)) · 𝐸) ≤ (𝐹𝑡)})
414 rabexg 5255 . . . . . . . . . . . . . 14 (𝑇 ∈ V → {𝑡𝑇 ∣ ((𝑖 + (1 / 3)) · 𝐸) ≤ (𝐹𝑡)} ∈ V)
41533, 414syl 17 . . . . . . . . . . . . 13 (𝜑 → {𝑡𝑇 ∣ ((𝑖 + (1 / 3)) · 𝐸) ≤ (𝐹𝑡)} ∈ V)
416415adantr 481 . . . . . . . . . . . 12 ((𝜑𝑖 ∈ (0...(𝐿 − 2))) → {𝑡𝑇 ∣ ((𝑖 + (1 / 3)) · 𝐸) ≤ (𝐹𝑡)} ∈ V)
417409, 413, 150, 416fvmptd3 6898 . . . . . . . . . . 11 ((𝜑𝑖 ∈ (0...(𝐿 − 2))) → (𝐵𝑖) = {𝑡𝑇 ∣ ((𝑖 + (1 / 3)) · 𝐸) ≤ (𝐹𝑡)})
418408, 417eleqtrrd 2842 . . . . . . . . . 10 ((𝜑𝑖 ∈ (0...(𝐿 − 2))) → 𝑆 ∈ (𝐵𝑖))
4191453ad2ant1 1132 . . . . . . . . . . . . . 14 ((𝜑𝑖 ∈ (0...(𝐿 − 2)) ∧ 𝑆 ∈ (𝐵𝑖)) → ((𝐿 − 2) ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ (𝐿 − 2) ≤ 𝑁))
420419, 146sylibr 233 . . . . . . . . . . . . 13 ((𝜑𝑖 ∈ (0...(𝐿 − 2)) ∧ 𝑆 ∈ (𝐵𝑖)) → 𝑁 ∈ (ℤ‘(𝐿 − 2)))
421420, 148syl 17 . . . . . . . . . . . 12 ((𝜑𝑖 ∈ (0...(𝐿 − 2)) ∧ 𝑆 ∈ (𝐵𝑖)) → (0...(𝐿 − 2)) ⊆ (0...𝑁))
422 simp2 1136 . . . . . . . . . . . 12 ((𝜑𝑖 ∈ (0...(𝐿 − 2)) ∧ 𝑆 ∈ (𝐵𝑖)) → 𝑖 ∈ (0...(𝐿 − 2)))
423421, 422sseldd 3922 . . . . . . . . . . 11 ((𝜑𝑖 ∈ (0...(𝐿 − 2)) ∧ 𝑆 ∈ (𝐵𝑖)) → 𝑖 ∈ (0...𝑁))
424 elex 3450 . . . . . . . . . . . . 13 (𝑆 ∈ (𝐵𝑖) → 𝑆 ∈ V)
4254243ad2ant3 1134 . . . . . . . . . . . 12 ((𝜑𝑖 ∈ (0...𝑁) ∧ 𝑆 ∈ (𝐵𝑖)) → 𝑆 ∈ V)
426 nfcv 2907 . . . . . . . . . . . . . . . . . . 19 𝑡(0...𝑁)
427 nfrab1 3317 . . . . . . . . . . . . . . . . . . 19 𝑡{𝑡𝑇 ∣ ((𝑗 + (1 / 3)) · 𝐸) ≤ (𝐹𝑡)}
428426, 427nfmpt 5181 . . . . . . . . . . . . . . . . . 18 𝑡(𝑗 ∈ (0...𝑁) ↦ {𝑡𝑇 ∣ ((𝑗 + (1 / 3)) · 𝐸) ≤ (𝐹𝑡)})
429409, 428nfcxfr 2905 . . . . . . . . . . . . . . . . 17 𝑡𝐵
430 nfcv 2907 . . . . . . . . . . . . . . . . 17 𝑡𝑖
431429, 430nffv 6784 . . . . . . . . . . . . . . . 16 𝑡(𝐵𝑖)
432431nfel2 2925 . . . . . . . . . . . . . . 15 𝑡 𝑆 ∈ (𝐵𝑖)
43388, 89, 432nf3an 1904 . . . . . . . . . . . . . 14 𝑡(𝜑𝑖 ∈ (0...𝑁) ∧ 𝑆 ∈ (𝐵𝑖))
434 nfv 1917 . . . . . . . . . . . . . 14 𝑡(1 − (𝐸 / 𝑁)) < ((𝑋𝑖)‘𝑆)
435433, 434nfim 1899 . . . . . . . . . . . . 13 𝑡((𝜑𝑖 ∈ (0...𝑁) ∧ 𝑆 ∈ (𝐵𝑖)) → (1 − (𝐸 / 𝑁)) < ((𝑋𝑖)‘𝑆))
436 eleq1 2826 . . . . . . . . . . . . . . 15 (𝑡 = 𝑆 → (𝑡 ∈ (𝐵𝑖) ↔ 𝑆 ∈ (𝐵𝑖)))
4374363anbi3d 1441 . . . . . . . . . . . . . 14 (𝑡 = 𝑆 → ((𝜑𝑖 ∈ (0...𝑁) ∧ 𝑡 ∈ (𝐵𝑖)) ↔ (𝜑𝑖 ∈ (0...𝑁) ∧ 𝑆 ∈ (𝐵𝑖))))
43893breq2d 5086 . . . . . . . . . . . . . 14 (𝑡 = 𝑆 → ((1 − (𝐸 / 𝑁)) < ((𝑋𝑖)‘𝑡) ↔ (1 − (𝐸 / 𝑁)) < ((𝑋𝑖)‘𝑆)))
439437, 438imbi12d 345 . . . . . . . . . . . . 13 (𝑡 = 𝑆 → (((𝜑𝑖 ∈ (0...𝑁) ∧ 𝑡 ∈ (𝐵𝑖)) → (1 − (𝐸 / 𝑁)) < ((𝑋𝑖)‘𝑡)) ↔ ((𝜑𝑖 ∈ (0...𝑁) ∧ 𝑆 ∈ (𝐵𝑖)) → (1 − (𝐸 / 𝑁)) < ((𝑋𝑖)‘𝑆))))
440 stoweidlem26.15 . . . . . . . . . . . . 13 ((𝜑𝑖 ∈ (0...𝑁) ∧ 𝑡 ∈ (𝐵𝑖)) → (1 − (𝐸 / 𝑁)) < ((𝑋𝑖)‘𝑡))
441435, 439, 440vtoclg1f 3504 . . . . . . . . . . . 12 (𝑆 ∈ V → ((𝜑𝑖 ∈ (0...𝑁) ∧ 𝑆 ∈ (𝐵𝑖)) → (1 − (𝐸 / 𝑁)) < ((𝑋𝑖)‘𝑆)))
442425, 441mpcom 38 . . . . . . . . . . 11 ((𝜑𝑖 ∈ (0...𝑁) ∧ 𝑆 ∈ (𝐵𝑖)) → (1 − (𝐸 / 𝑁)) < ((𝑋𝑖)‘𝑆))
443423, 442syld3an2 1410 . . . . . . . . . 10 ((𝜑𝑖 ∈ (0...(𝐿 − 2)) ∧ 𝑆 ∈ (𝐵𝑖)) → (1 − (𝐸 / 𝑁)) < ((𝑋𝑖)‘𝑆))
444418, 443mpd3an3 1461 . . . . . . . . 9 ((𝜑𝑖 ∈ (0...(𝐿 − 2))) → (1 − (𝐸 / 𝑁)) < ((𝑋𝑖)‘𝑆))
445444adantlr 712 . . . . . . . 8 (((𝜑 ∧ ¬ 𝐿 = 1) ∧ 𝑖 ∈ (0...(𝐿 − 2))) → (1 − (𝐸 / 𝑁)) < ((𝑋𝑖)‘𝑆))
446279, 281, 282, 285, 445fsumlt 15512 . . . . . . 7 ((𝜑 ∧ ¬ 𝐿 = 1) → Σ𝑖 ∈ (0...(𝐿 − 2))(1 − (𝐸 / 𝑁)) < Σ𝑖 ∈ (0...(𝐿 − 2))((𝑋𝑖)‘𝑆))
447278, 446eqbrtrrd 5098 . . . . . 6 ((𝜑 ∧ ¬ 𝐿 = 1) → ((1 − (𝐸 / 𝑁)) · (𝐿 − 1)) < Σ𝑖 ∈ (0...(𝐿 − 2))((𝑋𝑖)‘𝑆))
448121adantr 481 . . . . . . 7 ((𝜑 ∧ ¬ 𝐿 = 1) → ((1 − (𝐸 / 𝑁)) · (𝐿 − 1)) ∈ ℝ)
449152adantr 481 . . . . . . 7 ((𝜑 ∧ ¬ 𝐿 = 1) → Σ𝑖 ∈ (0...(𝐿 − 2))((𝑋𝑖)‘𝑆) ∈ ℝ)
450307adantr 481 . . . . . . 7 ((𝜑 ∧ ¬ 𝐿 = 1) → (𝐸 ∈ ℝ ∧ 0 < 𝐸))
451 ltmul2 11826 . . . . . . 7 ((((1 − (𝐸 / 𝑁)) · (𝐿 − 1)) ∈ ℝ ∧ Σ𝑖 ∈ (0...(𝐿 − 2))((𝑋𝑖)‘𝑆) ∈ ℝ ∧ (𝐸 ∈ ℝ ∧ 0 < 𝐸)) → (((1 − (𝐸 / 𝑁)) · (𝐿 − 1)) < Σ𝑖 ∈ (0...(𝐿 − 2))((𝑋𝑖)‘𝑆) ↔ (𝐸 · ((1 − (𝐸 / 𝑁)) · (𝐿 − 1))) < (𝐸 · Σ𝑖 ∈ (0...(𝐿 − 2))((𝑋𝑖)‘𝑆))))
452448, 449, 450, 451syl3anc 1370 . . . . . 6 ((𝜑 ∧ ¬ 𝐿 = 1) → (((1 − (𝐸 / 𝑁)) · (𝐿 − 1)) < Σ𝑖 ∈ (0...(𝐿 − 2))((𝑋𝑖)‘𝑆) ↔ (𝐸 · ((1 − (𝐸 / 𝑁)) · (𝐿 − 1))) < (𝐸 · Σ𝑖 ∈ (0...(𝐿 − 2))((𝑋𝑖)‘𝑆))))
453447, 452mpbid 231 . . . . 5 ((𝜑 ∧ ¬ 𝐿 = 1) → (𝐸 · ((1 − (𝐸 / 𝑁)) · (𝐿 − 1))) < (𝐸 · Σ𝑖 ∈ (0...(𝐿 − 2))((𝑋𝑖)‘𝑆)))
454115, 123, 154, 227, 453lttrd 11136 . . . 4 ((𝜑 ∧ ¬ 𝐿 = 1) → ((𝐿 − (4 / 3)) · 𝐸) < (𝐸 · Σ𝑖 ∈ (0...(𝐿 − 2))((𝑋𝑖)‘𝑆)))
455150, 52syldan 591 . . . . . . . . . 10 ((𝜑𝑖 ∈ (0...(𝐿 − 2))) → (𝐸 · ((𝑋𝑖)‘𝑆)) ∈ ℝ)
456455adantlr 712 . . . . . . . . 9 (((𝜑 ∧ ¬ 𝐿 = 1) ∧ 𝑖 ∈ (0...(𝐿 − 2))) → (𝐸 · ((𝑋𝑖)‘𝑆)) ∈ ℝ)
457456recnd 11003 . . . . . . . 8 (((𝜑 ∧ ¬ 𝐿 = 1) ∧ 𝑖 ∈ (0...(𝐿 − 2))) → (𝐸 · ((𝑋𝑖)‘𝑆)) ∈ ℂ)
458279, 457fsumcl 15445 . . . . . . 7 ((𝜑 ∧ ¬ 𝐿 = 1) → Σ𝑖 ∈ (0...(𝐿 − 2))(𝐸 · ((𝑋𝑖)‘𝑆)) ∈ ℂ)
459458addid1d 11175 . . . . . 6 ((𝜑 ∧ ¬ 𝐿 = 1) → (Σ𝑖 ∈ (0...(𝐿 − 2))(𝐸 · ((𝑋𝑖)‘𝑆)) + 0) = Σ𝑖 ∈ (0...(𝐿 − 2))(𝐸 · ((𝑋𝑖)‘𝑆)))
460 0red 10978 . . . . . . 7 ((𝜑 ∧ ¬ 𝐿 = 1) → 0 ∈ ℝ)
461 fzfid 13693 . . . . . . . 8 ((𝜑 ∧ ¬ 𝐿 = 1) → ((𝐿 − 1)...𝑁) ∈ Fin)
46214adantr 481 . . . . . . . . . 10 ((𝜑𝑖 ∈ ((𝐿 − 1)...𝑁)) → 𝐸 ∈ ℝ)
463 0zd 12331 . . . . . . . . . . . 12 ((𝜑𝑖 ∈ ((𝐿 − 1)...𝑁)) → 0 ∈ ℤ)
464129adantr 481 . . . . . . . . . . . 12 ((𝜑𝑖 ∈ ((𝐿 − 1)...𝑁)) → 𝑁 ∈ ℤ)
465 elfzelz 13256 . . . . . . . . . . . . 13 (𝑖 ∈ ((𝐿 − 1)...𝑁) → 𝑖 ∈ ℤ)
466465adantl 482 . . . . . . . . . . . 12 ((𝜑𝑖 ∈ ((𝐿 − 1)...𝑁)) → 𝑖 ∈ ℤ)
467 0red 10978 . . . . . . . . . . . . 13 ((𝜑𝑖 ∈ ((𝐿 − 1)...𝑁)) → 0 ∈ ℝ)
468120adantr 481 . . . . . . . . . . . . 13 ((𝜑𝑖 ∈ ((𝐿 − 1)...𝑁)) → (𝐿 − 1) ∈ ℝ)
469465zred 12426 . . . . . . . . . . . . . 14 (𝑖 ∈ ((𝐿 − 1)...𝑁) → 𝑖 ∈ ℝ)
470469adantl 482 . . . . . . . . . . . . 13 ((𝜑𝑖 ∈ ((𝐿 − 1)...𝑁)) → 𝑖 ∈ ℝ)
471 1m1e0 12045 . . . . . . . . . . . . . . 15 (1 − 1) = 0
472116, 108, 116, 364lesub1dd 11591 . . . . . . . . . . . . . . 15 (𝜑 → (1 − 1) ≤ (𝐿 − 1))
473471, 472eqbrtrrid 5110 . . . . . . . . . . . . . 14 (𝜑 → 0 ≤ (𝐿 − 1))
474473adantr 481 . . . . . . . . . . . . 13 ((𝜑𝑖 ∈ ((𝐿 − 1)...𝑁)) → 0 ≤ (𝐿 − 1))
475 simpr 485 . . . . . . . . . . . . . . 15 ((𝜑𝑖 ∈ ((𝐿 − 1)...𝑁)) → 𝑖 ∈ ((𝐿 − 1)...𝑁))
476375adantr 481 . . . . . . . . . . . . . . . 16 ((𝜑𝑖 ∈ ((𝐿 − 1)...𝑁)) → (𝐿 − 1) ∈ ℤ)
477 elfz 13245 . . . . . . . . . . . . . . . 16 ((𝑖 ∈ ℤ ∧ (𝐿 − 1) ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑖 ∈ ((𝐿 − 1)...𝑁) ↔ ((𝐿 − 1) ≤ 𝑖𝑖𝑁)))
478466, 476, 464, 477syl3anc 1370 . . . . . . . . . . . . . . 15 ((𝜑𝑖 ∈ ((𝐿 − 1)...𝑁)) → (𝑖 ∈ ((𝐿 − 1)...𝑁) ↔ ((𝐿 − 1) ≤ 𝑖𝑖𝑁)))
479475, 478mpbid 231 . . . . . . . . . . . . . 14 ((𝜑𝑖 ∈ ((𝐿 − 1)...𝑁)) → ((𝐿 − 1) ≤ 𝑖𝑖𝑁))
480479simpld 495 . . . . . . . . . . . . 13 ((𝜑𝑖 ∈ ((𝐿 − 1)...𝑁)) → (𝐿 − 1) ≤ 𝑖)
481467, 468, 470, 474, 480letrd 11132 . . . . . . . . . . . 12 ((𝜑𝑖 ∈ ((𝐿 − 1)...𝑁)) → 0 ≤ 𝑖)
482 elfzle2 13260 . . . . . . . . . . . . 13 (𝑖 ∈ ((𝐿 − 1)...𝑁) → 𝑖𝑁)
483482adantl 482 . . . . . . . . . . . 12 ((𝜑𝑖 ∈ ((𝐿 − 1)...𝑁)) → 𝑖𝑁)
484463, 464, 466, 481, 483elfzd 13247 . . . . . . . . . . 11 ((𝜑𝑖 ∈ ((𝐿 − 1)...𝑁)) → 𝑖 ∈ (0...𝑁))
485484, 51syldan 591 . . . . . . . . . 10 ((𝜑𝑖 ∈ ((𝐿 − 1)...𝑁)) → ((𝑋𝑖)‘𝑆) ∈ ℝ)
486462, 485remulcld 11005 . . . . . . . . 9 ((𝜑𝑖 ∈ ((𝐿 − 1)...𝑁)) → (𝐸 · ((𝑋𝑖)‘𝑆)) ∈ ℝ)
487486adantlr 712 . . . . . . . 8 (((𝜑 ∧ ¬ 𝐿 = 1) ∧ 𝑖 ∈ ((𝐿 − 1)...𝑁)) → (𝐸 · ((𝑋𝑖)‘𝑆)) ∈ ℝ)
488461, 487fsumrecl 15446 . . . . . . 7 ((𝜑 ∧ ¬ 𝐿 = 1) → Σ𝑖 ∈ ((𝐿 − 1)...𝑁)(𝐸 · ((𝑋𝑖)‘𝑆)) ∈ ℝ)
489279, 456fsumrecl 15446 . . . . . . 7 ((𝜑 ∧ ¬ 𝐿 = 1) → Σ𝑖 ∈ (0...(𝐿 − 2))(𝐸 · ((𝑋𝑖)‘𝑆)) ∈ ℝ)
490 fzfid 13693 . . . . . . . . 9 (𝜑 → ((𝐿 − 1)...𝑁) ∈ Fin)
491176adantr 481 . . . . . . . . . . 11 ((𝜑𝑖 ∈ ((𝐿 − 1)...𝑁)) → 𝐸 ∈ ℂ)
492491mul01d 11174 . . . . . . . . . 10 ((𝜑𝑖 ∈ ((𝐿 − 1)...𝑁)) → (𝐸 · 0) = 0)
493484, 100syldan 591 . . . . . . . . . . 11 ((𝜑𝑖 ∈ ((𝐿 − 1)...𝑁)) → 0 ≤ ((𝑋𝑖)‘𝑆))
494307adantr 481 . . . . . . . . . . . 12 ((𝜑𝑖 ∈ ((𝐿 − 1)...𝑁)) → (𝐸 ∈ ℝ ∧ 0 < 𝐸))
495 lemul2 11828 . . . . . . . . . . . 12 ((0 ∈ ℝ ∧ ((𝑋𝑖)‘𝑆) ∈ ℝ ∧ (𝐸 ∈ ℝ ∧ 0 < 𝐸)) → (0 ≤ ((𝑋𝑖)‘𝑆) ↔ (𝐸 · 0) ≤ (𝐸 · ((𝑋𝑖)‘𝑆))))
496467, 485, 494, 495syl3anc 1370 . . . . . . . . . . 11 ((𝜑𝑖 ∈ ((𝐿 − 1)...𝑁)) → (0 ≤ ((𝑋𝑖)‘𝑆) ↔ (𝐸 · 0) ≤ (𝐸 · ((𝑋𝑖)‘𝑆))))
497493, 496mpbid 231 . . . . . . . . . 10 ((𝜑𝑖 ∈ ((𝐿 − 1)...𝑁)) → (𝐸 · 0) ≤ (𝐸 · ((𝑋𝑖)‘𝑆)))
498492, 497eqbrtrrd 5098 . . . . . . . . 9 ((𝜑𝑖 ∈ ((𝐿 − 1)...𝑁)) → 0 ≤ (𝐸 · ((𝑋𝑖)‘𝑆)))
499490, 486, 498fsumge0 15507 . . . . . . . 8 (𝜑 → 0 ≤ Σ𝑖 ∈ ((𝐿 − 1)...𝑁)(𝐸 · ((𝑋𝑖)‘𝑆)))
500499adantr 481 . . . . . . 7 ((𝜑 ∧ ¬ 𝐿 = 1) → 0 ≤ Σ𝑖 ∈ ((𝐿 − 1)...𝑁)(𝐸 · ((𝑋𝑖)‘𝑆)))
501460, 488, 489, 500leadd2dd 11590 . . . . . 6 ((𝜑 ∧ ¬ 𝐿 = 1) → (Σ𝑖 ∈ (0...(𝐿 − 2))(𝐸 · ((𝑋𝑖)‘𝑆)) + 0) ≤ (Σ𝑖 ∈ (0...(𝐿 − 2))(𝐸 · ((𝑋𝑖)‘𝑆)) + Σ𝑖 ∈ ((𝐿 − 1)...𝑁)(𝐸 · ((𝑋𝑖)‘𝑆))))
502459, 501eqbrtrrd 5098 . . . . 5 ((𝜑 ∧ ¬ 𝐿 = 1) → Σ𝑖 ∈ (0...(𝐿 − 2))(𝐸 · ((𝑋𝑖)‘𝑆)) ≤ (Σ𝑖 ∈ (0...(𝐿 − 2))(𝐸 · ((𝑋𝑖)‘𝑆)) + Σ𝑖 ∈ ((𝐿 − 1)...𝑁)(𝐸 · ((𝑋𝑖)‘𝑆))))
503151recnd 11003 . . . . . . 7 ((𝜑𝑖 ∈ (0...(𝐿 − 2))) → ((𝑋𝑖)‘𝑆) ∈ ℂ)
504124, 176, 503fsummulc2 15496 . . . . . 6 (𝜑 → (𝐸 · Σ𝑖 ∈ (0...(𝐿 − 2))((𝑋𝑖)‘𝑆)) = Σ𝑖 ∈ (0...(𝐿 − 2))(𝐸 · ((𝑋𝑖)‘𝑆)))
505504adantr 481 . . . . 5 ((𝜑 ∧ ¬ 𝐿 = 1) → (𝐸 · Σ𝑖 ∈ (0...(𝐿 − 2))((𝑋𝑖)‘𝑆)) = Σ𝑖 ∈ (0...(𝐿 − 2))(𝐸 · ((𝑋𝑖)‘𝑆)))
506 stoweidlem26.2 . . . . . . . . 9 𝑗𝜑
507 elfzelz 13256 . . . . . . . . . . . . . . . 16 (𝑗 ∈ (0...(𝐿 − 2)) → 𝑗 ∈ ℤ)
508507adantl 482 . . . . . . . . . . . . . . 15 ((𝜑𝑗 ∈ (0...(𝐿 − 2))) → 𝑗 ∈ ℤ)
509508zred 12426 . . . . . . . . . . . . . 14 ((𝜑𝑗 ∈ (0...(𝐿 − 2))) → 𝑗 ∈ ℝ)
510312adantr 481 . . . . . . . . . . . . . 14 ((𝜑𝑗 ∈ (0...(𝐿 − 2))) → (𝐿 − 2) ∈ ℝ)
511120adantr 481 . . . . . . . . . . . . . 14 ((𝜑𝑗 ∈ (0...(𝐿 − 2))) → (𝐿 − 1) ∈ ℝ)
512 simpr 485 . . . . . . . . . . . . . . . 16 ((𝜑𝑗 ∈ (0...(𝐿 − 2))) → 𝑗 ∈ (0...(𝐿 − 2)))
513 0zd 12331 . . . . . . . . . . . . . . . . 17 ((𝜑𝑗 ∈ (0...(𝐿 − 2))) → 0 ∈ ℤ)
514128adantr 481 . . . . . . . . . . . . . . . . 17 ((𝜑𝑗 ∈ (0...(𝐿 − 2))) → (𝐿 − 2) ∈ ℤ)
515 elfz 13245 . . . . . . . . . . . . . . . . 17 ((𝑗 ∈ ℤ ∧ 0 ∈ ℤ ∧ (𝐿 − 2) ∈ ℤ) → (𝑗 ∈ (0...(𝐿 − 2)) ↔ (0 ≤ 𝑗𝑗 ≤ (𝐿 − 2))))
516508, 513, 514, 515syl3anc 1370 . . . . . . . . . . . . . . . 16 ((𝜑𝑗 ∈ (0...(𝐿 − 2))) → (𝑗 ∈ (0...(𝐿 − 2)) ↔ (0 ≤ 𝑗𝑗 ≤ (𝐿 − 2))))
517512, 516mpbid 231 . . . . . . . . . . . . . . 15 ((𝜑𝑗 ∈ (0...(𝐿 − 2))) → (0 ≤ 𝑗𝑗 ≤ (𝐿 − 2)))
518517simprd 496 . . . . . . . . . . . . . 14 ((𝜑𝑗 ∈ (0...(𝐿 − 2))) → 𝑗 ≤ (𝐿 − 2))
519116, 132, 108ltsub2d 11585 . . . . . . . . . . . . . . . 16 (𝜑 → (1 < 2 ↔ (𝐿 − 2) < (𝐿 − 1)))
520349, 519mpbii 232 . . . . . . . . . . . . . . 15 (𝜑 → (𝐿 − 2) < (𝐿 − 1))
521520adantr 481 . . . . . . . . . . . . . 14 ((𝜑𝑗 ∈ (0...(𝐿 − 2))) → (𝐿 − 2) < (𝐿 − 1))
522509, 510, 511, 518, 521lelttrd 11133 . . . . . . . . . . . . 13 ((𝜑𝑗 ∈ (0...(𝐿 − 2))) → 𝑗 < (𝐿 − 1))
523509, 511ltnled 11122 . . . . . . . . . . . . 13 ((𝜑𝑗 ∈ (0...(𝐿 − 2))) → (𝑗 < (𝐿 − 1) ↔ ¬ (𝐿 − 1) ≤ 𝑗))
524522, 523mpbid 231 . . . . . . . . . . . 12 ((𝜑𝑗 ∈ (0...(𝐿 − 2))) → ¬ (𝐿 − 1) ≤ 𝑗)
525524intnanrd 490 . . . . . . . . . . 11 ((𝜑𝑗 ∈ (0...(𝐿 − 2))) → ¬ ((𝐿 − 1) ≤ 𝑗𝑗𝑁))
526375adantr 481 . . . . . . . . . . . 12 ((𝜑𝑗 ∈ (0...(𝐿 − 2))) → (𝐿 − 1) ∈ ℤ)
527129adantr 481 . . . . . . . . . . . 12 ((𝜑𝑗 ∈ (0...(𝐿 − 2))) → 𝑁 ∈ ℤ)
528 elfz 13245 . . . . . . . . . . . 12 ((𝑗 ∈ ℤ ∧ (𝐿 − 1) ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑗 ∈ ((𝐿 − 1)...𝑁) ↔ ((𝐿 − 1) ≤ 𝑗𝑗𝑁)))
529508, 526, 527, 528syl3anc 1370 . . . . . . . . . . 11 ((𝜑𝑗 ∈ (0...(𝐿 − 2))) → (𝑗 ∈ ((𝐿 − 1)...𝑁) ↔ ((𝐿 − 1) ≤ 𝑗𝑗𝑁)))
530525, 529mtbird 325 . . . . . . . . . 10 ((𝜑𝑗 ∈ (0...(𝐿 − 2))) → ¬ 𝑗 ∈ ((𝐿 − 1)...𝑁))
531530ex 413 . . . . . . . . 9 (𝜑 → (𝑗 ∈ (0...(𝐿 − 2)) → ¬ 𝑗 ∈ ((𝐿 − 1)...𝑁)))
532506, 531ralrimi 3141 . . . . . . . 8 (𝜑 → ∀𝑗 ∈ (0...(𝐿 − 2)) ¬ 𝑗 ∈ ((𝐿 − 1)...𝑁))
533 disj 4381 . . . . . . . 8 (((0...(𝐿 − 2)) ∩ ((𝐿 − 1)...𝑁)) = ∅ ↔ ∀𝑗 ∈ (0...(𝐿 − 2)) ¬ 𝑗 ∈ ((𝐿 − 1)...𝑁))
534532, 533sylibr 233 . . . . . . 7 (𝜑 → ((0...(𝐿 − 2)) ∩ ((𝐿 − 1)...𝑁)) = ∅)
535534adantr 481 . . . . . 6 ((𝜑 ∧ ¬ 𝐿 = 1) → ((0...(𝐿 − 2)) ∩ ((𝐿 − 1)...𝑁)) = ∅)
536144adantr 481 . . . . . . . . 9 ((𝜑 ∧ ¬ 𝐿 = 1) → (𝐿 − 2) ≤ 𝑁)
537128, 374, 1293jca 1127 . . . . . . . . . . 11 (𝜑 → ((𝐿 − 2) ∈ ℤ ∧ 0 ∈ ℤ ∧ 𝑁 ∈ ℤ))
538537adantr 481 . . . . . . . . . 10 ((𝜑 ∧ ¬ 𝐿 = 1) → ((𝐿 − 2) ∈ ℤ ∧ 0 ∈ ℤ ∧ 𝑁 ∈ ℤ))
539 elfz 13245 . . . . . . . . . 10 (((𝐿 − 2) ∈ ℤ ∧ 0 ∈ ℤ ∧ 𝑁 ∈ ℤ) → ((𝐿 − 2) ∈ (0...𝑁) ↔ (0 ≤ (𝐿 − 2) ∧ (𝐿 − 2) ≤ 𝑁)))
540538, 539syl 17 . . . . . . . . 9 ((𝜑 ∧ ¬ 𝐿 = 1) → ((𝐿 − 2) ∈ (0...𝑁) ↔ (0 ≤ (𝐿 − 2) ∧ (𝐿 − 2) ≤ 𝑁)))
541252, 536, 540mpbir2and 710 . . . . . . . 8 ((𝜑 ∧ ¬ 𝐿 = 1) → (𝐿 − 2) ∈ (0...𝑁))
542 fzsplit 13282 . . . . . . . 8 ((𝐿 − 2) ∈ (0...𝑁) → (0...𝑁) = ((0...(𝐿 − 2)) ∪ (((𝐿 − 2) + 1)...𝑁)))
543541, 542syl 17 . . . . . . 7 ((𝜑 ∧ ¬ 𝐿 = 1) → (0...𝑁) = ((0...(𝐿 − 2)) ∪ (((𝐿 − 2) + 1)...𝑁)))
544263, 269, 2703eqtrd 2782 . . . . . . . . . 10 (𝜑 → ((𝐿 − 2) + 1) = (𝐿 − 1))
545544oveq1d 7290 . . . . . . . . 9 (𝜑 → (((𝐿 − 2) + 1)...𝑁) = ((𝐿 − 1)...𝑁))
546545uneq2d 4097 . . . . . . . 8 (𝜑 → ((0...(𝐿 − 2)) ∪ (((𝐿 − 2) + 1)...𝑁)) = ((0...(𝐿 − 2)) ∪ ((𝐿 − 1)...𝑁)))
547546adantr 481 . . . . . . 7 ((𝜑 ∧ ¬ 𝐿 = 1) → ((0...(𝐿 − 2)) ∪ (((𝐿 − 2) + 1)...𝑁)) = ((0...(𝐿 − 2)) ∪ ((𝐿 − 1)...𝑁)))
548543, 547eqtrd 2778 . . . . . 6 ((𝜑 ∧ ¬ 𝐿 = 1) → (0...𝑁) = ((0...(𝐿 − 2)) ∪ ((𝐿 − 1)...𝑁)))
549 fzfid 13693 . . . . . 6 ((𝜑 ∧ ¬ 𝐿 = 1) → (0...𝑁) ∈ Fin)
550176adantr 481 . . . . . . . 8 ((𝜑𝑖 ∈ (0...𝑁)) → 𝐸 ∈ ℂ)
55151recnd 11003 . . . . . . . 8 ((𝜑𝑖 ∈ (0...𝑁)) → ((𝑋𝑖)‘𝑆) ∈ ℂ)
552550, 551mulcld 10995 . . . . . . 7 ((𝜑𝑖 ∈ (0...𝑁)) → (𝐸 · ((𝑋𝑖)‘𝑆)) ∈ ℂ)
553552adantlr 712 . . . . . 6 (((𝜑 ∧ ¬ 𝐿 = 1) ∧ 𝑖 ∈ (0...𝑁)) → (𝐸 · ((𝑋𝑖)‘𝑆)) ∈ ℂ)
554535, 548, 549, 553fsumsplit 15453 . . . . 5 ((𝜑 ∧ ¬ 𝐿 = 1) → Σ𝑖 ∈ (0...𝑁)(𝐸 · ((𝑋𝑖)‘𝑆)) = (Σ𝑖 ∈ (0...(𝐿 − 2))(𝐸 · ((𝑋𝑖)‘𝑆)) + Σ𝑖 ∈ ((𝐿 − 1)...𝑁)(𝐸 · ((𝑋𝑖)‘𝑆))))
555502, 505, 5543brtr4d 5106 . . . 4 ((𝜑 ∧ ¬ 𝐿 = 1) → (𝐸 · Σ𝑖 ∈ (0...(𝐿 − 2))((𝑋𝑖)‘𝑆)) ≤ Σ𝑖 ∈ (0...𝑁)(𝐸 · ((𝑋𝑖)‘𝑆)))
556114, 153, 533jca 1127 . . . . . 6 (𝜑 → (((𝐿 − (4 / 3)) · 𝐸) ∈ ℝ ∧ (𝐸 · Σ𝑖 ∈ (0...(𝐿 − 2))((𝑋𝑖)‘𝑆)) ∈ ℝ ∧ Σ𝑖 ∈ (0...𝑁)(𝐸 · ((𝑋𝑖)‘𝑆)) ∈ ℝ))
557556adantr 481 . . . . 5 ((𝜑 ∧ ¬ 𝐿 = 1) → (((𝐿 − (4 / 3)) · 𝐸) ∈ ℝ ∧ (𝐸 · Σ𝑖 ∈ (0...(𝐿 − 2))((𝑋𝑖)‘𝑆)) ∈ ℝ ∧ Σ𝑖 ∈ (0...𝑁)(𝐸 · ((𝑋𝑖)‘𝑆)) ∈ ℝ))
558 ltletr 11067 . . . . 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 696 . . 3 ((𝜑 ∧ ¬ 𝐿 = 1) → ((𝐿 − (4 / 3)) · 𝐸) < Σ𝑖 ∈ (0...𝑁)(𝐸 · ((𝑋𝑖)‘𝑆)))
561105, 560pm2.61dan 810 . 2 (𝜑 → ((𝐿 − (4 / 3)) · 𝐸) < Σ𝑖 ∈ (0...𝑁)(𝐸 · ((𝑋𝑖)‘𝑆)))
562 sumex 15399 . . 3 Σ𝑖 ∈ (0...𝑁)(𝐸 · ((𝑋𝑖)‘𝑆)) ∈ V
56393oveq2d 7291 . . . . 5 (𝑡 = 𝑆 → (𝐸 · ((𝑋𝑖)‘𝑡)) = (𝐸 · ((𝑋𝑖)‘𝑆)))
564563sumeq2sdv 15416 . . . 4 (𝑡 = 𝑆 → Σ𝑖 ∈ (0...𝑁)(𝐸 · ((𝑋𝑖)‘𝑡)) = Σ𝑖 ∈ (0...𝑁)(𝐸 · ((𝑋𝑖)‘𝑆)))
565 eqid 2738 . . . 4 (𝑡𝑇 ↦ Σ𝑖 ∈ (0...𝑁)(𝐸 · ((𝑋𝑖)‘𝑡))) = (𝑡𝑇 ↦ Σ𝑖 ∈ (0...𝑁)(𝐸 · ((𝑋𝑖)‘𝑡)))
566564, 565fvmptg 6873 . . 3 ((𝑆𝑇 ∧ Σ𝑖 ∈ (0...𝑁)(𝐸 · ((𝑋𝑖)‘𝑆)) ∈ V) → ((𝑡𝑇 ↦ Σ𝑖 ∈ (0...𝑁)(𝐸 · ((𝑋𝑖)‘𝑡)))‘𝑆) = Σ𝑖 ∈ (0...𝑁)(𝐸 · ((𝑋𝑖)‘𝑆)))
56749, 562, 566sylancl 586 . 2 (𝜑 → ((𝑡𝑇 ↦ Σ𝑖 ∈ (0...𝑁)(𝐸 · ((𝑋𝑖)‘𝑡)))‘𝑆) = Σ𝑖 ∈ (0...𝑁)(𝐸 · ((𝑋𝑖)‘𝑆)))
568561, 567breqtrrd 5102 1 (𝜑 → ((𝐿 − (4 / 3)) · 𝐸) < ((𝑡𝑇 ↦ Σ𝑖 ∈ (0...𝑁)(𝐸 · ((𝑋𝑖)‘𝑡)))‘𝑆))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 205  wa 396  wo 844  w3a 1086   = wceq 1539  wnf 1786  wcel 2106  wnfc 2887  wne 2943  wral 3064  {crab 3068  Vcvv 3432  cdif 3884  cun 3885  cin 3886  wss 3887  c0 4256   class class class wbr 5074  cmpt 5157  wf 6429  cfv 6433  (class class class)co 7275  Fincfn 8733  cc 10869  cr 10870  0cc0 10871  1c1 10872   + caddc 10874   · cmul 10876   < clt 11009  cle 11010  cmin 11205  -cneg 11206   / cdiv 11632  cn 11973  2c2 12028  3c3 12029  4c4 12030  0cn0 12233  cz 12319  cuz 12582  +crp 12730  ...cfz 13239  chash 14044  Σcsu 15397
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2709  ax-rep 5209  ax-sep 5223  ax-nul 5230  ax-pow 5288  ax-pr 5352  ax-un 7588  ax-inf2 9399  ax-cnex 10927  ax-resscn 10928  ax-1cn 10929  ax-icn 10930  ax-addcl 10931  ax-addrcl 10932  ax-mulcl 10933  ax-mulrcl 10934  ax-mulcom 10935  ax-addass 10936  ax-mulass 10937  ax-distr 10938  ax-i2m1 10939  ax-1ne0 10940  ax-1rid 10941  ax-rnegex 10942  ax-rrecex 10943  ax-cnre 10944  ax-pre-lttri 10945  ax-pre-lttrn 10946  ax-pre-ltadd 10947  ax-pre-mulgt0 10948  ax-pre-sup 10949
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3or 1087  df-3an 1088  df-tru 1542  df-fal 1552  df-ex 1783  df-nf 1787  df-sb 2068  df-mo 2540  df-eu 2569  df-clab 2716  df-cleq 2730  df-clel 2816  df-nfc 2889  df-ne 2944  df-nel 3050  df-ral 3069  df-rex 3070  df-rmo 3071  df-reu 3072  df-rab 3073  df-v 3434  df-sbc 3717  df-csb 3833  df-dif 3890  df-un 3892  df-in 3894  df-ss 3904  df-pss 3906  df-nul 4257  df-if 4460  df-pw 4535  df-sn 4562  df-pr 4564  df-op 4568  df-uni 4840  df-int 4880  df-iun 4926  df-br 5075  df-opab 5137  df-mpt 5158  df-tr 5192  df-id 5489  df-eprel 5495  df-po 5503  df-so 5504  df-fr 5544  df-se 5545  df-we 5546  df-xp 5595  df-rel 5596  df-cnv 5597  df-co 5598  df-dm 5599  df-rn 5600  df-res 5601  df-ima 5602  df-pred 6202  df-ord 6269  df-on 6270  df-lim 6271  df-suc 6272  df-iota 6391  df-fun 6435  df-fn 6436  df-f 6437  df-f1 6438  df-fo 6439  df-f1o 6440  df-fv 6441  df-isom 6442  df-riota 7232  df-ov 7278  df-oprab 7279  df-mpo 7280  df-om 7713  df-1st 7831  df-2nd 7832  df-frecs 8097  df-wrecs 8128  df-recs 8202  df-rdg 8241  df-1o 8297  df-er 8498  df-en 8734  df-dom 8735  df-sdom 8736  df-fin 8737  df-sup 9201  df-oi 9269  df-card 9697  df-pnf 11011  df-mnf 11012  df-xr 11013  df-ltxr 11014  df-le 11015  df-sub 11207  df-neg 11208  df-div 11633  df-nn 11974  df-2 12036  df-3 12037  df-4 12038  df-n0 12234  df-z 12320  df-uz 12583  df-rp 12731  df-ico 13085  df-fz 13240  df-fzo 13383  df-seq 13722  df-exp 13783  df-hash 14045  df-cj 14810  df-re 14811  df-im 14812  df-sqrt 14946  df-abs 14947  df-clim 15197  df-sum 15398
This theorem is referenced by:  stoweidlem34  43575
  Copyright terms: Public domain W3C validator