Mathbox for Glauco Siliprandi < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  stoweidlem11 Structured version   Visualization version   GIF version

Theorem stoweidlem11 42714
 Description: This lemma is used to prove that there is a function 𝑔 as in the proof of [BrosowskiDeutsh] p. 92 (at the top of page 92): this lemma proves that g(t) < ( j + 1 / 3 ) * ε. Here 𝐸 is used to represent ε in the paper. (Contributed by Glauco Siliprandi, 20-Apr-2017.)
Hypotheses
Ref Expression
stoweidlem11.1 (𝜑𝑁 ∈ ℕ)
stoweidlem11.2 (𝜑𝑡𝑇)
stoweidlem11.3 (𝜑𝑗 ∈ (1...𝑁))
stoweidlem11.4 ((𝜑𝑖 ∈ (0...𝑁)) → (𝑋𝑖):𝑇⟶ℝ)
stoweidlem11.5 ((𝜑𝑖 ∈ (0...𝑁)) → ((𝑋𝑖)‘𝑡) ≤ 1)
stoweidlem11.6 ((𝜑𝑖 ∈ (𝑗...𝑁)) → ((𝑋𝑖)‘𝑡) < (𝐸 / 𝑁))
stoweidlem11.7 (𝜑𝐸 ∈ ℝ+)
stoweidlem11.8 (𝜑𝐸 < (1 / 3))
Assertion
Ref Expression
stoweidlem11 (𝜑 → ((𝑡𝑇 ↦ Σ𝑖 ∈ (0...𝑁)(𝐸 · ((𝑋𝑖)‘𝑡)))‘𝑡) < ((𝑗 + (1 / 3)) · 𝐸))
Distinct variable groups:   𝑖,𝑗   𝑡,𝑖,𝐸   𝑖,𝑁,𝑡   𝜑,𝑖   𝑡,𝑇   𝑡,𝑋
Allowed substitution hints:   𝜑(𝑡,𝑗)   𝑇(𝑖,𝑗)   𝐸(𝑗)   𝑁(𝑗)   𝑋(𝑖,𝑗)

