Proof of Theorem stoweidlem11
Step | Hyp | Ref
| Expression |
1 | | stoweidlem11.2 |
. . 3
⊢ (𝜑 → 𝑡 ∈ 𝑇) |
2 | | sumex 15251 |
. . 3
⊢
Σ𝑖 ∈
(0...𝑁)(𝐸 · ((𝑋‘𝑖)‘𝑡)) ∈ V |
3 | | eqid 2737 |
. . . 4
⊢ (𝑡 ∈ 𝑇 ↦ Σ𝑖 ∈ (0...𝑁)(𝐸 · ((𝑋‘𝑖)‘𝑡))) = (𝑡 ∈ 𝑇 ↦ Σ𝑖 ∈ (0...𝑁)(𝐸 · ((𝑋‘𝑖)‘𝑡))) |
4 | 3 | fvmpt2 6829 |
. . 3
⊢ ((𝑡 ∈ 𝑇 ∧ Σ𝑖 ∈ (0...𝑁)(𝐸 · ((𝑋‘𝑖)‘𝑡)) ∈ V) → ((𝑡 ∈ 𝑇 ↦ Σ𝑖 ∈ (0...𝑁)(𝐸 · ((𝑋‘𝑖)‘𝑡)))‘𝑡) = Σ𝑖 ∈ (0...𝑁)(𝐸 · ((𝑋‘𝑖)‘𝑡))) |
5 | 1, 2, 4 | sylancl 589 |
. 2
⊢ (𝜑 → ((𝑡 ∈ 𝑇 ↦ Σ𝑖 ∈ (0...𝑁)(𝐸 · ((𝑋‘𝑖)‘𝑡)))‘𝑡) = Σ𝑖 ∈ (0...𝑁)(𝐸 · ((𝑋‘𝑖)‘𝑡))) |
6 | | fzfid 13546 |
. . . 4
⊢ (𝜑 → (0...𝑁) ∈ Fin) |
7 | | stoweidlem11.7 |
. . . . . . 7
⊢ (𝜑 → 𝐸 ∈
ℝ+) |
8 | 7 | rpred 12628 |
. . . . . 6
⊢ (𝜑 → 𝐸 ∈ ℝ) |
9 | 8 | adantr 484 |
. . . . 5
⊢ ((𝜑 ∧ 𝑖 ∈ (0...𝑁)) → 𝐸 ∈ ℝ) |
10 | | stoweidlem11.4 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑖 ∈ (0...𝑁)) → (𝑋‘𝑖):𝑇⟶ℝ) |
11 | 1 | adantr 484 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑖 ∈ (0...𝑁)) → 𝑡 ∈ 𝑇) |
12 | 10, 11 | ffvelrnd 6905 |
. . . . 5
⊢ ((𝜑 ∧ 𝑖 ∈ (0...𝑁)) → ((𝑋‘𝑖)‘𝑡) ∈ ℝ) |
13 | 9, 12 | remulcld 10863 |
. . . 4
⊢ ((𝜑 ∧ 𝑖 ∈ (0...𝑁)) → (𝐸 · ((𝑋‘𝑖)‘𝑡)) ∈ ℝ) |
14 | 6, 13 | fsumrecl 15298 |
. . 3
⊢ (𝜑 → Σ𝑖 ∈ (0...𝑁)(𝐸 · ((𝑋‘𝑖)‘𝑡)) ∈ ℝ) |
15 | | stoweidlem11.3 |
. . . . . . 7
⊢ (𝜑 → 𝑗 ∈ (1...𝑁)) |
16 | 15 | elfzelzd 13113 |
. . . . . 6
⊢ (𝜑 → 𝑗 ∈ ℤ) |
17 | 16 | zred 12282 |
. . . . 5
⊢ (𝜑 → 𝑗 ∈ ℝ) |
18 | 8, 17 | remulcld 10863 |
. . . 4
⊢ (𝜑 → (𝐸 · 𝑗) ∈ ℝ) |
19 | | stoweidlem11.1 |
. . . . . . . 8
⊢ (𝜑 → 𝑁 ∈ ℕ) |
20 | 19 | nnred 11845 |
. . . . . . 7
⊢ (𝜑 → 𝑁 ∈ ℝ) |
21 | 20, 17 | resubcld 11260 |
. . . . . 6
⊢ (𝜑 → (𝑁 − 𝑗) ∈ ℝ) |
22 | | 1red 10834 |
. . . . . 6
⊢ (𝜑 → 1 ∈
ℝ) |
23 | 21, 22 | readdcld 10862 |
. . . . 5
⊢ (𝜑 → ((𝑁 − 𝑗) + 1) ∈ ℝ) |
24 | 8, 19 | nndivred 11884 |
. . . . . 6
⊢ (𝜑 → (𝐸 / 𝑁) ∈ ℝ) |
25 | 8, 24 | remulcld 10863 |
. . . . 5
⊢ (𝜑 → (𝐸 · (𝐸 / 𝑁)) ∈ ℝ) |
26 | 23, 25 | remulcld 10863 |
. . . 4
⊢ (𝜑 → (((𝑁 − 𝑗) + 1) · (𝐸 · (𝐸 / 𝑁))) ∈ ℝ) |
27 | 18, 26 | readdcld 10862 |
. . 3
⊢ (𝜑 → ((𝐸 · 𝑗) + (((𝑁 − 𝑗) + 1) · (𝐸 · (𝐸 / 𝑁)))) ∈ ℝ) |
28 | | 3re 11910 |
. . . . . . 7
⊢ 3 ∈
ℝ |
29 | 28 | a1i 11 |
. . . . . 6
⊢ (𝜑 → 3 ∈
ℝ) |
30 | | 3ne0 11936 |
. . . . . . 7
⊢ 3 ≠
0 |
31 | 30 | a1i 11 |
. . . . . 6
⊢ (𝜑 → 3 ≠ 0) |
32 | 29, 31 | rereccld 11659 |
. . . . 5
⊢ (𝜑 → (1 / 3) ∈
ℝ) |
33 | 17, 32 | readdcld 10862 |
. . . 4
⊢ (𝜑 → (𝑗 + (1 / 3)) ∈ ℝ) |
34 | 33, 8 | remulcld 10863 |
. . 3
⊢ (𝜑 → ((𝑗 + (1 / 3)) · 𝐸) ∈ ℝ) |
35 | | fzfid 13546 |
. . . . . 6
⊢ (𝜑 → (0...(𝑗 − 1)) ∈ Fin) |
36 | 8 | adantr 484 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑖 ∈ (0...(𝑗 − 1))) → 𝐸 ∈ ℝ) |
37 | | elfzelz 13112 |
. . . . . . . . . . . 12
⊢ (𝑗 ∈ (1...𝑁) → 𝑗 ∈ ℤ) |
38 | | peano2zm 12220 |
. . . . . . . . . . . 12
⊢ (𝑗 ∈ ℤ → (𝑗 − 1) ∈
ℤ) |
39 | 15, 37, 38 | 3syl 18 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝑗 − 1) ∈ ℤ) |
40 | 19 | nnzd 12281 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝑁 ∈ ℤ) |
41 | 17, 22 | resubcld 11260 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝑗 − 1) ∈ ℝ) |
42 | 17 | lem1d 11765 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝑗 − 1) ≤ 𝑗) |
43 | | elfzuz3 13109 |
. . . . . . . . . . . . 13
⊢ (𝑗 ∈ (1...𝑁) → 𝑁 ∈ (ℤ≥‘𝑗)) |
44 | | eluzle 12451 |
. . . . . . . . . . . . 13
⊢ (𝑁 ∈
(ℤ≥‘𝑗) → 𝑗 ≤ 𝑁) |
45 | 15, 43, 44 | 3syl 18 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝑗 ≤ 𝑁) |
46 | 41, 17, 20, 42, 45 | letrd 10989 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝑗 − 1) ≤ 𝑁) |
47 | | eluz2 12444 |
. . . . . . . . . . 11
⊢ (𝑁 ∈
(ℤ≥‘(𝑗 − 1)) ↔ ((𝑗 − 1) ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ (𝑗 − 1) ≤ 𝑁)) |
48 | 39, 40, 46, 47 | syl3anbrc 1345 |
. . . . . . . . . 10
⊢ (𝜑 → 𝑁 ∈ (ℤ≥‘(𝑗 − 1))) |
49 | | fzss2 13152 |
. . . . . . . . . 10
⊢ (𝑁 ∈
(ℤ≥‘(𝑗 − 1)) → (0...(𝑗 − 1)) ⊆ (0...𝑁)) |
50 | 48, 49 | syl 17 |
. . . . . . . . 9
⊢ (𝜑 → (0...(𝑗 − 1)) ⊆ (0...𝑁)) |
51 | 50 | sselda 3901 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑖 ∈ (0...(𝑗 − 1))) → 𝑖 ∈ (0...𝑁)) |
52 | 51, 12 | syldan 594 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑖 ∈ (0...(𝑗 − 1))) → ((𝑋‘𝑖)‘𝑡) ∈ ℝ) |
53 | 36, 52 | remulcld 10863 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑖 ∈ (0...(𝑗 − 1))) → (𝐸 · ((𝑋‘𝑖)‘𝑡)) ∈ ℝ) |
54 | 35, 53 | fsumrecl 15298 |
. . . . 5
⊢ (𝜑 → Σ𝑖 ∈ (0...(𝑗 − 1))(𝐸 · ((𝑋‘𝑖)‘𝑡)) ∈ ℝ) |
55 | 54, 26 | readdcld 10862 |
. . . 4
⊢ (𝜑 → (Σ𝑖 ∈ (0...(𝑗 − 1))(𝐸 · ((𝑋‘𝑖)‘𝑡)) + (((𝑁 − 𝑗) + 1) · (𝐸 · (𝐸 / 𝑁)))) ∈ ℝ) |
56 | 17 | ltm1d 11764 |
. . . . . . 7
⊢ (𝜑 → (𝑗 − 1) < 𝑗) |
57 | | fzdisj 13139 |
. . . . . . 7
⊢ ((𝑗 − 1) < 𝑗 → ((0...(𝑗 − 1)) ∩ (𝑗...𝑁)) = ∅) |
58 | 56, 57 | syl 17 |
. . . . . 6
⊢ (𝜑 → ((0...(𝑗 − 1)) ∩ (𝑗...𝑁)) = ∅) |
59 | | fzssp1 13155 |
. . . . . . . . . 10
⊢
(0...(𝑁 − 1))
⊆ (0...((𝑁 − 1)
+ 1)) |
60 | 19 | nncnd 11846 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝑁 ∈ ℂ) |
61 | | 1cnd 10828 |
. . . . . . . . . . . 12
⊢ (𝜑 → 1 ∈
ℂ) |
62 | 60, 61 | npcand 11193 |
. . . . . . . . . . 11
⊢ (𝜑 → ((𝑁 − 1) + 1) = 𝑁) |
63 | 62 | oveq2d 7229 |
. . . . . . . . . 10
⊢ (𝜑 → (0...((𝑁 − 1) + 1)) = (0...𝑁)) |
64 | 59, 63 | sseqtrid 3953 |
. . . . . . . . 9
⊢ (𝜑 → (0...(𝑁 − 1)) ⊆ (0...𝑁)) |
65 | | 1zzd 12208 |
. . . . . . . . . . . 12
⊢ (𝜑 → 1 ∈
ℤ) |
66 | | fzsubel 13148 |
. . . . . . . . . . . 12
⊢ (((1
∈ ℤ ∧ 𝑁
∈ ℤ) ∧ (𝑗
∈ ℤ ∧ 1 ∈ ℤ)) → (𝑗 ∈ (1...𝑁) ↔ (𝑗 − 1) ∈ ((1 − 1)...(𝑁 − 1)))) |
67 | 65, 40, 16, 65, 66 | syl22anc 839 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝑗 ∈ (1...𝑁) ↔ (𝑗 − 1) ∈ ((1 − 1)...(𝑁 − 1)))) |
68 | 15, 67 | mpbid 235 |
. . . . . . . . . 10
⊢ (𝜑 → (𝑗 − 1) ∈ ((1 − 1)...(𝑁 − 1))) |
69 | | 1m1e0 11902 |
. . . . . . . . . . 11
⊢ (1
− 1) = 0 |
70 | 69 | oveq1i 7223 |
. . . . . . . . . 10
⊢ ((1
− 1)...(𝑁 − 1))
= (0...(𝑁 −
1)) |
71 | 68, 70 | eleqtrdi 2848 |
. . . . . . . . 9
⊢ (𝜑 → (𝑗 − 1) ∈ (0...(𝑁 − 1))) |
72 | 64, 71 | sseldd 3902 |
. . . . . . . 8
⊢ (𝜑 → (𝑗 − 1) ∈ (0...𝑁)) |
73 | | fzsplit 13138 |
. . . . . . . 8
⊢ ((𝑗 − 1) ∈ (0...𝑁) → (0...𝑁) = ((0...(𝑗 − 1)) ∪ (((𝑗 − 1) + 1)...𝑁))) |
74 | 72, 73 | syl 17 |
. . . . . . 7
⊢ (𝜑 → (0...𝑁) = ((0...(𝑗 − 1)) ∪ (((𝑗 − 1) + 1)...𝑁))) |
75 | 16 | zcnd 12283 |
. . . . . . . . . 10
⊢ (𝜑 → 𝑗 ∈ ℂ) |
76 | 75, 61 | npcand 11193 |
. . . . . . . . 9
⊢ (𝜑 → ((𝑗 − 1) + 1) = 𝑗) |
77 | 76 | oveq1d 7228 |
. . . . . . . 8
⊢ (𝜑 → (((𝑗 − 1) + 1)...𝑁) = (𝑗...𝑁)) |
78 | 77 | uneq2d 4077 |
. . . . . . 7
⊢ (𝜑 → ((0...(𝑗 − 1)) ∪ (((𝑗 − 1) + 1)...𝑁)) = ((0...(𝑗 − 1)) ∪ (𝑗...𝑁))) |
79 | 74, 78 | eqtrd 2777 |
. . . . . 6
⊢ (𝜑 → (0...𝑁) = ((0...(𝑗 − 1)) ∪ (𝑗...𝑁))) |
80 | 7 | rpcnd 12630 |
. . . . . . . 8
⊢ (𝜑 → 𝐸 ∈ ℂ) |
81 | 80 | adantr 484 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑖 ∈ (0...𝑁)) → 𝐸 ∈ ℂ) |
82 | 12 | recnd 10861 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑖 ∈ (0...𝑁)) → ((𝑋‘𝑖)‘𝑡) ∈ ℂ) |
83 | 81, 82 | mulcld 10853 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑖 ∈ (0...𝑁)) → (𝐸 · ((𝑋‘𝑖)‘𝑡)) ∈ ℂ) |
84 | 58, 79, 6, 83 | fsumsplit 15305 |
. . . . 5
⊢ (𝜑 → Σ𝑖 ∈ (0...𝑁)(𝐸 · ((𝑋‘𝑖)‘𝑡)) = (Σ𝑖 ∈ (0...(𝑗 − 1))(𝐸 · ((𝑋‘𝑖)‘𝑡)) + Σ𝑖 ∈ (𝑗...𝑁)(𝐸 · ((𝑋‘𝑖)‘𝑡)))) |
85 | | fzfid 13546 |
. . . . . . 7
⊢ (𝜑 → (𝑗...𝑁) ∈ Fin) |
86 | 8 | adantr 484 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑖 ∈ (𝑗...𝑁)) → 𝐸 ∈ ℝ) |
87 | | 0zd 12188 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 0 ∈
ℤ) |
88 | | 0red 10836 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → 0 ∈
ℝ) |
89 | | 0le1 11355 |
. . . . . . . . . . . . . . 15
⊢ 0 ≤
1 |
90 | 89 | a1i 11 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → 0 ≤ 1) |
91 | | elfzuz 13108 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑗 ∈ (1...𝑁) → 𝑗 ∈
(ℤ≥‘1)) |
92 | 15, 91 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → 𝑗 ∈
(ℤ≥‘1)) |
93 | | eluz2 12444 |
. . . . . . . . . . . . . . . 16
⊢ (𝑗 ∈
(ℤ≥‘1) ↔ (1 ∈ ℤ ∧ 𝑗 ∈ ℤ ∧ 1 ≤
𝑗)) |
94 | 92, 93 | sylib 221 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (1 ∈ ℤ ∧
𝑗 ∈ ℤ ∧ 1
≤ 𝑗)) |
95 | 94 | simp3d 1146 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → 1 ≤ 𝑗) |
96 | 88, 22, 17, 90, 95 | letrd 10989 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 0 ≤ 𝑗) |
97 | | eluz2 12444 |
. . . . . . . . . . . . 13
⊢ (𝑗 ∈
(ℤ≥‘0) ↔ (0 ∈ ℤ ∧ 𝑗 ∈ ℤ ∧ 0 ≤
𝑗)) |
98 | 87, 16, 96, 97 | syl3anbrc 1345 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝑗 ∈
(ℤ≥‘0)) |
99 | | fzss1 13151 |
. . . . . . . . . . . 12
⊢ (𝑗 ∈
(ℤ≥‘0) → (𝑗...𝑁) ⊆ (0...𝑁)) |
100 | 98, 99 | syl 17 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝑗...𝑁) ⊆ (0...𝑁)) |
101 | 100 | sselda 3901 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑖 ∈ (𝑗...𝑁)) → 𝑖 ∈ (0...𝑁)) |
102 | 101, 10 | syldan 594 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑖 ∈ (𝑗...𝑁)) → (𝑋‘𝑖):𝑇⟶ℝ) |
103 | 1 | adantr 484 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑖 ∈ (𝑗...𝑁)) → 𝑡 ∈ 𝑇) |
104 | 102, 103 | ffvelrnd 6905 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑖 ∈ (𝑗...𝑁)) → ((𝑋‘𝑖)‘𝑡) ∈ ℝ) |
105 | 86, 104 | remulcld 10863 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑖 ∈ (𝑗...𝑁)) → (𝐸 · ((𝑋‘𝑖)‘𝑡)) ∈ ℝ) |
106 | 85, 105 | fsumrecl 15298 |
. . . . . 6
⊢ (𝜑 → Σ𝑖 ∈ (𝑗...𝑁)(𝐸 · ((𝑋‘𝑖)‘𝑡)) ∈ ℝ) |
107 | | eluzfz2 13120 |
. . . . . . . . 9
⊢ (𝑁 ∈
(ℤ≥‘𝑗) → 𝑁 ∈ (𝑗...𝑁)) |
108 | | ne0i 4249 |
. . . . . . . . 9
⊢ (𝑁 ∈ (𝑗...𝑁) → (𝑗...𝑁) ≠ ∅) |
109 | 15, 43, 107, 108 | 4syl 19 |
. . . . . . . 8
⊢ (𝜑 → (𝑗...𝑁) ≠ ∅) |
110 | 19 | adantr 484 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑖 ∈ (𝑗...𝑁)) → 𝑁 ∈ ℕ) |
111 | 86, 110 | nndivred 11884 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑖 ∈ (𝑗...𝑁)) → (𝐸 / 𝑁) ∈ ℝ) |
112 | 86, 111 | remulcld 10863 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑖 ∈ (𝑗...𝑁)) → (𝐸 · (𝐸 / 𝑁)) ∈ ℝ) |
113 | | stoweidlem11.6 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑖 ∈ (𝑗...𝑁)) → ((𝑋‘𝑖)‘𝑡) < (𝐸 / 𝑁)) |
114 | 7 | rpgt0d 12631 |
. . . . . . . . . . 11
⊢ (𝜑 → 0 < 𝐸) |
115 | 114 | adantr 484 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑖 ∈ (𝑗...𝑁)) → 0 < 𝐸) |
116 | | ltmul2 11683 |
. . . . . . . . . 10
⊢ ((((𝑋‘𝑖)‘𝑡) ∈ ℝ ∧ (𝐸 / 𝑁) ∈ ℝ ∧ (𝐸 ∈ ℝ ∧ 0 < 𝐸)) → (((𝑋‘𝑖)‘𝑡) < (𝐸 / 𝑁) ↔ (𝐸 · ((𝑋‘𝑖)‘𝑡)) < (𝐸 · (𝐸 / 𝑁)))) |
117 | 104, 111,
86, 115, 116 | syl112anc 1376 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑖 ∈ (𝑗...𝑁)) → (((𝑋‘𝑖)‘𝑡) < (𝐸 / 𝑁) ↔ (𝐸 · ((𝑋‘𝑖)‘𝑡)) < (𝐸 · (𝐸 / 𝑁)))) |
118 | 113, 117 | mpbid 235 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑖 ∈ (𝑗...𝑁)) → (𝐸 · ((𝑋‘𝑖)‘𝑡)) < (𝐸 · (𝐸 / 𝑁))) |
119 | 85, 109, 105, 112, 118 | fsumlt 15364 |
. . . . . . 7
⊢ (𝜑 → Σ𝑖 ∈ (𝑗...𝑁)(𝐸 · ((𝑋‘𝑖)‘𝑡)) < Σ𝑖 ∈ (𝑗...𝑁)(𝐸 · (𝐸 / 𝑁))) |
120 | 19 | nnne0d 11880 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝑁 ≠ 0) |
121 | 80, 60, 120 | divcld 11608 |
. . . . . . . . . 10
⊢ (𝜑 → (𝐸 / 𝑁) ∈ ℂ) |
122 | 80, 121 | mulcld 10853 |
. . . . . . . . 9
⊢ (𝜑 → (𝐸 · (𝐸 / 𝑁)) ∈ ℂ) |
123 | | fsumconst 15354 |
. . . . . . . . 9
⊢ (((𝑗...𝑁) ∈ Fin ∧ (𝐸 · (𝐸 / 𝑁)) ∈ ℂ) → Σ𝑖 ∈ (𝑗...𝑁)(𝐸 · (𝐸 / 𝑁)) = ((♯‘(𝑗...𝑁)) · (𝐸 · (𝐸 / 𝑁)))) |
124 | 85, 122, 123 | syl2anc 587 |
. . . . . . . 8
⊢ (𝜑 → Σ𝑖 ∈ (𝑗...𝑁)(𝐸 · (𝐸 / 𝑁)) = ((♯‘(𝑗...𝑁)) · (𝐸 · (𝐸 / 𝑁)))) |
125 | | hashfz 13994 |
. . . . . . . . . 10
⊢ (𝑁 ∈
(ℤ≥‘𝑗) → (♯‘(𝑗...𝑁)) = ((𝑁 − 𝑗) + 1)) |
126 | 15, 43, 125 | 3syl 18 |
. . . . . . . . 9
⊢ (𝜑 → (♯‘(𝑗...𝑁)) = ((𝑁 − 𝑗) + 1)) |
127 | 126 | oveq1d 7228 |
. . . . . . . 8
⊢ (𝜑 → ((♯‘(𝑗...𝑁)) · (𝐸 · (𝐸 / 𝑁))) = (((𝑁 − 𝑗) + 1) · (𝐸 · (𝐸 / 𝑁)))) |
128 | 124, 127 | eqtrd 2777 |
. . . . . . 7
⊢ (𝜑 → Σ𝑖 ∈ (𝑗...𝑁)(𝐸 · (𝐸 / 𝑁)) = (((𝑁 − 𝑗) + 1) · (𝐸 · (𝐸 / 𝑁)))) |
129 | 119, 128 | breqtrd 5079 |
. . . . . 6
⊢ (𝜑 → Σ𝑖 ∈ (𝑗...𝑁)(𝐸 · ((𝑋‘𝑖)‘𝑡)) < (((𝑁 − 𝑗) + 1) · (𝐸 · (𝐸 / 𝑁)))) |
130 | 106, 26, 54, 129 | ltadd2dd 10991 |
. . . . 5
⊢ (𝜑 → (Σ𝑖 ∈ (0...(𝑗 − 1))(𝐸 · ((𝑋‘𝑖)‘𝑡)) + Σ𝑖 ∈ (𝑗...𝑁)(𝐸 · ((𝑋‘𝑖)‘𝑡))) < (Σ𝑖 ∈ (0...(𝑗 − 1))(𝐸 · ((𝑋‘𝑖)‘𝑡)) + (((𝑁 − 𝑗) + 1) · (𝐸 · (𝐸 / 𝑁))))) |
131 | 84, 130 | eqbrtrd 5075 |
. . . 4
⊢ (𝜑 → Σ𝑖 ∈ (0...𝑁)(𝐸 · ((𝑋‘𝑖)‘𝑡)) < (Σ𝑖 ∈ (0...(𝑗 − 1))(𝐸 · ((𝑋‘𝑖)‘𝑡)) + (((𝑁 − 𝑗) + 1) · (𝐸 · (𝐸 / 𝑁))))) |
132 | | stoweidlem11.5 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑖 ∈ (0...𝑁)) → ((𝑋‘𝑖)‘𝑡) ≤ 1) |
133 | 51, 132 | syldan 594 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑖 ∈ (0...(𝑗 − 1))) → ((𝑋‘𝑖)‘𝑡) ≤ 1) |
134 | | 1red 10834 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑖 ∈ (0...(𝑗 − 1))) → 1 ∈
ℝ) |
135 | 114 | adantr 484 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑖 ∈ (0...(𝑗 − 1))) → 0 < 𝐸) |
136 | | lemul2 11685 |
. . . . . . . . . 10
⊢ ((((𝑋‘𝑖)‘𝑡) ∈ ℝ ∧ 1 ∈ ℝ ∧
(𝐸 ∈ ℝ ∧ 0
< 𝐸)) → (((𝑋‘𝑖)‘𝑡) ≤ 1 ↔ (𝐸 · ((𝑋‘𝑖)‘𝑡)) ≤ (𝐸 · 1))) |
137 | 52, 134, 36, 135, 136 | syl112anc 1376 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑖 ∈ (0...(𝑗 − 1))) → (((𝑋‘𝑖)‘𝑡) ≤ 1 ↔ (𝐸 · ((𝑋‘𝑖)‘𝑡)) ≤ (𝐸 · 1))) |
138 | 133, 137 | mpbid 235 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑖 ∈ (0...(𝑗 − 1))) → (𝐸 · ((𝑋‘𝑖)‘𝑡)) ≤ (𝐸 · 1)) |
139 | 80 | mulid1d 10850 |
. . . . . . . . 9
⊢ (𝜑 → (𝐸 · 1) = 𝐸) |
140 | 139 | adantr 484 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑖 ∈ (0...(𝑗 − 1))) → (𝐸 · 1) = 𝐸) |
141 | 138, 140 | breqtrd 5079 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑖 ∈ (0...(𝑗 − 1))) → (𝐸 · ((𝑋‘𝑖)‘𝑡)) ≤ 𝐸) |
142 | 35, 53, 36, 141 | fsumle 15363 |
. . . . . 6
⊢ (𝜑 → Σ𝑖 ∈ (0...(𝑗 − 1))(𝐸 · ((𝑋‘𝑖)‘𝑡)) ≤ Σ𝑖 ∈ (0...(𝑗 − 1))𝐸) |
143 | | fsumconst 15354 |
. . . . . . . 8
⊢
(((0...(𝑗 −
1)) ∈ Fin ∧ 𝐸
∈ ℂ) → Σ𝑖 ∈ (0...(𝑗 − 1))𝐸 = ((♯‘(0...(𝑗 − 1))) · 𝐸)) |
144 | 35, 80, 143 | syl2anc 587 |
. . . . . . 7
⊢ (𝜑 → Σ𝑖 ∈ (0...(𝑗 − 1))𝐸 = ((♯‘(0...(𝑗 − 1))) · 𝐸)) |
145 | | 0z 12187 |
. . . . . . . . . . 11
⊢ 0 ∈
ℤ |
146 | | 1e0p1 12335 |
. . . . . . . . . . . . 13
⊢ 1 = (0 +
1) |
147 | 146 | fveq2i 6720 |
. . . . . . . . . . . 12
⊢
(ℤ≥‘1) = (ℤ≥‘(0 +
1)) |
148 | 92, 147 | eleqtrdi 2848 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝑗 ∈ (ℤ≥‘(0 +
1))) |
149 | | eluzp1m1 12464 |
. . . . . . . . . . 11
⊢ ((0
∈ ℤ ∧ 𝑗
∈ (ℤ≥‘(0 + 1))) → (𝑗 − 1) ∈
(ℤ≥‘0)) |
150 | 145, 148,
149 | sylancr 590 |
. . . . . . . . . 10
⊢ (𝜑 → (𝑗 − 1) ∈
(ℤ≥‘0)) |
151 | | hashfz 13994 |
. . . . . . . . . 10
⊢ ((𝑗 − 1) ∈
(ℤ≥‘0) → (♯‘(0...(𝑗 − 1))) = (((𝑗 − 1) − 0) + 1)) |
152 | 150, 151 | syl 17 |
. . . . . . . . 9
⊢ (𝜑 → (♯‘(0...(𝑗 − 1))) = (((𝑗 − 1) − 0) +
1)) |
153 | 75, 61 | subcld 11189 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝑗 − 1) ∈ ℂ) |
154 | 153 | subid1d 11178 |
. . . . . . . . . 10
⊢ (𝜑 → ((𝑗 − 1) − 0) = (𝑗 − 1)) |
155 | 154 | oveq1d 7228 |
. . . . . . . . 9
⊢ (𝜑 → (((𝑗 − 1) − 0) + 1) = ((𝑗 − 1) +
1)) |
156 | 152, 155,
76 | 3eqtrd 2781 |
. . . . . . . 8
⊢ (𝜑 → (♯‘(0...(𝑗 − 1))) = 𝑗) |
157 | 156 | oveq1d 7228 |
. . . . . . 7
⊢ (𝜑 →
((♯‘(0...(𝑗
− 1))) · 𝐸) =
(𝑗 · 𝐸)) |
158 | 75, 80 | mulcomd 10854 |
. . . . . . 7
⊢ (𝜑 → (𝑗 · 𝐸) = (𝐸 · 𝑗)) |
159 | 144, 157,
158 | 3eqtrd 2781 |
. . . . . 6
⊢ (𝜑 → Σ𝑖 ∈ (0...(𝑗 − 1))𝐸 = (𝐸 · 𝑗)) |
160 | 142, 159 | breqtrd 5079 |
. . . . 5
⊢ (𝜑 → Σ𝑖 ∈ (0...(𝑗 − 1))(𝐸 · ((𝑋‘𝑖)‘𝑡)) ≤ (𝐸 · 𝑗)) |
161 | 54, 18, 26, 160 | leadd1dd 11446 |
. . . 4
⊢ (𝜑 → (Σ𝑖 ∈ (0...(𝑗 − 1))(𝐸 · ((𝑋‘𝑖)‘𝑡)) + (((𝑁 − 𝑗) + 1) · (𝐸 · (𝐸 / 𝑁)))) ≤ ((𝐸 · 𝑗) + (((𝑁 − 𝑗) + 1) · (𝐸 · (𝐸 / 𝑁))))) |
162 | 14, 55, 27, 131, 161 | ltletrd 10992 |
. . 3
⊢ (𝜑 → Σ𝑖 ∈ (0...𝑁)(𝐸 · ((𝑋‘𝑖)‘𝑡)) < ((𝐸 · 𝑗) + (((𝑁 − 𝑗) + 1) · (𝐸 · (𝐸 / 𝑁))))) |
163 | 8, 8 | remulcld 10863 |
. . . . 5
⊢ (𝜑 → (𝐸 · 𝐸) ∈ ℝ) |
164 | 18, 163 | readdcld 10862 |
. . . 4
⊢ (𝜑 → ((𝐸 · 𝑗) + (𝐸 · 𝐸)) ∈ ℝ) |
165 | 60, 75 | subcld 11189 |
. . . . . . . 8
⊢ (𝜑 → (𝑁 − 𝑗) ∈ ℂ) |
166 | 165, 61 | addcld 10852 |
. . . . . . 7
⊢ (𝜑 → ((𝑁 − 𝑗) + 1) ∈ ℂ) |
167 | 80, 166, 121 | mul12d 11041 |
. . . . . 6
⊢ (𝜑 → (𝐸 · (((𝑁 − 𝑗) + 1) · (𝐸 / 𝑁))) = (((𝑁 − 𝑗) + 1) · (𝐸 · (𝐸 / 𝑁)))) |
168 | 167 | oveq2d 7229 |
. . . . 5
⊢ (𝜑 → ((𝐸 · 𝑗) + (𝐸 · (((𝑁 − 𝑗) + 1) · (𝐸 / 𝑁)))) = ((𝐸 · 𝑗) + (((𝑁 − 𝑗) + 1) · (𝐸 · (𝐸 / 𝑁))))) |
169 | 23, 24 | remulcld 10863 |
. . . . . . 7
⊢ (𝜑 → (((𝑁 − 𝑗) + 1) · (𝐸 / 𝑁)) ∈ ℝ) |
170 | 8, 169 | remulcld 10863 |
. . . . . 6
⊢ (𝜑 → (𝐸 · (((𝑁 − 𝑗) + 1) · (𝐸 / 𝑁))) ∈ ℝ) |
171 | 166, 80, 60, 120 | div12d 11644 |
. . . . . . . 8
⊢ (𝜑 → (((𝑁 − 𝑗) + 1) · (𝐸 / 𝑁)) = (𝐸 · (((𝑁 − 𝑗) + 1) / 𝑁))) |
172 | 22, 17 | resubcld 11260 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (1 − 𝑗) ∈
ℝ) |
173 | | elfzle1 13115 |
. . . . . . . . . . . . . . . 16
⊢ (𝑗 ∈ (1...𝑁) → 1 ≤ 𝑗) |
174 | 15, 173 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → 1 ≤ 𝑗) |
175 | 22, 17 | suble0d 11423 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → ((1 − 𝑗) ≤ 0 ↔ 1 ≤ 𝑗)) |
176 | 174, 175 | mpbird 260 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (1 − 𝑗) ≤ 0) |
177 | 172, 88, 20, 176 | leadd2dd 11447 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (𝑁 + (1 − 𝑗)) ≤ (𝑁 + 0)) |
178 | 60, 61, 75 | addsub12d 11212 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (𝑁 + (1 − 𝑗)) = (1 + (𝑁 − 𝑗))) |
179 | 61, 165 | addcomd 11034 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (1 + (𝑁 − 𝑗)) = ((𝑁 − 𝑗) + 1)) |
180 | 178, 179 | eqtrd 2777 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (𝑁 + (1 − 𝑗)) = ((𝑁 − 𝑗) + 1)) |
181 | 60 | addid1d 11032 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (𝑁 + 0) = 𝑁) |
182 | 177, 180,
181 | 3brtr3d 5084 |
. . . . . . . . . . . 12
⊢ (𝜑 → ((𝑁 − 𝑗) + 1) ≤ 𝑁) |
183 | 19 | nngt0d 11879 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 0 < 𝑁) |
184 | | lediv1 11697 |
. . . . . . . . . . . . 13
⊢ ((((𝑁 − 𝑗) + 1) ∈ ℝ ∧ 𝑁 ∈ ℝ ∧ (𝑁 ∈ ℝ ∧ 0 < 𝑁)) → (((𝑁 − 𝑗) + 1) ≤ 𝑁 ↔ (((𝑁 − 𝑗) + 1) / 𝑁) ≤ (𝑁 / 𝑁))) |
185 | 23, 20, 20, 183, 184 | syl112anc 1376 |
. . . . . . . . . . . 12
⊢ (𝜑 → (((𝑁 − 𝑗) + 1) ≤ 𝑁 ↔ (((𝑁 − 𝑗) + 1) / 𝑁) ≤ (𝑁 / 𝑁))) |
186 | 182, 185 | mpbid 235 |
. . . . . . . . . . 11
⊢ (𝜑 → (((𝑁 − 𝑗) + 1) / 𝑁) ≤ (𝑁 / 𝑁)) |
187 | 60, 120 | dividd 11606 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝑁 / 𝑁) = 1) |
188 | 186, 187 | breqtrd 5079 |
. . . . . . . . . 10
⊢ (𝜑 → (((𝑁 − 𝑗) + 1) / 𝑁) ≤ 1) |
189 | 23, 19 | nndivred 11884 |
. . . . . . . . . . 11
⊢ (𝜑 → (((𝑁 − 𝑗) + 1) / 𝑁) ∈ ℝ) |
190 | 189, 22, 7 | lemul2d 12672 |
. . . . . . . . . 10
⊢ (𝜑 → ((((𝑁 − 𝑗) + 1) / 𝑁) ≤ 1 ↔ (𝐸 · (((𝑁 − 𝑗) + 1) / 𝑁)) ≤ (𝐸 · 1))) |
191 | 188, 190 | mpbid 235 |
. . . . . . . . 9
⊢ (𝜑 → (𝐸 · (((𝑁 − 𝑗) + 1) / 𝑁)) ≤ (𝐸 · 1)) |
192 | 191, 139 | breqtrd 5079 |
. . . . . . . 8
⊢ (𝜑 → (𝐸 · (((𝑁 − 𝑗) + 1) / 𝑁)) ≤ 𝐸) |
193 | 171, 192 | eqbrtrd 5075 |
. . . . . . 7
⊢ (𝜑 → (((𝑁 − 𝑗) + 1) · (𝐸 / 𝑁)) ≤ 𝐸) |
194 | 169, 8, 7 | lemul2d 12672 |
. . . . . . 7
⊢ (𝜑 → ((((𝑁 − 𝑗) + 1) · (𝐸 / 𝑁)) ≤ 𝐸 ↔ (𝐸 · (((𝑁 − 𝑗) + 1) · (𝐸 / 𝑁))) ≤ (𝐸 · 𝐸))) |
195 | 193, 194 | mpbid 235 |
. . . . . 6
⊢ (𝜑 → (𝐸 · (((𝑁 − 𝑗) + 1) · (𝐸 / 𝑁))) ≤ (𝐸 · 𝐸)) |
196 | 170, 163,
18, 195 | leadd2dd 11447 |
. . . . 5
⊢ (𝜑 → ((𝐸 · 𝑗) + (𝐸 · (((𝑁 − 𝑗) + 1) · (𝐸 / 𝑁)))) ≤ ((𝐸 · 𝑗) + (𝐸 · 𝐸))) |
197 | 168, 196 | eqbrtrrd 5077 |
. . . 4
⊢ (𝜑 → ((𝐸 · 𝑗) + (((𝑁 − 𝑗) + 1) · (𝐸 · (𝐸 / 𝑁)))) ≤ ((𝐸 · 𝑗) + (𝐸 · 𝐸))) |
198 | 80, 75 | mulcomd 10854 |
. . . . . . 7
⊢ (𝜑 → (𝐸 · 𝑗) = (𝑗 · 𝐸)) |
199 | 198 | oveq1d 7228 |
. . . . . 6
⊢ (𝜑 → ((𝐸 · 𝑗) + (𝐸 · 𝐸)) = ((𝑗 · 𝐸) + (𝐸 · 𝐸))) |
200 | 75, 80, 80 | adddird 10858 |
. . . . . 6
⊢ (𝜑 → ((𝑗 + 𝐸) · 𝐸) = ((𝑗 · 𝐸) + (𝐸 · 𝐸))) |
201 | 199, 200 | eqtr4d 2780 |
. . . . 5
⊢ (𝜑 → ((𝐸 · 𝑗) + (𝐸 · 𝐸)) = ((𝑗 + 𝐸) · 𝐸)) |
202 | 17, 8 | readdcld 10862 |
. . . . . 6
⊢ (𝜑 → (𝑗 + 𝐸) ∈ ℝ) |
203 | | stoweidlem11.8 |
. . . . . . 7
⊢ (𝜑 → 𝐸 < (1 / 3)) |
204 | 8, 32, 17, 203 | ltadd2dd 10991 |
. . . . . 6
⊢ (𝜑 → (𝑗 + 𝐸) < (𝑗 + (1 / 3))) |
205 | 202, 33, 7, 204 | ltmul1dd 12683 |
. . . . 5
⊢ (𝜑 → ((𝑗 + 𝐸) · 𝐸) < ((𝑗 + (1 / 3)) · 𝐸)) |
206 | 201, 205 | eqbrtrd 5075 |
. . . 4
⊢ (𝜑 → ((𝐸 · 𝑗) + (𝐸 · 𝐸)) < ((𝑗 + (1 / 3)) · 𝐸)) |
207 | 27, 164, 34, 197, 206 | lelttrd 10990 |
. . 3
⊢ (𝜑 → ((𝐸 · 𝑗) + (((𝑁 − 𝑗) + 1) · (𝐸 · (𝐸 / 𝑁)))) < ((𝑗 + (1 / 3)) · 𝐸)) |
208 | 14, 27, 34, 162, 207 | lttrd 10993 |
. 2
⊢ (𝜑 → Σ𝑖 ∈ (0...𝑁)(𝐸 · ((𝑋‘𝑖)‘𝑡)) < ((𝑗 + (1 / 3)) · 𝐸)) |
209 | 5, 208 | eqbrtrd 5075 |
1
⊢ (𝜑 → ((𝑡 ∈ 𝑇 ↦ Σ𝑖 ∈ (0...𝑁)(𝐸 · ((𝑋‘𝑖)‘𝑡)))‘𝑡) < ((𝑗 + (1 / 3)) · 𝐸)) |