Metamath Proof Explorer

Theorem stoweidlem26

Description: This lemma is used to prove that there is a function g as in the proof of BrosowskiDeutsh p. 92: this lemma proves that g(t) > ( j - 4 / 3 ) * ε. Here L is used to represent j in the paper, D is used to represent A in the paper, S is used to represent t, and E is used to represent ε. (Contributed by Glauco Siliprandi, 20-Apr-2017)

Ref Expression
Hypotheses 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 stoweidlem26 ( 𝜑 → ( ( 𝐿 − ( 4 / 3 ) ) · 𝐸 ) < ( ( 𝑡 ∈ 𝑇 ↦ Σ 𝑖 ∈ ( 0 ... 𝑁 ) ( 𝐸 · ( ( 𝑋 ‘ 𝑖 ) ‘ 𝑡 ) ) ) ‘ 𝑆 ) )

Proof

Step Hyp Ref Expression
1 stoweidlem26.1 ⊢ Ⅎ 𝑡 𝐹
2 stoweidlem26.2 ⊢ Ⅎ 𝑗 𝜑
3 stoweidlem26.3 ⊢ Ⅎ 𝑡 𝜑
4 stoweidlem26.4 ⊢ 𝐷 = ( 𝑗 ∈ ( 0 ... 𝑁 ) ↦ { 𝑡 ∈ 𝑇 ∣ ( 𝐹 ‘ 𝑡 ) ≤ ( ( 𝑗 − ( 1 / 3 ) ) · 𝐸 ) } )
5 stoweidlem26.5 ⊢ 𝐵 = ( 𝑗 ∈ ( 0 ... 𝑁 ) ↦ { 𝑡 ∈ 𝑇 ∣ ( ( 𝑗 + ( 1 / 3 ) ) · 𝐸 ) ≤ ( 𝐹 ‘ 𝑡 ) } )
6 stoweidlem26.6 ⊢ ( 𝜑 → 𝑁 ∈ ℕ )
7 stoweidlem26.7 ⊢ ( 𝜑 → 𝑇 ∈ V )
8 stoweidlem26.8 ⊢ ( 𝜑 → 𝐿 ∈ ( 1 ... 𝑁 ) )
9 stoweidlem26.9 ⊢ ( 𝜑 → 𝑆 ∈ ( ( 𝐷 ‘ 𝐿 ) ∖ ( 𝐷 ‘ ( 𝐿 − 1 ) ) ) )
10 stoweidlem26.10 ⊢ ( 𝜑 → 𝐹 : 𝑇 ⟶ ℝ )
11 stoweidlem26.11 ⊢ ( 𝜑 → 𝐸 ∈ ℝ+ )
12 stoweidlem26.12 ⊢ ( 𝜑 → 𝐸 < ( 1 / 3 ) )
13 stoweidlem26.13 ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ... 𝑁 ) ) → ( 𝑋 ‘ 𝑖 ) : 𝑇 ⟶ ℝ )
14 stoweidlem26.14 ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ... 𝑁 ) ∧ 𝑡 ∈ 𝑇 ) → 0 ≤ ( ( 𝑋 ‘ 𝑖 ) ‘ 𝑡 ) )
15 stoweidlem26.15 ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ... 𝑁 ) ∧ 𝑡 ∈ ( 𝐵 ‘ 𝑖 ) ) → ( 1 − ( 𝐸 / 𝑁 ) ) < ( ( 𝑋 ‘ 𝑖 ) ‘ 𝑡 ) )
16 1re ⊢ 1 ∈ ℝ
17 eleq1 ⊢ ( 𝐿 = 1 → ( 𝐿 ∈ ℝ ↔ 1 ∈ ℝ ) )
18 16 17 mpbiri ⊢ ( 𝐿 = 1 → 𝐿 ∈ ℝ )
19 18 adantl ⊢ ( ( 𝜑 ∧ 𝐿 = 1 ) → 𝐿 ∈ ℝ )
20 4re ⊢ 4 ∈ ℝ
21 20 a1i ⊢ ( ( 𝜑 ∧ 𝐿 = 1 ) → 4 ∈ ℝ )
22 3re ⊢ 3 ∈ ℝ
23 22 a1i ⊢ ( ( 𝜑 ∧ 𝐿 = 1 ) → 3 ∈ ℝ )
24 3ne0 ⊢ 3 ≠ 0
25 24 a1i ⊢ ( ( 𝜑 ∧ 𝐿 = 1 ) → 3 ≠ 0 )
26 21 23 25 redivcld ⊢ ( ( 𝜑 ∧ 𝐿 = 1 ) → ( 4 / 3 ) ∈ ℝ )
27 19 26 resubcld ⊢ ( ( 𝜑 ∧ 𝐿 = 1 ) → ( 𝐿 − ( 4 / 3 ) ) ∈ ℝ )
28 11 rpred ⊢ ( 𝜑 → 𝐸 ∈ ℝ )
29 28 adantr ⊢ ( ( 𝜑 ∧ 𝐿 = 1 ) → 𝐸 ∈ ℝ )
30 27 29 remulcld ⊢ ( ( 𝜑 ∧ 𝐿 = 1 ) → ( ( 𝐿 − ( 4 / 3 ) ) · 𝐸 ) ∈ ℝ )
31 0red ⊢ ( ( 𝜑 ∧ 𝐿 = 1 ) → 0 ∈ ℝ )
32 fzfid ⊢ ( 𝜑 → ( 0 ... 𝑁 ) ∈ Fin )
33 28 adantr ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ... 𝑁 ) ) → 𝐸 ∈ ℝ )
34 eldif ⊢ ( 𝑆 ∈ ( ( 𝐷 ‘ 𝐿 ) ∖ ( 𝐷 ‘ ( 𝐿 − 1 ) ) ) ↔ ( 𝑆 ∈ ( 𝐷 ‘ 𝐿 ) ∧ ¬ 𝑆 ∈ ( 𝐷 ‘ ( 𝐿 − 1 ) ) ) )
35 9 34 sylib ⊢ ( 𝜑 → ( 𝑆 ∈ ( 𝐷 ‘ 𝐿 ) ∧ ¬ 𝑆 ∈ ( 𝐷 ‘ ( 𝐿 − 1 ) ) ) )
36 35 simpld ⊢ ( 𝜑 → 𝑆 ∈ ( 𝐷 ‘ 𝐿 ) )
37 oveq1 ⊢ ( 𝑗 = 𝐿 → ( 𝑗 − ( 1 / 3 ) ) = ( 𝐿 − ( 1 / 3 ) ) )
38 37 oveq1d ⊢ ( 𝑗 = 𝐿 → ( ( 𝑗 − ( 1 / 3 ) ) · 𝐸 ) = ( ( 𝐿 − ( 1 / 3 ) ) · 𝐸 ) )
39 38 breq2d ⊢ ( 𝑗 = 𝐿 → ( ( 𝐹 ‘ 𝑡 ) ≤ ( ( 𝑗 − ( 1 / 3 ) ) · 𝐸 ) ↔ ( 𝐹 ‘ 𝑡 ) ≤ ( ( 𝐿 − ( 1 / 3 ) ) · 𝐸 ) ) )
40 39 rabbidv ⊢ ( 𝑗 = 𝐿 → { 𝑡 ∈ 𝑇 ∣ ( 𝐹 ‘ 𝑡 ) ≤ ( ( 𝑗 − ( 1 / 3 ) ) · 𝐸 ) } = { 𝑡 ∈ 𝑇 ∣ ( 𝐹 ‘ 𝑡 ) ≤ ( ( 𝐿 − ( 1 / 3 ) ) · 𝐸 ) } )
41 fz1ssfz0 ⊢ ( 1 ... 𝑁 ) ⊆ ( 0 ... 𝑁 )
42 41 8 sselid ⊢ ( 𝜑 → 𝐿 ∈ ( 0 ... 𝑁 ) )
43 rabexg ⊢ ( 𝑇 ∈ V → { 𝑡 ∈ 𝑇 ∣ ( 𝐹 ‘ 𝑡 ) ≤ ( ( 𝐿 − ( 1 / 3 ) ) · 𝐸 ) } ∈ V )
44 7 43 syl ⊢ ( 𝜑 → { 𝑡 ∈ 𝑇 ∣ ( 𝐹 ‘ 𝑡 ) ≤ ( ( 𝐿 − ( 1 / 3 ) ) · 𝐸 ) } ∈ V )
45 4 40 42 44 fvmptd3 ⊢ ( 𝜑 → ( 𝐷 ‘ 𝐿 ) = { 𝑡 ∈ 𝑇 ∣ ( 𝐹 ‘ 𝑡 ) ≤ ( ( 𝐿 − ( 1 / 3 ) ) · 𝐸 ) } )
46 36 45 eleqtrd ⊢ ( 𝜑 → 𝑆 ∈ { 𝑡 ∈ 𝑇 ∣ ( 𝐹 ‘ 𝑡 ) ≤ ( ( 𝐿 − ( 1 / 3 ) ) · 𝐸 ) } )
47 nfcv ⊢ Ⅎ 𝑡 𝑆
48 nfcv ⊢ Ⅎ 𝑡 𝑇
49 1 47 nffv ⊢ Ⅎ 𝑡 ( 𝐹 ‘ 𝑆 )
50 nfcv ⊢ Ⅎ 𝑡 ≤
51 nfcv ⊢ Ⅎ 𝑡 ( ( 𝐿 − ( 1 / 3 ) ) · 𝐸 )
52 49 50 51 nfbr ⊢ Ⅎ 𝑡 ( 𝐹 ‘ 𝑆 ) ≤ ( ( 𝐿 − ( 1 / 3 ) ) · 𝐸 )
53 fveq2 ⊢ ( 𝑡 = 𝑆 → ( 𝐹 ‘ 𝑡 ) = ( 𝐹 ‘ 𝑆 ) )
54 53 breq1d ⊢ ( 𝑡 = 𝑆 → ( ( 𝐹 ‘ 𝑡 ) ≤ ( ( 𝐿 − ( 1 / 3 ) ) · 𝐸 ) ↔ ( 𝐹 ‘ 𝑆 ) ≤ ( ( 𝐿 − ( 1 / 3 ) ) · 𝐸 ) ) )
55 47 48 52 54 elrabf ⊢ ( 𝑆 ∈ { 𝑡 ∈ 𝑇 ∣ ( 𝐹 ‘ 𝑡 ) ≤ ( ( 𝐿 − ( 1 / 3 ) ) · 𝐸 ) } ↔ ( 𝑆 ∈ 𝑇 ∧ ( 𝐹 ‘ 𝑆 ) ≤ ( ( 𝐿 − ( 1 / 3 ) ) · 𝐸 ) ) )
56 46 55 sylib ⊢ ( 𝜑 → ( 𝑆 ∈ 𝑇 ∧ ( 𝐹 ‘ 𝑆 ) ≤ ( ( 𝐿 − ( 1 / 3 ) ) · 𝐸 ) ) )
57 56 simpld ⊢ ( 𝜑 → 𝑆 ∈ 𝑇 )
58 57 adantr ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ... 𝑁 ) ) → 𝑆 ∈ 𝑇 )
59 13 58 ffvelcdmd ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ... 𝑁 ) ) → ( ( 𝑋 ‘ 𝑖 ) ‘ 𝑆 ) ∈ ℝ )
60 33 59 remulcld ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ... 𝑁 ) ) → ( 𝐸 · ( ( 𝑋 ‘ 𝑖 ) ‘ 𝑆 ) ) ∈ ℝ )
61 32 60 fsumrecl ⊢ ( 𝜑 → Σ 𝑖 ∈ ( 0 ... 𝑁 ) ( 𝐸 · ( ( 𝑋 ‘ 𝑖 ) ‘ 𝑆 ) ) ∈ ℝ )
62 61 adantr ⊢ ( ( 𝜑 ∧ 𝐿 = 1 ) → Σ 𝑖 ∈ ( 0 ... 𝑁 ) ( 𝐸 · ( ( 𝑋 ‘ 𝑖 ) ‘ 𝑆 ) ) ∈ ℝ )
63 20 22 24 redivcli ⊢ ( 4 / 3 ) ∈ ℝ
64 63 a1i ⊢ ( ( 𝜑 ∧ 𝐿 = 1 ) → ( 4 / 3 ) ∈ ℝ )
65 19 64 resubcld ⊢ ( ( 𝜑 ∧ 𝐿 = 1 ) → ( 𝐿 − ( 4 / 3 ) ) ∈ ℝ )
66 19 recnd ⊢ ( ( 𝜑 ∧ 𝐿 = 1 ) → 𝐿 ∈ ℂ )
67 66 subid1d ⊢ ( ( 𝜑 ∧ 𝐿 = 1 ) → ( 𝐿 − 0 ) = 𝐿 )
68 3cn ⊢ 3 ∈ ℂ
69 68 24 dividi ⊢ ( 3 / 3 ) = 1
70 3lt4 ⊢ 3 < 4
71 3pos ⊢ 0 < 3
72 22 20 22 71 ltdiv1ii ⊢ ( 3 < 4 ↔ ( 3 / 3 ) < ( 4 / 3 ) )
73 70 72 mpbi ⊢ ( 3 / 3 ) < ( 4 / 3 )
74 69 73 eqbrtrri ⊢ 1 < ( 4 / 3 )
75 breq1 ⊢ ( 𝐿 = 1 → ( 𝐿 < ( 4 / 3 ) ↔ 1 < ( 4 / 3 ) ) )
76 75 adantl ⊢ ( ( 𝜑 ∧ 𝐿 = 1 ) → ( 𝐿 < ( 4 / 3 ) ↔ 1 < ( 4 / 3 ) ) )
77 74 76 mpbiri ⊢ ( ( 𝜑 ∧ 𝐿 = 1 ) → 𝐿 < ( 4 / 3 ) )
78 67 77 eqbrtrd ⊢ ( ( 𝜑 ∧ 𝐿 = 1 ) → ( 𝐿 − 0 ) < ( 4 / 3 ) )
79 19 31 64 78 ltsub23d ⊢ ( ( 𝜑 ∧ 𝐿 = 1 ) → ( 𝐿 − ( 4 / 3 ) ) < 0 )
80 11 rpgt0d ⊢ ( 𝜑 → 0 < 𝐸 )
81 80 adantr ⊢ ( ( 𝜑 ∧ 𝐿 = 1 ) → 0 < 𝐸 )
82 mulltgt0 ⊢ ( ( ( ( 𝐿 − ( 4 / 3 ) ) ∈ ℝ ∧ ( 𝐿 − ( 4 / 3 ) ) < 0 ) ∧ ( 𝐸 ∈ ℝ ∧ 0 < 𝐸 ) ) → ( ( 𝐿 − ( 4 / 3 ) ) · 𝐸 ) < 0 )
83 65 79 29 81 82 syl22anc ⊢ ( ( 𝜑 ∧ 𝐿 = 1 ) → ( ( 𝐿 − ( 4 / 3 ) ) · 𝐸 ) < 0 )
84 0cn ⊢ 0 ∈ ℂ
85 fsumconst ⊢ ( ( ( 0 ... 𝑁 ) ∈ Fin ∧ 0 ∈ ℂ ) → Σ 𝑖 ∈ ( 0 ... 𝑁 ) 0 = ( ( ♯ ‘ ( 0 ... 𝑁 ) ) · 0 ) )
86 32 84 85 sylancl ⊢ ( 𝜑 → Σ 𝑖 ∈ ( 0 ... 𝑁 ) 0 = ( ( ♯ ‘ ( 0 ... 𝑁 ) ) · 0 ) )
87 hashcl ⊢ ( ( 0 ... 𝑁 ) ∈ Fin → ( ♯ ‘ ( 0 ... 𝑁 ) ) ∈ ℕ0 )
88 nn0cn ⊢ ( ( ♯ ‘ ( 0 ... 𝑁 ) ) ∈ ℕ0 → ( ♯ ‘ ( 0 ... 𝑁 ) ) ∈ ℂ )
89 32 87 88 3syl ⊢ ( 𝜑 → ( ♯ ‘ ( 0 ... 𝑁 ) ) ∈ ℂ )
90 89 mul01d ⊢ ( 𝜑 → ( ( ♯ ‘ ( 0 ... 𝑁 ) ) · 0 ) = 0 )
91 86 90 eqtrd ⊢ ( 𝜑 → Σ 𝑖 ∈ ( 0 ... 𝑁 ) 0 = 0 )
92 91 adantr ⊢ ( ( 𝜑 ∧ 𝐿 = 1 ) → Σ 𝑖 ∈ ( 0 ... 𝑁 ) 0 = 0 )
93 0red ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ... 𝑁 ) ) → 0 ∈ ℝ )
94 11 rpge0d ⊢ ( 𝜑 → 0 ≤ 𝐸 )
95 94 adantr ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ... 𝑁 ) ) → 0 ≤ 𝐸 )
96 nfv ⊢ Ⅎ 𝑡 𝑖 ∈ ( 0 ... 𝑁 )
97 3 96 nfan ⊢ Ⅎ 𝑡 ( 𝜑 ∧ 𝑖 ∈ ( 0 ... 𝑁 ) )
98 nfv ⊢ Ⅎ 𝑡 0 ≤ ( ( 𝑋 ‘ 𝑖 ) ‘ 𝑆 )
99 97 98 nfim ⊢ Ⅎ 𝑡 ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ... 𝑁 ) ) → 0 ≤ ( ( 𝑋 ‘ 𝑖 ) ‘ 𝑆 ) )
100 fveq2 ⊢ ( 𝑡 = 𝑆 → ( ( 𝑋 ‘ 𝑖 ) ‘ 𝑡 ) = ( ( 𝑋 ‘ 𝑖 ) ‘ 𝑆 ) )
101 100 breq2d ⊢ ( 𝑡 = 𝑆 → ( 0 ≤ ( ( 𝑋 ‘ 𝑖 ) ‘ 𝑡 ) ↔ 0 ≤ ( ( 𝑋 ‘ 𝑖 ) ‘ 𝑆 ) ) )
102 101 imbi2d ⊢ ( 𝑡 = 𝑆 → ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ... 𝑁 ) ) → 0 ≤ ( ( 𝑋 ‘ 𝑖 ) ‘ 𝑡 ) ) ↔ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ... 𝑁 ) ) → 0 ≤ ( ( 𝑋 ‘ 𝑖 ) ‘ 𝑆 ) ) ) )
103 14 3expia ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ... 𝑁 ) ) → ( 𝑡 ∈ 𝑇 → 0 ≤ ( ( 𝑋 ‘ 𝑖 ) ‘ 𝑡 ) ) )
104 103 com12 ⊢ ( 𝑡 ∈ 𝑇 → ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ... 𝑁 ) ) → 0 ≤ ( ( 𝑋 ‘ 𝑖 ) ‘ 𝑡 ) ) )
105 47 99 102 104 vtoclgaf ⊢ ( 𝑆 ∈ 𝑇 → ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ... 𝑁 ) ) → 0 ≤ ( ( 𝑋 ‘ 𝑖 ) ‘ 𝑆 ) ) )
106 58 105 mpcom ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ... 𝑁 ) ) → 0 ≤ ( ( 𝑋 ‘ 𝑖 ) ‘ 𝑆 ) )
107 33 59 95 106 mulge0d ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ... 𝑁 ) ) → 0 ≤ ( 𝐸 · ( ( 𝑋 ‘ 𝑖 ) ‘ 𝑆 ) ) )
108 32 93 60 107 fsumle ⊢ ( 𝜑 → Σ 𝑖 ∈ ( 0 ... 𝑁 ) 0 ≤ Σ 𝑖 ∈ ( 0 ... 𝑁 ) ( 𝐸 · ( ( 𝑋 ‘ 𝑖 ) ‘ 𝑆 ) ) )
109 108 adantr ⊢ ( ( 𝜑 ∧ 𝐿 = 1 ) → Σ 𝑖 ∈ ( 0 ... 𝑁 ) 0 ≤ Σ 𝑖 ∈ ( 0 ... 𝑁 ) ( 𝐸 · ( ( 𝑋 ‘ 𝑖 ) ‘ 𝑆 ) ) )
110 92 109 eqbrtrrd ⊢ ( ( 𝜑 ∧ 𝐿 = 1 ) → 0 ≤ Σ 𝑖 ∈ ( 0 ... 𝑁 ) ( 𝐸 · ( ( 𝑋 ‘ 𝑖 ) ‘ 𝑆 ) ) )
111 30 31 62 83 110 ltletrd ⊢ ( ( 𝜑 ∧ 𝐿 = 1 ) → ( ( 𝐿 − ( 4 / 3 ) ) · 𝐸 ) < Σ 𝑖 ∈ ( 0 ... 𝑁 ) ( 𝐸 · ( ( 𝑋 ‘ 𝑖 ) ‘ 𝑆 ) ) )
112 elfzelz ⊢ ( 𝐿 ∈ ( 1 ... 𝑁 ) → 𝐿 ∈ ℤ )
113 zre ⊢ ( 𝐿 ∈ ℤ → 𝐿 ∈ ℝ )
114 8 112 113 3syl ⊢ ( 𝜑 → 𝐿 ∈ ℝ )
115 20 a1i ⊢ ( 𝜑 → 4 ∈ ℝ )
116 22 a1i ⊢ ( 𝜑 → 3 ∈ ℝ )
117 24 a1i ⊢ ( 𝜑 → 3 ≠ 0 )
118 115 116 117 redivcld ⊢ ( 𝜑 → ( 4 / 3 ) ∈ ℝ )
119 114 118 resubcld ⊢ ( 𝜑 → ( 𝐿 − ( 4 / 3 ) ) ∈ ℝ )
120 119 28 remulcld ⊢ ( 𝜑 → ( ( 𝐿 − ( 4 / 3 ) ) · 𝐸 ) ∈ ℝ )
121 120 adantr ⊢ ( ( 𝜑 ∧ ¬ 𝐿 = 1 ) → ( ( 𝐿 − ( 4 / 3 ) ) · 𝐸 ) ∈ ℝ )
122 16 a1i ⊢ ( 𝜑 → 1 ∈ ℝ )
123 28 6 nndivred ⊢ ( 𝜑 → ( 𝐸 / 𝑁 ) ∈ ℝ )
124 122 123 resubcld ⊢ ( 𝜑 → ( 1 − ( 𝐸 / 𝑁 ) ) ∈ ℝ )
125 114 122 resubcld ⊢ ( 𝜑 → ( 𝐿 − 1 ) ∈ ℝ )
126 124 125 remulcld ⊢ ( 𝜑 → ( ( 1 − ( 𝐸 / 𝑁 ) ) · ( 𝐿 − 1 ) ) ∈ ℝ )
127 28 126 remulcld ⊢ ( 𝜑 → ( 𝐸 · ( ( 1 − ( 𝐸 / 𝑁 ) ) · ( 𝐿 − 1 ) ) ) ∈ ℝ )
128 127 adantr ⊢ ( ( 𝜑 ∧ ¬ 𝐿 = 1 ) → ( 𝐸 · ( ( 1 − ( 𝐸 / 𝑁 ) ) · ( 𝐿 − 1 ) ) ) ∈ ℝ )
129 fzfid ⊢ ( 𝜑 → ( 0 ... ( 𝐿 − 2 ) ) ∈ Fin )
130 8 elfzelzd ⊢ ( 𝜑 → 𝐿 ∈ ℤ )
131 2z ⊢ 2 ∈ ℤ
132 131 a1i ⊢ ( 𝜑 → 2 ∈ ℤ )
133 130 132 zsubcld ⊢ ( 𝜑 → ( 𝐿 − 2 ) ∈ ℤ )
134 6 nnzd ⊢ ( 𝜑 → 𝑁 ∈ ℤ )
135 130 zred ⊢ ( 𝜑 → 𝐿 ∈ ℝ )
136 2re ⊢ 2 ∈ ℝ
137 136 a1i ⊢ ( 𝜑 → 2 ∈ ℝ )
138 135 137 resubcld ⊢ ( 𝜑 → ( 𝐿 − 2 ) ∈ ℝ )
139 6 nnred ⊢ ( 𝜑 → 𝑁 ∈ ℝ )
140 0le2 ⊢ 0 ≤ 2
141 0red ⊢ ( 𝜑 → 0 ∈ ℝ )
142 141 137 135 lesub2d ⊢ ( 𝜑 → ( 0 ≤ 2 ↔ ( 𝐿 − 2 ) ≤ ( 𝐿 − 0 ) ) )
143 140 142 mpbii ⊢ ( 𝜑 → ( 𝐿 − 2 ) ≤ ( 𝐿 − 0 ) )
144 130 zcnd ⊢ ( 𝜑 → 𝐿 ∈ ℂ )
145 144 subid1d ⊢ ( 𝜑 → ( 𝐿 − 0 ) = 𝐿 )
146 143 145 breqtrd ⊢ ( 𝜑 → ( 𝐿 − 2 ) ≤ 𝐿 )
147 elfzle2 ⊢ ( 𝐿 ∈ ( 1 ... 𝑁 ) → 𝐿 ≤ 𝑁 )
148 8 147 syl ⊢ ( 𝜑 → 𝐿 ≤ 𝑁 )
149 138 135 139 146 148 letrd ⊢ ( 𝜑 → ( 𝐿 − 2 ) ≤ 𝑁 )
150 133 134 149 3jca ⊢ ( 𝜑 → ( ( 𝐿 − 2 ) ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ ( 𝐿 − 2 ) ≤ 𝑁 ) )
151 eluz2 ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ ( 𝐿 − 2 ) ) ↔ ( ( 𝐿 − 2 ) ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ ( 𝐿 − 2 ) ≤ 𝑁 ) )
152 150 151 sylibr ⊢ ( 𝜑 → 𝑁 ∈ ( ℤ≥ ‘ ( 𝐿 − 2 ) ) )
153 fzss2 ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ ( 𝐿 − 2 ) ) → ( 0 ... ( 𝐿 − 2 ) ) ⊆ ( 0 ... 𝑁 ) )
154 152 153 syl ⊢ ( 𝜑 → ( 0 ... ( 𝐿 − 2 ) ) ⊆ ( 0 ... 𝑁 ) )
155 154 sselda ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ... ( 𝐿 − 2 ) ) ) → 𝑖 ∈ ( 0 ... 𝑁 ) )
156 155 59 syldan ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ... ( 𝐿 − 2 ) ) ) → ( ( 𝑋 ‘ 𝑖 ) ‘ 𝑆 ) ∈ ℝ )
157 129 156 fsumrecl ⊢ ( 𝜑 → Σ 𝑖 ∈ ( 0 ... ( 𝐿 − 2 ) ) ( ( 𝑋 ‘ 𝑖 ) ‘ 𝑆 ) ∈ ℝ )
158 28 157 remulcld ⊢ ( 𝜑 → ( 𝐸 · Σ 𝑖 ∈ ( 0 ... ( 𝐿 − 2 ) ) ( ( 𝑋 ‘ 𝑖 ) ‘ 𝑆 ) ) ∈ ℝ )
159 158 adantr ⊢ ( ( 𝜑 ∧ ¬ 𝐿 = 1 ) → ( 𝐸 · Σ 𝑖 ∈ ( 0 ... ( 𝐿 − 2 ) ) ( ( 𝑋 ‘ 𝑖 ) ‘ 𝑆 ) ) ∈ ℝ )
160 28 125 remulcld ⊢ ( 𝜑 → ( 𝐸 · ( 𝐿 − 1 ) ) ∈ ℝ )
161 28 28 remulcld ⊢ ( 𝜑 → ( 𝐸 · 𝐸 ) ∈ ℝ )
162 160 161 resubcld ⊢ ( 𝜑 → ( ( 𝐸 · ( 𝐿 − 1 ) ) − ( 𝐸 · 𝐸 ) ) ∈ ℝ )
163 125 6 nndivred ⊢ ( 𝜑 → ( ( 𝐿 − 1 ) / 𝑁 ) ∈ ℝ )
164 161 163 remulcld ⊢ ( 𝜑 → ( ( 𝐸 · 𝐸 ) · ( ( 𝐿 − 1 ) / 𝑁 ) ) ∈ ℝ )
165 160 164 resubcld ⊢ ( 𝜑 → ( ( 𝐸 · ( 𝐿 − 1 ) ) − ( ( 𝐸 · 𝐸 ) · ( ( 𝐿 − 1 ) / 𝑁 ) ) ) ∈ ℝ )
166 125 28 resubcld ⊢ ( 𝜑 → ( ( 𝐿 − 1 ) − 𝐸 ) ∈ ℝ )
167 122 28 readdcld ⊢ ( 𝜑 → ( 1 + 𝐸 ) ∈ ℝ )
168 16 22 24 redivcli ⊢ ( 1 / 3 ) ∈ ℝ
169 168 a1i ⊢ ( 𝜑 → ( 1 / 3 ) ∈ ℝ )
170 28 169 122 12 ltadd2dd ⊢ ( 𝜑 → ( 1 + 𝐸 ) < ( 1 + ( 1 / 3 ) ) )
171 ax-1cn ⊢ 1 ∈ ℂ
172 68 171 68 24 divdiri ⊢ ( ( 3 + 1 ) / 3 ) = ( ( 3 / 3 ) + ( 1 / 3 ) )
173 3p1e4 ⊢ ( 3 + 1 ) = 4
174 173 oveq1i ⊢ ( ( 3 + 1 ) / 3 ) = ( 4 / 3 )
175 69 oveq1i ⊢ ( ( 3 / 3 ) + ( 1 / 3 ) ) = ( 1 + ( 1 / 3 ) )
176 172 174 175 3eqtr3ri ⊢ ( 1 + ( 1 / 3 ) ) = ( 4 / 3 )
177 170 176 breqtrdi ⊢ ( 𝜑 → ( 1 + 𝐸 ) < ( 4 / 3 ) )
178 167 118 114 177 ltsub2dd ⊢ ( 𝜑 → ( 𝐿 − ( 4 / 3 ) ) < ( 𝐿 − ( 1 + 𝐸 ) ) )
179 171 a1i ⊢ ( 𝜑 → 1 ∈ ℂ )
180 11 rpcnd ⊢ ( 𝜑 → 𝐸 ∈ ℂ )
181 144 179 180 subsub4d ⊢ ( 𝜑 → ( ( 𝐿 − 1 ) − 𝐸 ) = ( 𝐿 − ( 1 + 𝐸 ) ) )
182 178 181 breqtrrd ⊢ ( 𝜑 → ( 𝐿 − ( 4 / 3 ) ) < ( ( 𝐿 − 1 ) − 𝐸 ) )
183 119 166 11 182 ltmul1dd ⊢ ( 𝜑 → ( ( 𝐿 − ( 4 / 3 ) ) · 𝐸 ) < ( ( ( 𝐿 − 1 ) − 𝐸 ) · 𝐸 ) )
184 144 179 subcld ⊢ ( 𝜑 → ( 𝐿 − 1 ) ∈ ℂ )
185 184 180 subcld ⊢ ( 𝜑 → ( ( 𝐿 − 1 ) − 𝐸 ) ∈ ℂ )
186 180 185 mulcomd ⊢ ( 𝜑 → ( 𝐸 · ( ( 𝐿 − 1 ) − 𝐸 ) ) = ( ( ( 𝐿 − 1 ) − 𝐸 ) · 𝐸 ) )
187 180 184 180 subdid ⊢ ( 𝜑 → ( 𝐸 · ( ( 𝐿 − 1 ) − 𝐸 ) ) = ( ( 𝐸 · ( 𝐿 − 1 ) ) − ( 𝐸 · 𝐸 ) ) )
188 186 187 eqtr3d ⊢ ( 𝜑 → ( ( ( 𝐿 − 1 ) − 𝐸 ) · 𝐸 ) = ( ( 𝐸 · ( 𝐿 − 1 ) ) − ( 𝐸 · 𝐸 ) ) )
189 183 188 breqtrd ⊢ ( 𝜑 → ( ( 𝐿 − ( 4 / 3 ) ) · 𝐸 ) < ( ( 𝐸 · ( 𝐿 − 1 ) ) − ( 𝐸 · 𝐸 ) ) )
190 1zzd ⊢ ( 𝜑 → 1 ∈ ℤ )
191 elfz ⊢ ( ( 𝐿 ∈ ℤ ∧ 1 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( 𝐿 ∈ ( 1 ... 𝑁 ) ↔ ( 1 ≤ 𝐿 ∧ 𝐿 ≤ 𝑁 ) ) )
192 130 190 134 191 syl3anc ⊢ ( 𝜑 → ( 𝐿 ∈ ( 1 ... 𝑁 ) ↔ ( 1 ≤ 𝐿 ∧ 𝐿 ≤ 𝑁 ) ) )
193 8 192 mpbid ⊢ ( 𝜑 → ( 1 ≤ 𝐿 ∧ 𝐿 ≤ 𝑁 ) )
194 193 simprd ⊢ ( 𝜑 → 𝐿 ≤ 𝑁 )
195 zlem1lt ⊢ ( ( 𝐿 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( 𝐿 ≤ 𝑁 ↔ ( 𝐿 − 1 ) < 𝑁 ) )
196 130 134 195 syl2anc ⊢ ( 𝜑 → ( 𝐿 ≤ 𝑁 ↔ ( 𝐿 − 1 ) < 𝑁 ) )
197 194 196 mpbid ⊢ ( 𝜑 → ( 𝐿 − 1 ) < 𝑁 )
198 6 nngt0d ⊢ ( 𝜑 → 0 < 𝑁 )
199 ltdiv1 ⊢ ( ( ( 𝐿 − 1 ) ∈ ℝ ∧ 𝑁 ∈ ℝ ∧ ( 𝑁 ∈ ℝ ∧ 0 < 𝑁 ) ) → ( ( 𝐿 − 1 ) < 𝑁 ↔ ( ( 𝐿 − 1 ) / 𝑁 ) < ( 𝑁 / 𝑁 ) ) )
200 125 139 139 198 199 syl112anc ⊢ ( 𝜑 → ( ( 𝐿 − 1 ) < 𝑁 ↔ ( ( 𝐿 − 1 ) / 𝑁 ) < ( 𝑁 / 𝑁 ) ) )
201 197 200 mpbid ⊢ ( 𝜑 → ( ( 𝐿 − 1 ) / 𝑁 ) < ( 𝑁 / 𝑁 ) )
202 6 nncnd ⊢ ( 𝜑 → 𝑁 ∈ ℂ )
203 6 nnne0d ⊢ ( 𝜑 → 𝑁 ≠ 0 )
204 202 203 dividd ⊢ ( 𝜑 → ( 𝑁 / 𝑁 ) = 1 )
205 201 204 breqtrd ⊢ ( 𝜑 → ( ( 𝐿 − 1 ) / 𝑁 ) < 1 )
206 28 28 80 80 mulgt0d ⊢ ( 𝜑 → 0 < ( 𝐸 · 𝐸 ) )
207 ltmul2 ⊢ ( ( ( ( 𝐿 − 1 ) / 𝑁 ) ∈ ℝ ∧ 1 ∈ ℝ ∧ ( ( 𝐸 · 𝐸 ) ∈ ℝ ∧ 0 < ( 𝐸 · 𝐸 ) ) ) → ( ( ( 𝐿 − 1 ) / 𝑁 ) < 1 ↔ ( ( 𝐸 · 𝐸 ) · ( ( 𝐿 − 1 ) / 𝑁 ) ) < ( ( 𝐸 · 𝐸 ) · 1 ) ) )
208 163 122 161 206 207 syl112anc ⊢ ( 𝜑 → ( ( ( 𝐿 − 1 ) / 𝑁 ) < 1 ↔ ( ( 𝐸 · 𝐸 ) · ( ( 𝐿 − 1 ) / 𝑁 ) ) < ( ( 𝐸 · 𝐸 ) · 1 ) ) )
209 205 208 mpbid ⊢ ( 𝜑 → ( ( 𝐸 · 𝐸 ) · ( ( 𝐿 − 1 ) / 𝑁 ) ) < ( ( 𝐸 · 𝐸 ) · 1 ) )
210 180 180 mulcld ⊢ ( 𝜑 → ( 𝐸 · 𝐸 ) ∈ ℂ )
211 210 mulridd ⊢ ( 𝜑 → ( ( 𝐸 · 𝐸 ) · 1 ) = ( 𝐸 · 𝐸 ) )
212 209 211 breqtrd ⊢ ( 𝜑 → ( ( 𝐸 · 𝐸 ) · ( ( 𝐿 − 1 ) / 𝑁 ) ) < ( 𝐸 · 𝐸 ) )
213 164 161 160 212 ltsub2dd ⊢ ( 𝜑 → ( ( 𝐸 · ( 𝐿 − 1 ) ) − ( 𝐸 · 𝐸 ) ) < ( ( 𝐸 · ( 𝐿 − 1 ) ) − ( ( 𝐸 · 𝐸 ) · ( ( 𝐿 − 1 ) / 𝑁 ) ) ) )
214 120 162 165 189 213 lttrd ⊢ ( 𝜑 → ( ( 𝐿 − ( 4 / 3 ) ) · 𝐸 ) < ( ( 𝐸 · ( 𝐿 − 1 ) ) − ( ( 𝐸 · 𝐸 ) · ( ( 𝐿 − 1 ) / 𝑁 ) ) ) )
215 180 202 203 divcld ⊢ ( 𝜑 → ( 𝐸 / 𝑁 ) ∈ ℂ )
216 179 215 184 subdird ⊢ ( 𝜑 → ( ( 1 − ( 𝐸 / 𝑁 ) ) · ( 𝐿 − 1 ) ) = ( ( 1 · ( 𝐿 − 1 ) ) − ( ( 𝐸 / 𝑁 ) · ( 𝐿 − 1 ) ) ) )
217 184 mullidd ⊢ ( 𝜑 → ( 1 · ( 𝐿 − 1 ) ) = ( 𝐿 − 1 ) )
218 217 oveq1d ⊢ ( 𝜑 → ( ( 1 · ( 𝐿 − 1 ) ) − ( ( 𝐸 / 𝑁 ) · ( 𝐿 − 1 ) ) ) = ( ( 𝐿 − 1 ) − ( ( 𝐸 / 𝑁 ) · ( 𝐿 − 1 ) ) ) )
219 216 218 eqtrd ⊢ ( 𝜑 → ( ( 1 − ( 𝐸 / 𝑁 ) ) · ( 𝐿 − 1 ) ) = ( ( 𝐿 − 1 ) − ( ( 𝐸 / 𝑁 ) · ( 𝐿 − 1 ) ) ) )
220 219 oveq2d ⊢ ( 𝜑 → ( 𝐸 · ( ( 1 − ( 𝐸 / 𝑁 ) ) · ( 𝐿 − 1 ) ) ) = ( 𝐸 · ( ( 𝐿 − 1 ) − ( ( 𝐸 / 𝑁 ) · ( 𝐿 − 1 ) ) ) ) )
221 215 184 mulcld ⊢ ( 𝜑 → ( ( 𝐸 / 𝑁 ) · ( 𝐿 − 1 ) ) ∈ ℂ )
222 180 184 221 subdid ⊢ ( 𝜑 → ( 𝐸 · ( ( 𝐿 − 1 ) − ( ( 𝐸 / 𝑁 ) · ( 𝐿 − 1 ) ) ) ) = ( ( 𝐸 · ( 𝐿 − 1 ) ) − ( 𝐸 · ( ( 𝐸 / 𝑁 ) · ( 𝐿 − 1 ) ) ) ) )
223 180 202 184 203 div32d ⊢ ( 𝜑 → ( ( 𝐸 / 𝑁 ) · ( 𝐿 − 1 ) ) = ( 𝐸 · ( ( 𝐿 − 1 ) / 𝑁 ) ) )
224 223 oveq2d ⊢ ( 𝜑 → ( 𝐸 · ( ( 𝐸 / 𝑁 ) · ( 𝐿 − 1 ) ) ) = ( 𝐸 · ( 𝐸 · ( ( 𝐿 − 1 ) / 𝑁 ) ) ) )
225 184 202 203 divcld ⊢ ( 𝜑 → ( ( 𝐿 − 1 ) / 𝑁 ) ∈ ℂ )
226 180 180 225 mulassd ⊢ ( 𝜑 → ( ( 𝐸 · 𝐸 ) · ( ( 𝐿 − 1 ) / 𝑁 ) ) = ( 𝐸 · ( 𝐸 · ( ( 𝐿 − 1 ) / 𝑁 ) ) ) )
227 224 226 eqtr4d ⊢ ( 𝜑 → ( 𝐸 · ( ( 𝐸 / 𝑁 ) · ( 𝐿 − 1 ) ) ) = ( ( 𝐸 · 𝐸 ) · ( ( 𝐿 − 1 ) / 𝑁 ) ) )
228 227 oveq2d ⊢ ( 𝜑 → ( ( 𝐸 · ( 𝐿 − 1 ) ) − ( 𝐸 · ( ( 𝐸 / 𝑁 ) · ( 𝐿 − 1 ) ) ) ) = ( ( 𝐸 · ( 𝐿 − 1 ) ) − ( ( 𝐸 · 𝐸 ) · ( ( 𝐿 − 1 ) / 𝑁 ) ) ) )
229 220 222 228 3eqtrd ⊢ ( 𝜑 → ( 𝐸 · ( ( 1 − ( 𝐸 / 𝑁 ) ) · ( 𝐿 − 1 ) ) ) = ( ( 𝐸 · ( 𝐿 − 1 ) ) − ( ( 𝐸 · 𝐸 ) · ( ( 𝐿 − 1 ) / 𝑁 ) ) ) )
230 214 229 breqtrrd ⊢ ( 𝜑 → ( ( 𝐿 − ( 4 / 3 ) ) · 𝐸 ) < ( 𝐸 · ( ( 1 − ( 𝐸 / 𝑁 ) ) · ( 𝐿 − 1 ) ) ) )
231 230 adantr ⊢ ( ( 𝜑 ∧ ¬ 𝐿 = 1 ) → ( ( 𝐿 − ( 4 / 3 ) ) · 𝐸 ) < ( 𝐸 · ( ( 1 − ( 𝐸 / 𝑁 ) ) · ( 𝐿 − 1 ) ) ) )
232 179 215 subcld ⊢ ( 𝜑 → ( 1 − ( 𝐸 / 𝑁 ) ) ∈ ℂ )
233 fsumconst ⊢ ( ( ( 0 ... ( 𝐿 − 2 ) ) ∈ Fin ∧ ( 1 − ( 𝐸 / 𝑁 ) ) ∈ ℂ ) → Σ 𝑖 ∈ ( 0 ... ( 𝐿 − 2 ) ) ( 1 − ( 𝐸 / 𝑁 ) ) = ( ( ♯ ‘ ( 0 ... ( 𝐿 − 2 ) ) ) · ( 1 − ( 𝐸 / 𝑁 ) ) ) )
234 129 232 233 syl2anc ⊢ ( 𝜑 → Σ 𝑖 ∈ ( 0 ... ( 𝐿 − 2 ) ) ( 1 − ( 𝐸 / 𝑁 ) ) = ( ( ♯ ‘ ( 0 ... ( 𝐿 − 2 ) ) ) · ( 1 − ( 𝐸 / 𝑁 ) ) ) )
235 234 adantr ⊢ ( ( 𝜑 ∧ ¬ 𝐿 = 1 ) → Σ 𝑖 ∈ ( 0 ... ( 𝐿 − 2 ) ) ( 1 − ( 𝐸 / 𝑁 ) ) = ( ( ♯ ‘ ( 0 ... ( 𝐿 − 2 ) ) ) · ( 1 − ( 𝐸 / 𝑁 ) ) ) )
236 0zd ⊢ ( ( 𝜑 ∧ ¬ 𝐿 = 1 ) → 0 ∈ ℤ )
237 8 adantr ⊢ ( ( 𝜑 ∧ ¬ 𝐿 = 1 ) → 𝐿 ∈ ( 1 ... 𝑁 ) )
238 237 elfzelzd ⊢ ( ( 𝜑 ∧ ¬ 𝐿 = 1 ) → 𝐿 ∈ ℤ )
239 131 a1i ⊢ ( ( 𝜑 ∧ ¬ 𝐿 = 1 ) → 2 ∈ ℤ )
240 238 239 zsubcld ⊢ ( ( 𝜑 ∧ ¬ 𝐿 = 1 ) → ( 𝐿 − 2 ) ∈ ℤ )
241 elnnuz ⊢ ( 𝑁 ∈ ℕ ↔ 𝑁 ∈ ( ℤ≥ ‘ 1 ) )
242 6 241 sylib ⊢ ( 𝜑 → 𝑁 ∈ ( ℤ≥ ‘ 1 ) )
243 elfzp12 ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 1 ) → ( 𝐿 ∈ ( 1 ... 𝑁 ) ↔ ( 𝐿 = 1 ∨ 𝐿 ∈ ( ( 1 + 1 ) ... 𝑁 ) ) ) )
244 242 243 syl ⊢ ( 𝜑 → ( 𝐿 ∈ ( 1 ... 𝑁 ) ↔ ( 𝐿 = 1 ∨ 𝐿 ∈ ( ( 1 + 1 ) ... 𝑁 ) ) ) )
245 8 244 mpbid ⊢ ( 𝜑 → ( 𝐿 = 1 ∨ 𝐿 ∈ ( ( 1 + 1 ) ... 𝑁 ) ) )
246 245 orcanai ⊢ ( ( 𝜑 ∧ ¬ 𝐿 = 1 ) → 𝐿 ∈ ( ( 1 + 1 ) ... 𝑁 ) )
247 1p1e2 ⊢ ( 1 + 1 ) = 2
248 247 a1i ⊢ ( ( 𝜑 ∧ ¬ 𝐿 = 1 ) → ( 1 + 1 ) = 2 )
249 248 oveq1d ⊢ ( ( 𝜑 ∧ ¬ 𝐿 = 1 ) → ( ( 1 + 1 ) ... 𝑁 ) = ( 2 ... 𝑁 ) )
250 246 249 eleqtrd ⊢ ( ( 𝜑 ∧ ¬ 𝐿 = 1 ) → 𝐿 ∈ ( 2 ... 𝑁 ) )
251 elfzle1 ⊢ ( 𝐿 ∈ ( 2 ... 𝑁 ) → 2 ≤ 𝐿 )
252 250 251 syl ⊢ ( ( 𝜑 ∧ ¬ 𝐿 = 1 ) → 2 ≤ 𝐿 )
253 114 adantr ⊢ ( ( 𝜑 ∧ ¬ 𝐿 = 1 ) → 𝐿 ∈ ℝ )
254 136 a1i ⊢ ( ( 𝜑 ∧ ¬ 𝐿 = 1 ) → 2 ∈ ℝ )
255 253 254 subge0d ⊢ ( ( 𝜑 ∧ ¬ 𝐿 = 1 ) → ( 0 ≤ ( 𝐿 − 2 ) ↔ 2 ≤ 𝐿 ) )
256 252 255 mpbird ⊢ ( ( 𝜑 ∧ ¬ 𝐿 = 1 ) → 0 ≤ ( 𝐿 − 2 ) )
257 236 240 256 3jca ⊢ ( ( 𝜑 ∧ ¬ 𝐿 = 1 ) → ( 0 ∈ ℤ ∧ ( 𝐿 − 2 ) ∈ ℤ ∧ 0 ≤ ( 𝐿 − 2 ) ) )
258 eluz2 ⊢ ( ( 𝐿 − 2 ) ∈ ( ℤ≥ ‘ 0 ) ↔ ( 0 ∈ ℤ ∧ ( 𝐿 − 2 ) ∈ ℤ ∧ 0 ≤ ( 𝐿 − 2 ) ) )
259 257 258 sylibr ⊢ ( ( 𝜑 ∧ ¬ 𝐿 = 1 ) → ( 𝐿 − 2 ) ∈ ( ℤ≥ ‘ 0 ) )
260 hashfz ⊢ ( ( 𝐿 − 2 ) ∈ ( ℤ≥ ‘ 0 ) → ( ♯ ‘ ( 0 ... ( 𝐿 − 2 ) ) ) = ( ( ( 𝐿 − 2 ) − 0 ) + 1 ) )
261 259 260 syl ⊢ ( ( 𝜑 ∧ ¬ 𝐿 = 1 ) → ( ♯ ‘ ( 0 ... ( 𝐿 − 2 ) ) ) = ( ( ( 𝐿 − 2 ) − 0 ) + 1 ) )
262 2cn ⊢ 2 ∈ ℂ
263 262 a1i ⊢ ( 𝜑 → 2 ∈ ℂ )
264 144 263 subcld ⊢ ( 𝜑 → ( 𝐿 − 2 ) ∈ ℂ )
265 264 subid1d ⊢ ( 𝜑 → ( ( 𝐿 − 2 ) − 0 ) = ( 𝐿 − 2 ) )
266 265 oveq1d ⊢ ( 𝜑 → ( ( ( 𝐿 − 2 ) − 0 ) + 1 ) = ( ( 𝐿 − 2 ) + 1 ) )
267 144 263 179 subadd23d ⊢ ( 𝜑 → ( ( 𝐿 − 2 ) + 1 ) = ( 𝐿 + ( 1 − 2 ) ) )
268 262 171 negsubdi2i ⊢ - ( 2 − 1 ) = ( 1 − 2 )
269 2m1e1 ⊢ ( 2 − 1 ) = 1
270 269 negeqi ⊢ - ( 2 − 1 ) = - 1
271 268 270 eqtr3i ⊢ ( 1 − 2 ) = - 1
272 271 a1i ⊢ ( 𝜑 → ( 1 − 2 ) = - 1 )
273 272 oveq2d ⊢ ( 𝜑 → ( 𝐿 + ( 1 − 2 ) ) = ( 𝐿 + - 1 ) )
274 144 179 negsubd ⊢ ( 𝜑 → ( 𝐿 + - 1 ) = ( 𝐿 − 1 ) )
275 273 274 eqtrd ⊢ ( 𝜑 → ( 𝐿 + ( 1 − 2 ) ) = ( 𝐿 − 1 ) )
276 266 267 275 3eqtrd ⊢ ( 𝜑 → ( ( ( 𝐿 − 2 ) − 0 ) + 1 ) = ( 𝐿 − 1 ) )
277 276 adantr ⊢ ( ( 𝜑 ∧ ¬ 𝐿 = 1 ) → ( ( ( 𝐿 − 2 ) − 0 ) + 1 ) = ( 𝐿 − 1 ) )
278 261 277 eqtrd ⊢ ( ( 𝜑 ∧ ¬ 𝐿 = 1 ) → ( ♯ ‘ ( 0 ... ( 𝐿 − 2 ) ) ) = ( 𝐿 − 1 ) )
279 278 oveq1d ⊢ ( ( 𝜑 ∧ ¬ 𝐿 = 1 ) → ( ( ♯ ‘ ( 0 ... ( 𝐿 − 2 ) ) ) · ( 1 − ( 𝐸 / 𝑁 ) ) ) = ( ( 𝐿 − 1 ) · ( 1 − ( 𝐸 / 𝑁 ) ) ) )
280 184 232 mulcomd ⊢ ( 𝜑 → ( ( 𝐿 − 1 ) · ( 1 − ( 𝐸 / 𝑁 ) ) ) = ( ( 1 − ( 𝐸 / 𝑁 ) ) · ( 𝐿 − 1 ) ) )
281 280 adantr ⊢ ( ( 𝜑 ∧ ¬ 𝐿 = 1 ) → ( ( 𝐿 − 1 ) · ( 1 − ( 𝐸 / 𝑁 ) ) ) = ( ( 1 − ( 𝐸 / 𝑁 ) ) · ( 𝐿 − 1 ) ) )
282 235 279 281 3eqtrd ⊢ ( ( 𝜑 ∧ ¬ 𝐿 = 1 ) → Σ 𝑖 ∈ ( 0 ... ( 𝐿 − 2 ) ) ( 1 − ( 𝐸 / 𝑁 ) ) = ( ( 1 − ( 𝐸 / 𝑁 ) ) · ( 𝐿 − 1 ) ) )
283 fzfid ⊢ ( ( 𝜑 ∧ ¬ 𝐿 = 1 ) → ( 0 ... ( 𝐿 − 2 ) ) ∈ Fin )
284 fzn0 ⊢ ( ( 0 ... ( 𝐿 − 2 ) ) ≠ ∅ ↔ ( 𝐿 − 2 ) ∈ ( ℤ≥ ‘ 0 ) )
285 259 284 sylibr ⊢ ( ( 𝜑 ∧ ¬ 𝐿 = 1 ) → ( 0 ... ( 𝐿 − 2 ) ) ≠ ∅ )
286 124 ad2antrr ⊢ ( ( ( 𝜑 ∧ ¬ 𝐿 = 1 ) ∧ 𝑖 ∈ ( 0 ... ( 𝐿 − 2 ) ) ) → ( 1 − ( 𝐸 / 𝑁 ) ) ∈ ℝ )
287 simpll ⊢ ( ( ( 𝜑 ∧ ¬ 𝐿 = 1 ) ∧ 𝑖 ∈ ( 0 ... ( 𝐿 − 2 ) ) ) → 𝜑 )
288 155 adantlr ⊢ ( ( ( 𝜑 ∧ ¬ 𝐿 = 1 ) ∧ 𝑖 ∈ ( 0 ... ( 𝐿 − 2 ) ) ) → 𝑖 ∈ ( 0 ... 𝑁 ) )
289 287 288 59 syl2anc ⊢ ( ( ( 𝜑 ∧ ¬ 𝐿 = 1 ) ∧ 𝑖 ∈ ( 0 ... ( 𝐿 − 2 ) ) ) → ( ( 𝑋 ‘ 𝑖 ) ‘ 𝑆 ) ∈ ℝ )
290 57 adantr ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ... ( 𝐿 − 2 ) ) ) → 𝑆 ∈ 𝑇 )
291 elfzelz ⊢ ( 𝑖 ∈ ( 0 ... ( 𝐿 − 2 ) ) → 𝑖 ∈ ℤ )
292 291 zred ⊢ ( 𝑖 ∈ ( 0 ... ( 𝐿 − 2 ) ) → 𝑖 ∈ ℝ )
293 292 adantl ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ... ( 𝐿 − 2 ) ) ) → 𝑖 ∈ ℝ )
294 168 a1i ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ... ( 𝐿 − 2 ) ) ) → ( 1 / 3 ) ∈ ℝ )
295 293 294 readdcld ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ... ( 𝐿 − 2 ) ) ) → ( 𝑖 + ( 1 / 3 ) ) ∈ ℝ )
296 28 adantr ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ... ( 𝐿 − 2 ) ) ) → 𝐸 ∈ ℝ )
297 295 296 remulcld ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ... ( 𝐿 − 2 ) ) ) → ( ( 𝑖 + ( 1 / 3 ) ) · 𝐸 ) ∈ ℝ )
298 114 adantr ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ... ( 𝐿 − 2 ) ) ) → 𝐿 ∈ ℝ )
299 136 a1i ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ... ( 𝐿 − 2 ) ) ) → 2 ∈ ℝ )
300 298 299 resubcld ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ... ( 𝐿 − 2 ) ) ) → ( 𝐿 − 2 ) ∈ ℝ )
301 300 294 readdcld ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ... ( 𝐿 − 2 ) ) ) → ( ( 𝐿 − 2 ) + ( 1 / 3 ) ) ∈ ℝ )
302 301 296 remulcld ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ... ( 𝐿 − 2 ) ) ) → ( ( ( 𝐿 − 2 ) + ( 1 / 3 ) ) · 𝐸 ) ∈ ℝ )
303 10 57 jca ⊢ ( 𝜑 → ( 𝐹 : 𝑇 ⟶ ℝ ∧ 𝑆 ∈ 𝑇 ) )
304 303 adantr ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ... ( 𝐿 − 2 ) ) ) → ( 𝐹 : 𝑇 ⟶ ℝ ∧ 𝑆 ∈ 𝑇 ) )
305 ffvelcdm ⊢ ( ( 𝐹 : 𝑇 ⟶ ℝ ∧ 𝑆 ∈ 𝑇 ) → ( 𝐹 ‘ 𝑆 ) ∈ ℝ )
306 304 305 syl ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ... ( 𝐿 − 2 ) ) ) → ( 𝐹 ‘ 𝑆 ) ∈ ℝ )
307 elfzle2 ⊢ ( 𝑖 ∈ ( 0 ... ( 𝐿 − 2 ) ) → 𝑖 ≤ ( 𝐿 − 2 ) )
308 307 adantl ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ... ( 𝐿 − 2 ) ) ) → 𝑖 ≤ ( 𝐿 − 2 ) )
309 293 300 294 308 leadd1dd ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ... ( 𝐿 − 2 ) ) ) → ( 𝑖 + ( 1 / 3 ) ) ≤ ( ( 𝐿 − 2 ) + ( 1 / 3 ) ) )
310 28 80 jca ⊢ ( 𝜑 → ( 𝐸 ∈ ℝ ∧ 0 < 𝐸 ) )
311 310 adantr ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ... ( 𝐿 − 2 ) ) ) → ( 𝐸 ∈ ℝ ∧ 0 < 𝐸 ) )
312 lemul1 ⊢ ( ( ( 𝑖 + ( 1 / 3 ) ) ∈ ℝ ∧ ( ( 𝐿 − 2 ) + ( 1 / 3 ) ) ∈ ℝ ∧ ( 𝐸 ∈ ℝ ∧ 0 < 𝐸 ) ) → ( ( 𝑖 + ( 1 / 3 ) ) ≤ ( ( 𝐿 − 2 ) + ( 1 / 3 ) ) ↔ ( ( 𝑖 + ( 1 / 3 ) ) · 𝐸 ) ≤ ( ( ( 𝐿 − 2 ) + ( 1 / 3 ) ) · 𝐸 ) ) )
313 295 301 311 312 syl3anc ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ... ( 𝐿 − 2 ) ) ) → ( ( 𝑖 + ( 1 / 3 ) ) ≤ ( ( 𝐿 − 2 ) + ( 1 / 3 ) ) ↔ ( ( 𝑖 + ( 1 / 3 ) ) · 𝐸 ) ≤ ( ( ( 𝐿 − 2 ) + ( 1 / 3 ) ) · 𝐸 ) ) )
314 309 313 mpbid ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ... ( 𝐿 − 2 ) ) ) → ( ( 𝑖 + ( 1 / 3 ) ) · 𝐸 ) ≤ ( ( ( 𝐿 − 2 ) + ( 1 / 3 ) ) · 𝐸 ) )
315 114 137 resubcld ⊢ ( 𝜑 → ( 𝐿 − 2 ) ∈ ℝ )
316 315 169 readdcld ⊢ ( 𝜑 → ( ( 𝐿 − 2 ) + ( 1 / 3 ) ) ∈ ℝ )
317 316 28 remulcld ⊢ ( 𝜑 → ( ( ( 𝐿 − 2 ) + ( 1 / 3 ) ) · 𝐸 ) ∈ ℝ )
318 10 57 ffvelcdmd ⊢ ( 𝜑 → ( 𝐹 ‘ 𝑆 ) ∈ ℝ )
319 125 169 resubcld ⊢ ( 𝜑 → ( ( 𝐿 − 1 ) − ( 1 / 3 ) ) ∈ ℝ )
320 319 28 remulcld ⊢ ( 𝜑 → ( ( ( 𝐿 − 1 ) − ( 1 / 3 ) ) · 𝐸 ) ∈ ℝ )
321 addrid ⊢ ( 1 ∈ ℂ → ( 1 + 0 ) = 1 )
322 321 eqcomd ⊢ ( 1 ∈ ℂ → 1 = ( 1 + 0 ) )
323 171 322 mp1i ⊢ ( 𝜑 → 1 = ( 1 + 0 ) )
324 179 subidd ⊢ ( 𝜑 → ( 1 − 1 ) = 0 )
325 324 eqcomd ⊢ ( 𝜑 → 0 = ( 1 − 1 ) )
326 325 oveq2d ⊢ ( 𝜑 → ( 1 + 0 ) = ( 1 + ( 1 − 1 ) ) )
327 addsubass ⊢ ( ( 1 ∈ ℂ ∧ 1 ∈ ℂ ∧ 1 ∈ ℂ ) → ( ( 1 + 1 ) − 1 ) = ( 1 + ( 1 − 1 ) ) )
328 327 eqcomd ⊢ ( ( 1 ∈ ℂ ∧ 1 ∈ ℂ ∧ 1 ∈ ℂ ) → ( 1 + ( 1 − 1 ) ) = ( ( 1 + 1 ) − 1 ) )
329 179 179 179 328 syl3anc ⊢ ( 𝜑 → ( 1 + ( 1 − 1 ) ) = ( ( 1 + 1 ) − 1 ) )
330 323 326 329 3eqtrd ⊢ ( 𝜑 → 1 = ( ( 1 + 1 ) − 1 ) )
331 330 oveq2d ⊢ ( 𝜑 → ( 𝐿 − 1 ) = ( 𝐿 − ( ( 1 + 1 ) − 1 ) ) )
332 247 a1i ⊢ ( 𝜑 → ( 1 + 1 ) = 2 )
333 332 oveq1d ⊢ ( 𝜑 → ( ( 1 + 1 ) − 1 ) = ( 2 − 1 ) )
334 333 oveq2d ⊢ ( 𝜑 → ( 𝐿 − ( ( 1 + 1 ) − 1 ) ) = ( 𝐿 − ( 2 − 1 ) ) )
335 144 263 179 subsubd ⊢ ( 𝜑 → ( 𝐿 − ( 2 − 1 ) ) = ( ( 𝐿 − 2 ) + 1 ) )
336 331 334 335 3eqtrd ⊢ ( 𝜑 → ( 𝐿 − 1 ) = ( ( 𝐿 − 2 ) + 1 ) )
337 336 oveq1d ⊢ ( 𝜑 → ( ( 𝐿 − 1 ) − ( 2 / 3 ) ) = ( ( ( 𝐿 − 2 ) + 1 ) − ( 2 / 3 ) ) )
338 262 68 24 divcli ⊢ ( 2 / 3 ) ∈ ℂ
339 338 a1i ⊢ ( 𝜑 → ( 2 / 3 ) ∈ ℂ )
340 264 179 339 addsubassd ⊢ ( 𝜑 → ( ( ( 𝐿 − 2 ) + 1 ) − ( 2 / 3 ) ) = ( ( 𝐿 − 2 ) + ( 1 − ( 2 / 3 ) ) ) )
341 171 68 24 divcli ⊢ ( 1 / 3 ) ∈ ℂ
342 df-3 ⊢ 3 = ( 2 + 1 )
343 342 oveq1i ⊢ ( 3 / 3 ) = ( ( 2 + 1 ) / 3 )
344 262 171 68 24 divdiri ⊢ ( ( 2 + 1 ) / 3 ) = ( ( 2 / 3 ) + ( 1 / 3 ) )
345 343 69 344 3eqtr3ri ⊢ ( ( 2 / 3 ) + ( 1 / 3 ) ) = 1
346 171 338 341 345 subaddrii ⊢ ( 1 − ( 2 / 3 ) ) = ( 1 / 3 )
347 346 a1i ⊢ ( 𝜑 → ( 1 − ( 2 / 3 ) ) = ( 1 / 3 ) )
348 347 oveq2d ⊢ ( 𝜑 → ( ( 𝐿 − 2 ) + ( 1 − ( 2 / 3 ) ) ) = ( ( 𝐿 − 2 ) + ( 1 / 3 ) ) )
349 337 340 348 3eqtrd ⊢ ( 𝜑 → ( ( 𝐿 − 1 ) − ( 2 / 3 ) ) = ( ( 𝐿 − 2 ) + ( 1 / 3 ) ) )
350 136 22 24 redivcli ⊢ ( 2 / 3 ) ∈ ℝ
351 350 a1i ⊢ ( 𝜑 → ( 2 / 3 ) ∈ ℝ )
352 1lt2 ⊢ 1 < 2
353 22 71 pm3.2i ⊢ ( 3 ∈ ℝ ∧ 0 < 3 )
354 16 136 353 3pm3.2i ⊢ ( 1 ∈ ℝ ∧ 2 ∈ ℝ ∧ ( 3 ∈ ℝ ∧ 0 < 3 ) )
355 ltdiv1 ⊢ ( ( 1 ∈ ℝ ∧ 2 ∈ ℝ ∧ ( 3 ∈ ℝ ∧ 0 < 3 ) ) → ( 1 < 2 ↔ ( 1 / 3 ) < ( 2 / 3 ) ) )
356 354 355 mp1i ⊢ ( 𝜑 → ( 1 < 2 ↔ ( 1 / 3 ) < ( 2 / 3 ) ) )
357 352 356 mpbii ⊢ ( 𝜑 → ( 1 / 3 ) < ( 2 / 3 ) )
358 169 351 125 357 ltsub2dd ⊢ ( 𝜑 → ( ( 𝐿 − 1 ) − ( 2 / 3 ) ) < ( ( 𝐿 − 1 ) − ( 1 / 3 ) ) )
359 349 358 eqbrtrrd ⊢ ( 𝜑 → ( ( 𝐿 − 2 ) + ( 1 / 3 ) ) < ( ( 𝐿 − 1 ) − ( 1 / 3 ) ) )
360 316 319 11 359 ltmul1dd ⊢ ( 𝜑 → ( ( ( 𝐿 − 2 ) + ( 1 / 3 ) ) · 𝐸 ) < ( ( ( 𝐿 − 1 ) − ( 1 / 3 ) ) · 𝐸 ) )
361 35 simprd ⊢ ( 𝜑 → ¬ 𝑆 ∈ ( 𝐷 ‘ ( 𝐿 − 1 ) ) )
362 oveq1 ⊢ ( 𝑗 = ( 𝐿 − 1 ) → ( 𝑗 − ( 1 / 3 ) ) = ( ( 𝐿 − 1 ) − ( 1 / 3 ) ) )
363 362 oveq1d ⊢ ( 𝑗 = ( 𝐿 − 1 ) → ( ( 𝑗 − ( 1 / 3 ) ) · 𝐸 ) = ( ( ( 𝐿 − 1 ) − ( 1 / 3 ) ) · 𝐸 ) )
364 363 breq2d ⊢ ( 𝑗 = ( 𝐿 − 1 ) → ( ( 𝐹 ‘ 𝑡 ) ≤ ( ( 𝑗 − ( 1 / 3 ) ) · 𝐸 ) ↔ ( 𝐹 ‘ 𝑡 ) ≤ ( ( ( 𝐿 − 1 ) − ( 1 / 3 ) ) · 𝐸 ) ) )
365 364 rabbidv ⊢ ( 𝑗 = ( 𝐿 − 1 ) → { 𝑡 ∈ 𝑇 ∣ ( 𝐹 ‘ 𝑡 ) ≤ ( ( 𝑗 − ( 1 / 3 ) ) · 𝐸 ) } = { 𝑡 ∈ 𝑇 ∣ ( 𝐹 ‘ 𝑡 ) ≤ ( ( ( 𝐿 − 1 ) − ( 1 / 3 ) ) · 𝐸 ) } )
366 134 peano2zd ⊢ ( 𝜑 → ( 𝑁 + 1 ) ∈ ℤ )
367 193 simpld ⊢ ( 𝜑 → 1 ≤ 𝐿 )
368 139 122 readdcld ⊢ ( 𝜑 → ( 𝑁 + 1 ) ∈ ℝ )
369 139 lep1d ⊢ ( 𝜑 → 𝑁 ≤ ( 𝑁 + 1 ) )
370 114 139 368 194 369 letrd ⊢ ( 𝜑 → 𝐿 ≤ ( 𝑁 + 1 ) )
371 190 366 130 367 370 elfzd ⊢ ( 𝜑 → 𝐿 ∈ ( 1 ... ( 𝑁 + 1 ) ) )
372 144 179 npcand ⊢ ( 𝜑 → ( ( 𝐿 − 1 ) + 1 ) = 𝐿 )
373 0p1e1 ⊢ ( 0 + 1 ) = 1
374 373 a1i ⊢ ( 𝜑 → ( 0 + 1 ) = 1 )
375 374 oveq1d ⊢ ( 𝜑 → ( ( 0 + 1 ) ... ( 𝑁 + 1 ) ) = ( 1 ... ( 𝑁 + 1 ) ) )
376 371 372 375 3eltr4d ⊢ ( 𝜑 → ( ( 𝐿 − 1 ) + 1 ) ∈ ( ( 0 + 1 ) ... ( 𝑁 + 1 ) ) )
377 0zd ⊢ ( 𝜑 → 0 ∈ ℤ )
378 130 190 zsubcld ⊢ ( 𝜑 → ( 𝐿 − 1 ) ∈ ℤ )
379 fzaddel ⊢ ( ( ( 0 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ ( ( 𝐿 − 1 ) ∈ ℤ ∧ 1 ∈ ℤ ) ) → ( ( 𝐿 − 1 ) ∈ ( 0 ... 𝑁 ) ↔ ( ( 𝐿 − 1 ) + 1 ) ∈ ( ( 0 + 1 ) ... ( 𝑁 + 1 ) ) ) )
380 377 134 378 190 379 syl22anc ⊢ ( 𝜑 → ( ( 𝐿 − 1 ) ∈ ( 0 ... 𝑁 ) ↔ ( ( 𝐿 − 1 ) + 1 ) ∈ ( ( 0 + 1 ) ... ( 𝑁 + 1 ) ) ) )
381 376 380 mpbird ⊢ ( 𝜑 → ( 𝐿 − 1 ) ∈ ( 0 ... 𝑁 ) )
382 rabexg ⊢ ( 𝑇 ∈ V → { 𝑡 ∈ 𝑇 ∣ ( 𝐹 ‘ 𝑡 ) ≤ ( ( ( 𝐿 − 1 ) − ( 1 / 3 ) ) · 𝐸 ) } ∈ V )
383 7 382 syl ⊢ ( 𝜑 → { 𝑡 ∈ 𝑇 ∣ ( 𝐹 ‘ 𝑡 ) ≤ ( ( ( 𝐿 − 1 ) − ( 1 / 3 ) ) · 𝐸 ) } ∈ V )
384 4 365 381 383 fvmptd3 ⊢ ( 𝜑 → ( 𝐷 ‘ ( 𝐿 − 1 ) ) = { 𝑡 ∈ 𝑇 ∣ ( 𝐹 ‘ 𝑡 ) ≤ ( ( ( 𝐿 − 1 ) − ( 1 / 3 ) ) · 𝐸 ) } )
385 361 384 neleqtrd ⊢ ( 𝜑 → ¬ 𝑆 ∈ { 𝑡 ∈ 𝑇 ∣ ( 𝐹 ‘ 𝑡 ) ≤ ( ( ( 𝐿 − 1 ) − ( 1 / 3 ) ) · 𝐸 ) } )
386 nfcv ⊢ Ⅎ 𝑡 ( ( ( 𝐿 − 1 ) − ( 1 / 3 ) ) · 𝐸 )
387 49 50 386 nfbr ⊢ Ⅎ 𝑡 ( 𝐹 ‘ 𝑆 ) ≤ ( ( ( 𝐿 − 1 ) − ( 1 / 3 ) ) · 𝐸 )
388 53 breq1d ⊢ ( 𝑡 = 𝑆 → ( ( 𝐹 ‘ 𝑡 ) ≤ ( ( ( 𝐿 − 1 ) − ( 1 / 3 ) ) · 𝐸 ) ↔ ( 𝐹 ‘ 𝑆 ) ≤ ( ( ( 𝐿 − 1 ) − ( 1 / 3 ) ) · 𝐸 ) ) )
389 47 48 387 388 elrabf ⊢ ( 𝑆 ∈ { 𝑡 ∈ 𝑇 ∣ ( 𝐹 ‘ 𝑡 ) ≤ ( ( ( 𝐿 − 1 ) − ( 1 / 3 ) ) · 𝐸 ) } ↔ ( 𝑆 ∈ 𝑇 ∧ ( 𝐹 ‘ 𝑆 ) ≤ ( ( ( 𝐿 − 1 ) − ( 1 / 3 ) ) · 𝐸 ) ) )
390 385 389 sylnib ⊢ ( 𝜑 → ¬ ( 𝑆 ∈ 𝑇 ∧ ( 𝐹 ‘ 𝑆 ) ≤ ( ( ( 𝐿 − 1 ) − ( 1 / 3 ) ) · 𝐸 ) ) )
391 ianor ⊢ ( ¬ ( 𝑆 ∈ 𝑇 ∧ ( 𝐹 ‘ 𝑆 ) ≤ ( ( ( 𝐿 − 1 ) − ( 1 / 3 ) ) · 𝐸 ) ) ↔ ( ¬ 𝑆 ∈ 𝑇 ∨ ¬ ( 𝐹 ‘ 𝑆 ) ≤ ( ( ( 𝐿 − 1 ) − ( 1 / 3 ) ) · 𝐸 ) ) )
392 390 391 sylib ⊢ ( 𝜑 → ( ¬ 𝑆 ∈ 𝑇 ∨ ¬ ( 𝐹 ‘ 𝑆 ) ≤ ( ( ( 𝐿 − 1 ) − ( 1 / 3 ) ) · 𝐸 ) ) )
393 olc ⊢ ( 𝑆 ∈ 𝑇 → ( ¬ ( 𝐹 ‘ 𝑆 ) ≤ ( ( ( 𝐿 − 1 ) − ( 1 / 3 ) ) · 𝐸 ) ∨ 𝑆 ∈ 𝑇 ) )
394 393 anim1i ⊢ ( ( 𝑆 ∈ 𝑇 ∧ ( ¬ 𝑆 ∈ 𝑇 ∨ ¬ ( 𝐹 ‘ 𝑆 ) ≤ ( ( ( 𝐿 − 1 ) − ( 1 / 3 ) ) · 𝐸 ) ) ) → ( ( ¬ ( 𝐹 ‘ 𝑆 ) ≤ ( ( ( 𝐿 − 1 ) − ( 1 / 3 ) ) · 𝐸 ) ∨ 𝑆 ∈ 𝑇 ) ∧ ( ¬ 𝑆 ∈ 𝑇 ∨ ¬ ( 𝐹 ‘ 𝑆 ) ≤ ( ( ( 𝐿 − 1 ) − ( 1 / 3 ) ) · 𝐸 ) ) ) )
395 57 392 394 syl2anc ⊢ ( 𝜑 → ( ( ¬ ( 𝐹 ‘ 𝑆 ) ≤ ( ( ( 𝐿 − 1 ) − ( 1 / 3 ) ) · 𝐸 ) ∨ 𝑆 ∈ 𝑇 ) ∧ ( ¬ 𝑆 ∈ 𝑇 ∨ ¬ ( 𝐹 ‘ 𝑆 ) ≤ ( ( ( 𝐿 − 1 ) − ( 1 / 3 ) ) · 𝐸 ) ) ) )
396 orcom ⊢ ( ( ¬ 𝑆 ∈ 𝑇 ∨ ¬ ( 𝐹 ‘ 𝑆 ) ≤ ( ( ( 𝐿 − 1 ) − ( 1 / 3 ) ) · 𝐸 ) ) ↔ ( ¬ ( 𝐹 ‘ 𝑆 ) ≤ ( ( ( 𝐿 − 1 ) − ( 1 / 3 ) ) · 𝐸 ) ∨ ¬ 𝑆 ∈ 𝑇 ) )
397 396 anbi2i ⊢ ( ( ( ¬ ( 𝐹 ‘ 𝑆 ) ≤ ( ( ( 𝐿 − 1 ) − ( 1 / 3 ) ) · 𝐸 ) ∨ 𝑆 ∈ 𝑇 ) ∧ ( ¬ 𝑆 ∈ 𝑇 ∨ ¬ ( 𝐹 ‘ 𝑆 ) ≤ ( ( ( 𝐿 − 1 ) − ( 1 / 3 ) ) · 𝐸 ) ) ) ↔ ( ( ¬ ( 𝐹 ‘ 𝑆 ) ≤ ( ( ( 𝐿 − 1 ) − ( 1 / 3 ) ) · 𝐸 ) ∨ 𝑆 ∈ 𝑇 ) ∧ ( ¬ ( 𝐹 ‘ 𝑆 ) ≤ ( ( ( 𝐿 − 1 ) − ( 1 / 3 ) ) · 𝐸 ) ∨ ¬ 𝑆 ∈ 𝑇 ) ) )
398 395 397 sylib ⊢ ( 𝜑 → ( ( ¬ ( 𝐹 ‘ 𝑆 ) ≤ ( ( ( 𝐿 − 1 ) − ( 1 / 3 ) ) · 𝐸 ) ∨ 𝑆 ∈ 𝑇 ) ∧ ( ¬ ( 𝐹 ‘ 𝑆 ) ≤ ( ( ( 𝐿 − 1 ) − ( 1 / 3 ) ) · 𝐸 ) ∨ ¬ 𝑆 ∈ 𝑇 ) ) )
399 pm4.43 ⊢ ( ¬ ( 𝐹 ‘ 𝑆 ) ≤ ( ( ( 𝐿 − 1 ) − ( 1 / 3 ) ) · 𝐸 ) ↔ ( ( ¬ ( 𝐹 ‘ 𝑆 ) ≤ ( ( ( 𝐿 − 1 ) − ( 1 / 3 ) ) · 𝐸 ) ∨ 𝑆 ∈ 𝑇 ) ∧ ( ¬ ( 𝐹 ‘ 𝑆 ) ≤ ( ( ( 𝐿 − 1 ) − ( 1 / 3 ) ) · 𝐸 ) ∨ ¬ 𝑆 ∈ 𝑇 ) ) )
400 398 399 sylibr ⊢ ( 𝜑 → ¬ ( 𝐹 ‘ 𝑆 ) ≤ ( ( ( 𝐿 − 1 ) − ( 1 / 3 ) ) · 𝐸 ) )
401 320 318 ltnled ⊢ ( 𝜑 → ( ( ( ( 𝐿 − 1 ) − ( 1 / 3 ) ) · 𝐸 ) < ( 𝐹 ‘ 𝑆 ) ↔ ¬ ( 𝐹 ‘ 𝑆 ) ≤ ( ( ( 𝐿 − 1 ) − ( 1 / 3 ) ) · 𝐸 ) ) )
402 400 401 mpbird ⊢ ( 𝜑 → ( ( ( 𝐿 − 1 ) − ( 1 / 3 ) ) · 𝐸 ) < ( 𝐹 ‘ 𝑆 ) )
403 317 320 318 360 402 lttrd ⊢ ( 𝜑 → ( ( ( 𝐿 − 2 ) + ( 1 / 3 ) ) · 𝐸 ) < ( 𝐹 ‘ 𝑆 ) )
404 317 318 403 ltled ⊢ ( 𝜑 → ( ( ( 𝐿 − 2 ) + ( 1 / 3 ) ) · 𝐸 ) ≤ ( 𝐹 ‘ 𝑆 ) )
405 404 adantr ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ... ( 𝐿 − 2 ) ) ) → ( ( ( 𝐿 − 2 ) + ( 1 / 3 ) ) · 𝐸 ) ≤ ( 𝐹 ‘ 𝑆 ) )
406 297 302 306 314 405 letrd ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ... ( 𝐿 − 2 ) ) ) → ( ( 𝑖 + ( 1 / 3 ) ) · 𝐸 ) ≤ ( 𝐹 ‘ 𝑆 ) )
407 nfcv ⊢ Ⅎ 𝑡 ( ( 𝑖 + ( 1 / 3 ) ) · 𝐸 )
408 407 50 49 nfbr ⊢ Ⅎ 𝑡 ( ( 𝑖 + ( 1 / 3 ) ) · 𝐸 ) ≤ ( 𝐹 ‘ 𝑆 )
409 53 breq2d ⊢ ( 𝑡 = 𝑆 → ( ( ( 𝑖 + ( 1 / 3 ) ) · 𝐸 ) ≤ ( 𝐹 ‘ 𝑡 ) ↔ ( ( 𝑖 + ( 1 / 3 ) ) · 𝐸 ) ≤ ( 𝐹 ‘ 𝑆 ) ) )
410 47 48 408 409 elrabf ⊢ ( 𝑆 ∈ { 𝑡 ∈ 𝑇 ∣ ( ( 𝑖 + ( 1 / 3 ) ) · 𝐸 ) ≤ ( 𝐹 ‘ 𝑡 ) } ↔ ( 𝑆 ∈ 𝑇 ∧ ( ( 𝑖 + ( 1 / 3 ) ) · 𝐸 ) ≤ ( 𝐹 ‘ 𝑆 ) ) )
411 290 406 410 sylanbrc ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ... ( 𝐿 − 2 ) ) ) → 𝑆 ∈ { 𝑡 ∈ 𝑇 ∣ ( ( 𝑖 + ( 1 / 3 ) ) · 𝐸 ) ≤ ( 𝐹 ‘ 𝑡 ) } )
412 oveq1 ⊢ ( 𝑗 = 𝑖 → ( 𝑗 + ( 1 / 3 ) ) = ( 𝑖 + ( 1 / 3 ) ) )
413 412 oveq1d ⊢ ( 𝑗 = 𝑖 → ( ( 𝑗 + ( 1 / 3 ) ) · 𝐸 ) = ( ( 𝑖 + ( 1 / 3 ) ) · 𝐸 ) )
414 413 breq1d ⊢ ( 𝑗 = 𝑖 → ( ( ( 𝑗 + ( 1 / 3 ) ) · 𝐸 ) ≤ ( 𝐹 ‘ 𝑡 ) ↔ ( ( 𝑖 + ( 1 / 3 ) ) · 𝐸 ) ≤ ( 𝐹 ‘ 𝑡 ) ) )
415 414 rabbidv ⊢ ( 𝑗 = 𝑖 → { 𝑡 ∈ 𝑇 ∣ ( ( 𝑗 + ( 1 / 3 ) ) · 𝐸 ) ≤ ( 𝐹 ‘ 𝑡 ) } = { 𝑡 ∈ 𝑇 ∣ ( ( 𝑖 + ( 1 / 3 ) ) · 𝐸 ) ≤ ( 𝐹 ‘ 𝑡 ) } )
416 rabexg ⊢ ( 𝑇 ∈ V → { 𝑡 ∈ 𝑇 ∣ ( ( 𝑖 + ( 1 / 3 ) ) · 𝐸 ) ≤ ( 𝐹 ‘ 𝑡 ) } ∈ V )
417 7 416 syl ⊢ ( 𝜑 → { 𝑡 ∈ 𝑇 ∣ ( ( 𝑖 + ( 1 / 3 ) ) · 𝐸 ) ≤ ( 𝐹 ‘ 𝑡 ) } ∈ V )
418 417 adantr ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ... ( 𝐿 − 2 ) ) ) → { 𝑡 ∈ 𝑇 ∣ ( ( 𝑖 + ( 1 / 3 ) ) · 𝐸 ) ≤ ( 𝐹 ‘ 𝑡 ) } ∈ V )
419 5 415 155 418 fvmptd3 ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ... ( 𝐿 − 2 ) ) ) → ( 𝐵 ‘ 𝑖 ) = { 𝑡 ∈ 𝑇 ∣ ( ( 𝑖 + ( 1 / 3 ) ) · 𝐸 ) ≤ ( 𝐹 ‘ 𝑡 ) } )
420 411 419 eleqtrrd ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ... ( 𝐿 − 2 ) ) ) → 𝑆 ∈ ( 𝐵 ‘ 𝑖 ) )
421 150 3ad2ant1 ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ... ( 𝐿 − 2 ) ) ∧ 𝑆 ∈ ( 𝐵 ‘ 𝑖 ) ) → ( ( 𝐿 − 2 ) ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ ( 𝐿 − 2 ) ≤ 𝑁 ) )
422 421 151 sylibr ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ... ( 𝐿 − 2 ) ) ∧ 𝑆 ∈ ( 𝐵 ‘ 𝑖 ) ) → 𝑁 ∈ ( ℤ≥ ‘ ( 𝐿 − 2 ) ) )
423 422 153 syl ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ... ( 𝐿 − 2 ) ) ∧ 𝑆 ∈ ( 𝐵 ‘ 𝑖 ) ) → ( 0 ... ( 𝐿 − 2 ) ) ⊆ ( 0 ... 𝑁 ) )
424 simp2 ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ... ( 𝐿 − 2 ) ) ∧ 𝑆 ∈ ( 𝐵 ‘ 𝑖 ) ) → 𝑖 ∈ ( 0 ... ( 𝐿 − 2 ) ) )
425 423 424 sseldd ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ... ( 𝐿 − 2 ) ) ∧ 𝑆 ∈ ( 𝐵 ‘ 𝑖 ) ) → 𝑖 ∈ ( 0 ... 𝑁 ) )
426 elex ⊢ ( 𝑆 ∈ ( 𝐵 ‘ 𝑖 ) → 𝑆 ∈ V )
427 426 3ad2ant3 ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ... 𝑁 ) ∧ 𝑆 ∈ ( 𝐵 ‘ 𝑖 ) ) → 𝑆 ∈ V )
428 nfcv ⊢ Ⅎ 𝑡 ( 0 ... 𝑁 )
429 nfrab1 ⊢ Ⅎ 𝑡 { 𝑡 ∈ 𝑇 ∣ ( ( 𝑗 + ( 1 / 3 ) ) · 𝐸 ) ≤ ( 𝐹 ‘ 𝑡 ) }
430 428 429 nfmpt ⊢ Ⅎ 𝑡 ( 𝑗 ∈ ( 0 ... 𝑁 ) ↦ { 𝑡 ∈ 𝑇 ∣ ( ( 𝑗 + ( 1 / 3 ) ) · 𝐸 ) ≤ ( 𝐹 ‘ 𝑡 ) } )
431 5 430 nfcxfr ⊢ Ⅎ 𝑡 𝐵
432 nfcv ⊢ Ⅎ 𝑡 𝑖
433 431 432 nffv ⊢ Ⅎ 𝑡 ( 𝐵 ‘ 𝑖 )
434 433 nfel2 ⊢ Ⅎ 𝑡 𝑆 ∈ ( 𝐵 ‘ 𝑖 )
435 3 96 434 nf3an ⊢ Ⅎ 𝑡 ( 𝜑 ∧ 𝑖 ∈ ( 0 ... 𝑁 ) ∧ 𝑆 ∈ ( 𝐵 ‘ 𝑖 ) )
436 nfv ⊢ Ⅎ 𝑡 ( 1 − ( 𝐸 / 𝑁 ) ) < ( ( 𝑋 ‘ 𝑖 ) ‘ 𝑆 )
437 435 436 nfim ⊢ Ⅎ 𝑡 ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ... 𝑁 ) ∧ 𝑆 ∈ ( 𝐵 ‘ 𝑖 ) ) → ( 1 − ( 𝐸 / 𝑁 ) ) < ( ( 𝑋 ‘ 𝑖 ) ‘ 𝑆 ) )
438 eleq1 ⊢ ( 𝑡 = 𝑆 → ( 𝑡 ∈ ( 𝐵 ‘ 𝑖 ) ↔ 𝑆 ∈ ( 𝐵 ‘ 𝑖 ) ) )
439 438 3anbi3d ⊢ ( 𝑡 = 𝑆 → ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ... 𝑁 ) ∧ 𝑡 ∈ ( 𝐵 ‘ 𝑖 ) ) ↔ ( 𝜑 ∧ 𝑖 ∈ ( 0 ... 𝑁 ) ∧ 𝑆 ∈ ( 𝐵 ‘ 𝑖 ) ) ) )
440 100 breq2d ⊢ ( 𝑡 = 𝑆 → ( ( 1 − ( 𝐸 / 𝑁 ) ) < ( ( 𝑋 ‘ 𝑖 ) ‘ 𝑡 ) ↔ ( 1 − ( 𝐸 / 𝑁 ) ) < ( ( 𝑋 ‘ 𝑖 ) ‘ 𝑆 ) ) )
441 439 440 imbi12d ⊢ ( 𝑡 = 𝑆 → ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ... 𝑁 ) ∧ 𝑡 ∈ ( 𝐵 ‘ 𝑖 ) ) → ( 1 − ( 𝐸 / 𝑁 ) ) < ( ( 𝑋 ‘ 𝑖 ) ‘ 𝑡 ) ) ↔ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ... 𝑁 ) ∧ 𝑆 ∈ ( 𝐵 ‘ 𝑖 ) ) → ( 1 − ( 𝐸 / 𝑁 ) ) < ( ( 𝑋 ‘ 𝑖 ) ‘ 𝑆 ) ) ) )
442 437 441 15 vtoclg1f ⊢ ( 𝑆 ∈ V → ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ... 𝑁 ) ∧ 𝑆 ∈ ( 𝐵 ‘ 𝑖 ) ) → ( 1 − ( 𝐸 / 𝑁 ) ) < ( ( 𝑋 ‘ 𝑖 ) ‘ 𝑆 ) ) )
443 427 442 mpcom ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ... 𝑁 ) ∧ 𝑆 ∈ ( 𝐵 ‘ 𝑖 ) ) → ( 1 − ( 𝐸 / 𝑁 ) ) < ( ( 𝑋 ‘ 𝑖 ) ‘ 𝑆 ) )
444 425 443 syld3an2 ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ... ( 𝐿 − 2 ) ) ∧ 𝑆 ∈ ( 𝐵 ‘ 𝑖 ) ) → ( 1 − ( 𝐸 / 𝑁 ) ) < ( ( 𝑋 ‘ 𝑖 ) ‘ 𝑆 ) )
445 420 444 mpd3an3 ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ... ( 𝐿 − 2 ) ) ) → ( 1 − ( 𝐸 / 𝑁 ) ) < ( ( 𝑋 ‘ 𝑖 ) ‘ 𝑆 ) )
446 445 adantlr ⊢ ( ( ( 𝜑 ∧ ¬ 𝐿 = 1 ) ∧ 𝑖 ∈ ( 0 ... ( 𝐿 − 2 ) ) ) → ( 1 − ( 𝐸 / 𝑁 ) ) < ( ( 𝑋 ‘ 𝑖 ) ‘ 𝑆 ) )
447 283 285 286 289 446 fsumlt ⊢ ( ( 𝜑 ∧ ¬ 𝐿 = 1 ) → Σ 𝑖 ∈ ( 0 ... ( 𝐿 − 2 ) ) ( 1 − ( 𝐸 / 𝑁 ) ) < Σ 𝑖 ∈ ( 0 ... ( 𝐿 − 2 ) ) ( ( 𝑋 ‘ 𝑖 ) ‘ 𝑆 ) )
448 282 447 eqbrtrrd ⊢ ( ( 𝜑 ∧ ¬ 𝐿 = 1 ) → ( ( 1 − ( 𝐸 / 𝑁 ) ) · ( 𝐿 − 1 ) ) < Σ 𝑖 ∈ ( 0 ... ( 𝐿 − 2 ) ) ( ( 𝑋 ‘ 𝑖 ) ‘ 𝑆 ) )
449 126 adantr ⊢ ( ( 𝜑 ∧ ¬ 𝐿 = 1 ) → ( ( 1 − ( 𝐸 / 𝑁 ) ) · ( 𝐿 − 1 ) ) ∈ ℝ )
450 157 adantr ⊢ ( ( 𝜑 ∧ ¬ 𝐿 = 1 ) → Σ 𝑖 ∈ ( 0 ... ( 𝐿 − 2 ) ) ( ( 𝑋 ‘ 𝑖 ) ‘ 𝑆 ) ∈ ℝ )
451 310 adantr ⊢ ( ( 𝜑 ∧ ¬ 𝐿 = 1 ) → ( 𝐸 ∈ ℝ ∧ 0 < 𝐸 ) )
452 ltmul2 ⊢ ( ( ( ( 1 − ( 𝐸 / 𝑁 ) ) · ( 𝐿 − 1 ) ) ∈ ℝ ∧ Σ 𝑖 ∈ ( 0 ... ( 𝐿 − 2 ) ) ( ( 𝑋 ‘ 𝑖 ) ‘ 𝑆 ) ∈ ℝ ∧ ( 𝐸 ∈ ℝ ∧ 0 < 𝐸 ) ) → ( ( ( 1 − ( 𝐸 / 𝑁 ) ) · ( 𝐿 − 1 ) ) < Σ 𝑖 ∈ ( 0 ... ( 𝐿 − 2 ) ) ( ( 𝑋 ‘ 𝑖 ) ‘ 𝑆 ) ↔ ( 𝐸 · ( ( 1 − ( 𝐸 / 𝑁 ) ) · ( 𝐿 − 1 ) ) ) < ( 𝐸 · Σ 𝑖 ∈ ( 0 ... ( 𝐿 − 2 ) ) ( ( 𝑋 ‘ 𝑖 ) ‘ 𝑆 ) ) ) )
453 449 450 451 452 syl3anc ⊢ ( ( 𝜑 ∧ ¬ 𝐿 = 1 ) → ( ( ( 1 − ( 𝐸 / 𝑁 ) ) · ( 𝐿 − 1 ) ) < Σ 𝑖 ∈ ( 0 ... ( 𝐿 − 2 ) ) ( ( 𝑋 ‘ 𝑖 ) ‘ 𝑆 ) ↔ ( 𝐸 · ( ( 1 − ( 𝐸 / 𝑁 ) ) · ( 𝐿 − 1 ) ) ) < ( 𝐸 · Σ 𝑖 ∈ ( 0 ... ( 𝐿 − 2 ) ) ( ( 𝑋 ‘ 𝑖 ) ‘ 𝑆 ) ) ) )
454 448 453 mpbid ⊢ ( ( 𝜑 ∧ ¬ 𝐿 = 1 ) → ( 𝐸 · ( ( 1 − ( 𝐸 / 𝑁 ) ) · ( 𝐿 − 1 ) ) ) < ( 𝐸 · Σ 𝑖 ∈ ( 0 ... ( 𝐿 − 2 ) ) ( ( 𝑋 ‘ 𝑖 ) ‘ 𝑆 ) ) )
455 121 128 159 231 454 lttrd ⊢ ( ( 𝜑 ∧ ¬ 𝐿 = 1 ) → ( ( 𝐿 − ( 4 / 3 ) ) · 𝐸 ) < ( 𝐸 · Σ 𝑖 ∈ ( 0 ... ( 𝐿 − 2 ) ) ( ( 𝑋 ‘ 𝑖 ) ‘ 𝑆 ) ) )
456 155 60 syldan ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ... ( 𝐿 − 2 ) ) ) → ( 𝐸 · ( ( 𝑋 ‘ 𝑖 ) ‘ 𝑆 ) ) ∈ ℝ )
457 456 adantlr ⊢ ( ( ( 𝜑 ∧ ¬ 𝐿 = 1 ) ∧ 𝑖 ∈ ( 0 ... ( 𝐿 − 2 ) ) ) → ( 𝐸 · ( ( 𝑋 ‘ 𝑖 ) ‘ 𝑆 ) ) ∈ ℝ )
458 457 recnd ⊢ ( ( ( 𝜑 ∧ ¬ 𝐿 = 1 ) ∧ 𝑖 ∈ ( 0 ... ( 𝐿 − 2 ) ) ) → ( 𝐸 · ( ( 𝑋 ‘ 𝑖 ) ‘ 𝑆 ) ) ∈ ℂ )
459 283 458 fsumcl ⊢ ( ( 𝜑 ∧ ¬ 𝐿 = 1 ) → Σ 𝑖 ∈ ( 0 ... ( 𝐿 − 2 ) ) ( 𝐸 · ( ( 𝑋 ‘ 𝑖 ) ‘ 𝑆 ) ) ∈ ℂ )
460 459 addridd ⊢ ( ( 𝜑 ∧ ¬ 𝐿 = 1 ) → ( Σ 𝑖 ∈ ( 0 ... ( 𝐿 − 2 ) ) ( 𝐸 · ( ( 𝑋 ‘ 𝑖 ) ‘ 𝑆 ) ) + 0 ) = Σ 𝑖 ∈ ( 0 ... ( 𝐿 − 2 ) ) ( 𝐸 · ( ( 𝑋 ‘ 𝑖 ) ‘ 𝑆 ) ) )
461 0red ⊢ ( ( 𝜑 ∧ ¬ 𝐿 = 1 ) → 0 ∈ ℝ )
462 fzfid ⊢ ( ( 𝜑 ∧ ¬ 𝐿 = 1 ) → ( ( 𝐿 − 1 ) ... 𝑁 ) ∈ Fin )
463 28 adantr ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( ( 𝐿 − 1 ) ... 𝑁 ) ) → 𝐸 ∈ ℝ )
464 0zd ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( ( 𝐿 − 1 ) ... 𝑁 ) ) → 0 ∈ ℤ )
465 134 adantr ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( ( 𝐿 − 1 ) ... 𝑁 ) ) → 𝑁 ∈ ℤ )
466 elfzelz ⊢ ( 𝑖 ∈ ( ( 𝐿 − 1 ) ... 𝑁 ) → 𝑖 ∈ ℤ )
467 466 adantl ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( ( 𝐿 − 1 ) ... 𝑁 ) ) → 𝑖 ∈ ℤ )
468 0red ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( ( 𝐿 − 1 ) ... 𝑁 ) ) → 0 ∈ ℝ )
469 125 adantr ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( ( 𝐿 − 1 ) ... 𝑁 ) ) → ( 𝐿 − 1 ) ∈ ℝ )
470 466 zred ⊢ ( 𝑖 ∈ ( ( 𝐿 − 1 ) ... 𝑁 ) → 𝑖 ∈ ℝ )
471 470 adantl ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( ( 𝐿 − 1 ) ... 𝑁 ) ) → 𝑖 ∈ ℝ )
472 1m1e0 ⊢ ( 1 − 1 ) = 0
473 122 114 122 367 lesub1dd ⊢ ( 𝜑 → ( 1 − 1 ) ≤ ( 𝐿 − 1 ) )
474 472 473 eqbrtrrid ⊢ ( 𝜑 → 0 ≤ ( 𝐿 − 1 ) )
475 474 adantr ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( ( 𝐿 − 1 ) ... 𝑁 ) ) → 0 ≤ ( 𝐿 − 1 ) )
476 simpr ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( ( 𝐿 − 1 ) ... 𝑁 ) ) → 𝑖 ∈ ( ( 𝐿 − 1 ) ... 𝑁 ) )
477 378 adantr ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( ( 𝐿 − 1 ) ... 𝑁 ) ) → ( 𝐿 − 1 ) ∈ ℤ )
478 elfz ⊢ ( ( 𝑖 ∈ ℤ ∧ ( 𝐿 − 1 ) ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( 𝑖 ∈ ( ( 𝐿 − 1 ) ... 𝑁 ) ↔ ( ( 𝐿 − 1 ) ≤ 𝑖 ∧ 𝑖 ≤ 𝑁 ) ) )
479 467 477 465 478 syl3anc ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( ( 𝐿 − 1 ) ... 𝑁 ) ) → ( 𝑖 ∈ ( ( 𝐿 − 1 ) ... 𝑁 ) ↔ ( ( 𝐿 − 1 ) ≤ 𝑖 ∧ 𝑖 ≤ 𝑁 ) ) )
480 476 479 mpbid ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( ( 𝐿 − 1 ) ... 𝑁 ) ) → ( ( 𝐿 − 1 ) ≤ 𝑖 ∧ 𝑖 ≤ 𝑁 ) )
481 480 simpld ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( ( 𝐿 − 1 ) ... 𝑁 ) ) → ( 𝐿 − 1 ) ≤ 𝑖 )
482 468 469 471 475 481 letrd ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( ( 𝐿 − 1 ) ... 𝑁 ) ) → 0 ≤ 𝑖 )
483 elfzle2 ⊢ ( 𝑖 ∈ ( ( 𝐿 − 1 ) ... 𝑁 ) → 𝑖 ≤ 𝑁 )
484 483 adantl ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( ( 𝐿 − 1 ) ... 𝑁 ) ) → 𝑖 ≤ 𝑁 )
485 464 465 467 482 484 elfzd ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( ( 𝐿 − 1 ) ... 𝑁 ) ) → 𝑖 ∈ ( 0 ... 𝑁 ) )
486 485 59 syldan ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( ( 𝐿 − 1 ) ... 𝑁 ) ) → ( ( 𝑋 ‘ 𝑖 ) ‘ 𝑆 ) ∈ ℝ )
487 463 486 remulcld ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( ( 𝐿 − 1 ) ... 𝑁 ) ) → ( 𝐸 · ( ( 𝑋 ‘ 𝑖 ) ‘ 𝑆 ) ) ∈ ℝ )
488 487 adantlr ⊢ ( ( ( 𝜑 ∧ ¬ 𝐿 = 1 ) ∧ 𝑖 ∈ ( ( 𝐿 − 1 ) ... 𝑁 ) ) → ( 𝐸 · ( ( 𝑋 ‘ 𝑖 ) ‘ 𝑆 ) ) ∈ ℝ )
489 462 488 fsumrecl ⊢ ( ( 𝜑 ∧ ¬ 𝐿 = 1 ) → Σ 𝑖 ∈ ( ( 𝐿 − 1 ) ... 𝑁 ) ( 𝐸 · ( ( 𝑋 ‘ 𝑖 ) ‘ 𝑆 ) ) ∈ ℝ )
490 283 457 fsumrecl ⊢ ( ( 𝜑 ∧ ¬ 𝐿 = 1 ) → Σ 𝑖 ∈ ( 0 ... ( 𝐿 − 2 ) ) ( 𝐸 · ( ( 𝑋 ‘ 𝑖 ) ‘ 𝑆 ) ) ∈ ℝ )
491 fzfid ⊢ ( 𝜑 → ( ( 𝐿 − 1 ) ... 𝑁 ) ∈ Fin )
492 180 adantr ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( ( 𝐿 − 1 ) ... 𝑁 ) ) → 𝐸 ∈ ℂ )
493 492 mul01d ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( ( 𝐿 − 1 ) ... 𝑁 ) ) → ( 𝐸 · 0 ) = 0 )
494 485 106 syldan ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( ( 𝐿 − 1 ) ... 𝑁 ) ) → 0 ≤ ( ( 𝑋 ‘ 𝑖 ) ‘ 𝑆 ) )
495 310 adantr ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( ( 𝐿 − 1 ) ... 𝑁 ) ) → ( 𝐸 ∈ ℝ ∧ 0 < 𝐸 ) )
496 lemul2 ⊢ ( ( 0 ∈ ℝ ∧ ( ( 𝑋 ‘ 𝑖 ) ‘ 𝑆 ) ∈ ℝ ∧ ( 𝐸 ∈ ℝ ∧ 0 < 𝐸 ) ) → ( 0 ≤ ( ( 𝑋 ‘ 𝑖 ) ‘ 𝑆 ) ↔ ( 𝐸 · 0 ) ≤ ( 𝐸 · ( ( 𝑋 ‘ 𝑖 ) ‘ 𝑆 ) ) ) )
497 468 486 495 496 syl3anc ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( ( 𝐿 − 1 ) ... 𝑁 ) ) → ( 0 ≤ ( ( 𝑋 ‘ 𝑖 ) ‘ 𝑆 ) ↔ ( 𝐸 · 0 ) ≤ ( 𝐸 · ( ( 𝑋 ‘ 𝑖 ) ‘ 𝑆 ) ) ) )
498 494 497 mpbid ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( ( 𝐿 − 1 ) ... 𝑁 ) ) → ( 𝐸 · 0 ) ≤ ( 𝐸 · ( ( 𝑋 ‘ 𝑖 ) ‘ 𝑆 ) ) )
499 493 498 eqbrtrrd ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( ( 𝐿 − 1 ) ... 𝑁 ) ) → 0 ≤ ( 𝐸 · ( ( 𝑋 ‘ 𝑖 ) ‘ 𝑆 ) ) )
500 491 487 499 fsumge0 ⊢ ( 𝜑 → 0 ≤ Σ 𝑖 ∈ ( ( 𝐿 − 1 ) ... 𝑁 ) ( 𝐸 · ( ( 𝑋 ‘ 𝑖 ) ‘ 𝑆 ) ) )
501 500 adantr ⊢ ( ( 𝜑 ∧ ¬ 𝐿 = 1 ) → 0 ≤ Σ 𝑖 ∈ ( ( 𝐿 − 1 ) ... 𝑁 ) ( 𝐸 · ( ( 𝑋 ‘ 𝑖 ) ‘ 𝑆 ) ) )
502 461 489 490 501 leadd2dd ⊢ ( ( 𝜑 ∧ ¬ 𝐿 = 1 ) → ( Σ 𝑖 ∈ ( 0 ... ( 𝐿 − 2 ) ) ( 𝐸 · ( ( 𝑋 ‘ 𝑖 ) ‘ 𝑆 ) ) + 0 ) ≤ ( Σ 𝑖 ∈ ( 0 ... ( 𝐿 − 2 ) ) ( 𝐸 · ( ( 𝑋 ‘ 𝑖 ) ‘ 𝑆 ) ) + Σ 𝑖 ∈ ( ( 𝐿 − 1 ) ... 𝑁 ) ( 𝐸 · ( ( 𝑋 ‘ 𝑖 ) ‘ 𝑆 ) ) ) )
503 460 502 eqbrtrrd ⊢ ( ( 𝜑 ∧ ¬ 𝐿 = 1 ) → Σ 𝑖 ∈ ( 0 ... ( 𝐿 − 2 ) ) ( 𝐸 · ( ( 𝑋 ‘ 𝑖 ) ‘ 𝑆 ) ) ≤ ( Σ 𝑖 ∈ ( 0 ... ( 𝐿 − 2 ) ) ( 𝐸 · ( ( 𝑋 ‘ 𝑖 ) ‘ 𝑆 ) ) + Σ 𝑖 ∈ ( ( 𝐿 − 1 ) ... 𝑁 ) ( 𝐸 · ( ( 𝑋 ‘ 𝑖 ) ‘ 𝑆 ) ) ) )
504 156 recnd ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ... ( 𝐿 − 2 ) ) ) → ( ( 𝑋 ‘ 𝑖 ) ‘ 𝑆 ) ∈ ℂ )
505 129 180 504 fsummulc2 ⊢ ( 𝜑 → ( 𝐸 · Σ 𝑖 ∈ ( 0 ... ( 𝐿 − 2 ) ) ( ( 𝑋 ‘ 𝑖 ) ‘ 𝑆 ) ) = Σ 𝑖 ∈ ( 0 ... ( 𝐿 − 2 ) ) ( 𝐸 · ( ( 𝑋 ‘ 𝑖 ) ‘ 𝑆 ) ) )
506 505 adantr ⊢ ( ( 𝜑 ∧ ¬ 𝐿 = 1 ) → ( 𝐸 · Σ 𝑖 ∈ ( 0 ... ( 𝐿 − 2 ) ) ( ( 𝑋 ‘ 𝑖 ) ‘ 𝑆 ) ) = Σ 𝑖 ∈ ( 0 ... ( 𝐿 − 2 ) ) ( 𝐸 · ( ( 𝑋 ‘ 𝑖 ) ‘ 𝑆 ) ) )
507 elfzelz ⊢ ( 𝑗 ∈ ( 0 ... ( 𝐿 − 2 ) ) → 𝑗 ∈ ℤ )
508 507 adantl ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ... ( 𝐿 − 2 ) ) ) → 𝑗 ∈ ℤ )
509 508 zred ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ... ( 𝐿 − 2 ) ) ) → 𝑗 ∈ ℝ )
510 315 adantr ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ... ( 𝐿 − 2 ) ) ) → ( 𝐿 − 2 ) ∈ ℝ )
511 125 adantr ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ... ( 𝐿 − 2 ) ) ) → ( 𝐿 − 1 ) ∈ ℝ )
512 simpr ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ... ( 𝐿 − 2 ) ) ) → 𝑗 ∈ ( 0 ... ( 𝐿 − 2 ) ) )
513 0zd ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ... ( 𝐿 − 2 ) ) ) → 0 ∈ ℤ )
514 133 adantr ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ... ( 𝐿 − 2 ) ) ) → ( 𝐿 − 2 ) ∈ ℤ )
515 elfz ⊢ ( ( 𝑗 ∈ ℤ ∧ 0 ∈ ℤ ∧ ( 𝐿 − 2 ) ∈ ℤ ) → ( 𝑗 ∈ ( 0 ... ( 𝐿 − 2 ) ) ↔ ( 0 ≤ 𝑗 ∧ 𝑗 ≤ ( 𝐿 − 2 ) ) ) )
516 508 513 514 515 syl3anc ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ... ( 𝐿 − 2 ) ) ) → ( 𝑗 ∈ ( 0 ... ( 𝐿 − 2 ) ) ↔ ( 0 ≤ 𝑗 ∧ 𝑗 ≤ ( 𝐿 − 2 ) ) ) )
517 512 516 mpbid ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ... ( 𝐿 − 2 ) ) ) → ( 0 ≤ 𝑗 ∧ 𝑗 ≤ ( 𝐿 − 2 ) ) )
518 517 simprd ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ... ( 𝐿 − 2 ) ) ) → 𝑗 ≤ ( 𝐿 − 2 ) )
519 122 137 114 ltsub2d ⊢ ( 𝜑 → ( 1 < 2 ↔ ( 𝐿 − 2 ) < ( 𝐿 − 1 ) ) )
520 352 519 mpbii ⊢ ( 𝜑 → ( 𝐿 − 2 ) < ( 𝐿 − 1 ) )
521 520 adantr ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ... ( 𝐿 − 2 ) ) ) → ( 𝐿 − 2 ) < ( 𝐿 − 1 ) )
522 509 510 511 518 521 lelttrd ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ... ( 𝐿 − 2 ) ) ) → 𝑗 < ( 𝐿 − 1 ) )
523 509 511 ltnled ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ... ( 𝐿 − 2 ) ) ) → ( 𝑗 < ( 𝐿 − 1 ) ↔ ¬ ( 𝐿 − 1 ) ≤ 𝑗 ) )
524 522 523 mpbid ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ... ( 𝐿 − 2 ) ) ) → ¬ ( 𝐿 − 1 ) ≤ 𝑗 )
525 524 intnanrd ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ... ( 𝐿 − 2 ) ) ) → ¬ ( ( 𝐿 − 1 ) ≤ 𝑗 ∧ 𝑗 ≤ 𝑁 ) )
526 378 adantr ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ... ( 𝐿 − 2 ) ) ) → ( 𝐿 − 1 ) ∈ ℤ )
527 134 adantr ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ... ( 𝐿 − 2 ) ) ) → 𝑁 ∈ ℤ )
528 elfz ⊢ ( ( 𝑗 ∈ ℤ ∧ ( 𝐿 − 1 ) ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( 𝑗 ∈ ( ( 𝐿 − 1 ) ... 𝑁 ) ↔ ( ( 𝐿 − 1 ) ≤ 𝑗 ∧ 𝑗 ≤ 𝑁 ) ) )
529 508 526 527 528 syl3anc ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ... ( 𝐿 − 2 ) ) ) → ( 𝑗 ∈ ( ( 𝐿 − 1 ) ... 𝑁 ) ↔ ( ( 𝐿 − 1 ) ≤ 𝑗 ∧ 𝑗 ≤ 𝑁 ) ) )
530 525 529 mtbird ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ... ( 𝐿 − 2 ) ) ) → ¬ 𝑗 ∈ ( ( 𝐿 − 1 ) ... 𝑁 ) )
531 530 ex ⊢ ( 𝜑 → ( 𝑗 ∈ ( 0 ... ( 𝐿 − 2 ) ) → ¬ 𝑗 ∈ ( ( 𝐿 − 1 ) ... 𝑁 ) ) )
532 2 531 ralrimi ⊢ ( 𝜑 → ∀ 𝑗 ∈ ( 0 ... ( 𝐿 − 2 ) ) ¬ 𝑗 ∈ ( ( 𝐿 − 1 ) ... 𝑁 ) )
533 disj ⊢ ( ( ( 0 ... ( 𝐿 − 2 ) ) ∩ ( ( 𝐿 − 1 ) ... 𝑁 ) ) = ∅ ↔ ∀ 𝑗 ∈ ( 0 ... ( 𝐿 − 2 ) ) ¬ 𝑗 ∈ ( ( 𝐿 − 1 ) ... 𝑁 ) )
534 532 533 sylibr ⊢ ( 𝜑 → ( ( 0 ... ( 𝐿 − 2 ) ) ∩ ( ( 𝐿 − 1 ) ... 𝑁 ) ) = ∅ )
535 534 adantr ⊢ ( ( 𝜑 ∧ ¬ 𝐿 = 1 ) → ( ( 0 ... ( 𝐿 − 2 ) ) ∩ ( ( 𝐿 − 1 ) ... 𝑁 ) ) = ∅ )
536 149 adantr ⊢ ( ( 𝜑 ∧ ¬ 𝐿 = 1 ) → ( 𝐿 − 2 ) ≤ 𝑁 )
537 133 377 134 3jca ⊢ ( 𝜑 → ( ( 𝐿 − 2 ) ∈ ℤ ∧ 0 ∈ ℤ ∧ 𝑁 ∈ ℤ ) )
538 537 adantr ⊢ ( ( 𝜑 ∧ ¬ 𝐿 = 1 ) → ( ( 𝐿 − 2 ) ∈ ℤ ∧ 0 ∈ ℤ ∧ 𝑁 ∈ ℤ ) )
539 elfz ⊢ ( ( ( 𝐿 − 2 ) ∈ ℤ ∧ 0 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( ( 𝐿 − 2 ) ∈ ( 0 ... 𝑁 ) ↔ ( 0 ≤ ( 𝐿 − 2 ) ∧ ( 𝐿 − 2 ) ≤ 𝑁 ) ) )
540 538 539 syl ⊢ ( ( 𝜑 ∧ ¬ 𝐿 = 1 ) → ( ( 𝐿 − 2 ) ∈ ( 0 ... 𝑁 ) ↔ ( 0 ≤ ( 𝐿 − 2 ) ∧ ( 𝐿 − 2 ) ≤ 𝑁 ) ) )
541 256 536 540 mpbir2and ⊢ ( ( 𝜑 ∧ ¬ 𝐿 = 1 ) → ( 𝐿 − 2 ) ∈ ( 0 ... 𝑁 ) )
542 fzsplit ⊢ ( ( 𝐿 − 2 ) ∈ ( 0 ... 𝑁 ) → ( 0 ... 𝑁 ) = ( ( 0 ... ( 𝐿 − 2 ) ) ∪ ( ( ( 𝐿 − 2 ) + 1 ) ... 𝑁 ) ) )
543 541 542 syl ⊢ ( ( 𝜑 ∧ ¬ 𝐿 = 1 ) → ( 0 ... 𝑁 ) = ( ( 0 ... ( 𝐿 − 2 ) ) ∪ ( ( ( 𝐿 − 2 ) + 1 ) ... 𝑁 ) ) )
544 267 273 274 3eqtrd ⊢ ( 𝜑 → ( ( 𝐿 − 2 ) + 1 ) = ( 𝐿 − 1 ) )
545 544 oveq1d ⊢ ( 𝜑 → ( ( ( 𝐿 − 2 ) + 1 ) ... 𝑁 ) = ( ( 𝐿 − 1 ) ... 𝑁 ) )
546 545 uneq2d ⊢ ( 𝜑 → ( ( 0 ... ( 𝐿 − 2 ) ) ∪ ( ( ( 𝐿 − 2 ) + 1 ) ... 𝑁 ) ) = ( ( 0 ... ( 𝐿 − 2 ) ) ∪ ( ( 𝐿 − 1 ) ... 𝑁 ) ) )
547 546 adantr ⊢ ( ( 𝜑 ∧ ¬ 𝐿 = 1 ) → ( ( 0 ... ( 𝐿 − 2 ) ) ∪ ( ( ( 𝐿 − 2 ) + 1 ) ... 𝑁 ) ) = ( ( 0 ... ( 𝐿 − 2 ) ) ∪ ( ( 𝐿 − 1 ) ... 𝑁 ) ) )
548 543 547 eqtrd ⊢ ( ( 𝜑 ∧ ¬ 𝐿 = 1 ) → ( 0 ... 𝑁 ) = ( ( 0 ... ( 𝐿 − 2 ) ) ∪ ( ( 𝐿 − 1 ) ... 𝑁 ) ) )
549 fzfid ⊢ ( ( 𝜑 ∧ ¬ 𝐿 = 1 ) → ( 0 ... 𝑁 ) ∈ Fin )
550 180 adantr ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ... 𝑁 ) ) → 𝐸 ∈ ℂ )
551 59 recnd ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ... 𝑁 ) ) → ( ( 𝑋 ‘ 𝑖 ) ‘ 𝑆 ) ∈ ℂ )
552 550 551 mulcld ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ... 𝑁 ) ) → ( 𝐸 · ( ( 𝑋 ‘ 𝑖 ) ‘ 𝑆 ) ) ∈ ℂ )
553 552 adantlr ⊢ ( ( ( 𝜑 ∧ ¬ 𝐿 = 1 ) ∧ 𝑖 ∈ ( 0 ... 𝑁 ) ) → ( 𝐸 · ( ( 𝑋 ‘ 𝑖 ) ‘ 𝑆 ) ) ∈ ℂ )
554 535 548 549 553 fsumsplit ⊢ ( ( 𝜑 ∧ ¬ 𝐿 = 1 ) → Σ 𝑖 ∈ ( 0 ... 𝑁 ) ( 𝐸 · ( ( 𝑋 ‘ 𝑖 ) ‘ 𝑆 ) ) = ( Σ 𝑖 ∈ ( 0 ... ( 𝐿 − 2 ) ) ( 𝐸 · ( ( 𝑋 ‘ 𝑖 ) ‘ 𝑆 ) ) + Σ 𝑖 ∈ ( ( 𝐿 − 1 ) ... 𝑁 ) ( 𝐸 · ( ( 𝑋 ‘ 𝑖 ) ‘ 𝑆 ) ) ) )
555 503 506 554 3brtr4d ⊢ ( ( 𝜑 ∧ ¬ 𝐿 = 1 ) → ( 𝐸 · Σ 𝑖 ∈ ( 0 ... ( 𝐿 − 2 ) ) ( ( 𝑋 ‘ 𝑖 ) ‘ 𝑆 ) ) ≤ Σ 𝑖 ∈ ( 0 ... 𝑁 ) ( 𝐸 · ( ( 𝑋 ‘ 𝑖 ) ‘ 𝑆 ) ) )
556 120 158 61 3jca ⊢ ( 𝜑 → ( ( ( 𝐿 − ( 4 / 3 ) ) · 𝐸 ) ∈ ℝ ∧ ( 𝐸 · Σ 𝑖 ∈ ( 0 ... ( 𝐿 − 2 ) ) ( ( 𝑋 ‘ 𝑖 ) ‘ 𝑆 ) ) ∈ ℝ ∧ Σ 𝑖 ∈ ( 0 ... 𝑁 ) ( 𝐸 · ( ( 𝑋 ‘ 𝑖 ) ‘ 𝑆 ) ) ∈ ℝ ) )
557 556 adantr ⊢ ( ( 𝜑 ∧ ¬ 𝐿 = 1 ) → ( ( ( 𝐿 − ( 4 / 3 ) ) · 𝐸 ) ∈ ℝ ∧ ( 𝐸 · Σ 𝑖 ∈ ( 0 ... ( 𝐿 − 2 ) ) ( ( 𝑋 ‘ 𝑖 ) ‘ 𝑆 ) ) ∈ ℝ ∧ Σ 𝑖 ∈ ( 0 ... 𝑁 ) ( 𝐸 · ( ( 𝑋 ‘ 𝑖 ) ‘ 𝑆 ) ) ∈ ℝ ) )
558 ltletr ⊢ ( ( ( ( 𝐿 − ( 4 / 3 ) ) · 𝐸 ) ∈ ℝ ∧ ( 𝐸 · Σ 𝑖 ∈ ( 0 ... ( 𝐿 − 2 ) ) ( ( 𝑋 ‘ 𝑖 ) ‘ 𝑆 ) ) ∈ ℝ ∧ Σ 𝑖 ∈ ( 0 ... 𝑁 ) ( 𝐸 · ( ( 𝑋 ‘ 𝑖 ) ‘ 𝑆 ) ) ∈ ℝ ) → ( ( ( ( 𝐿 − ( 4 / 3 ) ) · 𝐸 ) < ( 𝐸 · Σ 𝑖 ∈ ( 0 ... ( 𝐿 − 2 ) ) ( ( 𝑋 ‘ 𝑖 ) ‘ 𝑆 ) ) ∧ ( 𝐸 · Σ 𝑖 ∈ ( 0 ... ( 𝐿 − 2 ) ) ( ( 𝑋 ‘ 𝑖 ) ‘ 𝑆 ) ) ≤ Σ 𝑖 ∈ ( 0 ... 𝑁 ) ( 𝐸 · ( ( 𝑋 ‘ 𝑖 ) ‘ 𝑆 ) ) ) → ( ( 𝐿 − ( 4 / 3 ) ) · 𝐸 ) < Σ 𝑖 ∈ ( 0 ... 𝑁 ) ( 𝐸 · ( ( 𝑋 ‘ 𝑖 ) ‘ 𝑆 ) ) ) )
559 557 558 syl ⊢ ( ( 𝜑 ∧ ¬ 𝐿 = 1 ) → ( ( ( ( 𝐿 − ( 4 / 3 ) ) · 𝐸 ) < ( 𝐸 · Σ 𝑖 ∈ ( 0 ... ( 𝐿 − 2 ) ) ( ( 𝑋 ‘ 𝑖 ) ‘ 𝑆 ) ) ∧ ( 𝐸 · Σ 𝑖 ∈ ( 0 ... ( 𝐿 − 2 ) ) ( ( 𝑋 ‘ 𝑖 ) ‘ 𝑆 ) ) ≤ Σ 𝑖 ∈ ( 0 ... 𝑁 ) ( 𝐸 · ( ( 𝑋 ‘ 𝑖 ) ‘ 𝑆 ) ) ) → ( ( 𝐿 − ( 4 / 3 ) ) · 𝐸 ) < Σ 𝑖 ∈ ( 0 ... 𝑁 ) ( 𝐸 · ( ( 𝑋 ‘ 𝑖 ) ‘ 𝑆 ) ) ) )
560 455 555 559 mp2and ⊢ ( ( 𝜑 ∧ ¬ 𝐿 = 1 ) → ( ( 𝐿 − ( 4 / 3 ) ) · 𝐸 ) < Σ 𝑖 ∈ ( 0 ... 𝑁 ) ( 𝐸 · ( ( 𝑋 ‘ 𝑖 ) ‘ 𝑆 ) ) )
561 111 560 pm2.61dan ⊢ ( 𝜑 → ( ( 𝐿 − ( 4 / 3 ) ) · 𝐸 ) < Σ 𝑖 ∈ ( 0 ... 𝑁 ) ( 𝐸 · ( ( 𝑋 ‘ 𝑖 ) ‘ 𝑆 ) ) )
562 sumex ⊢ Σ 𝑖 ∈ ( 0 ... 𝑁 ) ( 𝐸 · ( ( 𝑋 ‘ 𝑖 ) ‘ 𝑆 ) ) ∈ V
563 100 oveq2d ⊢ ( 𝑡 = 𝑆 → ( 𝐸 · ( ( 𝑋 ‘ 𝑖 ) ‘ 𝑡 ) ) = ( 𝐸 · ( ( 𝑋 ‘ 𝑖 ) ‘ 𝑆 ) ) )
564 563 sumeq2sdv ⊢ ( 𝑡 = 𝑆 → Σ 𝑖 ∈ ( 0 ... 𝑁 ) ( 𝐸 · ( ( 𝑋 ‘ 𝑖 ) ‘ 𝑡 ) ) = Σ 𝑖 ∈ ( 0 ... 𝑁 ) ( 𝐸 · ( ( 𝑋 ‘ 𝑖 ) ‘ 𝑆 ) ) )
565 eqid ⊢ ( 𝑡 ∈ 𝑇 ↦ Σ 𝑖 ∈ ( 0 ... 𝑁 ) ( 𝐸 · ( ( 𝑋 ‘ 𝑖 ) ‘ 𝑡 ) ) ) = ( 𝑡 ∈ 𝑇 ↦ Σ 𝑖 ∈ ( 0 ... 𝑁 ) ( 𝐸 · ( ( 𝑋 ‘ 𝑖 ) ‘ 𝑡 ) ) )
566 564 565 fvmptg ⊢ ( ( 𝑆 ∈ 𝑇 ∧ Σ 𝑖 ∈ ( 0 ... 𝑁 ) ( 𝐸 · ( ( 𝑋 ‘ 𝑖 ) ‘ 𝑆 ) ) ∈ V ) → ( ( 𝑡 ∈ 𝑇 ↦ Σ 𝑖 ∈ ( 0 ... 𝑁 ) ( 𝐸 · ( ( 𝑋 ‘ 𝑖 ) ‘ 𝑡 ) ) ) ‘ 𝑆 ) = Σ 𝑖 ∈ ( 0 ... 𝑁 ) ( 𝐸 · ( ( 𝑋 ‘ 𝑖 ) ‘ 𝑆 ) ) )
567 57 562 566 sylancl ⊢ ( 𝜑 → ( ( 𝑡 ∈ 𝑇 ↦ Σ 𝑖 ∈ ( 0 ... 𝑁 ) ( 𝐸 · ( ( 𝑋 ‘ 𝑖 ) ‘ 𝑡 ) ) ) ‘ 𝑆 ) = Σ 𝑖 ∈ ( 0 ... 𝑁 ) ( 𝐸 · ( ( 𝑋 ‘ 𝑖 ) ‘ 𝑆 ) ) )
568 561 567 breqtrrd ⊢ ( 𝜑 → ( ( 𝐿 − ( 4 / 3 ) ) · 𝐸 ) < ( ( 𝑡 ∈ 𝑇 ↦ Σ 𝑖 ∈ ( 0 ... 𝑁 ) ( 𝐸 · ( ( 𝑋 ‘ 𝑖 ) ‘ 𝑡 ) ) ) ‘ 𝑆 ) )