Metamath Proof Explorer

Theorem stoweidlem11

Description: This lemma is used to prove that there is a function g as in the proof of BrosowskiDeutsh p. 92 (at the top of page 92): this lemma proves that g(t) < ( j + 1 / 3 ) * ε. Here E is used to represent ε in the paper. (Contributed by Glauco Siliprandi, 20-Apr-2017)

Ref Expression
Hypotheses stoweidlem11.1 ⊢ ( 𝜑 → 𝑁 ∈ ℕ )
stoweidlem11.2 ⊢ ( 𝜑 → 𝑡 ∈ 𝑇 )
stoweidlem11.3 ⊢ ( 𝜑 → 𝑗 ∈ ( 1 ... 𝑁 ) )
stoweidlem11.4 ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ... 𝑁 ) ) → ( 𝑋 ‘ 𝑖 ) : 𝑇 ⟶ ℝ )
stoweidlem11.5 ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ... 𝑁 ) ) → ( ( 𝑋 ‘ 𝑖 ) ‘ 𝑡 ) ≤ 1 )
stoweidlem11.6 ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 𝑗 ... 𝑁 ) ) → ( ( 𝑋 ‘ 𝑖 ) ‘ 𝑡 ) < ( 𝐸 / 𝑁 ) )
stoweidlem11.7 ⊢ ( 𝜑 → 𝐸 ∈ ℝ+ )
stoweidlem11.8 ⊢ ( 𝜑 → 𝐸 < ( 1 / 3 ) )
Assertion stoweidlem11 ( 𝜑 → ( ( 𝑡 ∈ 𝑇 ↦ Σ 𝑖 ∈ ( 0 ... 𝑁 ) ( 𝐸 · ( ( 𝑋 ‘ 𝑖 ) ‘ 𝑡 ) ) ) ‘ 𝑡 ) < ( ( 𝑗 + ( 1 / 3 ) ) · 𝐸 ) )

Proof

