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