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 44341
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 11162 . . . . . . . 8 1 ∈ ℝ
2 eleq1 2826 . . . . . . . 8 (𝐿 = 1 β†’ (𝐿 ∈ ℝ ↔ 1 ∈ ℝ))
31, 2mpbiri 258 . . . . . . 7 (𝐿 = 1 β†’ 𝐿 ∈ ℝ)
43adantl 483 . . . . . 6 ((πœ‘ ∧ 𝐿 = 1) β†’ 𝐿 ∈ ℝ)
5 4re 12244 . . . . . . . 8 4 ∈ ℝ
65a1i 11 . . . . . . 7 ((πœ‘ ∧ 𝐿 = 1) β†’ 4 ∈ ℝ)
7 3re 12240 . . . . . . . 8 3 ∈ ℝ
87a1i 11 . . . . . . 7 ((πœ‘ ∧ 𝐿 = 1) β†’ 3 ∈ ℝ)
9 3ne0 12266 . . . . . . . 8 3 β‰  0
109a1i 11 . . . . . . 7 ((πœ‘ ∧ 𝐿 = 1) β†’ 3 β‰  0)
116, 8, 10redivcld 11990 . . . . . 6 ((πœ‘ ∧ 𝐿 = 1) β†’ (4 / 3) ∈ ℝ)
124, 11resubcld 11590 . . . . 5 ((πœ‘ ∧ 𝐿 = 1) β†’ (𝐿 βˆ’ (4 / 3)) ∈ ℝ)
13 stoweidlem26.11 . . . . . . 7 (πœ‘ β†’ 𝐸 ∈ ℝ+)
1413rpred 12964 . . . . . 6 (πœ‘ β†’ 𝐸 ∈ ℝ)
1514adantr 482 . . . . 5 ((πœ‘ ∧ 𝐿 = 1) β†’ 𝐸 ∈ ℝ)
1612, 15remulcld 11192 . . . 4 ((πœ‘ ∧ 𝐿 = 1) β†’ ((𝐿 βˆ’ (4 / 3)) Β· 𝐸) ∈ ℝ)
17 0red 11165 . . . 4 ((πœ‘ ∧ 𝐿 = 1) β†’ 0 ∈ ℝ)
18 fzfid 13885 . . . . . 6 (πœ‘ β†’ (0...𝑁) ∈ Fin)
1914adantr 482 . . . . . . 7 ((πœ‘ ∧ 𝑖 ∈ (0...𝑁)) β†’ 𝐸 ∈ ℝ)
20 stoweidlem26.13 . . . . . . . 8 ((πœ‘ ∧ 𝑖 ∈ (0...𝑁)) β†’ (π‘‹β€˜π‘–):π‘‡βŸΆβ„)
21 stoweidlem26.9 . . . . . . . . . . . . . 14 (πœ‘ β†’ 𝑆 ∈ ((π·β€˜πΏ) βˆ– (π·β€˜(𝐿 βˆ’ 1))))
22 eldif 3925 . . . . . . . . . . . . . 14 (𝑆 ∈ ((π·β€˜πΏ) βˆ– (π·β€˜(𝐿 βˆ’ 1))) ↔ (𝑆 ∈ (π·β€˜πΏ) ∧ Β¬ 𝑆 ∈ (π·β€˜(𝐿 βˆ’ 1))))
2321, 22sylib 217 . . . . . . . . . . . . 13 (πœ‘ β†’ (𝑆 ∈ (π·β€˜πΏ) ∧ Β¬ 𝑆 ∈ (π·β€˜(𝐿 βˆ’ 1))))
2423simpld 496 . . . . . . . . . . . 12 (πœ‘ β†’ 𝑆 ∈ (π·β€˜πΏ))
25 stoweidlem26.4 . . . . . . . . . . . . 13 𝐷 = (𝑗 ∈ (0...𝑁) ↦ {𝑑 ∈ 𝑇 ∣ (πΉβ€˜π‘‘) ≀ ((𝑗 βˆ’ (1 / 3)) Β· 𝐸)})
26 oveq1 7369 . . . . . . . . . . . . . . . 16 (𝑗 = 𝐿 β†’ (𝑗 βˆ’ (1 / 3)) = (𝐿 βˆ’ (1 / 3)))
2726oveq1d 7377 . . . . . . . . . . . . . . 15 (𝑗 = 𝐿 β†’ ((𝑗 βˆ’ (1 / 3)) Β· 𝐸) = ((𝐿 βˆ’ (1 / 3)) Β· 𝐸))
2827breq2d 5122 . . . . . . . . . . . . . 14 (𝑗 = 𝐿 β†’ ((πΉβ€˜π‘‘) ≀ ((𝑗 βˆ’ (1 / 3)) Β· 𝐸) ↔ (πΉβ€˜π‘‘) ≀ ((𝐿 βˆ’ (1 / 3)) Β· 𝐸)))
2928rabbidv 3418 . . . . . . . . . . . . 13 (𝑗 = 𝐿 β†’ {𝑑 ∈ 𝑇 ∣ (πΉβ€˜π‘‘) ≀ ((𝑗 βˆ’ (1 / 3)) Β· 𝐸)} = {𝑑 ∈ 𝑇 ∣ (πΉβ€˜π‘‘) ≀ ((𝐿 βˆ’ (1 / 3)) Β· 𝐸)})
30 fz1ssfz0 13544 . . . . . . . . . . . . . 14 (1...𝑁) βŠ† (0...𝑁)
31 stoweidlem26.8 . . . . . . . . . . . . . 14 (πœ‘ β†’ 𝐿 ∈ (1...𝑁))
3230, 31sselid 3947 . . . . . . . . . . . . 13 (πœ‘ β†’ 𝐿 ∈ (0...𝑁))
33 stoweidlem26.7 . . . . . . . . . . . . . 14 (πœ‘ β†’ 𝑇 ∈ V)
34 rabexg 5293 . . . . . . . . . . . . . 14 (𝑇 ∈ V β†’ {𝑑 ∈ 𝑇 ∣ (πΉβ€˜π‘‘) ≀ ((𝐿 βˆ’ (1 / 3)) Β· 𝐸)} ∈ V)
3533, 34syl 17 . . . . . . . . . . . . 13 (πœ‘ β†’ {𝑑 ∈ 𝑇 ∣ (πΉβ€˜π‘‘) ≀ ((𝐿 βˆ’ (1 / 3)) Β· 𝐸)} ∈ V)
3625, 29, 32, 35fvmptd3 6976 . . . . . . . . . . . 12 (πœ‘ β†’ (π·β€˜πΏ) = {𝑑 ∈ 𝑇 ∣ (πΉβ€˜π‘‘) ≀ ((𝐿 βˆ’ (1 / 3)) Β· 𝐸)})
3724, 36eleqtrd 2840 . . . . . . . . . . 11 (πœ‘ β†’ 𝑆 ∈ {𝑑 ∈ 𝑇 ∣ (πΉβ€˜π‘‘) ≀ ((𝐿 βˆ’ (1 / 3)) Β· 𝐸)})
38 nfcv 2908 . . . . . . . . . . . 12 Ⅎ𝑑𝑆
39 nfcv 2908 . . . . . . . . . . . 12 Ⅎ𝑑𝑇
40 stoweidlem26.1 . . . . . . . . . . . . . 14 Ⅎ𝑑𝐹
4140, 38nffv 6857 . . . . . . . . . . . . 13 Ⅎ𝑑(πΉβ€˜π‘†)
42 nfcv 2908 . . . . . . . . . . . . 13 Ⅎ𝑑 ≀
43 nfcv 2908 . . . . . . . . . . . . 13 Ⅎ𝑑((𝐿 βˆ’ (1 / 3)) Β· 𝐸)
4441, 42, 43nfbr 5157 . . . . . . . . . . . 12 Ⅎ𝑑(πΉβ€˜π‘†) ≀ ((𝐿 βˆ’ (1 / 3)) Β· 𝐸)
45 fveq2 6847 . . . . . . . . . . . . 13 (𝑑 = 𝑆 β†’ (πΉβ€˜π‘‘) = (πΉβ€˜π‘†))
4645breq1d 5120 . . . . . . . . . . . 12 (𝑑 = 𝑆 β†’ ((πΉβ€˜π‘‘) ≀ ((𝐿 βˆ’ (1 / 3)) Β· 𝐸) ↔ (πΉβ€˜π‘†) ≀ ((𝐿 βˆ’ (1 / 3)) Β· 𝐸)))
4738, 39, 44, 46elrabf 3646 . . . . . . . . . . 11 (𝑆 ∈ {𝑑 ∈ 𝑇 ∣ (πΉβ€˜π‘‘) ≀ ((𝐿 βˆ’ (1 / 3)) Β· 𝐸)} ↔ (𝑆 ∈ 𝑇 ∧ (πΉβ€˜π‘†) ≀ ((𝐿 βˆ’ (1 / 3)) Β· 𝐸)))
4837, 47sylib 217 . . . . . . . . . 10 (πœ‘ β†’ (𝑆 ∈ 𝑇 ∧ (πΉβ€˜π‘†) ≀ ((𝐿 βˆ’ (1 / 3)) Β· 𝐸)))
4948simpld 496 . . . . . . . . 9 (πœ‘ β†’ 𝑆 ∈ 𝑇)
5049adantr 482 . . . . . . . 8 ((πœ‘ ∧ 𝑖 ∈ (0...𝑁)) β†’ 𝑆 ∈ 𝑇)
5120, 50ffvelcdmd 7041 . . . . . . 7 ((πœ‘ ∧ 𝑖 ∈ (0...𝑁)) β†’ ((π‘‹β€˜π‘–)β€˜π‘†) ∈ ℝ)
5219, 51remulcld 11192 . . . . . 6 ((πœ‘ ∧ 𝑖 ∈ (0...𝑁)) β†’ (𝐸 Β· ((π‘‹β€˜π‘–)β€˜π‘†)) ∈ ℝ)
5318, 52fsumrecl 15626 . . . . 5 (πœ‘ β†’ Σ𝑖 ∈ (0...𝑁)(𝐸 Β· ((π‘‹β€˜π‘–)β€˜π‘†)) ∈ ℝ)
5453adantr 482 . . . 4 ((πœ‘ ∧ 𝐿 = 1) β†’ Σ𝑖 ∈ (0...𝑁)(𝐸 Β· ((π‘‹β€˜π‘–)β€˜π‘†)) ∈ ℝ)
555, 7, 9redivcli 11929 . . . . . . 7 (4 / 3) ∈ ℝ
5655a1i 11 . . . . . 6 ((πœ‘ ∧ 𝐿 = 1) β†’ (4 / 3) ∈ ℝ)
574, 56resubcld 11590 . . . . 5 ((πœ‘ ∧ 𝐿 = 1) β†’ (𝐿 βˆ’ (4 / 3)) ∈ ℝ)
584recnd 11190 . . . . . . . 8 ((πœ‘ ∧ 𝐿 = 1) β†’ 𝐿 ∈ β„‚)
5958subid1d 11508 . . . . . . 7 ((πœ‘ ∧ 𝐿 = 1) β†’ (𝐿 βˆ’ 0) = 𝐿)
60 3cn 12241 . . . . . . . . . 10 3 ∈ β„‚
6160, 9dividi 11895 . . . . . . . . 9 (3 / 3) = 1
62 3lt4 12334 . . . . . . . . . 10 3 < 4
63 3pos 12265 . . . . . . . . . . 11 0 < 3
647, 5, 7, 63ltdiv1ii 12091 . . . . . . . . . 10 (3 < 4 ↔ (3 / 3) < (4 / 3))
6562, 64mpbi 229 . . . . . . . . 9 (3 / 3) < (4 / 3)
6661, 65eqbrtrri 5133 . . . . . . . 8 1 < (4 / 3)
67 breq1 5113 . . . . . . . . 9 (𝐿 = 1 β†’ (𝐿 < (4 / 3) ↔ 1 < (4 / 3)))
6867adantl 483 . . . . . . . 8 ((πœ‘ ∧ 𝐿 = 1) β†’ (𝐿 < (4 / 3) ↔ 1 < (4 / 3)))
6966, 68mpbiri 258 . . . . . . 7 ((πœ‘ ∧ 𝐿 = 1) β†’ 𝐿 < (4 / 3))
7059, 69eqbrtrd 5132 . . . . . 6 ((πœ‘ ∧ 𝐿 = 1) β†’ (𝐿 βˆ’ 0) < (4 / 3))
714, 17, 56, 70ltsub23d 11767 . . . . 5 ((πœ‘ ∧ 𝐿 = 1) β†’ (𝐿 βˆ’ (4 / 3)) < 0)
7213rpgt0d 12967 . . . . . 6 (πœ‘ β†’ 0 < 𝐸)
7372adantr 482 . . . . 5 ((πœ‘ ∧ 𝐿 = 1) β†’ 0 < 𝐸)
74 mulltgt0 43301 . . . . 5 ((((𝐿 βˆ’ (4 / 3)) ∈ ℝ ∧ (𝐿 βˆ’ (4 / 3)) < 0) ∧ (𝐸 ∈ ℝ ∧ 0 < 𝐸)) β†’ ((𝐿 βˆ’ (4 / 3)) Β· 𝐸) < 0)
7557, 71, 15, 73, 74syl22anc 838 . . . 4 ((πœ‘ ∧ 𝐿 = 1) β†’ ((𝐿 βˆ’ (4 / 3)) Β· 𝐸) < 0)
76 0cn 11154 . . . . . . . 8 0 ∈ β„‚
77 fsumconst 15682 . . . . . . . 8 (((0...𝑁) ∈ Fin ∧ 0 ∈ β„‚) β†’ Σ𝑖 ∈ (0...𝑁)0 = ((β™―β€˜(0...𝑁)) Β· 0))
7818, 76, 77sylancl 587 . . . . . . 7 (πœ‘ β†’ Σ𝑖 ∈ (0...𝑁)0 = ((β™―β€˜(0...𝑁)) Β· 0))
79 hashcl 14263 . . . . . . . . 9 ((0...𝑁) ∈ Fin β†’ (β™―β€˜(0...𝑁)) ∈ β„•0)
80 nn0cn 12430 . . . . . . . . 9 ((β™―β€˜(0...𝑁)) ∈ β„•0 β†’ (β™―β€˜(0...𝑁)) ∈ β„‚)
8118, 79, 803syl 18 . . . . . . . 8 (πœ‘ β†’ (β™―β€˜(0...𝑁)) ∈ β„‚)
8281mul01d 11361 . . . . . . 7 (πœ‘ β†’ ((β™―β€˜(0...𝑁)) Β· 0) = 0)
8378, 82eqtrd 2777 . . . . . 6 (πœ‘ β†’ Σ𝑖 ∈ (0...𝑁)0 = 0)
8483adantr 482 . . . . 5 ((πœ‘ ∧ 𝐿 = 1) β†’ Σ𝑖 ∈ (0...𝑁)0 = 0)
85 0red 11165 . . . . . . 7 ((πœ‘ ∧ 𝑖 ∈ (0...𝑁)) β†’ 0 ∈ ℝ)
8613rpge0d 12968 . . . . . . . . 9 (πœ‘ β†’ 0 ≀ 𝐸)
8786adantr 482 . . . . . . . 8 ((πœ‘ ∧ 𝑖 ∈ (0...𝑁)) β†’ 0 ≀ 𝐸)
88 stoweidlem26.3 . . . . . . . . . . . 12 β„²π‘‘πœ‘
89 nfv 1918 . . . . . . . . . . . 12 Ⅎ𝑑 𝑖 ∈ (0...𝑁)
9088, 89nfan 1903 . . . . . . . . . . 11 Ⅎ𝑑(πœ‘ ∧ 𝑖 ∈ (0...𝑁))
91 nfv 1918 . . . . . . . . . . 11 Ⅎ𝑑0 ≀ ((π‘‹β€˜π‘–)β€˜π‘†)
9290, 91nfim 1900 . . . . . . . . . 10 Ⅎ𝑑((πœ‘ ∧ 𝑖 ∈ (0...𝑁)) β†’ 0 ≀ ((π‘‹β€˜π‘–)β€˜π‘†))
93 fveq2 6847 . . . . . . . . . . . 12 (𝑑 = 𝑆 β†’ ((π‘‹β€˜π‘–)β€˜π‘‘) = ((π‘‹β€˜π‘–)β€˜π‘†))
9493breq2d 5122 . . . . . . . . . . 11 (𝑑 = 𝑆 β†’ (0 ≀ ((π‘‹β€˜π‘–)β€˜π‘‘) ↔ 0 ≀ ((π‘‹β€˜π‘–)β€˜π‘†)))
9594imbi2d 341 . . . . . . . . . 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 3536 . . . . . . . . 9 (𝑆 ∈ 𝑇 β†’ ((πœ‘ ∧ 𝑖 ∈ (0...𝑁)) β†’ 0 ≀ ((π‘‹β€˜π‘–)β€˜π‘†)))
10050, 99mpcom 38 . . . . . . . 8 ((πœ‘ ∧ 𝑖 ∈ (0...𝑁)) β†’ 0 ≀ ((π‘‹β€˜π‘–)β€˜π‘†))
10119, 51, 87, 100mulge0d 11739 . . . . . . 7 ((πœ‘ ∧ 𝑖 ∈ (0...𝑁)) β†’ 0 ≀ (𝐸 Β· ((π‘‹β€˜π‘–)β€˜π‘†)))
10218, 85, 52, 101fsumle 15691 . . . . . 6 (πœ‘ β†’ Σ𝑖 ∈ (0...𝑁)0 ≀ Σ𝑖 ∈ (0...𝑁)(𝐸 Β· ((π‘‹β€˜π‘–)β€˜π‘†)))
103102adantr 482 . . . . 5 ((πœ‘ ∧ 𝐿 = 1) β†’ Σ𝑖 ∈ (0...𝑁)0 ≀ Σ𝑖 ∈ (0...𝑁)(𝐸 Β· ((π‘‹β€˜π‘–)β€˜π‘†)))
10484, 103eqbrtrrd 5134 . . . 4 ((πœ‘ ∧ 𝐿 = 1) β†’ 0 ≀ Σ𝑖 ∈ (0...𝑁)(𝐸 Β· ((π‘‹β€˜π‘–)β€˜π‘†)))
10516, 17, 54, 75, 104ltletrd 11322 . . 3 ((πœ‘ ∧ 𝐿 = 1) β†’ ((𝐿 βˆ’ (4 / 3)) Β· 𝐸) < Σ𝑖 ∈ (0...𝑁)(𝐸 Β· ((π‘‹β€˜π‘–)β€˜π‘†)))
106 elfzelz 13448 . . . . . . . . 9 (𝐿 ∈ (1...𝑁) β†’ 𝐿 ∈ β„€)
107 zre 12510 . . . . . . . . 9 (𝐿 ∈ β„€ β†’ 𝐿 ∈ ℝ)
10831, 106, 1073syl 18 . . . . . . . 8 (πœ‘ β†’ 𝐿 ∈ ℝ)
1095a1i 11 . . . . . . . . 9 (πœ‘ β†’ 4 ∈ ℝ)
1107a1i 11 . . . . . . . . 9 (πœ‘ β†’ 3 ∈ ℝ)
1119a1i 11 . . . . . . . . 9 (πœ‘ β†’ 3 β‰  0)
112109, 110, 111redivcld 11990 . . . . . . . 8 (πœ‘ β†’ (4 / 3) ∈ ℝ)
113108, 112resubcld 11590 . . . . . . 7 (πœ‘ β†’ (𝐿 βˆ’ (4 / 3)) ∈ ℝ)
114113, 14remulcld 11192 . . . . . 6 (πœ‘ β†’ ((𝐿 βˆ’ (4 / 3)) Β· 𝐸) ∈ ℝ)
115114adantr 482 . . . . 5 ((πœ‘ ∧ Β¬ 𝐿 = 1) β†’ ((𝐿 βˆ’ (4 / 3)) Β· 𝐸) ∈ ℝ)
1161a1i 11 . . . . . . . . 9 (πœ‘ β†’ 1 ∈ ℝ)
117 stoweidlem26.6 . . . . . . . . . 10 (πœ‘ β†’ 𝑁 ∈ β„•)
11814, 117nndivred 12214 . . . . . . . . 9 (πœ‘ β†’ (𝐸 / 𝑁) ∈ ℝ)
119116, 118resubcld 11590 . . . . . . . 8 (πœ‘ β†’ (1 βˆ’ (𝐸 / 𝑁)) ∈ ℝ)
120108, 116resubcld 11590 . . . . . . . 8 (πœ‘ β†’ (𝐿 βˆ’ 1) ∈ ℝ)
121119, 120remulcld 11192 . . . . . . 7 (πœ‘ β†’ ((1 βˆ’ (𝐸 / 𝑁)) Β· (𝐿 βˆ’ 1)) ∈ ℝ)
12214, 121remulcld 11192 . . . . . 6 (πœ‘ β†’ (𝐸 Β· ((1 βˆ’ (𝐸 / 𝑁)) Β· (𝐿 βˆ’ 1))) ∈ ℝ)
123122adantr 482 . . . . 5 ((πœ‘ ∧ Β¬ 𝐿 = 1) β†’ (𝐸 Β· ((1 βˆ’ (𝐸 / 𝑁)) Β· (𝐿 βˆ’ 1))) ∈ ℝ)
124 fzfid 13885 . . . . . . . 8 (πœ‘ β†’ (0...(𝐿 βˆ’ 2)) ∈ Fin)
12531elfzelzd 13449 . . . . . . . . . . . . . 14 (πœ‘ β†’ 𝐿 ∈ β„€)
126 2z 12542 . . . . . . . . . . . . . . 15 2 ∈ β„€
127126a1i 11 . . . . . . . . . . . . . 14 (πœ‘ β†’ 2 ∈ β„€)
128125, 127zsubcld 12619 . . . . . . . . . . . . 13 (πœ‘ β†’ (𝐿 βˆ’ 2) ∈ β„€)
129117nnzd 12533 . . . . . . . . . . . . 13 (πœ‘ β†’ 𝑁 ∈ β„€)
130125zred 12614 . . . . . . . . . . . . . . 15 (πœ‘ β†’ 𝐿 ∈ ℝ)
131 2re 12234 . . . . . . . . . . . . . . . 16 2 ∈ ℝ
132131a1i 11 . . . . . . . . . . . . . . 15 (πœ‘ β†’ 2 ∈ ℝ)
133130, 132resubcld 11590 . . . . . . . . . . . . . 14 (πœ‘ β†’ (𝐿 βˆ’ 2) ∈ ℝ)
134117nnred 12175 . . . . . . . . . . . . . 14 (πœ‘ β†’ 𝑁 ∈ ℝ)
135 0le2 12262 . . . . . . . . . . . . . . . 16 0 ≀ 2
136 0red 11165 . . . . . . . . . . . . . . . . 17 (πœ‘ β†’ 0 ∈ ℝ)
137136, 132, 130lesub2d 11770 . . . . . . . . . . . . . . . 16 (πœ‘ β†’ (0 ≀ 2 ↔ (𝐿 βˆ’ 2) ≀ (𝐿 βˆ’ 0)))
138135, 137mpbii 232 . . . . . . . . . . . . . . 15 (πœ‘ β†’ (𝐿 βˆ’ 2) ≀ (𝐿 βˆ’ 0))
139125zcnd 12615 . . . . . . . . . . . . . . . 16 (πœ‘ β†’ 𝐿 ∈ β„‚)
140139subid1d 11508 . . . . . . . . . . . . . . 15 (πœ‘ β†’ (𝐿 βˆ’ 0) = 𝐿)
141138, 140breqtrd 5136 . . . . . . . . . . . . . 14 (πœ‘ β†’ (𝐿 βˆ’ 2) ≀ 𝐿)
142 elfzle2 13452 . . . . . . . . . . . . . . 15 (𝐿 ∈ (1...𝑁) β†’ 𝐿 ≀ 𝑁)
14331, 142syl 17 . . . . . . . . . . . . . 14 (πœ‘ β†’ 𝐿 ≀ 𝑁)
144133, 130, 134, 141, 143letrd 11319 . . . . . . . . . . . . 13 (πœ‘ β†’ (𝐿 βˆ’ 2) ≀ 𝑁)
145128, 129, 1443jca 1129 . . . . . . . . . . . 12 (πœ‘ β†’ ((𝐿 βˆ’ 2) ∈ β„€ ∧ 𝑁 ∈ β„€ ∧ (𝐿 βˆ’ 2) ≀ 𝑁))
146 eluz2 12776 . . . . . . . . . . . 12 (𝑁 ∈ (β„€β‰₯β€˜(𝐿 βˆ’ 2)) ↔ ((𝐿 βˆ’ 2) ∈ β„€ ∧ 𝑁 ∈ β„€ ∧ (𝐿 βˆ’ 2) ≀ 𝑁))
147145, 146sylibr 233 . . . . . . . . . . 11 (πœ‘ β†’ 𝑁 ∈ (β„€β‰₯β€˜(𝐿 βˆ’ 2)))
148 fzss2 13488 . . . . . . . . . . 11 (𝑁 ∈ (β„€β‰₯β€˜(𝐿 βˆ’ 2)) β†’ (0...(𝐿 βˆ’ 2)) βŠ† (0...𝑁))
149147, 148syl 17 . . . . . . . . . 10 (πœ‘ β†’ (0...(𝐿 βˆ’ 2)) βŠ† (0...𝑁))
150149sselda 3949 . . . . . . . . 9 ((πœ‘ ∧ 𝑖 ∈ (0...(𝐿 βˆ’ 2))) β†’ 𝑖 ∈ (0...𝑁))
151150, 51syldan 592 . . . . . . . 8 ((πœ‘ ∧ 𝑖 ∈ (0...(𝐿 βˆ’ 2))) β†’ ((π‘‹β€˜π‘–)β€˜π‘†) ∈ ℝ)
152124, 151fsumrecl 15626 . . . . . . 7 (πœ‘ β†’ Σ𝑖 ∈ (0...(𝐿 βˆ’ 2))((π‘‹β€˜π‘–)β€˜π‘†) ∈ ℝ)
15314, 152remulcld 11192 . . . . . 6 (πœ‘ β†’ (𝐸 Β· Σ𝑖 ∈ (0...(𝐿 βˆ’ 2))((π‘‹β€˜π‘–)β€˜π‘†)) ∈ ℝ)
154153adantr 482 . . . . 5 ((πœ‘ ∧ Β¬ 𝐿 = 1) β†’ (𝐸 Β· Σ𝑖 ∈ (0...(𝐿 βˆ’ 2))((π‘‹β€˜π‘–)β€˜π‘†)) ∈ ℝ)
15514, 120remulcld 11192 . . . . . . . . 9 (πœ‘ β†’ (𝐸 Β· (𝐿 βˆ’ 1)) ∈ ℝ)
15614, 14remulcld 11192 . . . . . . . . 9 (πœ‘ β†’ (𝐸 Β· 𝐸) ∈ ℝ)
157155, 156resubcld 11590 . . . . . . . 8 (πœ‘ β†’ ((𝐸 Β· (𝐿 βˆ’ 1)) βˆ’ (𝐸 Β· 𝐸)) ∈ ℝ)
158120, 117nndivred 12214 . . . . . . . . . 10 (πœ‘ β†’ ((𝐿 βˆ’ 1) / 𝑁) ∈ ℝ)
159156, 158remulcld 11192 . . . . . . . . 9 (πœ‘ β†’ ((𝐸 Β· 𝐸) Β· ((𝐿 βˆ’ 1) / 𝑁)) ∈ ℝ)
160155, 159resubcld 11590 . . . . . . . 8 (πœ‘ β†’ ((𝐸 Β· (𝐿 βˆ’ 1)) βˆ’ ((𝐸 Β· 𝐸) Β· ((𝐿 βˆ’ 1) / 𝑁))) ∈ ℝ)
161120, 14resubcld 11590 . . . . . . . . . 10 (πœ‘ β†’ ((𝐿 βˆ’ 1) βˆ’ 𝐸) ∈ ℝ)
162116, 14readdcld 11191 . . . . . . . . . . . 12 (πœ‘ β†’ (1 + 𝐸) ∈ ℝ)
1631, 7, 9redivcli 11929 . . . . . . . . . . . . . . 15 (1 / 3) ∈ ℝ
164163a1i 11 . . . . . . . . . . . . . 14 (πœ‘ β†’ (1 / 3) ∈ ℝ)
165 stoweidlem26.12 . . . . . . . . . . . . . 14 (πœ‘ β†’ 𝐸 < (1 / 3))
16614, 164, 116, 165ltadd2dd 11321 . . . . . . . . . . . . 13 (πœ‘ β†’ (1 + 𝐸) < (1 + (1 / 3)))
167 ax-1cn 11116 . . . . . . . . . . . . . . 15 1 ∈ β„‚
16860, 167, 60, 9divdiri 11919 . . . . . . . . . . . . . 14 ((3 + 1) / 3) = ((3 / 3) + (1 / 3))
169 3p1e4 12305 . . . . . . . . . . . . . . 15 (3 + 1) = 4
170169oveq1i 7372 . . . . . . . . . . . . . 14 ((3 + 1) / 3) = (4 / 3)
17161oveq1i 7372 . . . . . . . . . . . . . 14 ((3 / 3) + (1 / 3)) = (1 + (1 / 3))
172168, 170, 1713eqtr3ri 2774 . . . . . . . . . . . . 13 (1 + (1 / 3)) = (4 / 3)
173166, 172breqtrdi 5151 . . . . . . . . . . . 12 (πœ‘ β†’ (1 + 𝐸) < (4 / 3))
174162, 112, 108, 173ltsub2dd 11775 . . . . . . . . . . 11 (πœ‘ β†’ (𝐿 βˆ’ (4 / 3)) < (𝐿 βˆ’ (1 + 𝐸)))
175167a1i 11 . . . . . . . . . . . 12 (πœ‘ β†’ 1 ∈ β„‚)
17613rpcnd 12966 . . . . . . . . . . . 12 (πœ‘ β†’ 𝐸 ∈ β„‚)
177139, 175, 176subsub4d 11550 . . . . . . . . . . 11 (πœ‘ β†’ ((𝐿 βˆ’ 1) βˆ’ 𝐸) = (𝐿 βˆ’ (1 + 𝐸)))
178174, 177breqtrrd 5138 . . . . . . . . . 10 (πœ‘ β†’ (𝐿 βˆ’ (4 / 3)) < ((𝐿 βˆ’ 1) βˆ’ 𝐸))
179113, 161, 13, 178ltmul1dd 13019 . . . . . . . . 9 (πœ‘ β†’ ((𝐿 βˆ’ (4 / 3)) Β· 𝐸) < (((𝐿 βˆ’ 1) βˆ’ 𝐸) Β· 𝐸))
180139, 175subcld 11519 . . . . . . . . . . . 12 (πœ‘ β†’ (𝐿 βˆ’ 1) ∈ β„‚)
181180, 176subcld 11519 . . . . . . . . . . 11 (πœ‘ β†’ ((𝐿 βˆ’ 1) βˆ’ 𝐸) ∈ β„‚)
182176, 181mulcomd 11183 . . . . . . . . . 10 (πœ‘ β†’ (𝐸 Β· ((𝐿 βˆ’ 1) βˆ’ 𝐸)) = (((𝐿 βˆ’ 1) βˆ’ 𝐸) Β· 𝐸))
183176, 180, 176subdid 11618 . . . . . . . . . 10 (πœ‘ β†’ (𝐸 Β· ((𝐿 βˆ’ 1) βˆ’ 𝐸)) = ((𝐸 Β· (𝐿 βˆ’ 1)) βˆ’ (𝐸 Β· 𝐸)))
184182, 183eqtr3d 2779 . . . . . . . . 9 (πœ‘ β†’ (((𝐿 βˆ’ 1) βˆ’ 𝐸) Β· 𝐸) = ((𝐸 Β· (𝐿 βˆ’ 1)) βˆ’ (𝐸 Β· 𝐸)))
185179, 184breqtrd 5136 . . . . . . . 8 (πœ‘ β†’ ((𝐿 βˆ’ (4 / 3)) Β· 𝐸) < ((𝐸 Β· (𝐿 βˆ’ 1)) βˆ’ (𝐸 Β· 𝐸)))
186 1zzd 12541 . . . . . . . . . . . . . . . . 17 (πœ‘ β†’ 1 ∈ β„€)
187 elfz 13437 . . . . . . . . . . . . . . . . 17 ((𝐿 ∈ β„€ ∧ 1 ∈ β„€ ∧ 𝑁 ∈ β„€) β†’ (𝐿 ∈ (1...𝑁) ↔ (1 ≀ 𝐿 ∧ 𝐿 ≀ 𝑁)))
188125, 186, 129, 187syl3anc 1372 . . . . . . . . . . . . . . . 16 (πœ‘ β†’ (𝐿 ∈ (1...𝑁) ↔ (1 ≀ 𝐿 ∧ 𝐿 ≀ 𝑁)))
18931, 188mpbid 231 . . . . . . . . . . . . . . 15 (πœ‘ β†’ (1 ≀ 𝐿 ∧ 𝐿 ≀ 𝑁))
190189simprd 497 . . . . . . . . . . . . . 14 (πœ‘ β†’ 𝐿 ≀ 𝑁)
191 zlem1lt 12562 . . . . . . . . . . . . . . 15 ((𝐿 ∈ β„€ ∧ 𝑁 ∈ β„€) β†’ (𝐿 ≀ 𝑁 ↔ (𝐿 βˆ’ 1) < 𝑁))
192125, 129, 191syl2anc 585 . . . . . . . . . . . . . 14 (πœ‘ β†’ (𝐿 ≀ 𝑁 ↔ (𝐿 βˆ’ 1) < 𝑁))
193190, 192mpbid 231 . . . . . . . . . . . . 13 (πœ‘ β†’ (𝐿 βˆ’ 1) < 𝑁)
194117nngt0d 12209 . . . . . . . . . . . . . 14 (πœ‘ β†’ 0 < 𝑁)
195 ltdiv1 12026 . . . . . . . . . . . . . 14 (((𝐿 βˆ’ 1) ∈ ℝ ∧ 𝑁 ∈ ℝ ∧ (𝑁 ∈ ℝ ∧ 0 < 𝑁)) β†’ ((𝐿 βˆ’ 1) < 𝑁 ↔ ((𝐿 βˆ’ 1) / 𝑁) < (𝑁 / 𝑁)))
196120, 134, 134, 194, 195syl112anc 1375 . . . . . . . . . . . . 13 (πœ‘ β†’ ((𝐿 βˆ’ 1) < 𝑁 ↔ ((𝐿 βˆ’ 1) / 𝑁) < (𝑁 / 𝑁)))
197193, 196mpbid 231 . . . . . . . . . . . 12 (πœ‘ β†’ ((𝐿 βˆ’ 1) / 𝑁) < (𝑁 / 𝑁))
198117nncnd 12176 . . . . . . . . . . . . 13 (πœ‘ β†’ 𝑁 ∈ β„‚)
199117nnne0d 12210 . . . . . . . . . . . . 13 (πœ‘ β†’ 𝑁 β‰  0)
200198, 199dividd 11936 . . . . . . . . . . . 12 (πœ‘ β†’ (𝑁 / 𝑁) = 1)
201197, 200breqtrd 5136 . . . . . . . . . . 11 (πœ‘ β†’ ((𝐿 βˆ’ 1) / 𝑁) < 1)
20214, 14, 72, 72mulgt0d 11317 . . . . . . . . . . . 12 (πœ‘ β†’ 0 < (𝐸 Β· 𝐸))
203 ltmul2 12013 . . . . . . . . . . . 12 ((((𝐿 βˆ’ 1) / 𝑁) ∈ ℝ ∧ 1 ∈ ℝ ∧ ((𝐸 Β· 𝐸) ∈ ℝ ∧ 0 < (𝐸 Β· 𝐸))) β†’ (((𝐿 βˆ’ 1) / 𝑁) < 1 ↔ ((𝐸 Β· 𝐸) Β· ((𝐿 βˆ’ 1) / 𝑁)) < ((𝐸 Β· 𝐸) Β· 1)))
204158, 116, 156, 202, 203syl112anc 1375 . . . . . . . . . . 11 (πœ‘ β†’ (((𝐿 βˆ’ 1) / 𝑁) < 1 ↔ ((𝐸 Β· 𝐸) Β· ((𝐿 βˆ’ 1) / 𝑁)) < ((𝐸 Β· 𝐸) Β· 1)))
205201, 204mpbid 231 . . . . . . . . . 10 (πœ‘ β†’ ((𝐸 Β· 𝐸) Β· ((𝐿 βˆ’ 1) / 𝑁)) < ((𝐸 Β· 𝐸) Β· 1))
206176, 176mulcld 11182 . . . . . . . . . . 11 (πœ‘ β†’ (𝐸 Β· 𝐸) ∈ β„‚)
207206mulid1d 11179 . . . . . . . . . 10 (πœ‘ β†’ ((𝐸 Β· 𝐸) Β· 1) = (𝐸 Β· 𝐸))
208205, 207breqtrd 5136 . . . . . . . . 9 (πœ‘ β†’ ((𝐸 Β· 𝐸) Β· ((𝐿 βˆ’ 1) / 𝑁)) < (𝐸 Β· 𝐸))
209159, 156, 155, 208ltsub2dd 11775 . . . . . . . 8 (πœ‘ β†’ ((𝐸 Β· (𝐿 βˆ’ 1)) βˆ’ (𝐸 Β· 𝐸)) < ((𝐸 Β· (𝐿 βˆ’ 1)) βˆ’ ((𝐸 Β· 𝐸) Β· ((𝐿 βˆ’ 1) / 𝑁))))
210114, 157, 160, 185, 209lttrd 11323 . . . . . . 7 (πœ‘ β†’ ((𝐿 βˆ’ (4 / 3)) Β· 𝐸) < ((𝐸 Β· (𝐿 βˆ’ 1)) βˆ’ ((𝐸 Β· 𝐸) Β· ((𝐿 βˆ’ 1) / 𝑁))))
211176, 198, 199divcld 11938 . . . . . . . . . . 11 (πœ‘ β†’ (𝐸 / 𝑁) ∈ β„‚)
212175, 211, 180subdird 11619 . . . . . . . . . 10 (πœ‘ β†’ ((1 βˆ’ (𝐸 / 𝑁)) Β· (𝐿 βˆ’ 1)) = ((1 Β· (𝐿 βˆ’ 1)) βˆ’ ((𝐸 / 𝑁) Β· (𝐿 βˆ’ 1))))
213180mulid2d 11180 . . . . . . . . . . 11 (πœ‘ β†’ (1 Β· (𝐿 βˆ’ 1)) = (𝐿 βˆ’ 1))
214213oveq1d 7377 . . . . . . . . . 10 (πœ‘ β†’ ((1 Β· (𝐿 βˆ’ 1)) βˆ’ ((𝐸 / 𝑁) Β· (𝐿 βˆ’ 1))) = ((𝐿 βˆ’ 1) βˆ’ ((𝐸 / 𝑁) Β· (𝐿 βˆ’ 1))))
215212, 214eqtrd 2777 . . . . . . . . 9 (πœ‘ β†’ ((1 βˆ’ (𝐸 / 𝑁)) Β· (𝐿 βˆ’ 1)) = ((𝐿 βˆ’ 1) βˆ’ ((𝐸 / 𝑁) Β· (𝐿 βˆ’ 1))))
216215oveq2d 7378 . . . . . . . 8 (πœ‘ β†’ (𝐸 Β· ((1 βˆ’ (𝐸 / 𝑁)) Β· (𝐿 βˆ’ 1))) = (𝐸 Β· ((𝐿 βˆ’ 1) βˆ’ ((𝐸 / 𝑁) Β· (𝐿 βˆ’ 1)))))
217211, 180mulcld 11182 . . . . . . . . 9 (πœ‘ β†’ ((𝐸 / 𝑁) Β· (𝐿 βˆ’ 1)) ∈ β„‚)
218176, 180, 217subdid 11618 . . . . . . . 8 (πœ‘ β†’ (𝐸 Β· ((𝐿 βˆ’ 1) βˆ’ ((𝐸 / 𝑁) Β· (𝐿 βˆ’ 1)))) = ((𝐸 Β· (𝐿 βˆ’ 1)) βˆ’ (𝐸 Β· ((𝐸 / 𝑁) Β· (𝐿 βˆ’ 1)))))
219176, 198, 180, 199div32d 11961 . . . . . . . . . . 11 (πœ‘ β†’ ((𝐸 / 𝑁) Β· (𝐿 βˆ’ 1)) = (𝐸 Β· ((𝐿 βˆ’ 1) / 𝑁)))
220219oveq2d 7378 . . . . . . . . . 10 (πœ‘ β†’ (𝐸 Β· ((𝐸 / 𝑁) Β· (𝐿 βˆ’ 1))) = (𝐸 Β· (𝐸 Β· ((𝐿 βˆ’ 1) / 𝑁))))
221180, 198, 199divcld 11938 . . . . . . . . . . 11 (πœ‘ β†’ ((𝐿 βˆ’ 1) / 𝑁) ∈ β„‚)
222176, 176, 221mulassd 11185 . . . . . . . . . 10 (πœ‘ β†’ ((𝐸 Β· 𝐸) Β· ((𝐿 βˆ’ 1) / 𝑁)) = (𝐸 Β· (𝐸 Β· ((𝐿 βˆ’ 1) / 𝑁))))
223220, 222eqtr4d 2780 . . . . . . . . 9 (πœ‘ β†’ (𝐸 Β· ((𝐸 / 𝑁) Β· (𝐿 βˆ’ 1))) = ((𝐸 Β· 𝐸) Β· ((𝐿 βˆ’ 1) / 𝑁)))
224223oveq2d 7378 . . . . . . . 8 (πœ‘ β†’ ((𝐸 Β· (𝐿 βˆ’ 1)) βˆ’ (𝐸 Β· ((𝐸 / 𝑁) Β· (𝐿 βˆ’ 1)))) = ((𝐸 Β· (𝐿 βˆ’ 1)) βˆ’ ((𝐸 Β· 𝐸) Β· ((𝐿 βˆ’ 1) / 𝑁))))
225216, 218, 2243eqtrd 2781 . . . . . . 7 (πœ‘ β†’ (𝐸 Β· ((1 βˆ’ (𝐸 / 𝑁)) Β· (𝐿 βˆ’ 1))) = ((𝐸 Β· (𝐿 βˆ’ 1)) βˆ’ ((𝐸 Β· 𝐸) Β· ((𝐿 βˆ’ 1) / 𝑁))))
226210, 225breqtrrd 5138 . . . . . 6 (πœ‘ β†’ ((𝐿 βˆ’ (4 / 3)) Β· 𝐸) < (𝐸 Β· ((1 βˆ’ (𝐸 / 𝑁)) Β· (𝐿 βˆ’ 1))))
227226adantr 482 . . . . 5 ((πœ‘ ∧ Β¬ 𝐿 = 1) β†’ ((𝐿 βˆ’ (4 / 3)) Β· 𝐸) < (𝐸 Β· ((1 βˆ’ (𝐸 / 𝑁)) Β· (𝐿 βˆ’ 1))))
228175, 211subcld 11519 . . . . . . . . . 10 (πœ‘ β†’ (1 βˆ’ (𝐸 / 𝑁)) ∈ β„‚)
229 fsumconst 15682 . . . . . . . . . 10 (((0...(𝐿 βˆ’ 2)) ∈ Fin ∧ (1 βˆ’ (𝐸 / 𝑁)) ∈ β„‚) β†’ Σ𝑖 ∈ (0...(𝐿 βˆ’ 2))(1 βˆ’ (𝐸 / 𝑁)) = ((β™―β€˜(0...(𝐿 βˆ’ 2))) Β· (1 βˆ’ (𝐸 / 𝑁))))
230124, 228, 229syl2anc 585 . . . . . . . . 9 (πœ‘ β†’ Σ𝑖 ∈ (0...(𝐿 βˆ’ 2))(1 βˆ’ (𝐸 / 𝑁)) = ((β™―β€˜(0...(𝐿 βˆ’ 2))) Β· (1 βˆ’ (𝐸 / 𝑁))))
231230adantr 482 . . . . . . . 8 ((πœ‘ ∧ Β¬ 𝐿 = 1) β†’ Σ𝑖 ∈ (0...(𝐿 βˆ’ 2))(1 βˆ’ (𝐸 / 𝑁)) = ((β™―β€˜(0...(𝐿 βˆ’ 2))) Β· (1 βˆ’ (𝐸 / 𝑁))))
232 0zd 12518 . . . . . . . . . . . . 13 ((πœ‘ ∧ Β¬ 𝐿 = 1) β†’ 0 ∈ β„€)
23331adantr 482 . . . . . . . . . . . . . . 15 ((πœ‘ ∧ Β¬ 𝐿 = 1) β†’ 𝐿 ∈ (1...𝑁))
234233elfzelzd 13449 . . . . . . . . . . . . . 14 ((πœ‘ ∧ Β¬ 𝐿 = 1) β†’ 𝐿 ∈ β„€)
235126a1i 11 . . . . . . . . . . . . . 14 ((πœ‘ ∧ Β¬ 𝐿 = 1) β†’ 2 ∈ β„€)
236234, 235zsubcld 12619 . . . . . . . . . . . . 13 ((πœ‘ ∧ Β¬ 𝐿 = 1) β†’ (𝐿 βˆ’ 2) ∈ β„€)
237 elnnuz 12814 . . . . . . . . . . . . . . . . . . . 20 (𝑁 ∈ β„• ↔ 𝑁 ∈ (β„€β‰₯β€˜1))
238117, 237sylib 217 . . . . . . . . . . . . . . . . . . 19 (πœ‘ β†’ 𝑁 ∈ (β„€β‰₯β€˜1))
239 elfzp12 13527 . . . . . . . . . . . . . . . . . . 19 (𝑁 ∈ (β„€β‰₯β€˜1) β†’ (𝐿 ∈ (1...𝑁) ↔ (𝐿 = 1 ∨ 𝐿 ∈ ((1 + 1)...𝑁))))
240238, 239syl 17 . . . . . . . . . . . . . . . . . 18 (πœ‘ β†’ (𝐿 ∈ (1...𝑁) ↔ (𝐿 = 1 ∨ 𝐿 ∈ ((1 + 1)...𝑁))))
24131, 240mpbid 231 . . . . . . . . . . . . . . . . 17 (πœ‘ β†’ (𝐿 = 1 ∨ 𝐿 ∈ ((1 + 1)...𝑁)))
242241orcanai 1002 . . . . . . . . . . . . . . . 16 ((πœ‘ ∧ Β¬ 𝐿 = 1) β†’ 𝐿 ∈ ((1 + 1)...𝑁))
243 1p1e2 12285 . . . . . . . . . . . . . . . . . 18 (1 + 1) = 2
244243a1i 11 . . . . . . . . . . . . . . . . 17 ((πœ‘ ∧ Β¬ 𝐿 = 1) β†’ (1 + 1) = 2)
245244oveq1d 7377 . . . . . . . . . . . . . . . 16 ((πœ‘ ∧ Β¬ 𝐿 = 1) β†’ ((1 + 1)...𝑁) = (2...𝑁))
246242, 245eleqtrd 2840 . . . . . . . . . . . . . . 15 ((πœ‘ ∧ Β¬ 𝐿 = 1) β†’ 𝐿 ∈ (2...𝑁))
247 elfzle1 13451 . . . . . . . . . . . . . . 15 (𝐿 ∈ (2...𝑁) β†’ 2 ≀ 𝐿)
248246, 247syl 17 . . . . . . . . . . . . . 14 ((πœ‘ ∧ Β¬ 𝐿 = 1) β†’ 2 ≀ 𝐿)
249108adantr 482 . . . . . . . . . . . . . . 15 ((πœ‘ ∧ Β¬ 𝐿 = 1) β†’ 𝐿 ∈ ℝ)
250131a1i 11 . . . . . . . . . . . . . . 15 ((πœ‘ ∧ Β¬ 𝐿 = 1) β†’ 2 ∈ ℝ)
251249, 250subge0d 11752 . . . . . . . . . . . . . 14 ((πœ‘ ∧ Β¬ 𝐿 = 1) β†’ (0 ≀ (𝐿 βˆ’ 2) ↔ 2 ≀ 𝐿))
252248, 251mpbird 257 . . . . . . . . . . . . 13 ((πœ‘ ∧ Β¬ 𝐿 = 1) β†’ 0 ≀ (𝐿 βˆ’ 2))
253232, 236, 2523jca 1129 . . . . . . . . . . . 12 ((πœ‘ ∧ Β¬ 𝐿 = 1) β†’ (0 ∈ β„€ ∧ (𝐿 βˆ’ 2) ∈ β„€ ∧ 0 ≀ (𝐿 βˆ’ 2)))
254 eluz2 12776 . . . . . . . . . . . 12 ((𝐿 βˆ’ 2) ∈ (β„€β‰₯β€˜0) ↔ (0 ∈ β„€ ∧ (𝐿 βˆ’ 2) ∈ β„€ ∧ 0 ≀ (𝐿 βˆ’ 2)))
255253, 254sylibr 233 . . . . . . . . . . 11 ((πœ‘ ∧ Β¬ 𝐿 = 1) β†’ (𝐿 βˆ’ 2) ∈ (β„€β‰₯β€˜0))
256 hashfz 14334 . . . . . . . . . . 11 ((𝐿 βˆ’ 2) ∈ (β„€β‰₯β€˜0) β†’ (β™―β€˜(0...(𝐿 βˆ’ 2))) = (((𝐿 βˆ’ 2) βˆ’ 0) + 1))
257255, 256syl 17 . . . . . . . . . 10 ((πœ‘ ∧ Β¬ 𝐿 = 1) β†’ (β™―β€˜(0...(𝐿 βˆ’ 2))) = (((𝐿 βˆ’ 2) βˆ’ 0) + 1))
258 2cn 12235 . . . . . . . . . . . . . . . 16 2 ∈ β„‚
259258a1i 11 . . . . . . . . . . . . . . 15 (πœ‘ β†’ 2 ∈ β„‚)
260139, 259subcld 11519 . . . . . . . . . . . . . 14 (πœ‘ β†’ (𝐿 βˆ’ 2) ∈ β„‚)
261260subid1d 11508 . . . . . . . . . . . . 13 (πœ‘ β†’ ((𝐿 βˆ’ 2) βˆ’ 0) = (𝐿 βˆ’ 2))
262261oveq1d 7377 . . . . . . . . . . . 12 (πœ‘ β†’ (((𝐿 βˆ’ 2) βˆ’ 0) + 1) = ((𝐿 βˆ’ 2) + 1))
263139, 259, 175subadd23d 11541 . . . . . . . . . . . 12 (πœ‘ β†’ ((𝐿 βˆ’ 2) + 1) = (𝐿 + (1 βˆ’ 2)))
264258, 167negsubdi2i 11494 . . . . . . . . . . . . . . . 16 -(2 βˆ’ 1) = (1 βˆ’ 2)
265 2m1e1 12286 . . . . . . . . . . . . . . . . 17 (2 βˆ’ 1) = 1
266265negeqi 11401 . . . . . . . . . . . . . . . 16 -(2 βˆ’ 1) = -1
267264, 266eqtr3i 2767 . . . . . . . . . . . . . . 15 (1 βˆ’ 2) = -1
268267a1i 11 . . . . . . . . . . . . . 14 (πœ‘ β†’ (1 βˆ’ 2) = -1)
269268oveq2d 7378 . . . . . . . . . . . . 13 (πœ‘ β†’ (𝐿 + (1 βˆ’ 2)) = (𝐿 + -1))
270139, 175negsubd 11525 . . . . . . . . . . . . 13 (πœ‘ β†’ (𝐿 + -1) = (𝐿 βˆ’ 1))
271269, 270eqtrd 2777 . . . . . . . . . . . 12 (πœ‘ β†’ (𝐿 + (1 βˆ’ 2)) = (𝐿 βˆ’ 1))
272262, 263, 2713eqtrd 2781 . . . . . . . . . . 11 (πœ‘ β†’ (((𝐿 βˆ’ 2) βˆ’ 0) + 1) = (𝐿 βˆ’ 1))
273272adantr 482 . . . . . . . . . 10 ((πœ‘ ∧ Β¬ 𝐿 = 1) β†’ (((𝐿 βˆ’ 2) βˆ’ 0) + 1) = (𝐿 βˆ’ 1))
274257, 273eqtrd 2777 . . . . . . . . 9 ((πœ‘ ∧ Β¬ 𝐿 = 1) β†’ (β™―β€˜(0...(𝐿 βˆ’ 2))) = (𝐿 βˆ’ 1))
275274oveq1d 7377 . . . . . . . 8 ((πœ‘ ∧ Β¬ 𝐿 = 1) β†’ ((β™―β€˜(0...(𝐿 βˆ’ 2))) Β· (1 βˆ’ (𝐸 / 𝑁))) = ((𝐿 βˆ’ 1) Β· (1 βˆ’ (𝐸 / 𝑁))))
276180, 228mulcomd 11183 . . . . . . . . 9 (πœ‘ β†’ ((𝐿 βˆ’ 1) Β· (1 βˆ’ (𝐸 / 𝑁))) = ((1 βˆ’ (𝐸 / 𝑁)) Β· (𝐿 βˆ’ 1)))
277276adantr 482 . . . . . . . 8 ((πœ‘ ∧ Β¬ 𝐿 = 1) β†’ ((𝐿 βˆ’ 1) Β· (1 βˆ’ (𝐸 / 𝑁))) = ((1 βˆ’ (𝐸 / 𝑁)) Β· (𝐿 βˆ’ 1)))
278231, 275, 2773eqtrd 2781 . . . . . . 7 ((πœ‘ ∧ Β¬ 𝐿 = 1) β†’ Σ𝑖 ∈ (0...(𝐿 βˆ’ 2))(1 βˆ’ (𝐸 / 𝑁)) = ((1 βˆ’ (𝐸 / 𝑁)) Β· (𝐿 βˆ’ 1)))
279 fzfid 13885 . . . . . . . 8 ((πœ‘ ∧ Β¬ 𝐿 = 1) β†’ (0...(𝐿 βˆ’ 2)) ∈ Fin)
280 fzn0 13462 . . . . . . . . 9 ((0...(𝐿 βˆ’ 2)) β‰  βˆ… ↔ (𝐿 βˆ’ 2) ∈ (β„€β‰₯β€˜0))
281255, 280sylibr 233 . . . . . . . 8 ((πœ‘ ∧ Β¬ 𝐿 = 1) β†’ (0...(𝐿 βˆ’ 2)) β‰  βˆ…)
282119ad2antrr 725 . . . . . . . 8 (((πœ‘ ∧ Β¬ 𝐿 = 1) ∧ 𝑖 ∈ (0...(𝐿 βˆ’ 2))) β†’ (1 βˆ’ (𝐸 / 𝑁)) ∈ ℝ)
283 simpll 766 . . . . . . . . 9 (((πœ‘ ∧ Β¬ 𝐿 = 1) ∧ 𝑖 ∈ (0...(𝐿 βˆ’ 2))) β†’ πœ‘)
284150adantlr 714 . . . . . . . . 9 (((πœ‘ ∧ Β¬ 𝐿 = 1) ∧ 𝑖 ∈ (0...(𝐿 βˆ’ 2))) β†’ 𝑖 ∈ (0...𝑁))
285283, 284, 51syl2anc 585 . . . . . . . 8 (((πœ‘ ∧ Β¬ 𝐿 = 1) ∧ 𝑖 ∈ (0...(𝐿 βˆ’ 2))) β†’ ((π‘‹β€˜π‘–)β€˜π‘†) ∈ ℝ)
28649adantr 482 . . . . . . . . . . . 12 ((πœ‘ ∧ 𝑖 ∈ (0...(𝐿 βˆ’ 2))) β†’ 𝑆 ∈ 𝑇)
287 elfzelz 13448 . . . . . . . . . . . . . . . . 17 (𝑖 ∈ (0...(𝐿 βˆ’ 2)) β†’ 𝑖 ∈ β„€)
288287zred 12614 . . . . . . . . . . . . . . . 16 (𝑖 ∈ (0...(𝐿 βˆ’ 2)) β†’ 𝑖 ∈ ℝ)
289288adantl 483 . . . . . . . . . . . . . . 15 ((πœ‘ ∧ 𝑖 ∈ (0...(𝐿 βˆ’ 2))) β†’ 𝑖 ∈ ℝ)
290163a1i 11 . . . . . . . . . . . . . . 15 ((πœ‘ ∧ 𝑖 ∈ (0...(𝐿 βˆ’ 2))) β†’ (1 / 3) ∈ ℝ)
291289, 290readdcld 11191 . . . . . . . . . . . . . 14 ((πœ‘ ∧ 𝑖 ∈ (0...(𝐿 βˆ’ 2))) β†’ (𝑖 + (1 / 3)) ∈ ℝ)
29214adantr 482 . . . . . . . . . . . . . 14 ((πœ‘ ∧ 𝑖 ∈ (0...(𝐿 βˆ’ 2))) β†’ 𝐸 ∈ ℝ)
293291, 292remulcld 11192 . . . . . . . . . . . . 13 ((πœ‘ ∧ 𝑖 ∈ (0...(𝐿 βˆ’ 2))) β†’ ((𝑖 + (1 / 3)) Β· 𝐸) ∈ ℝ)
294108adantr 482 . . . . . . . . . . . . . . . 16 ((πœ‘ ∧ 𝑖 ∈ (0...(𝐿 βˆ’ 2))) β†’ 𝐿 ∈ ℝ)
295131a1i 11 . . . . . . . . . . . . . . . 16 ((πœ‘ ∧ 𝑖 ∈ (0...(𝐿 βˆ’ 2))) β†’ 2 ∈ ℝ)
296294, 295resubcld 11590 . . . . . . . . . . . . . . 15 ((πœ‘ ∧ 𝑖 ∈ (0...(𝐿 βˆ’ 2))) β†’ (𝐿 βˆ’ 2) ∈ ℝ)
297296, 290readdcld 11191 . . . . . . . . . . . . . 14 ((πœ‘ ∧ 𝑖 ∈ (0...(𝐿 βˆ’ 2))) β†’ ((𝐿 βˆ’ 2) + (1 / 3)) ∈ ℝ)
298297, 292remulcld 11192 . . . . . . . . . . . . 13 ((πœ‘ ∧ 𝑖 ∈ (0...(𝐿 βˆ’ 2))) β†’ (((𝐿 βˆ’ 2) + (1 / 3)) Β· 𝐸) ∈ ℝ)
299 stoweidlem26.10 . . . . . . . . . . . . . . . 16 (πœ‘ β†’ 𝐹:π‘‡βŸΆβ„)
300299, 49jca 513 . . . . . . . . . . . . . . 15 (πœ‘ β†’ (𝐹:π‘‡βŸΆβ„ ∧ 𝑆 ∈ 𝑇))
301300adantr 482 . . . . . . . . . . . . . 14 ((πœ‘ ∧ 𝑖 ∈ (0...(𝐿 βˆ’ 2))) β†’ (𝐹:π‘‡βŸΆβ„ ∧ 𝑆 ∈ 𝑇))
302 ffvelcdm 7037 . . . . . . . . . . . . . 14 ((𝐹:π‘‡βŸΆβ„ ∧ 𝑆 ∈ 𝑇) β†’ (πΉβ€˜π‘†) ∈ ℝ)
303301, 302syl 17 . . . . . . . . . . . . 13 ((πœ‘ ∧ 𝑖 ∈ (0...(𝐿 βˆ’ 2))) β†’ (πΉβ€˜π‘†) ∈ ℝ)
304 elfzle2 13452 . . . . . . . . . . . . . . . 16 (𝑖 ∈ (0...(𝐿 βˆ’ 2)) β†’ 𝑖 ≀ (𝐿 βˆ’ 2))
305304adantl 483 . . . . . . . . . . . . . . 15 ((πœ‘ ∧ 𝑖 ∈ (0...(𝐿 βˆ’ 2))) β†’ 𝑖 ≀ (𝐿 βˆ’ 2))
306289, 296, 290, 305leadd1dd 11776 . . . . . . . . . . . . . 14 ((πœ‘ ∧ 𝑖 ∈ (0...(𝐿 βˆ’ 2))) β†’ (𝑖 + (1 / 3)) ≀ ((𝐿 βˆ’ 2) + (1 / 3)))
30714, 72jca 513 . . . . . . . . . . . . . . . 16 (πœ‘ β†’ (𝐸 ∈ ℝ ∧ 0 < 𝐸))
308307adantr 482 . . . . . . . . . . . . . . 15 ((πœ‘ ∧ 𝑖 ∈ (0...(𝐿 βˆ’ 2))) β†’ (𝐸 ∈ ℝ ∧ 0 < 𝐸))
309 lemul1 12014 . . . . . . . . . . . . . . 15 (((𝑖 + (1 / 3)) ∈ ℝ ∧ ((𝐿 βˆ’ 2) + (1 / 3)) ∈ ℝ ∧ (𝐸 ∈ ℝ ∧ 0 < 𝐸)) β†’ ((𝑖 + (1 / 3)) ≀ ((𝐿 βˆ’ 2) + (1 / 3)) ↔ ((𝑖 + (1 / 3)) Β· 𝐸) ≀ (((𝐿 βˆ’ 2) + (1 / 3)) Β· 𝐸)))
310291, 297, 308, 309syl3anc 1372 . . . . . . . . . . . . . 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 11590 . . . . . . . . . . . . . . . . 17 (πœ‘ β†’ (𝐿 βˆ’ 2) ∈ ℝ)
313312, 164readdcld 11191 . . . . . . . . . . . . . . . 16 (πœ‘ β†’ ((𝐿 βˆ’ 2) + (1 / 3)) ∈ ℝ)
314313, 14remulcld 11192 . . . . . . . . . . . . . . 15 (πœ‘ β†’ (((𝐿 βˆ’ 2) + (1 / 3)) Β· 𝐸) ∈ ℝ)
315299, 49ffvelcdmd 7041 . . . . . . . . . . . . . . 15 (πœ‘ β†’ (πΉβ€˜π‘†) ∈ ℝ)
316120, 164resubcld 11590 . . . . . . . . . . . . . . . . 17 (πœ‘ β†’ ((𝐿 βˆ’ 1) βˆ’ (1 / 3)) ∈ ℝ)
317316, 14remulcld 11192 . . . . . . . . . . . . . . . 16 (πœ‘ β†’ (((𝐿 βˆ’ 1) βˆ’ (1 / 3)) Β· 𝐸) ∈ ℝ)
318 addid1 11342 . . . . . . . . . . . . . . . . . . . . . . . . 25 (1 ∈ β„‚ β†’ (1 + 0) = 1)
319318eqcomd 2743 . . . . . . . . . . . . . . . . . . . . . . . 24 (1 ∈ β„‚ β†’ 1 = (1 + 0))
320167, 319mp1i 13 . . . . . . . . . . . . . . . . . . . . . . 23 (πœ‘ β†’ 1 = (1 + 0))
321175subidd 11507 . . . . . . . . . . . . . . . . . . . . . . . . 25 (πœ‘ β†’ (1 βˆ’ 1) = 0)
322321eqcomd 2743 . . . . . . . . . . . . . . . . . . . . . . . 24 (πœ‘ β†’ 0 = (1 βˆ’ 1))
323322oveq2d 7378 . . . . . . . . . . . . . . . . . . . . . . 23 (πœ‘ β†’ (1 + 0) = (1 + (1 βˆ’ 1)))
324 addsubass 11418 . . . . . . . . . . . . . . . . . . . . . . . . 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 1372 . . . . . . . . . . . . . . . . . . . . . . 23 (πœ‘ β†’ (1 + (1 βˆ’ 1)) = ((1 + 1) βˆ’ 1))
327320, 323, 3263eqtrd 2781 . . . . . . . . . . . . . . . . . . . . . 22 (πœ‘ β†’ 1 = ((1 + 1) βˆ’ 1))
328327oveq2d 7378 . . . . . . . . . . . . . . . . . . . . 21 (πœ‘ β†’ (𝐿 βˆ’ 1) = (𝐿 βˆ’ ((1 + 1) βˆ’ 1)))
329243a1i 11 . . . . . . . . . . . . . . . . . . . . . . 23 (πœ‘ β†’ (1 + 1) = 2)
330329oveq1d 7377 . . . . . . . . . . . . . . . . . . . . . 22 (πœ‘ β†’ ((1 + 1) βˆ’ 1) = (2 βˆ’ 1))
331330oveq2d 7378 . . . . . . . . . . . . . . . . . . . . 21 (πœ‘ β†’ (𝐿 βˆ’ ((1 + 1) βˆ’ 1)) = (𝐿 βˆ’ (2 βˆ’ 1)))
332139, 259, 175subsubd 11547 . . . . . . . . . . . . . . . . . . . . 21 (πœ‘ β†’ (𝐿 βˆ’ (2 βˆ’ 1)) = ((𝐿 βˆ’ 2) + 1))
333328, 331, 3323eqtrd 2781 . . . . . . . . . . . . . . . . . . . 20 (πœ‘ β†’ (𝐿 βˆ’ 1) = ((𝐿 βˆ’ 2) + 1))
334333oveq1d 7377 . . . . . . . . . . . . . . . . . . 19 (πœ‘ β†’ ((𝐿 βˆ’ 1) βˆ’ (2 / 3)) = (((𝐿 βˆ’ 2) + 1) βˆ’ (2 / 3)))
335258, 60, 9divcli 11904 . . . . . . . . . . . . . . . . . . . . 21 (2 / 3) ∈ β„‚
336335a1i 11 . . . . . . . . . . . . . . . . . . . 20 (πœ‘ β†’ (2 / 3) ∈ β„‚)
337260, 175, 336addsubassd 11539 . . . . . . . . . . . . . . . . . . 19 (πœ‘ β†’ (((𝐿 βˆ’ 2) + 1) βˆ’ (2 / 3)) = ((𝐿 βˆ’ 2) + (1 βˆ’ (2 / 3))))
338167, 60, 9divcli 11904 . . . . . . . . . . . . . . . . . . . . . 22 (1 / 3) ∈ β„‚
339 df-3 12224 . . . . . . . . . . . . . . . . . . . . . . . 24 3 = (2 + 1)
340339oveq1i 7372 . . . . . . . . . . . . . . . . . . . . . . 23 (3 / 3) = ((2 + 1) / 3)
341258, 167, 60, 9divdiri 11919 . . . . . . . . . . . . . . . . . . . . . . 23 ((2 + 1) / 3) = ((2 / 3) + (1 / 3))
342340, 61, 3413eqtr3ri 2774 . . . . . . . . . . . . . . . . . . . . . 22 ((2 / 3) + (1 / 3)) = 1
343167, 335, 338, 342subaddrii 11497 . . . . . . . . . . . . . . . . . . . . 21 (1 βˆ’ (2 / 3)) = (1 / 3)
344343a1i 11 . . . . . . . . . . . . . . . . . . . 20 (πœ‘ β†’ (1 βˆ’ (2 / 3)) = (1 / 3))
345344oveq2d 7378 . . . . . . . . . . . . . . . . . . 19 (πœ‘ β†’ ((𝐿 βˆ’ 2) + (1 βˆ’ (2 / 3))) = ((𝐿 βˆ’ 2) + (1 / 3)))
346334, 337, 3453eqtrd 2781 . . . . . . . . . . . . . . . . . 18 (πœ‘ β†’ ((𝐿 βˆ’ 1) βˆ’ (2 / 3)) = ((𝐿 βˆ’ 2) + (1 / 3)))
347131, 7, 9redivcli 11929 . . . . . . . . . . . . . . . . . . . 20 (2 / 3) ∈ ℝ
348347a1i 11 . . . . . . . . . . . . . . . . . . 19 (πœ‘ β†’ (2 / 3) ∈ ℝ)
349 1lt2 12331 . . . . . . . . . . . . . . . . . . . 20 1 < 2
3507, 63pm3.2i 472 . . . . . . . . . . . . . . . . . . . . . 22 (3 ∈ ℝ ∧ 0 < 3)
3511, 131, 3503pm3.2i 1340 . . . . . . . . . . . . . . . . . . . . 21 (1 ∈ ℝ ∧ 2 ∈ ℝ ∧ (3 ∈ ℝ ∧ 0 < 3))
352 ltdiv1 12026 . . . . . . . . . . . . . . . . . . . . 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 11775 . . . . . . . . . . . . . . . . . 18 (πœ‘ β†’ ((𝐿 βˆ’ 1) βˆ’ (2 / 3)) < ((𝐿 βˆ’ 1) βˆ’ (1 / 3)))
356346, 355eqbrtrrd 5134 . . . . . . . . . . . . . . . . 17 (πœ‘ β†’ ((𝐿 βˆ’ 2) + (1 / 3)) < ((𝐿 βˆ’ 1) βˆ’ (1 / 3)))
357313, 316, 13, 356ltmul1dd 13019 . . . . . . . . . . . . . . . 16 (πœ‘ β†’ (((𝐿 βˆ’ 2) + (1 / 3)) Β· 𝐸) < (((𝐿 βˆ’ 1) βˆ’ (1 / 3)) Β· 𝐸))
35823simprd 497 . . . . . . . . . . . . . . . . . . . . . . 23 (πœ‘ β†’ Β¬ 𝑆 ∈ (π·β€˜(𝐿 βˆ’ 1)))
359 oveq1 7369 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑗 = (𝐿 βˆ’ 1) β†’ (𝑗 βˆ’ (1 / 3)) = ((𝐿 βˆ’ 1) βˆ’ (1 / 3)))
360359oveq1d 7377 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑗 = (𝐿 βˆ’ 1) β†’ ((𝑗 βˆ’ (1 / 3)) Β· 𝐸) = (((𝐿 βˆ’ 1) βˆ’ (1 / 3)) Β· 𝐸))
361360breq2d 5122 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑗 = (𝐿 βˆ’ 1) β†’ ((πΉβ€˜π‘‘) ≀ ((𝑗 βˆ’ (1 / 3)) Β· 𝐸) ↔ (πΉβ€˜π‘‘) ≀ (((𝐿 βˆ’ 1) βˆ’ (1 / 3)) Β· 𝐸)))
362361rabbidv 3418 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑗 = (𝐿 βˆ’ 1) β†’ {𝑑 ∈ 𝑇 ∣ (πΉβ€˜π‘‘) ≀ ((𝑗 βˆ’ (1 / 3)) Β· 𝐸)} = {𝑑 ∈ 𝑇 ∣ (πΉβ€˜π‘‘) ≀ (((𝐿 βˆ’ 1) βˆ’ (1 / 3)) Β· 𝐸)})
363129peano2zd 12617 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (πœ‘ β†’ (𝑁 + 1) ∈ β„€)
364189simpld 496 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (πœ‘ β†’ 1 ≀ 𝐿)
365134, 116readdcld 11191 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (πœ‘ β†’ (𝑁 + 1) ∈ ℝ)
366134lep1d 12093 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (πœ‘ β†’ 𝑁 ≀ (𝑁 + 1))
367108, 134, 365, 190, 366letrd 11319 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (πœ‘ β†’ 𝐿 ≀ (𝑁 + 1))
368186, 363, 125, 364, 367elfzd 13439 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (πœ‘ β†’ 𝐿 ∈ (1...(𝑁 + 1)))
369139, 175npcand 11523 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (πœ‘ β†’ ((𝐿 βˆ’ 1) + 1) = 𝐿)
370 0p1e1 12282 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (0 + 1) = 1
371370a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (πœ‘ β†’ (0 + 1) = 1)
372371oveq1d 7377 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (πœ‘ β†’ ((0 + 1)...(𝑁 + 1)) = (1...(𝑁 + 1)))
373368, 369, 3723eltr4d 2853 . . . . . . . . . . . . . . . . . . . . . . . . 25 (πœ‘ β†’ ((𝐿 βˆ’ 1) + 1) ∈ ((0 + 1)...(𝑁 + 1)))
374 0zd 12518 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (πœ‘ β†’ 0 ∈ β„€)
375125, 186zsubcld 12619 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (πœ‘ β†’ (𝐿 βˆ’ 1) ∈ β„€)
376 fzaddel 13482 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((0 ∈ β„€ ∧ 𝑁 ∈ β„€) ∧ ((𝐿 βˆ’ 1) ∈ β„€ ∧ 1 ∈ β„€)) β†’ ((𝐿 βˆ’ 1) ∈ (0...𝑁) ↔ ((𝐿 βˆ’ 1) + 1) ∈ ((0 + 1)...(𝑁 + 1))))
377374, 129, 375, 186, 376syl22anc 838 . . . . . . . . . . . . . . . . . . . . . . . . 25 (πœ‘ β†’ ((𝐿 βˆ’ 1) ∈ (0...𝑁) ↔ ((𝐿 βˆ’ 1) + 1) ∈ ((0 + 1)...(𝑁 + 1))))
378373, 377mpbird 257 . . . . . . . . . . . . . . . . . . . . . . . 24 (πœ‘ β†’ (𝐿 βˆ’ 1) ∈ (0...𝑁))
379 rabexg 5293 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑇 ∈ V β†’ {𝑑 ∈ 𝑇 ∣ (πΉβ€˜π‘‘) ≀ (((𝐿 βˆ’ 1) βˆ’ (1 / 3)) Β· 𝐸)} ∈ V)
38033, 379syl 17 . . . . . . . . . . . . . . . . . . . . . . . 24 (πœ‘ β†’ {𝑑 ∈ 𝑇 ∣ (πΉβ€˜π‘‘) ≀ (((𝐿 βˆ’ 1) βˆ’ (1 / 3)) Β· 𝐸)} ∈ V)
38125, 362, 378, 380fvmptd3 6976 . . . . . . . . . . . . . . . . . . . . . . 23 (πœ‘ β†’ (π·β€˜(𝐿 βˆ’ 1)) = {𝑑 ∈ 𝑇 ∣ (πΉβ€˜π‘‘) ≀ (((𝐿 βˆ’ 1) βˆ’ (1 / 3)) Β· 𝐸)})
382358, 381neleqtrd 2860 . . . . . . . . . . . . . . . . . . . . . 22 (πœ‘ β†’ Β¬ 𝑆 ∈ {𝑑 ∈ 𝑇 ∣ (πΉβ€˜π‘‘) ≀ (((𝐿 βˆ’ 1) βˆ’ (1 / 3)) Β· 𝐸)})
383 nfcv 2908 . . . . . . . . . . . . . . . . . . . . . . . 24 Ⅎ𝑑(((𝐿 βˆ’ 1) βˆ’ (1 / 3)) Β· 𝐸)
38441, 42, 383nfbr 5157 . . . . . . . . . . . . . . . . . . . . . . 23 Ⅎ𝑑(πΉβ€˜π‘†) ≀ (((𝐿 βˆ’ 1) βˆ’ (1 / 3)) Β· 𝐸)
38545breq1d 5120 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑑 = 𝑆 β†’ ((πΉβ€˜π‘‘) ≀ (((𝐿 βˆ’ 1) βˆ’ (1 / 3)) Β· 𝐸) ↔ (πΉβ€˜π‘†) ≀ (((𝐿 βˆ’ 1) βˆ’ (1 / 3)) Β· 𝐸)))
38638, 39, 384, 385elrabf 3646 . . . . . . . . . . . . . . . . . . . . . 22 (𝑆 ∈ {𝑑 ∈ 𝑇 ∣ (πΉβ€˜π‘‘) ≀ (((𝐿 βˆ’ 1) βˆ’ (1 / 3)) Β· 𝐸)} ↔ (𝑆 ∈ 𝑇 ∧ (πΉβ€˜π‘†) ≀ (((𝐿 βˆ’ 1) βˆ’ (1 / 3)) Β· 𝐸)))
387382, 386sylnib 328 . . . . . . . . . . . . . . . . . . . . 21 (πœ‘ β†’ Β¬ (𝑆 ∈ 𝑇 ∧ (πΉβ€˜π‘†) ≀ (((𝐿 βˆ’ 1) βˆ’ (1 / 3)) Β· 𝐸)))
388 ianor 981 . . . . . . . . . . . . . . . . . . . . 21 (Β¬ (𝑆 ∈ 𝑇 ∧ (πΉβ€˜π‘†) ≀ (((𝐿 βˆ’ 1) βˆ’ (1 / 3)) Β· 𝐸)) ↔ (Β¬ 𝑆 ∈ 𝑇 ∨ Β¬ (πΉβ€˜π‘†) ≀ (((𝐿 βˆ’ 1) βˆ’ (1 / 3)) Β· 𝐸)))
389387, 388sylib 217 . . . . . . . . . . . . . . . . . . . 20 (πœ‘ β†’ (Β¬ 𝑆 ∈ 𝑇 ∨ Β¬ (πΉβ€˜π‘†) ≀ (((𝐿 βˆ’ 1) βˆ’ (1 / 3)) Β· 𝐸)))
390 olc 867 . . . . . . . . . . . . . . . . . . . . 21 (𝑆 ∈ 𝑇 β†’ (Β¬ (πΉβ€˜π‘†) ≀ (((𝐿 βˆ’ 1) βˆ’ (1 / 3)) Β· 𝐸) ∨ 𝑆 ∈ 𝑇))
391390anim1i 616 . . . . . . . . . . . . . . . . . . . 20 ((𝑆 ∈ 𝑇 ∧ (Β¬ 𝑆 ∈ 𝑇 ∨ Β¬ (πΉβ€˜π‘†) ≀ (((𝐿 βˆ’ 1) βˆ’ (1 / 3)) Β· 𝐸))) β†’ ((Β¬ (πΉβ€˜π‘†) ≀ (((𝐿 βˆ’ 1) βˆ’ (1 / 3)) Β· 𝐸) ∨ 𝑆 ∈ 𝑇) ∧ (Β¬ 𝑆 ∈ 𝑇 ∨ Β¬ (πΉβ€˜π‘†) ≀ (((𝐿 βˆ’ 1) βˆ’ (1 / 3)) Β· 𝐸))))
39249, 389, 391syl2anc 585 . . . . . . . . . . . . . . . . . . 19 (πœ‘ β†’ ((Β¬ (πΉβ€˜π‘†) ≀ (((𝐿 βˆ’ 1) βˆ’ (1 / 3)) Β· 𝐸) ∨ 𝑆 ∈ 𝑇) ∧ (Β¬ 𝑆 ∈ 𝑇 ∨ Β¬ (πΉβ€˜π‘†) ≀ (((𝐿 βˆ’ 1) βˆ’ (1 / 3)) Β· 𝐸))))
393 orcom 869 . . . . . . . . . . . . . . . . . . . 20 ((Β¬ 𝑆 ∈ 𝑇 ∨ Β¬ (πΉβ€˜π‘†) ≀ (((𝐿 βˆ’ 1) βˆ’ (1 / 3)) Β· 𝐸)) ↔ (Β¬ (πΉβ€˜π‘†) ≀ (((𝐿 βˆ’ 1) βˆ’ (1 / 3)) Β· 𝐸) ∨ Β¬ 𝑆 ∈ 𝑇))
394393anbi2i 624 . . . . . . . . . . . . . . . . . . 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 1022 . . . . . . . . . . . . . . . . . 18 (Β¬ (πΉβ€˜π‘†) ≀ (((𝐿 βˆ’ 1) βˆ’ (1 / 3)) Β· 𝐸) ↔ ((Β¬ (πΉβ€˜π‘†) ≀ (((𝐿 βˆ’ 1) βˆ’ (1 / 3)) Β· 𝐸) ∨ 𝑆 ∈ 𝑇) ∧ (Β¬ (πΉβ€˜π‘†) ≀ (((𝐿 βˆ’ 1) βˆ’ (1 / 3)) Β· 𝐸) ∨ Β¬ 𝑆 ∈ 𝑇)))
397395, 396sylibr 233 . . . . . . . . . . . . . . . . 17 (πœ‘ β†’ Β¬ (πΉβ€˜π‘†) ≀ (((𝐿 βˆ’ 1) βˆ’ (1 / 3)) Β· 𝐸))
398317, 315ltnled 11309 . . . . . . . . . . . . . . . . 17 (πœ‘ β†’ ((((𝐿 βˆ’ 1) βˆ’ (1 / 3)) Β· 𝐸) < (πΉβ€˜π‘†) ↔ Β¬ (πΉβ€˜π‘†) ≀ (((𝐿 βˆ’ 1) βˆ’ (1 / 3)) Β· 𝐸)))
399397, 398mpbird 257 . . . . . . . . . . . . . . . 16 (πœ‘ β†’ (((𝐿 βˆ’ 1) βˆ’ (1 / 3)) Β· 𝐸) < (πΉβ€˜π‘†))
400314, 317, 315, 357, 399lttrd 11323 . . . . . . . . . . . . . . 15 (πœ‘ β†’ (((𝐿 βˆ’ 2) + (1 / 3)) Β· 𝐸) < (πΉβ€˜π‘†))
401314, 315, 400ltled 11310 . . . . . . . . . . . . . 14 (πœ‘ β†’ (((𝐿 βˆ’ 2) + (1 / 3)) Β· 𝐸) ≀ (πΉβ€˜π‘†))
402401adantr 482 . . . . . . . . . . . . 13 ((πœ‘ ∧ 𝑖 ∈ (0...(𝐿 βˆ’ 2))) β†’ (((𝐿 βˆ’ 2) + (1 / 3)) Β· 𝐸) ≀ (πΉβ€˜π‘†))
403293, 298, 303, 311, 402letrd 11319 . . . . . . . . . . . 12 ((πœ‘ ∧ 𝑖 ∈ (0...(𝐿 βˆ’ 2))) β†’ ((𝑖 + (1 / 3)) Β· 𝐸) ≀ (πΉβ€˜π‘†))
404 nfcv 2908 . . . . . . . . . . . . . 14 Ⅎ𝑑((𝑖 + (1 / 3)) Β· 𝐸)
405404, 42, 41nfbr 5157 . . . . . . . . . . . . 13 Ⅎ𝑑((𝑖 + (1 / 3)) Β· 𝐸) ≀ (πΉβ€˜π‘†)
40645breq2d 5122 . . . . . . . . . . . . 13 (𝑑 = 𝑆 β†’ (((𝑖 + (1 / 3)) Β· 𝐸) ≀ (πΉβ€˜π‘‘) ↔ ((𝑖 + (1 / 3)) Β· 𝐸) ≀ (πΉβ€˜π‘†)))
40738, 39, 405, 406elrabf 3646 . . . . . . . . . . . 12 (𝑆 ∈ {𝑑 ∈ 𝑇 ∣ ((𝑖 + (1 / 3)) Β· 𝐸) ≀ (πΉβ€˜π‘‘)} ↔ (𝑆 ∈ 𝑇 ∧ ((𝑖 + (1 / 3)) Β· 𝐸) ≀ (πΉβ€˜π‘†)))
408286, 403, 407sylanbrc 584 . . . . . . . . . . 11 ((πœ‘ ∧ 𝑖 ∈ (0...(𝐿 βˆ’ 2))) β†’ 𝑆 ∈ {𝑑 ∈ 𝑇 ∣ ((𝑖 + (1 / 3)) Β· 𝐸) ≀ (πΉβ€˜π‘‘)})
409 stoweidlem26.5 . . . . . . . . . . . 12 𝐡 = (𝑗 ∈ (0...𝑁) ↦ {𝑑 ∈ 𝑇 ∣ ((𝑗 + (1 / 3)) Β· 𝐸) ≀ (πΉβ€˜π‘‘)})
410 oveq1 7369 . . . . . . . . . . . . . . 15 (𝑗 = 𝑖 β†’ (𝑗 + (1 / 3)) = (𝑖 + (1 / 3)))
411410oveq1d 7377 . . . . . . . . . . . . . 14 (𝑗 = 𝑖 β†’ ((𝑗 + (1 / 3)) Β· 𝐸) = ((𝑖 + (1 / 3)) Β· 𝐸))
412411breq1d 5120 . . . . . . . . . . . . 13 (𝑗 = 𝑖 β†’ (((𝑗 + (1 / 3)) Β· 𝐸) ≀ (πΉβ€˜π‘‘) ↔ ((𝑖 + (1 / 3)) Β· 𝐸) ≀ (πΉβ€˜π‘‘)))
413412rabbidv 3418 . . . . . . . . . . . 12 (𝑗 = 𝑖 β†’ {𝑑 ∈ 𝑇 ∣ ((𝑗 + (1 / 3)) Β· 𝐸) ≀ (πΉβ€˜π‘‘)} = {𝑑 ∈ 𝑇 ∣ ((𝑖 + (1 / 3)) Β· 𝐸) ≀ (πΉβ€˜π‘‘)})
414 rabexg 5293 . . . . . . . . . . . . . 14 (𝑇 ∈ V β†’ {𝑑 ∈ 𝑇 ∣ ((𝑖 + (1 / 3)) Β· 𝐸) ≀ (πΉβ€˜π‘‘)} ∈ V)
41533, 414syl 17 . . . . . . . . . . . . 13 (πœ‘ β†’ {𝑑 ∈ 𝑇 ∣ ((𝑖 + (1 / 3)) Β· 𝐸) ≀ (πΉβ€˜π‘‘)} ∈ V)
416415adantr 482 . . . . . . . . . . . 12 ((πœ‘ ∧ 𝑖 ∈ (0...(𝐿 βˆ’ 2))) β†’ {𝑑 ∈ 𝑇 ∣ ((𝑖 + (1 / 3)) Β· 𝐸) ≀ (πΉβ€˜π‘‘)} ∈ V)
417409, 413, 150, 416fvmptd3 6976 . . . . . . . . . . 11 ((πœ‘ ∧ 𝑖 ∈ (0...(𝐿 βˆ’ 2))) β†’ (π΅β€˜π‘–) = {𝑑 ∈ 𝑇 ∣ ((𝑖 + (1 / 3)) Β· 𝐸) ≀ (πΉβ€˜π‘‘)})
418408, 417eleqtrrd 2841 . . . . . . . . . 10 ((πœ‘ ∧ 𝑖 ∈ (0...(𝐿 βˆ’ 2))) β†’ 𝑆 ∈ (π΅β€˜π‘–))
4191453ad2ant1 1134 . . . . . . . . . . . . . 14 ((πœ‘ ∧ 𝑖 ∈ (0...(𝐿 βˆ’ 2)) ∧ 𝑆 ∈ (π΅β€˜π‘–)) β†’ ((𝐿 βˆ’ 2) ∈ β„€ ∧ 𝑁 ∈ β„€ ∧ (𝐿 βˆ’ 2) ≀ 𝑁))
420419, 146sylibr 233 . . . . . . . . . . . . 13 ((πœ‘ ∧ 𝑖 ∈ (0...(𝐿 βˆ’ 2)) ∧ 𝑆 ∈ (π΅β€˜π‘–)) β†’ 𝑁 ∈ (β„€β‰₯β€˜(𝐿 βˆ’ 2)))
421420, 148syl 17 . . . . . . . . . . . 12 ((πœ‘ ∧ 𝑖 ∈ (0...(𝐿 βˆ’ 2)) ∧ 𝑆 ∈ (π΅β€˜π‘–)) β†’ (0...(𝐿 βˆ’ 2)) βŠ† (0...𝑁))
422 simp2 1138 . . . . . . . . . . . 12 ((πœ‘ ∧ 𝑖 ∈ (0...(𝐿 βˆ’ 2)) ∧ 𝑆 ∈ (π΅β€˜π‘–)) β†’ 𝑖 ∈ (0...(𝐿 βˆ’ 2)))
423421, 422sseldd 3950 . . . . . . . . . . 11 ((πœ‘ ∧ 𝑖 ∈ (0...(𝐿 βˆ’ 2)) ∧ 𝑆 ∈ (π΅β€˜π‘–)) β†’ 𝑖 ∈ (0...𝑁))
424 elex 3466 . . . . . . . . . . . . 13 (𝑆 ∈ (π΅β€˜π‘–) β†’ 𝑆 ∈ V)
4254243ad2ant3 1136 . . . . . . . . . . . 12 ((πœ‘ ∧ 𝑖 ∈ (0...𝑁) ∧ 𝑆 ∈ (π΅β€˜π‘–)) β†’ 𝑆 ∈ V)
426 nfcv 2908 . . . . . . . . . . . . . . . . . . 19 Ⅎ𝑑(0...𝑁)
427 nfrab1 3429 . . . . . . . . . . . . . . . . . . 19 Ⅎ𝑑{𝑑 ∈ 𝑇 ∣ ((𝑗 + (1 / 3)) Β· 𝐸) ≀ (πΉβ€˜π‘‘)}
428426, 427nfmpt 5217 . . . . . . . . . . . . . . . . . 18 Ⅎ𝑑(𝑗 ∈ (0...𝑁) ↦ {𝑑 ∈ 𝑇 ∣ ((𝑗 + (1 / 3)) Β· 𝐸) ≀ (πΉβ€˜π‘‘)})
429409, 428nfcxfr 2906 . . . . . . . . . . . . . . . . 17 Ⅎ𝑑𝐡
430 nfcv 2908 . . . . . . . . . . . . . . . . 17 Ⅎ𝑑𝑖
431429, 430nffv 6857 . . . . . . . . . . . . . . . 16 Ⅎ𝑑(π΅β€˜π‘–)
432431nfel2 2926 . . . . . . . . . . . . . . 15 Ⅎ𝑑 𝑆 ∈ (π΅β€˜π‘–)
43388, 89, 432nf3an 1905 . . . . . . . . . . . . . 14 Ⅎ𝑑(πœ‘ ∧ 𝑖 ∈ (0...𝑁) ∧ 𝑆 ∈ (π΅β€˜π‘–))
434 nfv 1918 . . . . . . . . . . . . . 14 Ⅎ𝑑(1 βˆ’ (𝐸 / 𝑁)) < ((π‘‹β€˜π‘–)β€˜π‘†)
435433, 434nfim 1900 . . . . . . . . . . . . 13 Ⅎ𝑑((πœ‘ ∧ 𝑖 ∈ (0...𝑁) ∧ 𝑆 ∈ (π΅β€˜π‘–)) β†’ (1 βˆ’ (𝐸 / 𝑁)) < ((π‘‹β€˜π‘–)β€˜π‘†))
436 eleq1 2826 . . . . . . . . . . . . . . 15 (𝑑 = 𝑆 β†’ (𝑑 ∈ (π΅β€˜π‘–) ↔ 𝑆 ∈ (π΅β€˜π‘–)))
4374363anbi3d 1443 . . . . . . . . . . . . . 14 (𝑑 = 𝑆 β†’ ((πœ‘ ∧ 𝑖 ∈ (0...𝑁) ∧ 𝑑 ∈ (π΅β€˜π‘–)) ↔ (πœ‘ ∧ 𝑖 ∈ (0...𝑁) ∧ 𝑆 ∈ (π΅β€˜π‘–))))
43893breq2d 5122 . . . . . . . . . . . . . 14 (𝑑 = 𝑆 β†’ ((1 βˆ’ (𝐸 / 𝑁)) < ((π‘‹β€˜π‘–)β€˜π‘‘) ↔ (1 βˆ’ (𝐸 / 𝑁)) < ((π‘‹β€˜π‘–)β€˜π‘†)))
439437, 438imbi12d 345 . . . . . . . . . . . . 13 (𝑑 = 𝑆 β†’ (((πœ‘ ∧ 𝑖 ∈ (0...𝑁) ∧ 𝑑 ∈ (π΅β€˜π‘–)) β†’ (1 βˆ’ (𝐸 / 𝑁)) < ((π‘‹β€˜π‘–)β€˜π‘‘)) ↔ ((πœ‘ ∧ 𝑖 ∈ (0...𝑁) ∧ 𝑆 ∈ (π΅β€˜π‘–)) β†’ (1 βˆ’ (𝐸 / 𝑁)) < ((π‘‹β€˜π‘–)β€˜π‘†))))
440 stoweidlem26.15 . . . . . . . . . . . . 13 ((πœ‘ ∧ 𝑖 ∈ (0...𝑁) ∧ 𝑑 ∈ (π΅β€˜π‘–)) β†’ (1 βˆ’ (𝐸 / 𝑁)) < ((π‘‹β€˜π‘–)β€˜π‘‘))
441435, 439, 440vtoclg1f 3527 . . . . . . . . . . . 12 (𝑆 ∈ V β†’ ((πœ‘ ∧ 𝑖 ∈ (0...𝑁) ∧ 𝑆 ∈ (π΅β€˜π‘–)) β†’ (1 βˆ’ (𝐸 / 𝑁)) < ((π‘‹β€˜π‘–)β€˜π‘†)))
442425, 441mpcom 38 . . . . . . . . . . 11 ((πœ‘ ∧ 𝑖 ∈ (0...𝑁) ∧ 𝑆 ∈ (π΅β€˜π‘–)) β†’ (1 βˆ’ (𝐸 / 𝑁)) < ((π‘‹β€˜π‘–)β€˜π‘†))
443423, 442syld3an2 1412 . . . . . . . . . 10 ((πœ‘ ∧ 𝑖 ∈ (0...(𝐿 βˆ’ 2)) ∧ 𝑆 ∈ (π΅β€˜π‘–)) β†’ (1 βˆ’ (𝐸 / 𝑁)) < ((π‘‹β€˜π‘–)β€˜π‘†))
444418, 443mpd3an3 1463 . . . . . . . . 9 ((πœ‘ ∧ 𝑖 ∈ (0...(𝐿 βˆ’ 2))) β†’ (1 βˆ’ (𝐸 / 𝑁)) < ((π‘‹β€˜π‘–)β€˜π‘†))
445444adantlr 714 . . . . . . . 8 (((πœ‘ ∧ Β¬ 𝐿 = 1) ∧ 𝑖 ∈ (0...(𝐿 βˆ’ 2))) β†’ (1 βˆ’ (𝐸 / 𝑁)) < ((π‘‹β€˜π‘–)β€˜π‘†))
446279, 281, 282, 285, 445fsumlt 15692 . . . . . . 7 ((πœ‘ ∧ Β¬ 𝐿 = 1) β†’ Σ𝑖 ∈ (0...(𝐿 βˆ’ 2))(1 βˆ’ (𝐸 / 𝑁)) < Σ𝑖 ∈ (0...(𝐿 βˆ’ 2))((π‘‹β€˜π‘–)β€˜π‘†))
447278, 446eqbrtrrd 5134 . . . . . 6 ((πœ‘ ∧ Β¬ 𝐿 = 1) β†’ ((1 βˆ’ (𝐸 / 𝑁)) Β· (𝐿 βˆ’ 1)) < Σ𝑖 ∈ (0...(𝐿 βˆ’ 2))((π‘‹β€˜π‘–)β€˜π‘†))
448121adantr 482 . . . . . . 7 ((πœ‘ ∧ Β¬ 𝐿 = 1) β†’ ((1 βˆ’ (𝐸 / 𝑁)) Β· (𝐿 βˆ’ 1)) ∈ ℝ)
449152adantr 482 . . . . . . 7 ((πœ‘ ∧ Β¬ 𝐿 = 1) β†’ Σ𝑖 ∈ (0...(𝐿 βˆ’ 2))((π‘‹β€˜π‘–)β€˜π‘†) ∈ ℝ)
450307adantr 482 . . . . . . 7 ((πœ‘ ∧ Β¬ 𝐿 = 1) β†’ (𝐸 ∈ ℝ ∧ 0 < 𝐸))
451 ltmul2 12013 . . . . . . 7 ((((1 βˆ’ (𝐸 / 𝑁)) Β· (𝐿 βˆ’ 1)) ∈ ℝ ∧ Σ𝑖 ∈ (0...(𝐿 βˆ’ 2))((π‘‹β€˜π‘–)β€˜π‘†) ∈ ℝ ∧ (𝐸 ∈ ℝ ∧ 0 < 𝐸)) β†’ (((1 βˆ’ (𝐸 / 𝑁)) Β· (𝐿 βˆ’ 1)) < Σ𝑖 ∈ (0...(𝐿 βˆ’ 2))((π‘‹β€˜π‘–)β€˜π‘†) ↔ (𝐸 Β· ((1 βˆ’ (𝐸 / 𝑁)) Β· (𝐿 βˆ’ 1))) < (𝐸 Β· Σ𝑖 ∈ (0...(𝐿 βˆ’ 2))((π‘‹β€˜π‘–)β€˜π‘†))))
452448, 449, 450, 451syl3anc 1372 . . . . . 6 ((πœ‘ ∧ Β¬ 𝐿 = 1) β†’ (((1 βˆ’ (𝐸 / 𝑁)) Β· (𝐿 βˆ’ 1)) < Σ𝑖 ∈ (0...(𝐿 βˆ’ 2))((π‘‹β€˜π‘–)β€˜π‘†) ↔ (𝐸 Β· ((1 βˆ’ (𝐸 / 𝑁)) Β· (𝐿 βˆ’ 1))) < (𝐸 Β· Σ𝑖 ∈ (0...(𝐿 βˆ’ 2))((π‘‹β€˜π‘–)β€˜π‘†))))
453447, 452mpbid 231 . . . . 5 ((πœ‘ ∧ Β¬ 𝐿 = 1) β†’ (𝐸 Β· ((1 βˆ’ (𝐸 / 𝑁)) Β· (𝐿 βˆ’ 1))) < (𝐸 Β· Σ𝑖 ∈ (0...(𝐿 βˆ’ 2))((π‘‹β€˜π‘–)β€˜π‘†)))
454115, 123, 154, 227, 453lttrd 11323 . . . 4 ((πœ‘ ∧ Β¬ 𝐿 = 1) β†’ ((𝐿 βˆ’ (4 / 3)) Β· 𝐸) < (𝐸 Β· Σ𝑖 ∈ (0...(𝐿 βˆ’ 2))((π‘‹β€˜π‘–)β€˜π‘†)))
455150, 52syldan 592 . . . . . . . . . 10 ((πœ‘ ∧ 𝑖 ∈ (0...(𝐿 βˆ’ 2))) β†’ (𝐸 Β· ((π‘‹β€˜π‘–)β€˜π‘†)) ∈ ℝ)
456455adantlr 714 . . . . . . . . 9 (((πœ‘ ∧ Β¬ 𝐿 = 1) ∧ 𝑖 ∈ (0...(𝐿 βˆ’ 2))) β†’ (𝐸 Β· ((π‘‹β€˜π‘–)β€˜π‘†)) ∈ ℝ)
457456recnd 11190 . . . . . . . 8 (((πœ‘ ∧ Β¬ 𝐿 = 1) ∧ 𝑖 ∈ (0...(𝐿 βˆ’ 2))) β†’ (𝐸 Β· ((π‘‹β€˜π‘–)β€˜π‘†)) ∈ β„‚)
458279, 457fsumcl 15625 . . . . . . 7 ((πœ‘ ∧ Β¬ 𝐿 = 1) β†’ Σ𝑖 ∈ (0...(𝐿 βˆ’ 2))(𝐸 Β· ((π‘‹β€˜π‘–)β€˜π‘†)) ∈ β„‚)
459458addid1d 11362 . . . . . 6 ((πœ‘ ∧ Β¬ 𝐿 = 1) β†’ (Σ𝑖 ∈ (0...(𝐿 βˆ’ 2))(𝐸 Β· ((π‘‹β€˜π‘–)β€˜π‘†)) + 0) = Σ𝑖 ∈ (0...(𝐿 βˆ’ 2))(𝐸 Β· ((π‘‹β€˜π‘–)β€˜π‘†)))
460 0red 11165 . . . . . . 7 ((πœ‘ ∧ Β¬ 𝐿 = 1) β†’ 0 ∈ ℝ)
461 fzfid 13885 . . . . . . . 8 ((πœ‘ ∧ Β¬ 𝐿 = 1) β†’ ((𝐿 βˆ’ 1)...𝑁) ∈ Fin)
46214adantr 482 . . . . . . . . . 10 ((πœ‘ ∧ 𝑖 ∈ ((𝐿 βˆ’ 1)...𝑁)) β†’ 𝐸 ∈ ℝ)
463 0zd 12518 . . . . . . . . . . . 12 ((πœ‘ ∧ 𝑖 ∈ ((𝐿 βˆ’ 1)...𝑁)) β†’ 0 ∈ β„€)
464129adantr 482 . . . . . . . . . . . 12 ((πœ‘ ∧ 𝑖 ∈ ((𝐿 βˆ’ 1)...𝑁)) β†’ 𝑁 ∈ β„€)
465 elfzelz 13448 . . . . . . . . . . . . 13 (𝑖 ∈ ((𝐿 βˆ’ 1)...𝑁) β†’ 𝑖 ∈ β„€)
466465adantl 483 . . . . . . . . . . . 12 ((πœ‘ ∧ 𝑖 ∈ ((𝐿 βˆ’ 1)...𝑁)) β†’ 𝑖 ∈ β„€)
467 0red 11165 . . . . . . . . . . . . 13 ((πœ‘ ∧ 𝑖 ∈ ((𝐿 βˆ’ 1)...𝑁)) β†’ 0 ∈ ℝ)
468120adantr 482 . . . . . . . . . . . . 13 ((πœ‘ ∧ 𝑖 ∈ ((𝐿 βˆ’ 1)...𝑁)) β†’ (𝐿 βˆ’ 1) ∈ ℝ)
469465zred 12614 . . . . . . . . . . . . . 14 (𝑖 ∈ ((𝐿 βˆ’ 1)...𝑁) β†’ 𝑖 ∈ ℝ)
470469adantl 483 . . . . . . . . . . . . 13 ((πœ‘ ∧ 𝑖 ∈ ((𝐿 βˆ’ 1)...𝑁)) β†’ 𝑖 ∈ ℝ)
471 1m1e0 12232 . . . . . . . . . . . . . . 15 (1 βˆ’ 1) = 0
472116, 108, 116, 364lesub1dd 11778 . . . . . . . . . . . . . . 15 (πœ‘ β†’ (1 βˆ’ 1) ≀ (𝐿 βˆ’ 1))
473471, 472eqbrtrrid 5146 . . . . . . . . . . . . . 14 (πœ‘ β†’ 0 ≀ (𝐿 βˆ’ 1))
474473adantr 482 . . . . . . . . . . . . 13 ((πœ‘ ∧ 𝑖 ∈ ((𝐿 βˆ’ 1)...𝑁)) β†’ 0 ≀ (𝐿 βˆ’ 1))
475 simpr 486 . . . . . . . . . . . . . . 15 ((πœ‘ ∧ 𝑖 ∈ ((𝐿 βˆ’ 1)...𝑁)) β†’ 𝑖 ∈ ((𝐿 βˆ’ 1)...𝑁))
476375adantr 482 . . . . . . . . . . . . . . . 16 ((πœ‘ ∧ 𝑖 ∈ ((𝐿 βˆ’ 1)...𝑁)) β†’ (𝐿 βˆ’ 1) ∈ β„€)
477 elfz 13437 . . . . . . . . . . . . . . . 16 ((𝑖 ∈ β„€ ∧ (𝐿 βˆ’ 1) ∈ β„€ ∧ 𝑁 ∈ β„€) β†’ (𝑖 ∈ ((𝐿 βˆ’ 1)...𝑁) ↔ ((𝐿 βˆ’ 1) ≀ 𝑖 ∧ 𝑖 ≀ 𝑁)))
478466, 476, 464, 477syl3anc 1372 . . . . . . . . . . . . . . 15 ((πœ‘ ∧ 𝑖 ∈ ((𝐿 βˆ’ 1)...𝑁)) β†’ (𝑖 ∈ ((𝐿 βˆ’ 1)...𝑁) ↔ ((𝐿 βˆ’ 1) ≀ 𝑖 ∧ 𝑖 ≀ 𝑁)))
479475, 478mpbid 231 . . . . . . . . . . . . . 14 ((πœ‘ ∧ 𝑖 ∈ ((𝐿 βˆ’ 1)...𝑁)) β†’ ((𝐿 βˆ’ 1) ≀ 𝑖 ∧ 𝑖 ≀ 𝑁))
480479simpld 496 . . . . . . . . . . . . 13 ((πœ‘ ∧ 𝑖 ∈ ((𝐿 βˆ’ 1)...𝑁)) β†’ (𝐿 βˆ’ 1) ≀ 𝑖)
481467, 468, 470, 474, 480letrd 11319 . . . . . . . . . . . 12 ((πœ‘ ∧ 𝑖 ∈ ((𝐿 βˆ’ 1)...𝑁)) β†’ 0 ≀ 𝑖)
482 elfzle2 13452 . . . . . . . . . . . . 13 (𝑖 ∈ ((𝐿 βˆ’ 1)...𝑁) β†’ 𝑖 ≀ 𝑁)
483482adantl 483 . . . . . . . . . . . 12 ((πœ‘ ∧ 𝑖 ∈ ((𝐿 βˆ’ 1)...𝑁)) β†’ 𝑖 ≀ 𝑁)
484463, 464, 466, 481, 483elfzd 13439 . . . . . . . . . . 11 ((πœ‘ ∧ 𝑖 ∈ ((𝐿 βˆ’ 1)...𝑁)) β†’ 𝑖 ∈ (0...𝑁))
485484, 51syldan 592 . . . . . . . . . 10 ((πœ‘ ∧ 𝑖 ∈ ((𝐿 βˆ’ 1)...𝑁)) β†’ ((π‘‹β€˜π‘–)β€˜π‘†) ∈ ℝ)
486462, 485remulcld 11192 . . . . . . . . 9 ((πœ‘ ∧ 𝑖 ∈ ((𝐿 βˆ’ 1)...𝑁)) β†’ (𝐸 Β· ((π‘‹β€˜π‘–)β€˜π‘†)) ∈ ℝ)
487486adantlr 714 . . . . . . . 8 (((πœ‘ ∧ Β¬ 𝐿 = 1) ∧ 𝑖 ∈ ((𝐿 βˆ’ 1)...𝑁)) β†’ (𝐸 Β· ((π‘‹β€˜π‘–)β€˜π‘†)) ∈ ℝ)
488461, 487fsumrecl 15626 . . . . . . 7 ((πœ‘ ∧ Β¬ 𝐿 = 1) β†’ Σ𝑖 ∈ ((𝐿 βˆ’ 1)...𝑁)(𝐸 Β· ((π‘‹β€˜π‘–)β€˜π‘†)) ∈ ℝ)
489279, 456fsumrecl 15626 . . . . . . 7 ((πœ‘ ∧ Β¬ 𝐿 = 1) β†’ Σ𝑖 ∈ (0...(𝐿 βˆ’ 2))(𝐸 Β· ((π‘‹β€˜π‘–)β€˜π‘†)) ∈ ℝ)
490 fzfid 13885 . . . . . . . . 9 (πœ‘ β†’ ((𝐿 βˆ’ 1)...𝑁) ∈ Fin)
491176adantr 482 . . . . . . . . . . 11 ((πœ‘ ∧ 𝑖 ∈ ((𝐿 βˆ’ 1)...𝑁)) β†’ 𝐸 ∈ β„‚)
492491mul01d 11361 . . . . . . . . . 10 ((πœ‘ ∧ 𝑖 ∈ ((𝐿 βˆ’ 1)...𝑁)) β†’ (𝐸 Β· 0) = 0)
493484, 100syldan 592 . . . . . . . . . . 11 ((πœ‘ ∧ 𝑖 ∈ ((𝐿 βˆ’ 1)...𝑁)) β†’ 0 ≀ ((π‘‹β€˜π‘–)β€˜π‘†))
494307adantr 482 . . . . . . . . . . . 12 ((πœ‘ ∧ 𝑖 ∈ ((𝐿 βˆ’ 1)...𝑁)) β†’ (𝐸 ∈ ℝ ∧ 0 < 𝐸))
495 lemul2 12015 . . . . . . . . . . . 12 ((0 ∈ ℝ ∧ ((π‘‹β€˜π‘–)β€˜π‘†) ∈ ℝ ∧ (𝐸 ∈ ℝ ∧ 0 < 𝐸)) β†’ (0 ≀ ((π‘‹β€˜π‘–)β€˜π‘†) ↔ (𝐸 Β· 0) ≀ (𝐸 Β· ((π‘‹β€˜π‘–)β€˜π‘†))))
496467, 485, 494, 495syl3anc 1372 . . . . . . . . . . 11 ((πœ‘ ∧ 𝑖 ∈ ((𝐿 βˆ’ 1)...𝑁)) β†’ (0 ≀ ((π‘‹β€˜π‘–)β€˜π‘†) ↔ (𝐸 Β· 0) ≀ (𝐸 Β· ((π‘‹β€˜π‘–)β€˜π‘†))))
497493, 496mpbid 231 . . . . . . . . . 10 ((πœ‘ ∧ 𝑖 ∈ ((𝐿 βˆ’ 1)...𝑁)) β†’ (𝐸 Β· 0) ≀ (𝐸 Β· ((π‘‹β€˜π‘–)β€˜π‘†)))
498492, 497eqbrtrrd 5134 . . . . . . . . 9 ((πœ‘ ∧ 𝑖 ∈ ((𝐿 βˆ’ 1)...𝑁)) β†’ 0 ≀ (𝐸 Β· ((π‘‹β€˜π‘–)β€˜π‘†)))
499490, 486, 498fsumge0 15687 . . . . . . . 8 (πœ‘ β†’ 0 ≀ Σ𝑖 ∈ ((𝐿 βˆ’ 1)...𝑁)(𝐸 Β· ((π‘‹β€˜π‘–)β€˜π‘†)))
500499adantr 482 . . . . . . 7 ((πœ‘ ∧ Β¬ 𝐿 = 1) β†’ 0 ≀ Σ𝑖 ∈ ((𝐿 βˆ’ 1)...𝑁)(𝐸 Β· ((π‘‹β€˜π‘–)β€˜π‘†)))
501460, 488, 489, 500leadd2dd 11777 . . . . . 6 ((πœ‘ ∧ Β¬ 𝐿 = 1) β†’ (Σ𝑖 ∈ (0...(𝐿 βˆ’ 2))(𝐸 Β· ((π‘‹β€˜π‘–)β€˜π‘†)) + 0) ≀ (Σ𝑖 ∈ (0...(𝐿 βˆ’ 2))(𝐸 Β· ((π‘‹β€˜π‘–)β€˜π‘†)) + Σ𝑖 ∈ ((𝐿 βˆ’ 1)...𝑁)(𝐸 Β· ((π‘‹β€˜π‘–)β€˜π‘†))))
502459, 501eqbrtrrd 5134 . . . . 5 ((πœ‘ ∧ Β¬ 𝐿 = 1) β†’ Σ𝑖 ∈ (0...(𝐿 βˆ’ 2))(𝐸 Β· ((π‘‹β€˜π‘–)β€˜π‘†)) ≀ (Σ𝑖 ∈ (0...(𝐿 βˆ’ 2))(𝐸 Β· ((π‘‹β€˜π‘–)β€˜π‘†)) + Σ𝑖 ∈ ((𝐿 βˆ’ 1)...𝑁)(𝐸 Β· ((π‘‹β€˜π‘–)β€˜π‘†))))
503151recnd 11190 . . . . . . 7 ((πœ‘ ∧ 𝑖 ∈ (0...(𝐿 βˆ’ 2))) β†’ ((π‘‹β€˜π‘–)β€˜π‘†) ∈ β„‚)
504124, 176, 503fsummulc2 15676 . . . . . 6 (πœ‘ β†’ (𝐸 Β· Σ𝑖 ∈ (0...(𝐿 βˆ’ 2))((π‘‹β€˜π‘–)β€˜π‘†)) = Σ𝑖 ∈ (0...(𝐿 βˆ’ 2))(𝐸 Β· ((π‘‹β€˜π‘–)β€˜π‘†)))
505504adantr 482 . . . . 5 ((πœ‘ ∧ Β¬ 𝐿 = 1) β†’ (𝐸 Β· Σ𝑖 ∈ (0...(𝐿 βˆ’ 2))((π‘‹β€˜π‘–)β€˜π‘†)) = Σ𝑖 ∈ (0...(𝐿 βˆ’ 2))(𝐸 Β· ((π‘‹β€˜π‘–)β€˜π‘†)))
506 stoweidlem26.2 . . . . . . . . 9 β„²π‘—πœ‘
507 elfzelz 13448 . . . . . . . . . . . . . . . 16 (𝑗 ∈ (0...(𝐿 βˆ’ 2)) β†’ 𝑗 ∈ β„€)
508507adantl 483 . . . . . . . . . . . . . . 15 ((πœ‘ ∧ 𝑗 ∈ (0...(𝐿 βˆ’ 2))) β†’ 𝑗 ∈ β„€)
509508zred 12614 . . . . . . . . . . . . . 14 ((πœ‘ ∧ 𝑗 ∈ (0...(𝐿 βˆ’ 2))) β†’ 𝑗 ∈ ℝ)
510312adantr 482 . . . . . . . . . . . . . 14 ((πœ‘ ∧ 𝑗 ∈ (0...(𝐿 βˆ’ 2))) β†’ (𝐿 βˆ’ 2) ∈ ℝ)
511120adantr 482 . . . . . . . . . . . . . 14 ((πœ‘ ∧ 𝑗 ∈ (0...(𝐿 βˆ’ 2))) β†’ (𝐿 βˆ’ 1) ∈ ℝ)
512 simpr 486 . . . . . . . . . . . . . . . 16 ((πœ‘ ∧ 𝑗 ∈ (0...(𝐿 βˆ’ 2))) β†’ 𝑗 ∈ (0...(𝐿 βˆ’ 2)))
513 0zd 12518 . . . . . . . . . . . . . . . . 17 ((πœ‘ ∧ 𝑗 ∈ (0...(𝐿 βˆ’ 2))) β†’ 0 ∈ β„€)
514128adantr 482 . . . . . . . . . . . . . . . . 17 ((πœ‘ ∧ 𝑗 ∈ (0...(𝐿 βˆ’ 2))) β†’ (𝐿 βˆ’ 2) ∈ β„€)
515 elfz 13437 . . . . . . . . . . . . . . . . 17 ((𝑗 ∈ β„€ ∧ 0 ∈ β„€ ∧ (𝐿 βˆ’ 2) ∈ β„€) β†’ (𝑗 ∈ (0...(𝐿 βˆ’ 2)) ↔ (0 ≀ 𝑗 ∧ 𝑗 ≀ (𝐿 βˆ’ 2))))
516508, 513, 514, 515syl3anc 1372 . . . . . . . . . . . . . . . 16 ((πœ‘ ∧ 𝑗 ∈ (0...(𝐿 βˆ’ 2))) β†’ (𝑗 ∈ (0...(𝐿 βˆ’ 2)) ↔ (0 ≀ 𝑗 ∧ 𝑗 ≀ (𝐿 βˆ’ 2))))
517512, 516mpbid 231 . . . . . . . . . . . . . . 15 ((πœ‘ ∧ 𝑗 ∈ (0...(𝐿 βˆ’ 2))) β†’ (0 ≀ 𝑗 ∧ 𝑗 ≀ (𝐿 βˆ’ 2)))
518517simprd 497 . . . . . . . . . . . . . 14 ((πœ‘ ∧ 𝑗 ∈ (0...(𝐿 βˆ’ 2))) β†’ 𝑗 ≀ (𝐿 βˆ’ 2))
519116, 132, 108ltsub2d 11772 . . . . . . . . . . . . . . . 16 (πœ‘ β†’ (1 < 2 ↔ (𝐿 βˆ’ 2) < (𝐿 βˆ’ 1)))
520349, 519mpbii 232 . . . . . . . . . . . . . . 15 (πœ‘ β†’ (𝐿 βˆ’ 2) < (𝐿 βˆ’ 1))
521520adantr 482 . . . . . . . . . . . . . 14 ((πœ‘ ∧ 𝑗 ∈ (0...(𝐿 βˆ’ 2))) β†’ (𝐿 βˆ’ 2) < (𝐿 βˆ’ 1))
522509, 510, 511, 518, 521lelttrd 11320 . . . . . . . . . . . . 13 ((πœ‘ ∧ 𝑗 ∈ (0...(𝐿 βˆ’ 2))) β†’ 𝑗 < (𝐿 βˆ’ 1))
523509, 511ltnled 11309 . . . . . . . . . . . . 13 ((πœ‘ ∧ 𝑗 ∈ (0...(𝐿 βˆ’ 2))) β†’ (𝑗 < (𝐿 βˆ’ 1) ↔ Β¬ (𝐿 βˆ’ 1) ≀ 𝑗))
524522, 523mpbid 231 . . . . . . . . . . . 12 ((πœ‘ ∧ 𝑗 ∈ (0...(𝐿 βˆ’ 2))) β†’ Β¬ (𝐿 βˆ’ 1) ≀ 𝑗)
525524intnanrd 491 . . . . . . . . . . 11 ((πœ‘ ∧ 𝑗 ∈ (0...(𝐿 βˆ’ 2))) β†’ Β¬ ((𝐿 βˆ’ 1) ≀ 𝑗 ∧ 𝑗 ≀ 𝑁))
526375adantr 482 . . . . . . . . . . . 12 ((πœ‘ ∧ 𝑗 ∈ (0...(𝐿 βˆ’ 2))) β†’ (𝐿 βˆ’ 1) ∈ β„€)
527129adantr 482 . . . . . . . . . . . 12 ((πœ‘ ∧ 𝑗 ∈ (0...(𝐿 βˆ’ 2))) β†’ 𝑁 ∈ β„€)
528 elfz 13437 . . . . . . . . . . . 12 ((𝑗 ∈ β„€ ∧ (𝐿 βˆ’ 1) ∈ β„€ ∧ 𝑁 ∈ β„€) β†’ (𝑗 ∈ ((𝐿 βˆ’ 1)...𝑁) ↔ ((𝐿 βˆ’ 1) ≀ 𝑗 ∧ 𝑗 ≀ 𝑁)))
529508, 526, 527, 528syl3anc 1372 . . . . . . . . . . 11 ((πœ‘ ∧ 𝑗 ∈ (0...(𝐿 βˆ’ 2))) β†’ (𝑗 ∈ ((𝐿 βˆ’ 1)...𝑁) ↔ ((𝐿 βˆ’ 1) ≀ 𝑗 ∧ 𝑗 ≀ 𝑁)))
530525, 529mtbird 325 . . . . . . . . . 10 ((πœ‘ ∧ 𝑗 ∈ (0...(𝐿 βˆ’ 2))) β†’ Β¬ 𝑗 ∈ ((𝐿 βˆ’ 1)...𝑁))
531530ex 414 . . . . . . . . 9 (πœ‘ β†’ (𝑗 ∈ (0...(𝐿 βˆ’ 2)) β†’ Β¬ 𝑗 ∈ ((𝐿 βˆ’ 1)...𝑁)))
532506, 531ralrimi 3243 . . . . . . . 8 (πœ‘ β†’ βˆ€π‘— ∈ (0...(𝐿 βˆ’ 2)) Β¬ 𝑗 ∈ ((𝐿 βˆ’ 1)...𝑁))
533 disj 4412 . . . . . . . 8 (((0...(𝐿 βˆ’ 2)) ∩ ((𝐿 βˆ’ 1)...𝑁)) = βˆ… ↔ βˆ€π‘— ∈ (0...(𝐿 βˆ’ 2)) Β¬ 𝑗 ∈ ((𝐿 βˆ’ 1)...𝑁))
534532, 533sylibr 233 . . . . . . 7 (πœ‘ β†’ ((0...(𝐿 βˆ’ 2)) ∩ ((𝐿 βˆ’ 1)...𝑁)) = βˆ…)
535534adantr 482 . . . . . 6 ((πœ‘ ∧ Β¬ 𝐿 = 1) β†’ ((0...(𝐿 βˆ’ 2)) ∩ ((𝐿 βˆ’ 1)...𝑁)) = βˆ…)
536144adantr 482 . . . . . . . . 9 ((πœ‘ ∧ Β¬ 𝐿 = 1) β†’ (𝐿 βˆ’ 2) ≀ 𝑁)
537128, 374, 1293jca 1129 . . . . . . . . . . 11 (πœ‘ β†’ ((𝐿 βˆ’ 2) ∈ β„€ ∧ 0 ∈ β„€ ∧ 𝑁 ∈ β„€))
538537adantr 482 . . . . . . . . . 10 ((πœ‘ ∧ Β¬ 𝐿 = 1) β†’ ((𝐿 βˆ’ 2) ∈ β„€ ∧ 0 ∈ β„€ ∧ 𝑁 ∈ β„€))
539 elfz 13437 . . . . . . . . . 10 (((𝐿 βˆ’ 2) ∈ β„€ ∧ 0 ∈ β„€ ∧ 𝑁 ∈ β„€) β†’ ((𝐿 βˆ’ 2) ∈ (0...𝑁) ↔ (0 ≀ (𝐿 βˆ’ 2) ∧ (𝐿 βˆ’ 2) ≀ 𝑁)))
540538, 539syl 17 . . . . . . . . 9 ((πœ‘ ∧ Β¬ 𝐿 = 1) β†’ ((𝐿 βˆ’ 2) ∈ (0...𝑁) ↔ (0 ≀ (𝐿 βˆ’ 2) ∧ (𝐿 βˆ’ 2) ≀ 𝑁)))
541252, 536, 540mpbir2and 712 . . . . . . . 8 ((πœ‘ ∧ Β¬ 𝐿 = 1) β†’ (𝐿 βˆ’ 2) ∈ (0...𝑁))
542 fzsplit 13474 . . . . . . . 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 7377 . . . . . . . . 9 (πœ‘ β†’ (((𝐿 βˆ’ 2) + 1)...𝑁) = ((𝐿 βˆ’ 1)...𝑁))
546545uneq2d 4128 . . . . . . . 8 (πœ‘ β†’ ((0...(𝐿 βˆ’ 2)) βˆͺ (((𝐿 βˆ’ 2) + 1)...𝑁)) = ((0...(𝐿 βˆ’ 2)) βˆͺ ((𝐿 βˆ’ 1)...𝑁)))
547546adantr 482 . . . . . . 7 ((πœ‘ ∧ Β¬ 𝐿 = 1) β†’ ((0...(𝐿 βˆ’ 2)) βˆͺ (((𝐿 βˆ’ 2) + 1)...𝑁)) = ((0...(𝐿 βˆ’ 2)) βˆͺ ((𝐿 βˆ’ 1)...𝑁)))
548543, 547eqtrd 2777 . . . . . 6 ((πœ‘ ∧ Β¬ 𝐿 = 1) β†’ (0...𝑁) = ((0...(𝐿 βˆ’ 2)) βˆͺ ((𝐿 βˆ’ 1)...𝑁)))
549 fzfid 13885 . . . . . 6 ((πœ‘ ∧ Β¬ 𝐿 = 1) β†’ (0...𝑁) ∈ Fin)
550176adantr 482 . . . . . . . 8 ((πœ‘ ∧ 𝑖 ∈ (0...𝑁)) β†’ 𝐸 ∈ β„‚)
55151recnd 11190 . . . . . . . 8 ((πœ‘ ∧ 𝑖 ∈ (0...𝑁)) β†’ ((π‘‹β€˜π‘–)β€˜π‘†) ∈ β„‚)
552550, 551mulcld 11182 . . . . . . 7 ((πœ‘ ∧ 𝑖 ∈ (0...𝑁)) β†’ (𝐸 Β· ((π‘‹β€˜π‘–)β€˜π‘†)) ∈ β„‚)
553552adantlr 714 . . . . . 6 (((πœ‘ ∧ Β¬ 𝐿 = 1) ∧ 𝑖 ∈ (0...𝑁)) β†’ (𝐸 Β· ((π‘‹β€˜π‘–)β€˜π‘†)) ∈ β„‚)
554535, 548, 549, 553fsumsplit 15633 . . . . 5 ((πœ‘ ∧ Β¬ 𝐿 = 1) β†’ Σ𝑖 ∈ (0...𝑁)(𝐸 Β· ((π‘‹β€˜π‘–)β€˜π‘†)) = (Σ𝑖 ∈ (0...(𝐿 βˆ’ 2))(𝐸 Β· ((π‘‹β€˜π‘–)β€˜π‘†)) + Σ𝑖 ∈ ((𝐿 βˆ’ 1)...𝑁)(𝐸 Β· ((π‘‹β€˜π‘–)β€˜π‘†))))
555502, 505, 5543brtr4d 5142 . . . 4 ((πœ‘ ∧ Β¬ 𝐿 = 1) β†’ (𝐸 Β· Σ𝑖 ∈ (0...(𝐿 βˆ’ 2))((π‘‹β€˜π‘–)β€˜π‘†)) ≀ Σ𝑖 ∈ (0...𝑁)(𝐸 Β· ((π‘‹β€˜π‘–)β€˜π‘†)))
556114, 153, 533jca 1129 . . . . . 6 (πœ‘ β†’ (((𝐿 βˆ’ (4 / 3)) Β· 𝐸) ∈ ℝ ∧ (𝐸 Β· Σ𝑖 ∈ (0...(𝐿 βˆ’ 2))((π‘‹β€˜π‘–)β€˜π‘†)) ∈ ℝ ∧ Σ𝑖 ∈ (0...𝑁)(𝐸 Β· ((π‘‹β€˜π‘–)β€˜π‘†)) ∈ ℝ))
557556adantr 482 . . . . 5 ((πœ‘ ∧ Β¬ 𝐿 = 1) β†’ (((𝐿 βˆ’ (4 / 3)) Β· 𝐸) ∈ ℝ ∧ (𝐸 Β· Σ𝑖 ∈ (0...(𝐿 βˆ’ 2))((π‘‹β€˜π‘–)β€˜π‘†)) ∈ ℝ ∧ Σ𝑖 ∈ (0...𝑁)(𝐸 Β· ((π‘‹β€˜π‘–)β€˜π‘†)) ∈ ℝ))
558 ltletr 11254 . . . . 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 698 . . 3 ((πœ‘ ∧ Β¬ 𝐿 = 1) β†’ ((𝐿 βˆ’ (4 / 3)) Β· 𝐸) < Σ𝑖 ∈ (0...𝑁)(𝐸 Β· ((π‘‹β€˜π‘–)β€˜π‘†)))
561105, 560pm2.61dan 812 . 2 (πœ‘ β†’ ((𝐿 βˆ’ (4 / 3)) Β· 𝐸) < Σ𝑖 ∈ (0...𝑁)(𝐸 Β· ((π‘‹β€˜π‘–)β€˜π‘†)))
562 sumex 15579 . . 3 Σ𝑖 ∈ (0...𝑁)(𝐸 Β· ((π‘‹β€˜π‘–)β€˜π‘†)) ∈ V
56393oveq2d 7378 . . . . 5 (𝑑 = 𝑆 β†’ (𝐸 Β· ((π‘‹β€˜π‘–)β€˜π‘‘)) = (𝐸 Β· ((π‘‹β€˜π‘–)β€˜π‘†)))
564563sumeq2sdv 15596 . . . 4 (𝑑 = 𝑆 β†’ Σ𝑖 ∈ (0...𝑁)(𝐸 Β· ((π‘‹β€˜π‘–)β€˜π‘‘)) = Σ𝑖 ∈ (0...𝑁)(𝐸 Β· ((π‘‹β€˜π‘–)β€˜π‘†)))
565 eqid 2737 . . . 4 (𝑑 ∈ 𝑇 ↦ Σ𝑖 ∈ (0...𝑁)(𝐸 Β· ((π‘‹β€˜π‘–)β€˜π‘‘))) = (𝑑 ∈ 𝑇 ↦ Σ𝑖 ∈ (0...𝑁)(𝐸 Β· ((π‘‹β€˜π‘–)β€˜π‘‘)))
566564, 565fvmptg 6951 . . 3 ((𝑆 ∈ 𝑇 ∧ Σ𝑖 ∈ (0...𝑁)(𝐸 Β· ((π‘‹β€˜π‘–)β€˜π‘†)) ∈ V) β†’ ((𝑑 ∈ 𝑇 ↦ Σ𝑖 ∈ (0...𝑁)(𝐸 Β· ((π‘‹β€˜π‘–)β€˜π‘‘)))β€˜π‘†) = Σ𝑖 ∈ (0...𝑁)(𝐸 Β· ((π‘‹β€˜π‘–)β€˜π‘†)))
56749, 562, 566sylancl 587 . 2 (πœ‘ β†’ ((𝑑 ∈ 𝑇 ↦ Σ𝑖 ∈ (0...𝑁)(𝐸 Β· ((π‘‹β€˜π‘–)β€˜π‘‘)))β€˜π‘†) = Σ𝑖 ∈ (0...𝑁)(𝐸 Β· ((π‘‹β€˜π‘–)β€˜π‘†)))
568561, 567breqtrrd 5138 1 (πœ‘ β†’ ((𝐿 βˆ’ (4 / 3)) Β· 𝐸) < ((𝑑 ∈ 𝑇 ↦ Σ𝑖 ∈ (0...𝑁)(𝐸 Β· ((π‘‹β€˜π‘–)β€˜π‘‘)))β€˜π‘†))
Colors of variables: wff setvar class
Syntax hints:  Β¬ wn 3   β†’ wi 4   ↔ wb 205   ∧ wa 397   ∨ wo 846   ∧ w3a 1088   = wceq 1542  β„²wnf 1786   ∈ wcel 2107  β„²wnfc 2888   β‰  wne 2944  βˆ€wral 3065  {crab 3410  Vcvv 3448   βˆ– cdif 3912   βˆͺ cun 3913   ∩ cin 3914   βŠ† wss 3915  βˆ…c0 4287   class class class wbr 5110   ↦ cmpt 5193  βŸΆwf 6497  β€˜cfv 6501  (class class class)co 7362  Fincfn 8890  β„‚cc 11056  β„cr 11057  0cc0 11058  1c1 11059   + caddc 11061   Β· cmul 11063   < clt 11196   ≀ cle 11197   βˆ’ cmin 11392  -cneg 11393   / cdiv 11819  β„•cn 12160  2c2 12215  3c3 12216  4c4 12217  β„•0cn0 12420  β„€cz 12506  β„€β‰₯cuz 12770  β„+crp 12922  ...cfz 13431  β™―chash 14237  Ξ£csu 15577
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 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2155  ax-12 2172  ax-ext 2708  ax-rep 5247  ax-sep 5261  ax-nul 5268  ax-pow 5325  ax-pr 5389  ax-un 7677  ax-inf2 9584  ax-cnex 11114  ax-resscn 11115  ax-1cn 11116  ax-icn 11117  ax-addcl 11118  ax-addrcl 11119  ax-mulcl 11120  ax-mulrcl 11121  ax-mulcom 11122  ax-addass 11123  ax-mulass 11124  ax-distr 11125  ax-i2m1 11126  ax-1ne0 11127  ax-1rid 11128  ax-rnegex 11129  ax-rrecex 11130  ax-cnre 11131  ax-pre-lttri 11132  ax-pre-lttrn 11133  ax-pre-ltadd 11134  ax-pre-mulgt0 11135  ax-pre-sup 11136
This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3or 1089  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-nf 1787  df-sb 2069  df-mo 2539  df-eu 2568  df-clab 2715  df-cleq 2729  df-clel 2815  df-nfc 2890  df-ne 2945  df-nel 3051  df-ral 3066  df-rex 3075  df-rmo 3356  df-reu 3357  df-rab 3411  df-v 3450  df-sbc 3745  df-csb 3861  df-dif 3918  df-un 3920  df-in 3922  df-ss 3932  df-pss 3934  df-nul 4288  df-if 4492  df-pw 4567  df-sn 4592  df-pr 4594  df-op 4598  df-uni 4871  df-int 4913  df-iun 4961  df-br 5111  df-opab 5173  df-mpt 5194  df-tr 5228  df-id 5536  df-eprel 5542  df-po 5550  df-so 5551  df-fr 5593  df-se 5594  df-we 5595  df-xp 5644  df-rel 5645  df-cnv 5646  df-co 5647  df-dm 5648  df-rn 5649  df-res 5650  df-ima 5651  df-pred 6258  df-ord 6325  df-on 6326  df-lim 6327  df-suc 6328  df-iota 6453  df-fun 6503  df-fn 6504  df-f 6505  df-f1 6506  df-fo 6507  df-f1o 6508  df-fv 6509  df-isom 6510  df-riota 7318  df-ov 7365  df-oprab 7366  df-mpo 7367  df-om 7808  df-1st 7926  df-2nd 7927  df-frecs 8217  df-wrecs 8248  df-recs 8322  df-rdg 8361  df-1o 8417  df-er 8655  df-en 8891  df-dom 8892  df-sdom 8893  df-fin 8894  df-sup 9385  df-oi 9453  df-card 9882  df-pnf 11198  df-mnf 11199  df-xr 11200  df-ltxr 11201  df-le 11202  df-sub 11394  df-neg 11395  df-div 11820  df-nn 12161  df-2 12223  df-3 12224  df-4 12225  df-n0 12421  df-z 12507  df-uz 12771  df-rp 12923  df-ico 13277  df-fz 13432  df-fzo 13575  df-seq 13914  df-exp 13975  df-hash 14238  df-cj 14991  df-re 14992  df-im 14993  df-sqrt 15127  df-abs 15128  df-clim 15377  df-sum 15578
This theorem is referenced by:  stoweidlem34  44349
  Copyright terms: Public domain W3C validator