Proof of Theorem stoweidlem11
StepHypRef Expression
1 stoweidlem11.2 . . 3 (𝜑𝑡𝑇)
2 sumex 15043 . . 3 Σ𝑖 ∈ (0...𝑁)(𝐸 · ((𝑋𝑖)‘𝑡)) ∈ V
3 eqid 2798 . . . 4 (𝑡𝑇 ↦ Σ𝑖 ∈ (0...𝑁)(𝐸 · ((𝑋𝑖)‘𝑡))) = (𝑡𝑇 ↦ Σ𝑖 ∈ (0...𝑁)(𝐸 · ((𝑋𝑖)‘𝑡)))
43fvmpt2 6761 . . 3 ((𝑡𝑇 ∧ Σ𝑖 ∈ (0...𝑁)(𝐸 · ((𝑋𝑖)‘𝑡)) ∈ V) → ((𝑡𝑇 ↦ Σ𝑖 ∈ (0...𝑁)(𝐸 · ((𝑋𝑖)‘𝑡)))‘𝑡) = Σ𝑖 ∈ (0...𝑁)(𝐸 · ((𝑋𝑖)‘𝑡)))
51, 2, 4sylancl 589 . 2 (𝜑 → ((𝑡𝑇 ↦ Σ𝑖 ∈ (0...𝑁)(𝐸 · ((𝑋𝑖)‘𝑡)))‘𝑡) = Σ𝑖 ∈ (0...𝑁)(𝐸 · ((𝑋𝑖)‘𝑡)))
6 fzfid 13343 . . . 4 (𝜑 → (0...𝑁) ∈ Fin)
7 stoweidlem11.7 . . . . . . 7 (𝜑𝐸 ∈ ℝ+)
87rpred 12426 . . . . . 6 (𝜑𝐸 ∈ ℝ)
98adantr 484 . . . . 5 ((𝜑𝑖 ∈ (0...𝑁)) → 𝐸 ∈ ℝ)
10 stoweidlem11.4 . . . . . 6 ((𝜑𝑖 ∈ (0...𝑁)) → (𝑋𝑖):𝑇⟶ℝ)
111adantr 484 . . . . . 6 ((𝜑𝑖 ∈ (0...𝑁)) → 𝑡𝑇)
1210, 11ffvelrnd 6834 . . . . 5 ((𝜑𝑖 ∈ (0...𝑁)) → ((𝑋𝑖)‘𝑡) ∈ ℝ)
139, 12remulcld 10667 . . . 4 ((𝜑𝑖 ∈ (0...𝑁)) → (𝐸 · ((𝑋𝑖)‘𝑡)) ∈ ℝ)
146, 13fsumrecl 15090 . . 3 (𝜑 → Σ𝑖 ∈ (0...𝑁)(𝐸 · ((𝑋𝑖)‘𝑡)) ∈ ℝ)
15 stoweidlem11.3 . . . . . . . . 9 (𝜑𝑗 ∈ (1...𝑁))
16 elfzuz 12905 . . . . . . . . 9 (𝑗 ∈ (1...𝑁) → 𝑗 ∈ (ℤ‘1))
1715, 16syl 17 . . . . . . . 8 (𝜑𝑗 ∈ (ℤ‘1))
18 eluz2 12244 . . . . . . . 8 (𝑗 ∈ (ℤ‘1) ↔ (1 ∈ ℤ ∧ 𝑗 ∈ ℤ ∧ 1 ≤ 𝑗))
1917, 18sylib 221 . . . . . . 7 (𝜑 → (1 ∈ ℤ ∧ 𝑗 ∈ ℤ ∧ 1 ≤ 𝑗))
2019simp2d 1140 . . . . . 6 (𝜑𝑗 ∈ ℤ)
2120zred 12082 . . . . 5 (𝜑𝑗 ∈ ℝ)
228, 21remulcld 10667 . . . 4 (𝜑 → (𝐸 · 𝑗) ∈ ℝ)
23 stoweidlem11.1 . . . . . . . 8 (𝜑𝑁 ∈ ℕ)
2423nnred 11647 . . . . . . 7 (𝜑𝑁 ∈ ℝ)
2524, 21resubcld 11064 . . . . . 6 (𝜑 → (𝑁𝑗) ∈ ℝ)
26 1red 10638 . . . . . 6 (𝜑 → 1 ∈ ℝ)
2725, 26readdcld 10666 . . . . 5 (𝜑 → ((𝑁𝑗) + 1) ∈ ℝ)
288, 23nndivred 11686 . . . . . 6 (𝜑 → (𝐸 / 𝑁) ∈ ℝ)
298, 28remulcld 10667 . . . . 5 (𝜑 → (𝐸 · (𝐸 / 𝑁)) ∈ ℝ)
3027, 29remulcld 10667 . . . 4 (𝜑 → (((𝑁𝑗) + 1) · (𝐸 · (𝐸 / 𝑁))) ∈ ℝ)
3122, 30readdcld 10666 . . 3 (𝜑 → ((𝐸 · 𝑗) + (((𝑁𝑗) + 1) · (𝐸 · (𝐸 / 𝑁)))) ∈ ℝ)
32 3re 11712 . . . . . . 7 3 ∈ ℝ
3332a1i 11 . . . . . 6 (𝜑 → 3 ∈ ℝ)
34 3ne0 11738 . . . . . . 7 3 ≠ 0
3534a1i 11 . . . . . 6 (𝜑 → 3 ≠ 0)
3633, 35rereccld 11463 . . . . 5 (𝜑 → (1 / 3) ∈ ℝ)
3721, 36readdcld 10666 . . . 4 (𝜑 → (𝑗 + (1 / 3)) ∈ ℝ)
3837, 8remulcld 10667 . . 3 (𝜑 → ((𝑗 + (1 / 3)) · 𝐸) ∈ ℝ)
39 fzfid 13343 . . . . . 6 (𝜑 → (0...(𝑗 − 1)) ∈ Fin)
408adantr 484 . . . . . . 7 ((𝜑𝑖 ∈ (0...(𝑗 − 1))) → 𝐸 ∈ ℝ)
41 elfzelz 12909 . . . . . . . . . . . 12 (𝑗 ∈ (1...𝑁) → 𝑗 ∈ ℤ)
42 peano2zm 12020 . . . . . . . . . . . 12 (𝑗 ∈ ℤ → (𝑗 − 1) ∈ ℤ)
4315, 41, 423syl 18 . . . . . . . . . . 11 (𝜑 → (𝑗 − 1) ∈ ℤ)
4423nnzd 12081 . . . . . . . . . . 11 (𝜑𝑁 ∈ ℤ)
4521, 26resubcld 11064 . . . . . . . . . . . 12 (𝜑 → (𝑗 − 1) ∈ ℝ)
4621lem1d 11569 . . . . . . . . . . . 12 (𝜑 → (𝑗 − 1) ≤ 𝑗)
47 elfzuz3 12906 . . . . . . . . . . . . 13 (𝑗 ∈ (1...𝑁) → 𝑁 ∈ (ℤ𝑗))
48 eluzle 12251 . . . . . . . . . . . . 13 (𝑁 ∈ (ℤ𝑗) → 𝑗𝑁)
4915, 47, 483syl 18 . . . . . . . . . . . 12 (𝜑𝑗𝑁)
5045, 21, 24, 46, 49letrd 10793 . . . . . . . . . . 11 (𝜑 → (𝑗 − 1) ≤ 𝑁)
51 eluz2 12244 . . . . . . . . . . 11 (𝑁 ∈ (ℤ‘(𝑗 − 1)) ↔ ((𝑗 − 1) ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ (𝑗 − 1) ≤ 𝑁))
5243, 44, 50, 51syl3anbrc 1340 . . . . . . . . . 10 (𝜑𝑁 ∈ (ℤ‘(𝑗 − 1)))
53 fzss2 12949 . . . . . . . . . 10 (𝑁 ∈ (ℤ‘(𝑗 − 1)) → (0...(𝑗 − 1)) ⊆ (0...𝑁))
5452, 53syl 17 . . . . . . . . 9 (𝜑 → (0...(𝑗 − 1)) ⊆ (0...𝑁))
5554sselda 3915 . . . . . . . 8 ((𝜑𝑖 ∈ (0...(𝑗 − 1))) → 𝑖 ∈ (0...𝑁))
5655, 12syldan 594 . . . . . . 7 ((𝜑𝑖 ∈ (0...(𝑗 − 1))) → ((𝑋𝑖)‘𝑡) ∈ ℝ)
5740, 56remulcld 10667 . . . . . 6 ((𝜑𝑖 ∈ (0...(𝑗 − 1))) → (𝐸 · ((𝑋𝑖)‘𝑡)) ∈ ℝ)
5839, 57fsumrecl 15090 . . . . 5 (𝜑 → Σ𝑖 ∈ (0...(𝑗 − 1))(𝐸 · ((𝑋𝑖)‘𝑡)) ∈ ℝ)
5958, 30readdcld 10666 . . . 4 (𝜑 → (Σ𝑖 ∈ (0...(𝑗 − 1))(𝐸 · ((𝑋𝑖)‘𝑡)) + (((𝑁𝑗) + 1) · (𝐸 · (𝐸 / 𝑁)))) ∈ ℝ)
6021ltm1d 11568 . . . . . . 7 (𝜑 → (𝑗 − 1) < 𝑗)
61 fzdisj 12936 . . . . . . 7 ((𝑗 − 1) < 𝑗 → ((0...(𝑗 − 1)) ∩ (𝑗...𝑁)) = ∅)
6260, 61syl 17 . . . . . 6 (𝜑 → ((0...(𝑗 − 1)) ∩ (𝑗...𝑁)) = ∅)
63 fzssp1 12952 . . . . . . . . . 10 (0...(𝑁 − 1)) ⊆ (0...((𝑁 − 1) + 1))
6423nncnd 11648 . . . . . . . . . . . 12 (𝜑𝑁 ∈ ℂ)
65 1cnd 10632 . . . . . . . . . . . 12 (𝜑 → 1 ∈ ℂ)
6664, 65npcand 10997 . . . . . . . . . . 11 (𝜑 → ((𝑁 − 1) + 1) = 𝑁)
6766oveq2d 7156 . . . . . . . . . 10 (𝜑 → (0...((𝑁 − 1) + 1)) = (0...𝑁))
6863, 67sseqtrid 3967 . . . . . . . . 9 (𝜑 → (0...(𝑁 − 1)) ⊆ (0...𝑁))
69 1zzd 12008 . . . . . . . . . . . 12 (𝜑 → 1 ∈ ℤ)
70 fzsubel 12945 . . . . . . . . . . . 12 (((1 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝑗 ∈ ℤ ∧ 1 ∈ ℤ)) → (𝑗 ∈ (1...𝑁) ↔ (𝑗 − 1) ∈ ((1 − 1)...(𝑁 − 1))))
7169, 44, 20, 69, 70syl22anc 837 . . . . . . . . . . 11 (𝜑 → (𝑗 ∈ (1...𝑁) ↔ (𝑗 − 1) ∈ ((1 − 1)...(𝑁 − 1))))
7215, 71mpbid 235 . . . . . . . . . 10 (𝜑 → (𝑗 − 1) ∈ ((1 − 1)...(𝑁 − 1)))
73 1m1e0 11704 . . . . . . . . . . 11 (1 − 1) = 0
7473oveq1i 7150 . . . . . . . . . 10 ((1 − 1)...(𝑁 − 1)) = (0...(𝑁 − 1))
7572, 74eleqtrdi 2900 . . . . . . . . 9 (𝜑 → (𝑗 − 1) ∈ (0...(𝑁 − 1)))
7668, 75sseldd 3916 . . . . . . . 8 (𝜑 → (𝑗 − 1) ∈ (0...𝑁))
77 fzsplit 12935 . . . . . . . 8 ((𝑗 − 1) ∈ (0...𝑁) → (0...𝑁) = ((0...(𝑗 − 1)) ∪ (((𝑗 − 1) + 1)...𝑁)))
7876, 77syl 17 . . . . . . 7 (𝜑 → (0...𝑁) = ((0...(𝑗 − 1)) ∪ (((𝑗 − 1) + 1)...𝑁)))
7920zcnd 12083 . . . . . . . . . 10 (𝜑𝑗 ∈ ℂ)
8079, 65npcand 10997 . . . . . . . . 9 (𝜑 → ((𝑗 − 1) + 1) = 𝑗)
8180oveq1d 7155 . . . . . . . 8 (𝜑 → (((𝑗 − 1) + 1)...𝑁) = (𝑗...𝑁))
8281uneq2d 4090 . . . . . . 7 (𝜑 → ((0...(𝑗 − 1)) ∪ (((𝑗 − 1) + 1)...𝑁)) = ((0...(𝑗 − 1)) ∪ (𝑗...𝑁)))
8378, 82eqtrd 2833 . . . . . 6 (𝜑 → (0...𝑁) = ((0...(𝑗 − 1)) ∪ (𝑗...𝑁)))
847rpcnd 12428 . . . . . . . 8 (𝜑𝐸 ∈ ℂ)
8584adantr 484 . . . . . . 7 ((𝜑𝑖 ∈ (0...𝑁)) → 𝐸 ∈ ℂ)
8612recnd 10665 . . . . . . 7 ((𝜑𝑖 ∈ (0...𝑁)) → ((𝑋𝑖)‘𝑡) ∈ ℂ)
8785, 86mulcld 10657 . . . . . 6 ((𝜑𝑖 ∈ (0...𝑁)) → (𝐸 · ((𝑋𝑖)‘𝑡)) ∈ ℂ)
8862, 83, 6, 87fsumsplit 15096 . . . . 5 (𝜑 → Σ𝑖 ∈ (0...𝑁)(𝐸 · ((𝑋𝑖)‘𝑡)) = (Σ𝑖 ∈ (0...(𝑗 − 1))(𝐸 · ((𝑋𝑖)‘𝑡)) + Σ𝑖 ∈ (𝑗...𝑁)(𝐸 · ((𝑋𝑖)‘𝑡))))
89 fzfid 13343 . . . . . . 7 (𝜑 → (𝑗...𝑁) ∈ Fin)
908adantr 484 . . . . . . . 8 ((𝜑𝑖 ∈ (𝑗...𝑁)) → 𝐸 ∈ ℝ)
91 0zd 11988 . . . . . . . . . . . . 13 (𝜑 → 0 ∈ ℤ)
92 0red 10640 . . . . . . . . . . . . . 14 (𝜑 → 0 ∈ ℝ)
93 0le1 11159 . . . . . . . . . . . . . . 15 0 ≤ 1
9493a1i 11 . . . . . . . . . . . . . 14 (𝜑 → 0 ≤ 1)
9519simp3d 1141 . . . . . . . . . . . . . 14 (𝜑 → 1 ≤ 𝑗)
9692, 26, 21, 94, 95letrd 10793 . . . . . . . . . . . . 13 (𝜑 → 0 ≤ 𝑗)
97 eluz2 12244 . . . . . . . . . . . . 13 (𝑗 ∈ (ℤ‘0) ↔ (0 ∈ ℤ ∧ 𝑗 ∈ ℤ ∧ 0 ≤ 𝑗))
9891, 20, 96, 97syl3anbrc 1340 . . . . . . . . . . . 12 (𝜑𝑗 ∈ (ℤ‘0))
99 fzss1 12948 . . . . . . . . . . . 12 (𝑗 ∈ (ℤ‘0) → (𝑗...𝑁) ⊆ (0...𝑁))
10098, 99syl 17 . . . . . . . . . . 11 (𝜑 → (𝑗...𝑁) ⊆ (0...𝑁))
101100sselda 3915 . . . . . . . . . 10 ((𝜑𝑖 ∈ (𝑗...𝑁)) → 𝑖 ∈ (0...𝑁))
102101, 10syldan 594 . . . . . . . . 9 ((𝜑𝑖 ∈ (𝑗...𝑁)) → (𝑋𝑖):𝑇⟶ℝ)
1031adantr 484 . . . . . . . . 9 ((𝜑𝑖 ∈ (𝑗...𝑁)) → 𝑡𝑇)
104102, 103ffvelrnd 6834 . . . . . . . 8 ((𝜑𝑖 ∈ (𝑗...𝑁)) → ((𝑋𝑖)‘𝑡) ∈ ℝ)
10590, 104remulcld 10667 . . . . . . 7 ((𝜑𝑖 ∈ (𝑗...𝑁)) → (𝐸 · ((𝑋𝑖)‘𝑡)) ∈ ℝ)
10689, 105fsumrecl 15090 . . . . . 6 (𝜑 → Σ𝑖 ∈ (𝑗...𝑁)(𝐸 · ((𝑋𝑖)‘𝑡)) ∈ ℝ)
107 eluzfz2 12917 . . . . . . . . 9 (𝑁 ∈ (ℤ𝑗) → 𝑁 ∈ (𝑗...𝑁))
108 ne0i 4250 . . . . . . . . 9 (𝑁 ∈ (𝑗...𝑁) → (𝑗...𝑁) ≠ ∅)
10915, 47, 107, 1084syl 19 . . . . . . . 8 (𝜑 → (𝑗...𝑁) ≠ ∅)
11023adantr 484 . . . . . . . . . 10 ((𝜑𝑖 ∈ (𝑗...𝑁)) → 𝑁 ∈ ℕ)
11190, 110nndivred 11686 . . . . . . . . 9 ((𝜑𝑖 ∈ (𝑗...𝑁)) → (𝐸 / 𝑁) ∈ ℝ)
11290, 111remulcld 10667 . . . . . . . 8 ((𝜑𝑖 ∈ (𝑗...𝑁)) → (𝐸 · (𝐸 / 𝑁)) ∈ ℝ)
113 stoweidlem11.6 . . . . . . . . 9 ((𝜑𝑖 ∈ (𝑗...𝑁)) → ((𝑋𝑖)‘𝑡) < (𝐸 / 𝑁))
1147rpgt0d 12429 . . . . . . . . . . 11 (𝜑 → 0 < 𝐸)
115114adantr 484 . . . . . . . . . 10 ((𝜑𝑖 ∈ (𝑗...𝑁)) → 0 < 𝐸)
116 ltmul2 11487 . . . . . . . . . 10 ((((𝑋𝑖)‘𝑡) ∈ ℝ ∧ (𝐸 / 𝑁) ∈ ℝ ∧ (𝐸 ∈ ℝ ∧ 0 < 𝐸)) → (((𝑋𝑖)‘𝑡) < (𝐸 / 𝑁) ↔ (𝐸 · ((𝑋𝑖)‘𝑡)) < (𝐸 · (𝐸 / 𝑁))))
117104, 111, 90, 115, 116syl112anc 1371 . . . . . . . . 9 ((𝜑𝑖 ∈ (𝑗...𝑁)) → (((𝑋𝑖)‘𝑡) < (𝐸 / 𝑁) ↔ (𝐸 · ((𝑋𝑖)‘𝑡)) < (𝐸 · (𝐸 / 𝑁))))
118113, 117mpbid 235 . . . . . . . 8 ((𝜑𝑖 ∈ (𝑗...𝑁)) → (𝐸 · ((𝑋𝑖)‘𝑡)) < (𝐸 · (𝐸 / 𝑁)))
11989, 109, 105, 112, 118fsumlt 15154 . . . . . . 7 (𝜑 → Σ𝑖 ∈ (𝑗...𝑁)(𝐸 · ((𝑋𝑖)‘𝑡)) < Σ𝑖 ∈ (𝑗...𝑁)(𝐸 · (𝐸 / 𝑁)))
12023nnne0d 11682 . . . . . . . . . . 11 (𝜑𝑁 ≠ 0)
12184, 64, 120divcld 11412 . . . . . . . . . 10 (𝜑 → (𝐸 / 𝑁) ∈ ℂ)
12284, 121mulcld 10657 . . . . . . . . 9 (𝜑 → (𝐸 · (𝐸 / 𝑁)) ∈ ℂ)
123 fsumconst 15144 . . . . . . . . 9 (((𝑗...𝑁) ∈ Fin ∧ (𝐸 · (𝐸 / 𝑁)) ∈ ℂ) → Σ𝑖 ∈ (𝑗...𝑁)(𝐸 · (𝐸 / 𝑁)) = ((♯‘(𝑗...𝑁)) · (𝐸 · (𝐸 / 𝑁))))
12489, 122, 123syl2anc 587 . . . . . . . 8 (𝜑 → Σ𝑖 ∈ (𝑗...𝑁)(𝐸 · (𝐸 / 𝑁)) = ((♯‘(𝑗...𝑁)) · (𝐸 · (𝐸 / 𝑁))))
125 hashfz 13791 . . . . . . . . . 10 (𝑁 ∈ (ℤ𝑗) → (♯‘(𝑗...𝑁)) = ((𝑁𝑗) + 1))
12615, 47, 1253syl 18 . . . . . . . . 9 (𝜑 → (♯‘(𝑗...𝑁)) = ((𝑁𝑗) + 1))
127126oveq1d 7155 . . . . . . . 8 (𝜑 → ((♯‘(𝑗...𝑁)) · (𝐸 · (𝐸 / 𝑁))) = (((𝑁𝑗) + 1) · (𝐸 · (𝐸 / 𝑁))))
128124, 127eqtrd 2833 . . . . . . 7 (𝜑 → Σ𝑖 ∈ (𝑗...𝑁)(𝐸 · (𝐸 / 𝑁)) = (((𝑁𝑗) + 1) · (𝐸 · (𝐸 / 𝑁))))
129119, 128breqtrd 5057 . . . . . 6 (𝜑 → Σ𝑖 ∈ (𝑗...𝑁)(𝐸 · ((𝑋𝑖)‘𝑡)) < (((𝑁𝑗) + 1) · (𝐸 · (𝐸 / 𝑁))))
130106, 30, 58, 129ltadd2dd 10795 . . . . 5 (𝜑 → (Σ𝑖 ∈ (0...(𝑗 − 1))(𝐸 · ((𝑋𝑖)‘𝑡)) + Σ𝑖 ∈ (𝑗...𝑁)(𝐸 · ((𝑋𝑖)‘𝑡))) < (Σ𝑖 ∈ (0...(𝑗 − 1))(𝐸 · ((𝑋𝑖)‘𝑡)) + (((𝑁𝑗) + 1) · (𝐸 · (𝐸 / 𝑁)))))
13188, 130eqbrtrd 5053 . . . 4 (𝜑 → Σ𝑖 ∈ (0...𝑁)(𝐸 · ((𝑋𝑖)‘𝑡)) < (Σ𝑖 ∈ (0...(𝑗 − 1))(𝐸 · ((𝑋𝑖)‘𝑡)) + (((𝑁𝑗) + 1) · (𝐸 · (𝐸 / 𝑁)))))
132 stoweidlem11.5 . . . . . . . . . 10 ((𝜑𝑖 ∈ (0...𝑁)) → ((𝑋𝑖)‘𝑡) ≤ 1)
13355, 132syldan 594 . . . . . . . . 9 ((𝜑𝑖 ∈ (0...(𝑗 − 1))) → ((𝑋𝑖)‘𝑡) ≤ 1)
134 1red 10638 . . . . . . . . . 10 ((𝜑𝑖 ∈ (0...(𝑗 − 1))) → 1 ∈ ℝ)
135114adantr 484 . . . . . . . . . 10 ((𝜑𝑖 ∈ (0...(𝑗 − 1))) → 0 < 𝐸)
136 lemul2 11489 . . . . . . . . . 10 ((((𝑋𝑖)‘𝑡) ∈ ℝ ∧ 1 ∈ ℝ ∧ (𝐸 ∈ ℝ ∧ 0 < 𝐸)) → (((𝑋𝑖)‘𝑡) ≤ 1 ↔ (𝐸 · ((𝑋𝑖)‘𝑡)) ≤ (𝐸 · 1)))
13756, 134, 40, 135, 136syl112anc 1371 . . . . . . . . 9 ((𝜑𝑖 ∈ (0...(𝑗 − 1))) → (((𝑋𝑖)‘𝑡) ≤ 1 ↔ (𝐸 · ((𝑋𝑖)‘𝑡)) ≤ (𝐸 · 1)))
138133, 137mpbid 235 . . . . . . . 8 ((𝜑𝑖 ∈ (0...(𝑗 − 1))) → (𝐸 · ((𝑋𝑖)‘𝑡)) ≤ (𝐸 · 1))
13984mulid1d 10654 . . . . . . . . 9 (𝜑 → (𝐸 · 1) = 𝐸)
140139adantr 484 . . . . . . . 8 ((𝜑𝑖 ∈ (0...(𝑗 − 1))) → (𝐸 · 1) = 𝐸)
141138, 140breqtrd 5057 . . . . . . 7 ((𝜑𝑖 ∈ (0...(𝑗 − 1))) → (𝐸 · ((𝑋𝑖)‘𝑡)) ≤ 𝐸)
14239, 57, 40, 141fsumle 15153 . . . . . 6 (𝜑 → Σ𝑖 ∈ (0...(𝑗 − 1))(𝐸 · ((𝑋𝑖)‘𝑡)) ≤ Σ𝑖 ∈ (0...(𝑗 − 1))𝐸)
143 fsumconst 15144 . . . . . . . 8 (((0...(𝑗 − 1)) ∈ Fin ∧ 𝐸 ∈ ℂ) → Σ𝑖 ∈ (0...(𝑗 − 1))𝐸 = ((♯‘(0...(𝑗 − 1))) · 𝐸))
14439, 84, 143syl2anc 587 . . . . . . 7 (𝜑 → Σ𝑖 ∈ (0...(𝑗 − 1))𝐸 = ((♯‘(0...(𝑗 − 1))) · 𝐸))
145 0z 11987 . . . . . . . . . . 11 0 ∈ ℤ
146 1e0p1 12135 . . . . . . . . . . . . 13 1 = (0 + 1)
147146fveq2i 6653 . . . . . . . . . . . 12 (ℤ‘1) = (ℤ‘(0 + 1))
14817, 147eleqtrdi 2900 . . . . . . . . . . 11 (𝜑𝑗 ∈ (ℤ‘(0 + 1)))
149 eluzp1m1 12263 . . . . . . . . . . 11 ((0 ∈ ℤ ∧ 𝑗 ∈ (ℤ‘(0 + 1))) → (𝑗 − 1) ∈ (ℤ‘0))
150145, 148, 149sylancr 590 . . . . . . . . . 10 (𝜑 → (𝑗 − 1) ∈ (ℤ‘0))
151 hashfz 13791 . . . . . . . . . 10 ((𝑗 − 1) ∈ (ℤ‘0) → (♯‘(0...(𝑗 − 1))) = (((𝑗 − 1) − 0) + 1))
152150, 151syl 17 . . . . . . . . 9 (𝜑 → (♯‘(0...(𝑗 − 1))) = (((𝑗 − 1) − 0) + 1))
15379, 65subcld 10993 . . . . . . . . . . 11 (𝜑 → (𝑗 − 1) ∈ ℂ)
154153subid1d 10982 . . . . . . . . . 10 (𝜑 → ((𝑗 − 1) − 0) = (𝑗 − 1))
155154oveq1d 7155 . . . . . . . . 9 (𝜑 → (((𝑗 − 1) − 0) + 1) = ((𝑗 − 1) + 1))
156152, 155, 803eqtrd 2837 . . . . . . . 8 (𝜑 → (♯‘(0...(𝑗 − 1))) = 𝑗)
157156oveq1d 7155 . . . . . . 7 (𝜑 → ((♯‘(0...(𝑗 − 1))) · 𝐸) = (𝑗 · 𝐸))
15879, 84mulcomd 10658 . . . . . . 7 (𝜑 → (𝑗 · 𝐸) = (𝐸 · 𝑗))
159144, 157, 1583eqtrd 2837 . . . . . 6 (𝜑 → Σ𝑖 ∈ (0...(𝑗 − 1))𝐸 = (𝐸 · 𝑗))
160142, 159breqtrd 5057 . . . . 5 (𝜑 → Σ𝑖 ∈ (0...(𝑗 − 1))(𝐸 · ((𝑋𝑖)‘𝑡)) ≤ (𝐸 · 𝑗))
16158, 22, 30, 160leadd1dd 11250 . . . 4 (𝜑 → (Σ𝑖 ∈ (0...(𝑗 − 1))(𝐸 · ((𝑋𝑖)‘𝑡)) + (((𝑁𝑗) + 1) · (𝐸 · (𝐸 / 𝑁)))) ≤ ((𝐸 · 𝑗) + (((𝑁𝑗) + 1) · (𝐸 · (𝐸 / 𝑁)))))
16214, 59, 31, 131, 161ltletrd 10796 . . 3 (𝜑 → Σ𝑖 ∈ (0...𝑁)(𝐸 · ((𝑋𝑖)‘𝑡)) < ((𝐸 · 𝑗) + (((𝑁𝑗) + 1) · (𝐸 · (𝐸 / 𝑁)))))
1638, 8remulcld 10667 . . . . 5 (𝜑 → (𝐸 · 𝐸) ∈ ℝ)
16422, 163readdcld 10666 . . . 4 (𝜑 → ((𝐸 · 𝑗) + (𝐸 · 𝐸)) ∈ ℝ)
16564, 79subcld 10993 . . . . . . . 8 (𝜑 → (𝑁𝑗) ∈ ℂ)
166165, 65addcld 10656 . . . . . . 7 (𝜑 → ((𝑁𝑗) + 1) ∈ ℂ)
16784, 166, 121mul12d 10845 . . . . . 6 (𝜑 → (𝐸 · (((𝑁𝑗) + 1) · (𝐸 / 𝑁))) = (((𝑁𝑗) + 1) · (𝐸 · (𝐸 / 𝑁))))
168167oveq2d 7156 . . . . 5 (𝜑 → ((𝐸 · 𝑗) + (𝐸 · (((𝑁𝑗) + 1) · (𝐸 / 𝑁)))) = ((𝐸 · 𝑗) + (((𝑁𝑗) + 1) · (𝐸 · (𝐸 / 𝑁)))))
16927, 28remulcld 10667 . . . . . . 7 (𝜑 → (((𝑁𝑗) + 1) · (𝐸 / 𝑁)) ∈ ℝ)
1708, 169remulcld 10667 . . . . . 6 (𝜑 → (𝐸 · (((𝑁𝑗) + 1) · (𝐸 / 𝑁))) ∈ ℝ)
171166, 84, 64, 120div12d 11448 . . . . . . . 8 (𝜑 → (((𝑁𝑗) + 1) · (𝐸 / 𝑁)) = (𝐸 · (((𝑁𝑗) + 1) / 𝑁)))
17226, 21resubcld 11064 . . . . . . . . . . . . . 14 (𝜑 → (1 − 𝑗) ∈ ℝ)
173 elfzle1 12912 . . . . . . . . . . . . . . . 16 (𝑗 ∈ (1...𝑁) → 1 ≤ 𝑗)
17415, 173syl 17 . . . . . . . . . . . . . . 15 (𝜑 → 1 ≤ 𝑗)
17526, 21suble0d 11227 . . . . . . . . . . . . . . 15 (𝜑 → ((1 − 𝑗) ≤ 0 ↔ 1 ≤ 𝑗))
176174, 175mpbird 260 . . . . . . . . . . . . . 14 (𝜑 → (1 − 𝑗) ≤ 0)
177172, 92, 24, 176leadd2dd 11251 . . . . . . . . . . . . 13 (𝜑 → (𝑁 + (1 − 𝑗)) ≤ (𝑁 + 0))
17864, 65, 79addsub12d 11016 . . . . . . . . . . . . . 14 (𝜑 → (𝑁 + (1 − 𝑗)) = (1 + (𝑁𝑗)))
17965, 165addcomd 10838 . . . . . . . . . . . . . 14 (𝜑 → (1 + (𝑁𝑗)) = ((𝑁𝑗) + 1))
180178, 179eqtrd 2833 . . . . . . . . . . . . 13 (𝜑 → (𝑁 + (1 − 𝑗)) = ((𝑁𝑗) + 1))
18164addid1d 10836 . . . . . . . . . . . . 13 (𝜑 → (𝑁 + 0) = 𝑁)
182177, 180, 1813brtr3d 5062 . . . . . . . . . . . 12 (𝜑 → ((𝑁𝑗) + 1) ≤ 𝑁)
18323nngt0d 11681 . . . . . . . . . . . . 13 (𝜑 → 0 < 𝑁)
184 lediv1 11501 . . . . . . . . . . . . 13 ((((𝑁𝑗) + 1) ∈ ℝ ∧ 𝑁 ∈ ℝ ∧ (𝑁 ∈ ℝ ∧ 0 < 𝑁)) → (((𝑁𝑗) + 1) ≤ 𝑁 ↔ (((𝑁𝑗) + 1) / 𝑁) ≤ (𝑁 / 𝑁)))
18527, 24, 24, 183, 184syl112anc 1371 . . . . . . . . . . . 12 (𝜑 → (((𝑁𝑗) + 1) ≤ 𝑁 ↔ (((𝑁𝑗) + 1) / 𝑁) ≤ (𝑁 / 𝑁)))
186182, 185mpbid 235 . . . . . . . . . . 11 (𝜑 → (((𝑁𝑗) + 1) / 𝑁) ≤ (𝑁 / 𝑁))
18764, 120dividd 11410 . . . . . . . . . . 11 (𝜑 → (𝑁 / 𝑁) = 1)
188186, 187breqtrd 5057 . . . . . . . . . 10 (𝜑 → (((𝑁𝑗) + 1) / 𝑁) ≤ 1)
18927, 23nndivred 11686 . . . . . . . . . . 11 (𝜑 → (((𝑁𝑗) + 1) / 𝑁) ∈ ℝ)
190189, 26, 7lemul2d 12470 . . . . . . . . . 10 (𝜑 → ((((𝑁𝑗) + 1) / 𝑁) ≤ 1 ↔ (𝐸 · (((𝑁𝑗) + 1) / 𝑁)) ≤ (𝐸 · 1)))
191188, 190mpbid 235 . . . . . . . . 9 (𝜑 → (𝐸 · (((𝑁𝑗) + 1) / 𝑁)) ≤ (𝐸 · 1))
192191, 139breqtrd 5057 . . . . . . . 8 (𝜑 → (𝐸 · (((𝑁𝑗) + 1) / 𝑁)) ≤ 𝐸)
193171, 192eqbrtrd 5053 . . . . . . 7 (𝜑 → (((𝑁𝑗) + 1) · (𝐸 / 𝑁)) ≤ 𝐸)
194169, 8, 7lemul2d 12470 . . . . . . 7 (𝜑 → ((((𝑁𝑗) + 1) · (𝐸 / 𝑁)) ≤ 𝐸 ↔ (𝐸 · (((𝑁𝑗) + 1) · (𝐸 / 𝑁))) ≤ (𝐸 · 𝐸)))
195193, 194mpbid 235 . . . . . 6 (𝜑 → (𝐸 · (((𝑁𝑗) + 1) · (𝐸 / 𝑁))) ≤ (𝐸 · 𝐸))
196170, 163, 22, 195leadd2dd 11251 . . . . 5 (𝜑 → ((𝐸 · 𝑗) + (𝐸 · (((𝑁𝑗) + 1) · (𝐸 / 𝑁)))) ≤ ((𝐸 · 𝑗) + (𝐸 · 𝐸)))
197168, 196eqbrtrrd 5055 . . . 4 (𝜑 → ((𝐸 · 𝑗) + (((𝑁𝑗) + 1) · (𝐸 · (𝐸 / 𝑁)))) ≤ ((𝐸 · 𝑗) + (𝐸 · 𝐸)))
19884, 79mulcomd 10658 . . . . . . 7 (𝜑 → (𝐸 · 𝑗) = (𝑗 · 𝐸))
199198oveq1d 7155 . . . . . 6 (𝜑 → ((𝐸 · 𝑗) + (𝐸 · 𝐸)) = ((𝑗 · 𝐸) + (𝐸 · 𝐸)))
20079, 84, 84adddird 10662 . . . . . 6 (𝜑 → ((𝑗 + 𝐸) · 𝐸) = ((𝑗 · 𝐸) + (𝐸 · 𝐸)))
201199, 200eqtr4d 2836 . . . . 5 (𝜑 → ((𝐸 · 𝑗) + (𝐸 · 𝐸)) = ((𝑗 + 𝐸) · 𝐸))
20221, 8readdcld 10666 . . . . . 6 (𝜑 → (𝑗 + 𝐸) ∈ ℝ)
203 stoweidlem11.8 . . . . . . 7 (𝜑𝐸 < (1 / 3))
2048, 36, 21, 203ltadd2dd 10795 . . . . . 6 (𝜑 → (𝑗 + 𝐸) < (𝑗 + (1 / 3)))
205202, 37, 7, 204ltmul1dd 12481 . . . . 5 (𝜑 → ((𝑗 + 𝐸) · 𝐸) < ((𝑗 + (1 / 3)) · 𝐸))
206201, 205eqbrtrd 5053 . . . 4 (𝜑 → ((𝐸 · 𝑗) + (𝐸 · 𝐸)) < ((𝑗 + (1 / 3)) · 𝐸))
20731, 164, 38, 197, 206lelttrd 10794 . . 3 (𝜑 → ((𝐸 · 𝑗) + (((𝑁𝑗) + 1) · (𝐸 · (𝐸 / 𝑁)))) < ((𝑗 + (1 / 3)) · 𝐸))
20814, 31, 38, 162, 207lttrd 10797 . 2 (𝜑 → Σ𝑖 ∈ (0...𝑁)(𝐸 · ((𝑋𝑖)‘𝑡)) < ((𝑗 + (1 / 3)) · 𝐸))
2095, 208eqbrtrd 5053 1 (𝜑 → ((𝑡𝑇 ↦ Σ𝑖 ∈ (0...𝑁)(𝐸 · ((𝑋𝑖)‘𝑡)))‘𝑡) < ((𝑗 + (1 / 3)) · 𝐸))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ↔ wb 209   ∧ wa 399   ∧ w3a 1084   = wceq 1538   ∈ wcel 2111   ≠ wne 2987  Vcvv 3441   ∪ cun 3879   ∩ cin 3880   ⊆ wss 3881  ∅c0 4243   class class class wbr 5031   ↦ cmpt 5111  ⟶wf 6323  ‘cfv 6327  (class class class)co 7140  Fincfn 8499  ℂcc 10531  ℝcr 10532  0cc0 10533  1c1 10534   + caddc 10536   · cmul 10538   < clt 10671   ≤ cle 10672   − cmin 10866   / cdiv 11293  ℕcn 11632  3c3 11688  ℤcz 11976  ℤ≥cuz 12238  ℝ+crp 12384  ...cfz 12892  ♯chash 13693  Σcsu 15041 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-10 2142  ax-11 2158  ax-12 2175  ax-ext 2770  ax-rep 5155  ax-sep 5168  ax-nul 5175  ax-pow 5232  ax-pr 5296  ax-un 7448  ax-inf2 9095  ax-cnex 10589  ax-resscn 10590  ax-1cn 10591  ax-icn 10592  ax-addcl 10593  ax-addrcl 10594  ax-mulcl 10595  ax-mulrcl 10596  ax-mulcom 10597  ax-addass 10598  ax-mulass 10599  ax-distr 10600  ax-i2m1 10601  ax-1ne0 10602  ax-1rid 10603  ax-rnegex 10604  ax-rrecex 10605  ax-cnre 10606  ax-pre-lttri 10607  ax-pre-lttrn 10608  ax-pre-ltadd 10609  ax-pre-mulgt0 10610  ax-pre-sup 10611 This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3or 1085  df-3an 1086  df-tru 1541  df-fal 1551  df-ex 1782  df-nf 1786  df-sb 2070  df-mo 2598  df-eu 2629  df-clab 2777  df-cleq 2791  df-clel 2870  df-nfc 2938  df-ne 2988  df-nel 3092  df-ral 3111  df-rex 3112  df-reu 3113  df-rmo 3114  df-rab 3115  df-v 3443  df-sbc 3721  df-csb 3829  df-dif 3884  df-un 3886  df-in 3888  df-ss 3898  df-pss 3900  df-nul 4244  df-if 4426  df-pw 4499  df-sn 4526  df-pr 4528  df-tp 4530  df-op 4532  df-uni 4802  df-int 4840  df-iun 4884  df-br 5032  df-opab 5094  df-mpt 5112  df-tr 5138  df-id 5426  df-eprel 5431  df-po 5439  df-so 5440  df-fr 5479  df-se 5480  df-we 5481  df-xp 5526  df-rel 5527  df-cnv 5528  df-co 5529  df-dm 5530  df-rn 5531  df-res 5532  df-ima 5533  df-pred 6119  df-ord 6165  df-on 6166  df-lim 6167  df-suc 6168  df-iota 6286  df-fun 6329  df-fn 6330  df-f 6331  df-f1 6332  df-fo 6333  df-f1o 6334  df-fv 6335  df-isom 6336  df-riota 7098  df-ov 7143  df-oprab 7144  df-mpo 7145  df-om 7568  df-1st 7678  df-2nd 7679  df-wrecs 7937  df-recs 7998  df-rdg 8036  df-1o 8092  df-oadd 8096  df-er 8279  df-en 8500  df-dom 8501  df-sdom 8502  df-fin 8503  df-sup 8897  df-oi 8965  df-card 9359  df-pnf 10673  df-mnf 10674  df-xr 10675  df-ltxr 10676  df-le 10677  df-sub 10868  df-neg 10869  df-div 11294  df-nn 11633  df-2 11695  df-3 11696  df-n0 11893  df-z 11977  df-uz 12239  df-rp 12385  df-ico 12739  df-fz 12893  df-fzo 13036  df-seq 13372  df-exp 13433  df-hash 13694  df-cj 14457  df-re 14458  df-im 14459  df-sqrt 14593  df-abs 14594  df-clim 14844  df-sum 15042 This theorem is referenced by:  stoweidlem34  42737
 Copyright terms: Public domain W3C validator