Step Hyp Ref Expression
1 stoweidlem11.1 ⊢ ( 𝜑 → 𝑁 ∈ ℕ )
2 stoweidlem11.2 ⊢ ( 𝜑 → 𝑡 ∈ 𝑇 )
3 stoweidlem11.3 ⊢ ( 𝜑 → 𝑗 ∈ ( 1 ... 𝑁 ) )
4 stoweidlem11.4 ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ... 𝑁 ) ) → ( 𝑋 ‘ 𝑖 ) : 𝑇 ⟶ ℝ )
5 stoweidlem11.5 ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ... 𝑁 ) ) → ( ( 𝑋 ‘ 𝑖 ) ‘ 𝑡 ) ≤ 1 )
6 stoweidlem11.6 ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 𝑗 ... 𝑁 ) ) → ( ( 𝑋 ‘ 𝑖 ) ‘ 𝑡 ) < ( 𝐸 / 𝑁 ) )
7 stoweidlem11.7 ⊢ ( 𝜑 → 𝐸 ∈ ℝ+ )
8 stoweidlem11.8 ⊢ ( 𝜑 → 𝐸 < ( 1 / 3 ) )
9 sumex ⊢ Σ 𝑖 ∈ ( 0 ... 𝑁 ) ( 𝐸 · ( ( 𝑋 ‘ 𝑖 ) ‘ 𝑡 ) ) ∈ V
10 eqid ⊢ ( 𝑡 ∈ 𝑇 ↦ Σ 𝑖 ∈ ( 0 ... 𝑁 ) ( 𝐸 · ( ( 𝑋 ‘ 𝑖 ) ‘ 𝑡 ) ) ) = ( 𝑡 ∈ 𝑇 ↦ Σ 𝑖 ∈ ( 0 ... 𝑁 ) ( 𝐸 · ( ( 𝑋 ‘ 𝑖 ) ‘ 𝑡 ) ) )
11 10 fvmpt2 ⊢ ( ( 𝑡 ∈ 𝑇 ∧ Σ 𝑖 ∈ ( 0 ... 𝑁 ) ( 𝐸 · ( ( 𝑋 ‘ 𝑖 ) ‘ 𝑡 ) ) ∈ V ) → ( ( 𝑡 ∈ 𝑇 ↦ Σ 𝑖 ∈ ( 0 ... 𝑁 ) ( 𝐸 · ( ( 𝑋 ‘ 𝑖 ) ‘ 𝑡 ) ) ) ‘ 𝑡 ) = Σ 𝑖 ∈ ( 0 ... 𝑁 ) ( 𝐸 · ( ( 𝑋 ‘ 𝑖 ) ‘ 𝑡 ) ) )
12 2 9 11 sylancl ⊢ ( 𝜑 → ( ( 𝑡 ∈ 𝑇 ↦ Σ 𝑖 ∈ ( 0 ... 𝑁 ) ( 𝐸 · ( ( 𝑋 ‘ 𝑖 ) ‘ 𝑡 ) ) ) ‘ 𝑡 ) = Σ 𝑖 ∈ ( 0 ... 𝑁 ) ( 𝐸 · ( ( 𝑋 ‘ 𝑖 ) ‘ 𝑡 ) ) )
13 fzfid ⊢ ( 𝜑 → ( 0 ... 𝑁 ) ∈ Fin )
14 7 rpred ⊢ ( 𝜑 → 𝐸 ∈ ℝ )
15 14 adantr ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ... 𝑁 ) ) → 𝐸 ∈ ℝ )
16 2 adantr ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ... 𝑁 ) ) → 𝑡 ∈ 𝑇 )
17 4 16 ffvelrnd ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ... 𝑁 ) ) → ( ( 𝑋 ‘ 𝑖 ) ‘ 𝑡 ) ∈ ℝ )
18 15 17 remulcld ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ... 𝑁 ) ) → ( 𝐸 · ( ( 𝑋 ‘ 𝑖 ) ‘ 𝑡 ) ) ∈ ℝ )
19 13 18 fsumrecl ⊢ ( 𝜑 → Σ 𝑖 ∈ ( 0 ... 𝑁 ) ( 𝐸 · ( ( 𝑋 ‘ 𝑖 ) ‘ 𝑡 ) ) ∈ ℝ )
20 elfzuz ⊢ ( 𝑗 ∈ ( 1 ... 𝑁 ) → 𝑗 ∈ ( ℤ≥ ‘ 1 ) )
21 3 20 syl ⊢ ( 𝜑 → 𝑗 ∈ ( ℤ≥ ‘ 1 ) )
22 eluz2 ⊢ ( 𝑗 ∈ ( ℤ≥ ‘ 1 ) ↔ ( 1 ∈ ℤ ∧ 𝑗 ∈ ℤ ∧ 1 ≤ 𝑗 ) )
23 21 22 sylib ⊢ ( 𝜑 → ( 1 ∈ ℤ ∧ 𝑗 ∈ ℤ ∧ 1 ≤ 𝑗 ) )
24 23 simp2d ⊢ ( 𝜑 → 𝑗 ∈ ℤ )
25 24 zred ⊢ ( 𝜑 → 𝑗 ∈ ℝ )
26 14 25 remulcld ⊢ ( 𝜑 → ( 𝐸 · 𝑗 ) ∈ ℝ )
27 1 nnred ⊢ ( 𝜑 → 𝑁 ∈ ℝ )
28 27 25 resubcld ⊢ ( 𝜑 → ( 𝑁 − 𝑗 ) ∈ ℝ )
29 1red ⊢ ( 𝜑 → 1 ∈ ℝ )
30 28 29 readdcld ⊢ ( 𝜑 → ( ( 𝑁 − 𝑗 ) + 1 ) ∈ ℝ )
31 14 1 nndivred ⊢ ( 𝜑 → ( 𝐸 / 𝑁 ) ∈ ℝ )
32 14 31 remulcld ⊢ ( 𝜑 → ( 𝐸 · ( 𝐸 / 𝑁 ) ) ∈ ℝ )
33 30 32 remulcld ⊢ ( 𝜑 → ( ( ( 𝑁 − 𝑗 ) + 1 ) · ( 𝐸 · ( 𝐸 / 𝑁 ) ) ) ∈ ℝ )
34 26 33 readdcld ⊢ ( 𝜑 → ( ( 𝐸 · 𝑗 ) + ( ( ( 𝑁 − 𝑗 ) + 1 ) · ( 𝐸 · ( 𝐸 / 𝑁 ) ) ) ) ∈ ℝ )
35 3re ⊢ 3 ∈ ℝ
36 35 a1i ⊢ ( 𝜑 → 3 ∈ ℝ )
37 3ne0 ⊢ 3 ≠ 0
38 37 a1i ⊢ ( 𝜑 → 3 ≠ 0 )
39 36 38 rereccld ⊢ ( 𝜑 → ( 1 / 3 ) ∈ ℝ )
40 25 39 readdcld ⊢ ( 𝜑 → ( 𝑗 + ( 1 / 3 ) ) ∈ ℝ )
41 40 14 remulcld ⊢ ( 𝜑 → ( ( 𝑗 + ( 1 / 3 ) ) · 𝐸 ) ∈ ℝ )
42 fzfid ⊢ ( 𝜑 → ( 0 ... ( 𝑗 − 1 ) ) ∈ Fin )
43 14 adantr ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ... ( 𝑗 − 1 ) ) ) → 𝐸 ∈ ℝ )
44 elfzelz ⊢ ( 𝑗 ∈ ( 1 ... 𝑁 ) → 𝑗 ∈ ℤ )
45 peano2zm ⊢ ( 𝑗 ∈ ℤ → ( 𝑗 − 1 ) ∈ ℤ )
46 3 44 45 3syl ⊢ ( 𝜑 → ( 𝑗 − 1 ) ∈ ℤ )
47 1 nnzd ⊢ ( 𝜑 → 𝑁 ∈ ℤ )
48 25 29 resubcld ⊢ ( 𝜑 → ( 𝑗 − 1 ) ∈ ℝ )
49 25 lem1d ⊢ ( 𝜑 → ( 𝑗 − 1 ) ≤ 𝑗 )
50 elfzuz3 ⊢ ( 𝑗 ∈ ( 1 ... 𝑁 ) → 𝑁 ∈ ( ℤ≥ ‘ 𝑗 ) )
51 eluzle ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 𝑗 ) → 𝑗 ≤ 𝑁 )
52 3 50 51 3syl ⊢ ( 𝜑 → 𝑗 ≤ 𝑁 )
53 48 25 27 49 52 letrd ⊢ ( 𝜑 → ( 𝑗 − 1 ) ≤ 𝑁 )
54 eluz2 ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ ( 𝑗 − 1 ) ) ↔ ( ( 𝑗 − 1 ) ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ ( 𝑗 − 1 ) ≤ 𝑁 ) )
55 46 47 53 54 syl3anbrc ⊢ ( 𝜑 → 𝑁 ∈ ( ℤ≥ ‘ ( 𝑗 − 1 ) ) )
56 fzss2 ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ ( 𝑗 − 1 ) ) → ( 0 ... ( 𝑗 − 1 ) ) ⊆ ( 0 ... 𝑁 ) )
57 55 56 syl ⊢ ( 𝜑 → ( 0 ... ( 𝑗 − 1 ) ) ⊆ ( 0 ... 𝑁 ) )
58 57 sselda ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ... ( 𝑗 − 1 ) ) ) → 𝑖 ∈ ( 0 ... 𝑁 ) )
59 58 17 syldan ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ... ( 𝑗 − 1 ) ) ) → ( ( 𝑋 ‘ 𝑖 ) ‘ 𝑡 ) ∈ ℝ )
60 43 59 remulcld ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ... ( 𝑗 − 1 ) ) ) → ( 𝐸 · ( ( 𝑋 ‘ 𝑖 ) ‘ 𝑡 ) ) ∈ ℝ )
61 42 60 fsumrecl ⊢ ( 𝜑 → Σ 𝑖 ∈ ( 0 ... ( 𝑗 − 1 ) ) ( 𝐸 · ( ( 𝑋 ‘ 𝑖 ) ‘ 𝑡 ) ) ∈ ℝ )
62 61 33 readdcld ⊢ ( 𝜑 → ( Σ 𝑖 ∈ ( 0 ... ( 𝑗 − 1 ) ) ( 𝐸 · ( ( 𝑋 ‘ 𝑖 ) ‘ 𝑡 ) ) + ( ( ( 𝑁 − 𝑗 ) + 1 ) · ( 𝐸 · ( 𝐸 / 𝑁 ) ) ) ) ∈ ℝ )
63 25 ltm1d ⊢ ( 𝜑 → ( 𝑗 − 1 ) < 𝑗 )
64 fzdisj ⊢ ( ( 𝑗 − 1 ) < 𝑗 → ( ( 0 ... ( 𝑗 − 1 ) ) ∩ ( 𝑗 ... 𝑁 ) ) = ∅ )
65 63 64 syl ⊢ ( 𝜑 → ( ( 0 ... ( 𝑗 − 1 ) ) ∩ ( 𝑗 ... 𝑁 ) ) = ∅ )
66 fzssp1 ⊢ ( 0 ... ( 𝑁 − 1 ) ) ⊆ ( 0 ... ( ( 𝑁 − 1 ) + 1 ) )
67 1 nncnd ⊢ ( 𝜑 → 𝑁 ∈ ℂ )
68 1cnd ⊢ ( 𝜑 → 1 ∈ ℂ )
69 67 68 npcand ⊢ ( 𝜑 → ( ( 𝑁 − 1 ) + 1 ) = 𝑁 )
70 69 oveq2d ⊢ ( 𝜑 → ( 0 ... ( ( 𝑁 − 1 ) + 1 ) ) = ( 0 ... 𝑁 ) )
71 66 70 sseqtrid ⊢ ( 𝜑 → ( 0 ... ( 𝑁 − 1 ) ) ⊆ ( 0 ... 𝑁 ) )
72 1zzd ⊢ ( 𝜑 → 1 ∈ ℤ )
73 fzsubel ⊢ ( ( ( 1 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ ( 𝑗 ∈ ℤ ∧ 1 ∈ ℤ ) ) → ( 𝑗 ∈ ( 1 ... 𝑁 ) ↔ ( 𝑗 − 1 ) ∈ ( ( 1 − 1 ) ... ( 𝑁 − 1 ) ) ) )
74 72 47 24 72 73 syl22anc ⊢ ( 𝜑 → ( 𝑗 ∈ ( 1 ... 𝑁 ) ↔ ( 𝑗 − 1 ) ∈ ( ( 1 − 1 ) ... ( 𝑁 − 1 ) ) ) )
75 3 74 mpbid ⊢ ( 𝜑 → ( 𝑗 − 1 ) ∈ ( ( 1 − 1 ) ... ( 𝑁 − 1 ) ) )
76 1m1e0 ⊢ ( 1 − 1 ) = 0
77 76 oveq1i ⊢ ( ( 1 − 1 ) ... ( 𝑁 − 1 ) ) = ( 0 ... ( 𝑁 − 1 ) )
78 75 77 eleqtrdi ⊢ ( 𝜑 → ( 𝑗 − 1 ) ∈ ( 0 ... ( 𝑁 − 1 ) ) )
79 71 78 sseldd ⊢ ( 𝜑 → ( 𝑗 − 1 ) ∈ ( 0 ... 𝑁 ) )
80 fzsplit ⊢ ( ( 𝑗 − 1 ) ∈ ( 0 ... 𝑁 ) → ( 0 ... 𝑁 ) = ( ( 0 ... ( 𝑗 − 1 ) ) ∪ ( ( ( 𝑗 − 1 ) + 1 ) ... 𝑁 ) ) )
81 79 80 syl ⊢ ( 𝜑 → ( 0 ... 𝑁 ) = ( ( 0 ... ( 𝑗 − 1 ) ) ∪ ( ( ( 𝑗 − 1 ) + 1 ) ... 𝑁 ) ) )
82 24 zcnd ⊢ ( 𝜑 → 𝑗 ∈ ℂ )
83 82 68 npcand ⊢ ( 𝜑 → ( ( 𝑗 − 1 ) + 1 ) = 𝑗 )
84 83 oveq1d ⊢ ( 𝜑 → ( ( ( 𝑗 − 1 ) + 1 ) ... 𝑁 ) = ( 𝑗 ... 𝑁 ) )
85 84 uneq2d ⊢ ( 𝜑 → ( ( 0 ... ( 𝑗 − 1 ) ) ∪ ( ( ( 𝑗 − 1 ) + 1 ) ... 𝑁 ) ) = ( ( 0 ... ( 𝑗 − 1 ) ) ∪ ( 𝑗 ... 𝑁 ) ) )
86 81 85 eqtrd ⊢ ( 𝜑 → ( 0 ... 𝑁 ) = ( ( 0 ... ( 𝑗 − 1 ) ) ∪ ( 𝑗 ... 𝑁 ) ) )
87 7 rpcnd ⊢ ( 𝜑 → 𝐸 ∈ ℂ )
88 87 adantr ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ... 𝑁 ) ) → 𝐸 ∈ ℂ )
89 17 recnd ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ... 𝑁 ) ) → ( ( 𝑋 ‘ 𝑖 ) ‘ 𝑡 ) ∈ ℂ )
90 88 89 mulcld ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ... 𝑁 ) ) → ( 𝐸 · ( ( 𝑋 ‘ 𝑖 ) ‘ 𝑡 ) ) ∈ ℂ )
91 65 86 13 90 fsumsplit ⊢ ( 𝜑 → Σ 𝑖 ∈ ( 0 ... 𝑁 ) ( 𝐸 · ( ( 𝑋 ‘ 𝑖 ) ‘ 𝑡 ) ) = ( Σ 𝑖 ∈ ( 0 ... ( 𝑗 − 1 ) ) ( 𝐸 · ( ( 𝑋 ‘ 𝑖 ) ‘ 𝑡 ) ) + Σ 𝑖 ∈ ( 𝑗 ... 𝑁 ) ( 𝐸 · ( ( 𝑋 ‘ 𝑖 ) ‘ 𝑡 ) ) ) )
92 fzfid ⊢ ( 𝜑 → ( 𝑗 ... 𝑁 ) ∈ Fin )
93 14 adantr ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 𝑗 ... 𝑁 ) ) → 𝐸 ∈ ℝ )
94 0zd ⊢ ( 𝜑 → 0 ∈ ℤ )
95 0red ⊢ ( 𝜑 → 0 ∈ ℝ )
96 0le1 ⊢ 0 ≤ 1
97 96 a1i ⊢ ( 𝜑 → 0 ≤ 1 )
98 23 simp3d ⊢ ( 𝜑 → 1 ≤ 𝑗 )
99 95 29 25 97 98 letrd ⊢ ( 𝜑 → 0 ≤ 𝑗 )
100 eluz2 ⊢ ( 𝑗 ∈ ( ℤ≥ ‘ 0 ) ↔ ( 0 ∈ ℤ ∧ 𝑗 ∈ ℤ ∧ 0 ≤ 𝑗 ) )
101 94 24 99 100 syl3anbrc ⊢ ( 𝜑 → 𝑗 ∈ ( ℤ≥ ‘ 0 ) )
102 fzss1 ⊢ ( 𝑗 ∈ ( ℤ≥ ‘ 0 ) → ( 𝑗 ... 𝑁 ) ⊆ ( 0 ... 𝑁 ) )
103 101 102 syl ⊢ ( 𝜑 → ( 𝑗 ... 𝑁 ) ⊆ ( 0 ... 𝑁 ) )
104 103 sselda ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 𝑗 ... 𝑁 ) ) → 𝑖 ∈ ( 0 ... 𝑁 ) )
105 104 4 syldan ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 𝑗 ... 𝑁 ) ) → ( 𝑋 ‘ 𝑖 ) : 𝑇 ⟶ ℝ )
106 2 adantr ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 𝑗 ... 𝑁 ) ) → 𝑡 ∈ 𝑇 )
107 105 106 ffvelrnd ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 𝑗 ... 𝑁 ) ) → ( ( 𝑋 ‘ 𝑖 ) ‘ 𝑡 ) ∈ ℝ )
108 93 107 remulcld ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 𝑗 ... 𝑁 ) ) → ( 𝐸 · ( ( 𝑋 ‘ 𝑖 ) ‘ 𝑡 ) ) ∈ ℝ )
109 92 108 fsumrecl ⊢ ( 𝜑 → Σ 𝑖 ∈ ( 𝑗 ... 𝑁 ) ( 𝐸 · ( ( 𝑋 ‘ 𝑖 ) ‘ 𝑡 ) ) ∈ ℝ )
110 eluzfz2 ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 𝑗 ) → 𝑁 ∈ ( 𝑗 ... 𝑁 ) )
111 ne0i ⊢ ( 𝑁 ∈ ( 𝑗 ... 𝑁 ) → ( 𝑗 ... 𝑁 ) ≠ ∅ )
112 3 50 110 111 4syl ⊢ ( 𝜑 → ( 𝑗 ... 𝑁 ) ≠ ∅ )
113 1 adantr ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 𝑗 ... 𝑁 ) ) → 𝑁 ∈ ℕ )
114 93 113 nndivred ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 𝑗 ... 𝑁 ) ) → ( 𝐸 / 𝑁 ) ∈ ℝ )
115 93 114 remulcld ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 𝑗 ... 𝑁 ) ) → ( 𝐸 · ( 𝐸 / 𝑁 ) ) ∈ ℝ )
116 7 rpgt0d ⊢ ( 𝜑 → 0 < 𝐸 )
117 116 adantr ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 𝑗 ... 𝑁 ) ) → 0 < 𝐸 )
118 ltmul2 ⊢ ( ( ( ( 𝑋 ‘ 𝑖 ) ‘ 𝑡 ) ∈ ℝ ∧ ( 𝐸 / 𝑁 ) ∈ ℝ ∧ ( 𝐸 ∈ ℝ ∧ 0 < 𝐸 ) ) → ( ( ( 𝑋 ‘ 𝑖 ) ‘ 𝑡 ) < ( 𝐸 / 𝑁 ) ↔ ( 𝐸 · ( ( 𝑋 ‘ 𝑖 ) ‘ 𝑡 ) ) < ( 𝐸 · ( 𝐸 / 𝑁 ) ) ) )
119 107 114 93 117 118 syl112anc ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 𝑗 ... 𝑁 ) ) → ( ( ( 𝑋 ‘ 𝑖 ) ‘ 𝑡 ) < ( 𝐸 / 𝑁 ) ↔ ( 𝐸 · ( ( 𝑋 ‘ 𝑖 ) ‘ 𝑡 ) ) < ( 𝐸 · ( 𝐸 / 𝑁 ) ) ) )
120 6 119 mpbid ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 𝑗 ... 𝑁 ) ) → ( 𝐸 · ( ( 𝑋 ‘ 𝑖 ) ‘ 𝑡 ) ) < ( 𝐸 · ( 𝐸 / 𝑁 ) ) )
121 92 112 108 115 120 fsumlt ⊢ ( 𝜑 → Σ 𝑖 ∈ ( 𝑗 ... 𝑁 ) ( 𝐸 · ( ( 𝑋 ‘ 𝑖 ) ‘ 𝑡 ) ) < Σ 𝑖 ∈ ( 𝑗 ... 𝑁 ) ( 𝐸 · ( 𝐸 / 𝑁 ) ) )
122 1 nnne0d ⊢ ( 𝜑 → 𝑁 ≠ 0 )
123 87 67 122 divcld ⊢ ( 𝜑 → ( 𝐸 / 𝑁 ) ∈ ℂ )
124 87 123 mulcld ⊢ ( 𝜑 → ( 𝐸 · ( 𝐸 / 𝑁 ) ) ∈ ℂ )
125 fsumconst ⊢ ( ( ( 𝑗 ... 𝑁 ) ∈ Fin ∧ ( 𝐸 · ( 𝐸 / 𝑁 ) ) ∈ ℂ ) → Σ 𝑖 ∈ ( 𝑗 ... 𝑁 ) ( 𝐸 · ( 𝐸 / 𝑁 ) ) = ( ( ♯ ‘ ( 𝑗 ... 𝑁 ) ) · ( 𝐸 · ( 𝐸 / 𝑁 ) ) ) )
126 92 124 125 syl2anc ⊢ ( 𝜑 → Σ 𝑖 ∈ ( 𝑗 ... 𝑁 ) ( 𝐸 · ( 𝐸 / 𝑁 ) ) = ( ( ♯ ‘ ( 𝑗 ... 𝑁 ) ) · ( 𝐸 · ( 𝐸 / 𝑁 ) ) ) )
127 hashfz ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 𝑗 ) → ( ♯ ‘ ( 𝑗 ... 𝑁 ) ) = ( ( 𝑁 − 𝑗 ) + 1 ) )
128 3 50 127 3syl ⊢ ( 𝜑 → ( ♯ ‘ ( 𝑗 ... 𝑁 ) ) = ( ( 𝑁 − 𝑗 ) + 1 ) )
129 128 oveq1d ⊢ ( 𝜑 → ( ( ♯ ‘ ( 𝑗 ... 𝑁 ) ) · ( 𝐸 · ( 𝐸 / 𝑁 ) ) ) = ( ( ( 𝑁 − 𝑗 ) + 1 ) · ( 𝐸 · ( 𝐸 / 𝑁 ) ) ) )
130 126 129 eqtrd ⊢ ( 𝜑 → Σ 𝑖 ∈ ( 𝑗 ... 𝑁 ) ( 𝐸 · ( 𝐸 / 𝑁 ) ) = ( ( ( 𝑁 − 𝑗 ) + 1 ) · ( 𝐸 · ( 𝐸 / 𝑁 ) ) ) )
131 121 130 breqtrd ⊢ ( 𝜑 → Σ 𝑖 ∈ ( 𝑗 ... 𝑁 ) ( 𝐸 · ( ( 𝑋 ‘ 𝑖 ) ‘ 𝑡 ) ) < ( ( ( 𝑁 − 𝑗 ) + 1 ) · ( 𝐸 · ( 𝐸 / 𝑁 ) ) ) )
132 109 33 61 131 ltadd2dd ⊢ ( 𝜑 → ( Σ 𝑖 ∈ ( 0 ... ( 𝑗 − 1 ) ) ( 𝐸 · ( ( 𝑋 ‘ 𝑖 ) ‘ 𝑡 ) ) + Σ 𝑖 ∈ ( 𝑗 ... 𝑁 ) ( 𝐸 · ( ( 𝑋 ‘ 𝑖 ) ‘ 𝑡 ) ) ) < ( Σ 𝑖 ∈ ( 0 ... ( 𝑗 − 1 ) ) ( 𝐸 · ( ( 𝑋 ‘ 𝑖 ) ‘ 𝑡 ) ) + ( ( ( 𝑁 − 𝑗 ) + 1 ) · ( 𝐸 · ( 𝐸 / 𝑁 ) ) ) ) )
133 91 132 eqbrtrd ⊢ ( 𝜑 → Σ 𝑖 ∈ ( 0 ... 𝑁 ) ( 𝐸 · ( ( 𝑋 ‘ 𝑖 ) ‘ 𝑡 ) ) < ( Σ 𝑖 ∈ ( 0 ... ( 𝑗 − 1 ) ) ( 𝐸 · ( ( 𝑋 ‘ 𝑖 ) ‘ 𝑡 ) ) + ( ( ( 𝑁 − 𝑗 ) + 1 ) · ( 𝐸 · ( 𝐸 / 𝑁 ) ) ) ) )
134 58 5 syldan ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ... ( 𝑗 − 1 ) ) ) → ( ( 𝑋 ‘ 𝑖 ) ‘ 𝑡 ) ≤ 1 )
135 1red ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ... ( 𝑗 − 1 ) ) ) → 1 ∈ ℝ )
136 116 adantr ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ... ( 𝑗 − 1 ) ) ) → 0 < 𝐸 )
137 lemul2 ⊢ ( ( ( ( 𝑋 ‘ 𝑖 ) ‘ 𝑡 ) ∈ ℝ ∧ 1 ∈ ℝ ∧ ( 𝐸 ∈ ℝ ∧ 0 < 𝐸 ) ) → ( ( ( 𝑋 ‘ 𝑖 ) ‘ 𝑡 ) ≤ 1 ↔ ( 𝐸 · ( ( 𝑋 ‘ 𝑖 ) ‘ 𝑡 ) ) ≤ ( 𝐸 · 1 ) ) )
138 59 135 43 136 137 syl112anc ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ... ( 𝑗 − 1 ) ) ) → ( ( ( 𝑋 ‘ 𝑖 ) ‘ 𝑡 ) ≤ 1 ↔ ( 𝐸 · ( ( 𝑋 ‘ 𝑖 ) ‘ 𝑡 ) ) ≤ ( 𝐸 · 1 ) ) )
139 134 138 mpbid ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ... ( 𝑗 − 1 ) ) ) → ( 𝐸 · ( ( 𝑋 ‘ 𝑖 ) ‘ 𝑡 ) ) ≤ ( 𝐸 · 1 ) )
140 87 mulid1d ⊢ ( 𝜑 → ( 𝐸 · 1 ) = 𝐸 )
141 140 adantr ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ... ( 𝑗 − 1 ) ) ) → ( 𝐸 · 1 ) = 𝐸 )
142 139 141 breqtrd ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ... ( 𝑗 − 1 ) ) ) → ( 𝐸 · ( ( 𝑋 ‘ 𝑖 ) ‘ 𝑡 ) ) ≤ 𝐸 )
143 42 60 43 142 fsumle ⊢ ( 𝜑 → Σ 𝑖 ∈ ( 0 ... ( 𝑗 − 1 ) ) ( 𝐸 · ( ( 𝑋 ‘ 𝑖 ) ‘ 𝑡 ) ) ≤ Σ 𝑖 ∈ ( 0 ... ( 𝑗 − 1 ) ) 𝐸 )
144 fsumconst ⊢ ( ( ( 0 ... ( 𝑗 − 1 ) ) ∈ Fin ∧ 𝐸 ∈ ℂ ) → Σ 𝑖 ∈ ( 0 ... ( 𝑗 − 1 ) ) 𝐸 = ( ( ♯ ‘ ( 0 ... ( 𝑗 − 1 ) ) ) · 𝐸 ) )
145 42 87 144 syl2anc ⊢ ( 𝜑 → Σ 𝑖 ∈ ( 0 ... ( 𝑗 − 1 ) ) 𝐸 = ( ( ♯ ‘ ( 0 ... ( 𝑗 − 1 ) ) ) · 𝐸 ) )
146 0z ⊢ 0 ∈ ℤ
147 1e0p1 ⊢ 1 = ( 0 + 1 )
148 147 fveq2i ⊢ ( ℤ≥ ‘ 1 ) = ( ℤ≥ ‘ ( 0 + 1 ) )
149 21 148 eleqtrdi ⊢ ( 𝜑 → 𝑗 ∈ ( ℤ≥ ‘ ( 0 + 1 ) ) )
150 eluzp1m1 ⊢ ( ( 0 ∈ ℤ ∧ 𝑗 ∈ ( ℤ≥ ‘ ( 0 + 1 ) ) ) → ( 𝑗 − 1 ) ∈ ( ℤ≥ ‘ 0 ) )
151 146 149 150 sylancr ⊢ ( 𝜑 → ( 𝑗 − 1 ) ∈ ( ℤ≥ ‘ 0 ) )
152 hashfz ⊢ ( ( 𝑗 − 1 ) ∈ ( ℤ≥ ‘ 0 ) → ( ♯ ‘ ( 0 ... ( 𝑗 − 1 ) ) ) = ( ( ( 𝑗 − 1 ) − 0 ) + 1 ) )
153 151 152 syl ⊢ ( 𝜑 → ( ♯ ‘ ( 0 ... ( 𝑗 − 1 ) ) ) = ( ( ( 𝑗 − 1 ) − 0 ) + 1 ) )
154 82 68 subcld ⊢ ( 𝜑 → ( 𝑗 − 1 ) ∈ ℂ )
155 154 subid1d ⊢ ( 𝜑 → ( ( 𝑗 − 1 ) − 0 ) = ( 𝑗 − 1 ) )
156 155 oveq1d ⊢ ( 𝜑 → ( ( ( 𝑗 − 1 ) − 0 ) + 1 ) = ( ( 𝑗 − 1 ) + 1 ) )
157 153 156 83 3eqtrd ⊢ ( 𝜑 → ( ♯ ‘ ( 0 ... ( 𝑗 − 1 ) ) ) = 𝑗 )
158 157 oveq1d ⊢ ( 𝜑 → ( ( ♯ ‘ ( 0 ... ( 𝑗 − 1 ) ) ) · 𝐸 ) = ( 𝑗 · 𝐸 ) )
159 82 87 mulcomd ⊢ ( 𝜑 → ( 𝑗 · 𝐸 ) = ( 𝐸 · 𝑗 ) )
160 145 158 159 3eqtrd ⊢ ( 𝜑 → Σ 𝑖 ∈ ( 0 ... ( 𝑗 − 1 ) ) 𝐸 = ( 𝐸 · 𝑗 ) )
161 143 160 breqtrd ⊢ ( 𝜑 → Σ 𝑖 ∈ ( 0 ... ( 𝑗 − 1 ) ) ( 𝐸 · ( ( 𝑋 ‘ 𝑖 ) ‘ 𝑡 ) ) ≤ ( 𝐸 · 𝑗 ) )
162 61 26 33 161 leadd1dd ⊢ ( 𝜑 → ( Σ 𝑖 ∈ ( 0 ... ( 𝑗 − 1 ) ) ( 𝐸 · ( ( 𝑋 ‘ 𝑖 ) ‘ 𝑡 ) ) + ( ( ( 𝑁 − 𝑗 ) + 1 ) · ( 𝐸 · ( 𝐸 / 𝑁 ) ) ) ) ≤ ( ( 𝐸 · 𝑗 ) + ( ( ( 𝑁 − 𝑗 ) + 1 ) · ( 𝐸 · ( 𝐸 / 𝑁 ) ) ) ) )
163 19 62 34 133 162 ltletrd ⊢ ( 𝜑 → Σ 𝑖 ∈ ( 0 ... 𝑁 ) ( 𝐸 · ( ( 𝑋 ‘ 𝑖 ) ‘ 𝑡 ) ) < ( ( 𝐸 · 𝑗 ) + ( ( ( 𝑁 − 𝑗 ) + 1 ) · ( 𝐸 · ( 𝐸 / 𝑁 ) ) ) ) )
164 14 14 remulcld ⊢ ( 𝜑 → ( 𝐸 · 𝐸 ) ∈ ℝ )
165 26 164 readdcld ⊢ ( 𝜑 → ( ( 𝐸 · 𝑗 ) + ( 𝐸 · 𝐸 ) ) ∈ ℝ )
166 67 82 subcld ⊢ ( 𝜑 → ( 𝑁 − 𝑗 ) ∈ ℂ )
167 166 68 addcld ⊢ ( 𝜑 → ( ( 𝑁 − 𝑗 ) + 1 ) ∈ ℂ )
168 87 167 123 mul12d ⊢ ( 𝜑 → ( 𝐸 · ( ( ( 𝑁 − 𝑗 ) + 1 ) · ( 𝐸 / 𝑁 ) ) ) = ( ( ( 𝑁 − 𝑗 ) + 1 ) · ( 𝐸 · ( 𝐸 / 𝑁 ) ) ) )
169 168 oveq2d ⊢ ( 𝜑 → ( ( 𝐸 · 𝑗 ) + ( 𝐸 · ( ( ( 𝑁 − 𝑗 ) + 1 ) · ( 𝐸 / 𝑁 ) ) ) ) = ( ( 𝐸 · 𝑗 ) + ( ( ( 𝑁 − 𝑗 ) + 1 ) · ( 𝐸 · ( 𝐸 / 𝑁 ) ) ) ) )
170 30 31 remulcld ⊢ ( 𝜑 → ( ( ( 𝑁 − 𝑗 ) + 1 ) · ( 𝐸 / 𝑁 ) ) ∈ ℝ )
171 14 170 remulcld ⊢ ( 𝜑 → ( 𝐸 · ( ( ( 𝑁 − 𝑗 ) + 1 ) · ( 𝐸 / 𝑁 ) ) ) ∈ ℝ )
172 167 87 67 122 div12d ⊢ ( 𝜑 → ( ( ( 𝑁 − 𝑗 ) + 1 ) · ( 𝐸 / 𝑁 ) ) = ( 𝐸 · ( ( ( 𝑁 − 𝑗 ) + 1 ) / 𝑁 ) ) )
173 29 25 resubcld ⊢ ( 𝜑 → ( 1 − 𝑗 ) ∈ ℝ )
174 elfzle1 ⊢ ( 𝑗 ∈ ( 1 ... 𝑁 ) → 1 ≤ 𝑗 )
175 3 174 syl ⊢ ( 𝜑 → 1 ≤ 𝑗 )
176 29 25 suble0d ⊢ ( 𝜑 → ( ( 1 − 𝑗 ) ≤ 0 ↔ 1 ≤ 𝑗 ) )
177 175 176 mpbird ⊢ ( 𝜑 → ( 1 − 𝑗 ) ≤ 0 )
178 173 95 27 177 leadd2dd ⊢ ( 𝜑 → ( 𝑁 + ( 1 − 𝑗 ) ) ≤ ( 𝑁 + 0 ) )
179 67 68 82 addsub12d ⊢ ( 𝜑 → ( 𝑁 + ( 1 − 𝑗 ) ) = ( 1 + ( 𝑁 − 𝑗 ) ) )
180 68 166 addcomd ⊢ ( 𝜑 → ( 1 + ( 𝑁 − 𝑗 ) ) = ( ( 𝑁 − 𝑗 ) + 1 ) )
181 179 180 eqtrd ⊢ ( 𝜑 → ( 𝑁 + ( 1 − 𝑗 ) ) = ( ( 𝑁 − 𝑗 ) + 1 ) )
182 67 addid1d ⊢ ( 𝜑 → ( 𝑁 + 0 ) = 𝑁 )
183 178 181 182 3brtr3d ⊢ ( 𝜑 → ( ( 𝑁 − 𝑗 ) + 1 ) ≤ 𝑁 )
184 1 nngt0d ⊢ ( 𝜑 → 0 < 𝑁 )
185 lediv1 ⊢ ( ( ( ( 𝑁 − 𝑗 ) + 1 ) ∈ ℝ ∧ 𝑁 ∈ ℝ ∧ ( 𝑁 ∈ ℝ ∧ 0 < 𝑁 ) ) → ( ( ( 𝑁 − 𝑗 ) + 1 ) ≤ 𝑁 ↔ ( ( ( 𝑁 − 𝑗 ) + 1 ) / 𝑁 ) ≤ ( 𝑁 / 𝑁 ) ) )
186 30 27 27 184 185 syl112anc ⊢ ( 𝜑 → ( ( ( 𝑁 − 𝑗 ) + 1 ) ≤ 𝑁 ↔ ( ( ( 𝑁 − 𝑗 ) + 1 ) / 𝑁 ) ≤ ( 𝑁 / 𝑁 ) ) )
187 183 186 mpbid ⊢ ( 𝜑 → ( ( ( 𝑁 − 𝑗 ) + 1 ) / 𝑁 ) ≤ ( 𝑁 / 𝑁 ) )
188 67 122 dividd ⊢ ( 𝜑 → ( 𝑁 / 𝑁 ) = 1 )
189 187 188 breqtrd ⊢ ( 𝜑 → ( ( ( 𝑁 − 𝑗 ) + 1 ) / 𝑁 ) ≤ 1 )
190 30 1 nndivred ⊢ ( 𝜑 → ( ( ( 𝑁 − 𝑗 ) + 1 ) / 𝑁 ) ∈ ℝ )
191 190 29 7 lemul2d ⊢ ( 𝜑 → ( ( ( ( 𝑁 − 𝑗 ) + 1 ) / 𝑁 ) ≤ 1 ↔ ( 𝐸 · ( ( ( 𝑁 − 𝑗 ) + 1 ) / 𝑁 ) ) ≤ ( 𝐸 · 1 ) ) )
192 189 191 mpbid ⊢ ( 𝜑 → ( 𝐸 · ( ( ( 𝑁 − 𝑗 ) + 1 ) / 𝑁 ) ) ≤ ( 𝐸 · 1 ) )
193 192 140 breqtrd ⊢ ( 𝜑 → ( 𝐸 · ( ( ( 𝑁 − 𝑗 ) + 1 ) / 𝑁 ) ) ≤ 𝐸 )
194 172 193 eqbrtrd ⊢ ( 𝜑 → ( ( ( 𝑁 − 𝑗 ) + 1 ) · ( 𝐸 / 𝑁 ) ) ≤ 𝐸 )
195 170 14 7 lemul2d ⊢ ( 𝜑 → ( ( ( ( 𝑁 − 𝑗 ) + 1 ) · ( 𝐸 / 𝑁 ) ) ≤ 𝐸 ↔ ( 𝐸 · ( ( ( 𝑁 − 𝑗 ) + 1 ) · ( 𝐸 / 𝑁 ) ) ) ≤ ( 𝐸 · 𝐸 ) ) )
196 194 195 mpbid ⊢ ( 𝜑 → ( 𝐸 · ( ( ( 𝑁 − 𝑗 ) + 1 ) · ( 𝐸 / 𝑁 ) ) ) ≤ ( 𝐸 · 𝐸 ) )
197 171 164 26 196 leadd2dd ⊢ ( 𝜑 → ( ( 𝐸 · 𝑗 ) + ( 𝐸 · ( ( ( 𝑁 − 𝑗 ) + 1 ) · ( 𝐸 / 𝑁 ) ) ) ) ≤ ( ( 𝐸 · 𝑗 ) + ( 𝐸 · 𝐸 ) ) )
198 169 197 eqbrtrrd ⊢ ( 𝜑 → ( ( 𝐸 · 𝑗 ) + ( ( ( 𝑁 − 𝑗 ) + 1 ) · ( 𝐸 · ( 𝐸 / 𝑁 ) ) ) ) ≤ ( ( 𝐸 · 𝑗 ) + ( 𝐸 · 𝐸 ) ) )
199 87 82 mulcomd ⊢ ( 𝜑 → ( 𝐸 · 𝑗 ) = ( 𝑗 · 𝐸 ) )
200 199 oveq1d ⊢ ( 𝜑 → ( ( 𝐸 · 𝑗 ) + ( 𝐸 · 𝐸 ) ) = ( ( 𝑗 · 𝐸 ) + ( 𝐸 · 𝐸 ) ) )
201 82 87 87 adddird ⊢ ( 𝜑 → ( ( 𝑗 + 𝐸 ) · 𝐸 ) = ( ( 𝑗 · 𝐸 ) + ( 𝐸 · 𝐸 ) ) )
202 200 201 eqtr4d ⊢ ( 𝜑 → ( ( 𝐸 · 𝑗 ) + ( 𝐸 · 𝐸 ) ) = ( ( 𝑗 + 𝐸 ) · 𝐸 ) )
203 25 14 readdcld ⊢ ( 𝜑 → ( 𝑗 + 𝐸 ) ∈ ℝ )
204 14 39 25 8 ltadd2dd ⊢ ( 𝜑 → ( 𝑗 + 𝐸 ) < ( 𝑗 + ( 1 / 3 ) ) )
205 203 40 7 204 ltmul1dd ⊢ ( 𝜑 → ( ( 𝑗 + 𝐸 ) · 𝐸 ) < ( ( 𝑗 + ( 1 / 3 ) ) · 𝐸 ) )
206 202 205 eqbrtrd ⊢ ( 𝜑 → ( ( 𝐸 · 𝑗 ) + ( 𝐸 · 𝐸 ) ) < ( ( 𝑗 + ( 1 / 3 ) ) · 𝐸 ) )
207 34 165 41 198 206 lelttrd ⊢ ( 𝜑 → ( ( 𝐸 · 𝑗 ) + ( ( ( 𝑁 − 𝑗 ) + 1 ) · ( 𝐸 · ( 𝐸 / 𝑁 ) ) ) ) < ( ( 𝑗 + ( 1 / 3 ) ) · 𝐸 ) )
208 19 34 41 163 207 lttrd ⊢ ( 𝜑 → Σ 𝑖 ∈ ( 0 ... 𝑁 ) ( 𝐸 · ( ( 𝑋 ‘ 𝑖 ) ‘ 𝑡 ) ) < ( ( 𝑗 + ( 1 / 3 ) ) · 𝐸 ) )
209 12 208 eqbrtrd ⊢ ( 𝜑 → ( ( 𝑡 ∈ 𝑇 ↦ Σ 𝑖 ∈ ( 0 ... 𝑁 ) ( 𝐸 · ( ( 𝑋 ‘ 𝑖 ) ‘ 𝑡 ) ) ) ‘ 𝑡 ) < ( ( 𝑗 + ( 1 / 3 ) ) · 𝐸 ) )