Proof of Theorem knoppndvlem6
Step | Hyp | Ref
| Expression |
1 | | knoppndvlem6.w |
. . . . 5
⊢ 𝑊 = (𝑤 ∈ ℝ ↦ Σ𝑖 ∈ ℕ0
((𝐹‘𝑤)‘𝑖)) |
2 | 1 | a1i 11 |
. . . 4
⊢ (𝜑 → 𝑊 = (𝑤 ∈ ℝ ↦ Σ𝑖 ∈ ℕ0
((𝐹‘𝑤)‘𝑖))) |
3 | | fveq2 6103 |
. . . . . . 7
⊢ (𝑤 = 𝐴 → (𝐹‘𝑤) = (𝐹‘𝐴)) |
4 | 3 | fveq1d 6105 |
. . . . . 6
⊢ (𝑤 = 𝐴 → ((𝐹‘𝑤)‘𝑖) = ((𝐹‘𝐴)‘𝑖)) |
5 | 4 | sumeq2sdv 14282 |
. . . . 5
⊢ (𝑤 = 𝐴 → Σ𝑖 ∈ ℕ0 ((𝐹‘𝑤)‘𝑖) = Σ𝑖 ∈ ℕ0 ((𝐹‘𝐴)‘𝑖)) |
6 | 5 | adantl 481 |
. . . 4
⊢ ((𝜑 ∧ 𝑤 = 𝐴) → Σ𝑖 ∈ ℕ0 ((𝐹‘𝑤)‘𝑖) = Σ𝑖 ∈ ℕ0 ((𝐹‘𝐴)‘𝑖)) |
7 | | knoppndvlem6.a |
. . . . . 6
⊢ 𝐴 = ((((2 · 𝑁)↑-𝐽) / 2) · 𝑀) |
8 | 7 | a1i 11 |
. . . . 5
⊢ (𝜑 → 𝐴 = ((((2 · 𝑁)↑-𝐽) / 2) · 𝑀)) |
9 | | knoppndvlem6.n |
. . . . . 6
⊢ (𝜑 → 𝑁 ∈ ℕ) |
10 | | knoppndvlem6.j |
. . . . . . 7
⊢ (𝜑 → 𝐽 ∈
ℕ0) |
11 | 10 | nn0zd 11356 |
. . . . . 6
⊢ (𝜑 → 𝐽 ∈ ℤ) |
12 | | knoppndvlem6.m |
. . . . . 6
⊢ (𝜑 → 𝑀 ∈ ℤ) |
13 | 9, 11, 12 | knoppndvlem1 31673 |
. . . . 5
⊢ (𝜑 → ((((2 · 𝑁)↑-𝐽) / 2) · 𝑀) ∈ ℝ) |
14 | 8, 13 | eqeltrd 2688 |
. . . 4
⊢ (𝜑 → 𝐴 ∈ ℝ) |
15 | | sumex 14266 |
. . . . 5
⊢
Σ𝑖 ∈
ℕ0 ((𝐹‘𝐴)‘𝑖) ∈ V |
16 | 15 | a1i 11 |
. . . 4
⊢ (𝜑 → Σ𝑖 ∈ ℕ0 ((𝐹‘𝐴)‘𝑖) ∈ V) |
17 | 2, 6, 14, 16 | fvmptd 6197 |
. . 3
⊢ (𝜑 → (𝑊‘𝐴) = Σ𝑖 ∈ ℕ0 ((𝐹‘𝐴)‘𝑖)) |
18 | | nn0uz 11598 |
. . . 4
⊢
ℕ0 = (ℤ≥‘0) |
19 | | eqid 2610 |
. . . 4
⊢
(ℤ≥‘(𝐽 + 1)) =
(ℤ≥‘(𝐽 + 1)) |
20 | | peano2nn0 11210 |
. . . . 5
⊢ (𝐽 ∈ ℕ0
→ (𝐽 + 1) ∈
ℕ0) |
21 | 10, 20 | syl 17 |
. . . 4
⊢ (𝜑 → (𝐽 + 1) ∈
ℕ0) |
22 | | eqidd 2611 |
. . . 4
⊢ ((𝜑 ∧ 𝑖 ∈ ℕ0) → ((𝐹‘𝐴)‘𝑖) = ((𝐹‘𝐴)‘𝑖)) |
23 | | knoppndvlem6.t |
. . . . . 6
⊢ 𝑇 = (𝑥 ∈ ℝ ↦
(abs‘((⌊‘(𝑥 + (1 / 2))) − 𝑥))) |
24 | | knoppndvlem6.f |
. . . . . 6
⊢ 𝐹 = (𝑦 ∈ ℝ ↦ (𝑛 ∈ ℕ0 ↦ ((𝐶↑𝑛) · (𝑇‘(((2 · 𝑁)↑𝑛) · 𝑦))))) |
25 | 9 | adantr 480 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑖 ∈ ℕ0) → 𝑁 ∈
ℕ) |
26 | | knoppndvlem6.c |
. . . . . . . . 9
⊢ (𝜑 → 𝐶 ∈ (-1(,)1)) |
27 | 26 | knoppndvlem3 31675 |
. . . . . . . 8
⊢ (𝜑 → (𝐶 ∈ ℝ ∧ (abs‘𝐶) < 1)) |
28 | 27 | simpld 474 |
. . . . . . 7
⊢ (𝜑 → 𝐶 ∈ ℝ) |
29 | 28 | adantr 480 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑖 ∈ ℕ0) → 𝐶 ∈
ℝ) |
30 | 14 | adantr 480 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑖 ∈ ℕ0) → 𝐴 ∈
ℝ) |
31 | | simpr 476 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑖 ∈ ℕ0) → 𝑖 ∈
ℕ0) |
32 | 23, 24, 25, 29, 30, 31 | knoppcnlem3 31655 |
. . . . 5
⊢ ((𝜑 ∧ 𝑖 ∈ ℕ0) → ((𝐹‘𝐴)‘𝑖) ∈ ℝ) |
33 | 32 | recnd 9947 |
. . . 4
⊢ ((𝜑 ∧ 𝑖 ∈ ℕ0) → ((𝐹‘𝐴)‘𝑖) ∈ ℂ) |
34 | 23, 24, 1, 14, 26, 9 | knoppndvlem4 31676 |
. . . . 5
⊢ (𝜑 → seq0( + , (𝐹‘𝐴)) ⇝ (𝑊‘𝐴)) |
35 | | seqex 12665 |
. . . . . 6
⊢ seq0( + ,
(𝐹‘𝐴)) ∈ V |
36 | | fvex 6113 |
. . . . . 6
⊢ (𝑊‘𝐴) ∈ V |
37 | 35, 36 | breldm 5251 |
. . . . 5
⊢ (seq0( +
, (𝐹‘𝐴)) ⇝ (𝑊‘𝐴) → seq0( + , (𝐹‘𝐴)) ∈ dom ⇝ ) |
38 | 34, 37 | syl 17 |
. . . 4
⊢ (𝜑 → seq0( + , (𝐹‘𝐴)) ∈ dom ⇝ ) |
39 | 18, 19, 21, 22, 33, 38 | isumsplit 14411 |
. . 3
⊢ (𝜑 → Σ𝑖 ∈ ℕ0 ((𝐹‘𝐴)‘𝑖) = (Σ𝑖 ∈ (0...((𝐽 + 1) − 1))((𝐹‘𝐴)‘𝑖) + Σ𝑖 ∈ (ℤ≥‘(𝐽 + 1))((𝐹‘𝐴)‘𝑖))) |
40 | 10 | nn0cnd 11230 |
. . . . . . 7
⊢ (𝜑 → 𝐽 ∈ ℂ) |
41 | | 1cnd 9935 |
. . . . . . 7
⊢ (𝜑 → 1 ∈
ℂ) |
42 | 40, 41 | pncand 10272 |
. . . . . 6
⊢ (𝜑 → ((𝐽 + 1) − 1) = 𝐽) |
43 | 42 | oveq2d 6565 |
. . . . 5
⊢ (𝜑 → (0...((𝐽 + 1) − 1)) = (0...𝐽)) |
44 | 43 | sumeq1d 14279 |
. . . 4
⊢ (𝜑 → Σ𝑖 ∈ (0...((𝐽 + 1) − 1))((𝐹‘𝐴)‘𝑖) = Σ𝑖 ∈ (0...𝐽)((𝐹‘𝐴)‘𝑖)) |
45 | 44 | oveq1d 6564 |
. . 3
⊢ (𝜑 → (Σ𝑖 ∈ (0...((𝐽 + 1) − 1))((𝐹‘𝐴)‘𝑖) + Σ𝑖 ∈ (ℤ≥‘(𝐽 + 1))((𝐹‘𝐴)‘𝑖)) = (Σ𝑖 ∈ (0...𝐽)((𝐹‘𝐴)‘𝑖) + Σ𝑖 ∈ (ℤ≥‘(𝐽 + 1))((𝐹‘𝐴)‘𝑖))) |
46 | 17, 39, 45 | 3eqtrd 2648 |
. 2
⊢ (𝜑 → (𝑊‘𝐴) = (Σ𝑖 ∈ (0...𝐽)((𝐹‘𝐴)‘𝑖) + Σ𝑖 ∈ (ℤ≥‘(𝐽 + 1))((𝐹‘𝐴)‘𝑖))) |
47 | 14 | adantr 480 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑖 ∈ (ℤ≥‘(𝐽 + 1))) → 𝐴 ∈ ℝ) |
48 | | eluznn0 11633 |
. . . . . . . . 9
⊢ (((𝐽 + 1) ∈ ℕ0
∧ 𝑖 ∈
(ℤ≥‘(𝐽 + 1))) → 𝑖 ∈ ℕ0) |
49 | 21, 48 | sylan 487 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑖 ∈ (ℤ≥‘(𝐽 + 1))) → 𝑖 ∈
ℕ0) |
50 | 24, 47, 49 | knoppcnlem1 31653 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑖 ∈ (ℤ≥‘(𝐽 + 1))) → ((𝐹‘𝐴)‘𝑖) = ((𝐶↑𝑖) · (𝑇‘(((2 · 𝑁)↑𝑖) · 𝐴)))) |
51 | 7 | a1i 11 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑖 ∈ (ℤ≥‘(𝐽 + 1))) → 𝐴 = ((((2 · 𝑁)↑-𝐽) / 2) · 𝑀)) |
52 | 51 | oveq2d 6565 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑖 ∈ (ℤ≥‘(𝐽 + 1))) → (((2 ·
𝑁)↑𝑖) · 𝐴) = (((2 · 𝑁)↑𝑖) · ((((2 · 𝑁)↑-𝐽) / 2) · 𝑀))) |
53 | 9 | adantr 480 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑖 ∈ (ℤ≥‘(𝐽 + 1))) → 𝑁 ∈ ℕ) |
54 | 49 | nn0zd 11356 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑖 ∈ (ℤ≥‘(𝐽 + 1))) → 𝑖 ∈
ℤ) |
55 | 11 | adantr 480 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑖 ∈ (ℤ≥‘(𝐽 + 1))) → 𝐽 ∈ ℤ) |
56 | 12 | adantr 480 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑖 ∈ (ℤ≥‘(𝐽 + 1))) → 𝑀 ∈ ℤ) |
57 | | eluzle 11576 |
. . . . . . . . . . . . 13
⊢ (𝑖 ∈
(ℤ≥‘(𝐽 + 1)) → (𝐽 + 1) ≤ 𝑖) |
58 | 57 | adantl 481 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑖 ∈ (ℤ≥‘(𝐽 + 1))) → (𝐽 + 1) ≤ 𝑖) |
59 | 55, 54 | jca 553 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑖 ∈ (ℤ≥‘(𝐽 + 1))) → (𝐽 ∈ ℤ ∧ 𝑖 ∈
ℤ)) |
60 | | zltp1le 11304 |
. . . . . . . . . . . . 13
⊢ ((𝐽 ∈ ℤ ∧ 𝑖 ∈ ℤ) → (𝐽 < 𝑖 ↔ (𝐽 + 1) ≤ 𝑖)) |
61 | 59, 60 | syl 17 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑖 ∈ (ℤ≥‘(𝐽 + 1))) → (𝐽 < 𝑖 ↔ (𝐽 + 1) ≤ 𝑖)) |
62 | 58, 61 | mpbird 246 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑖 ∈ (ℤ≥‘(𝐽 + 1))) → 𝐽 < 𝑖) |
63 | 53, 54, 55, 56, 62 | knoppndvlem2 31674 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑖 ∈ (ℤ≥‘(𝐽 + 1))) → (((2 ·
𝑁)↑𝑖) · ((((2 · 𝑁)↑-𝐽) / 2) · 𝑀)) ∈ ℤ) |
64 | 52, 63 | eqeltrd 2688 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑖 ∈ (ℤ≥‘(𝐽 + 1))) → (((2 ·
𝑁)↑𝑖) · 𝐴) ∈ ℤ) |
65 | 23, 64 | dnizeq0 31635 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑖 ∈ (ℤ≥‘(𝐽 + 1))) → (𝑇‘(((2 · 𝑁)↑𝑖) · 𝐴)) = 0) |
66 | 65 | oveq2d 6565 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑖 ∈ (ℤ≥‘(𝐽 + 1))) → ((𝐶↑𝑖) · (𝑇‘(((2 · 𝑁)↑𝑖) · 𝐴))) = ((𝐶↑𝑖) · 0)) |
67 | 28 | recnd 9947 |
. . . . . . . . . 10
⊢ (𝜑 → 𝐶 ∈ ℂ) |
68 | 67 | adantr 480 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑖 ∈ (ℤ≥‘(𝐽 + 1))) → 𝐶 ∈ ℂ) |
69 | 68, 49 | expcld 12870 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑖 ∈ (ℤ≥‘(𝐽 + 1))) → (𝐶↑𝑖) ∈ ℂ) |
70 | 69 | mul01d 10114 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑖 ∈ (ℤ≥‘(𝐽 + 1))) → ((𝐶↑𝑖) · 0) = 0) |
71 | 50, 66, 70 | 3eqtrd 2648 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑖 ∈ (ℤ≥‘(𝐽 + 1))) → ((𝐹‘𝐴)‘𝑖) = 0) |
72 | 71 | sumeq2dv 14281 |
. . . . 5
⊢ (𝜑 → Σ𝑖 ∈ (ℤ≥‘(𝐽 + 1))((𝐹‘𝐴)‘𝑖) = Σ𝑖 ∈ (ℤ≥‘(𝐽 + 1))0) |
73 | | ssid 3587 |
. . . . . . . 8
⊢
(ℤ≥‘(𝐽 + 1)) ⊆
(ℤ≥‘(𝐽 + 1)) |
74 | 73 | a1i 11 |
. . . . . . 7
⊢ (𝜑 →
(ℤ≥‘(𝐽 + 1)) ⊆
(ℤ≥‘(𝐽 + 1))) |
75 | 74 | orcd 406 |
. . . . . 6
⊢ (𝜑 →
((ℤ≥‘(𝐽 + 1)) ⊆
(ℤ≥‘(𝐽 + 1)) ∨
(ℤ≥‘(𝐽 + 1)) ∈ Fin)) |
76 | | sumz 14300 |
. . . . . 6
⊢
(((ℤ≥‘(𝐽 + 1)) ⊆
(ℤ≥‘(𝐽 + 1)) ∨
(ℤ≥‘(𝐽 + 1)) ∈ Fin) → Σ𝑖 ∈
(ℤ≥‘(𝐽 + 1))0 = 0) |
77 | 75, 76 | syl 17 |
. . . . 5
⊢ (𝜑 → Σ𝑖 ∈ (ℤ≥‘(𝐽 + 1))0 = 0) |
78 | 72, 77 | eqtrd 2644 |
. . . 4
⊢ (𝜑 → Σ𝑖 ∈ (ℤ≥‘(𝐽 + 1))((𝐹‘𝐴)‘𝑖) = 0) |
79 | 78 | oveq2d 6565 |
. . 3
⊢ (𝜑 → (Σ𝑖 ∈ (0...𝐽)((𝐹‘𝐴)‘𝑖) + Σ𝑖 ∈ (ℤ≥‘(𝐽 + 1))((𝐹‘𝐴)‘𝑖)) = (Σ𝑖 ∈ (0...𝐽)((𝐹‘𝐴)‘𝑖) + 0)) |
80 | 23, 24, 14, 28, 9 | knoppndvlem5 31677 |
. . . . 5
⊢ (𝜑 → Σ𝑖 ∈ (0...𝐽)((𝐹‘𝐴)‘𝑖) ∈ ℝ) |
81 | 80 | recnd 9947 |
. . . 4
⊢ (𝜑 → Σ𝑖 ∈ (0...𝐽)((𝐹‘𝐴)‘𝑖) ∈ ℂ) |
82 | 81 | addid1d 10115 |
. . 3
⊢ (𝜑 → (Σ𝑖 ∈ (0...𝐽)((𝐹‘𝐴)‘𝑖) + 0) = Σ𝑖 ∈ (0...𝐽)((𝐹‘𝐴)‘𝑖)) |
83 | 79, 82 | eqtrd 2644 |
. 2
⊢ (𝜑 → (Σ𝑖 ∈ (0...𝐽)((𝐹‘𝐴)‘𝑖) + Σ𝑖 ∈ (ℤ≥‘(𝐽 + 1))((𝐹‘𝐴)‘𝑖)) = Σ𝑖 ∈ (0...𝐽)((𝐹‘𝐴)‘𝑖)) |
84 | 46, 83 | eqtrd 2644 |
1
⊢ (𝜑 → (𝑊‘𝐴) = Σ𝑖 ∈ (0...𝐽)((𝐹‘𝐴)‘𝑖)) |