Step | Hyp | Ref
| Expression |
1 | | nn0uz 12364 |
. 2
⊢
ℕ0 = (ℤ≥‘0) |
2 | | 0zd 12076 |
. 2
⊢ (𝜑 → 0 ∈
ℤ) |
3 | | reex 10708 |
. . 3
⊢ ℝ
∈ V |
4 | 3 | a1i 11 |
. 2
⊢ (𝜑 → ℝ ∈
V) |
5 | | knoppcnlem6.t |
. . 3
⊢ 𝑇 = (𝑥 ∈ ℝ ↦
(abs‘((⌊‘(𝑥 + (1 / 2))) − 𝑥))) |
6 | | knoppcnlem6.f |
. . 3
⊢ 𝐹 = (𝑦 ∈ ℝ ↦ (𝑛 ∈ ℕ0 ↦ ((𝐶↑𝑛) · (𝑇‘(((2 · 𝑁)↑𝑛) · 𝑦))))) |
7 | | knoppcnlem6.n |
. . 3
⊢ (𝜑 → 𝑁 ∈ ℕ) |
8 | | knoppcnlem6.1 |
. . 3
⊢ (𝜑 → 𝐶 ∈ ℝ) |
9 | 5, 6, 7, 8 | knoppcnlem5 34322 |
. 2
⊢ (𝜑 → (𝑚 ∈ ℕ0 ↦ (𝑧 ∈ ℝ ↦ ((𝐹‘𝑧)‘𝑚))):ℕ0⟶(ℂ
↑m ℝ)) |
10 | | nn0ex 11984 |
. . . 4
⊢
ℕ0 ∈ V |
11 | 10 | mptex 6998 |
. . 3
⊢ (𝑚 ∈ ℕ0
↦ ((abs‘𝐶)↑𝑚)) ∈ V |
12 | 11 | a1i 11 |
. 2
⊢ (𝜑 → (𝑚 ∈ ℕ0 ↦
((abs‘𝐶)↑𝑚)) ∈ V) |
13 | | eqid 2738 |
. . . . 5
⊢ (𝑚 ∈ ℕ0
↦ ((abs‘𝐶)↑𝑚)) = (𝑚 ∈ ℕ0 ↦
((abs‘𝐶)↑𝑚)) |
14 | 13 | a1i 11 |
. . . 4
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → (𝑚 ∈ ℕ0
↦ ((abs‘𝐶)↑𝑚)) = (𝑚 ∈ ℕ0 ↦
((abs‘𝐶)↑𝑚))) |
15 | | simpr 488 |
. . . . 5
⊢ (((𝜑 ∧ 𝑘 ∈ ℕ0) ∧ 𝑚 = 𝑘) → 𝑚 = 𝑘) |
16 | 15 | oveq2d 7188 |
. . . 4
⊢ (((𝜑 ∧ 𝑘 ∈ ℕ0) ∧ 𝑚 = 𝑘) → ((abs‘𝐶)↑𝑚) = ((abs‘𝐶)↑𝑘)) |
17 | | simpr 488 |
. . . 4
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → 𝑘 ∈
ℕ0) |
18 | | ovexd 7207 |
. . . 4
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) →
((abs‘𝐶)↑𝑘) ∈ V) |
19 | 14, 16, 17, 18 | fvmptd 6784 |
. . 3
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → ((𝑚 ∈ ℕ0
↦ ((abs‘𝐶)↑𝑚))‘𝑘) = ((abs‘𝐶)↑𝑘)) |
20 | 8 | recnd 10749 |
. . . . . 6
⊢ (𝜑 → 𝐶 ∈ ℂ) |
21 | 20 | abscld 14888 |
. . . . 5
⊢ (𝜑 → (abs‘𝐶) ∈
ℝ) |
22 | 21 | adantr 484 |
. . . 4
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) →
(abs‘𝐶) ∈
ℝ) |
23 | 22, 17 | reexpcld 13621 |
. . 3
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) →
((abs‘𝐶)↑𝑘) ∈
ℝ) |
24 | 19, 23 | eqeltrd 2833 |
. 2
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → ((𝑚 ∈ ℕ0
↦ ((abs‘𝐶)↑𝑚))‘𝑘) ∈ ℝ) |
25 | | eqid 2738 |
. . . . . . 7
⊢ (𝑚 ∈ ℕ0
↦ (𝑧 ∈ ℝ
↦ ((𝐹‘𝑧)‘𝑚))) = (𝑚 ∈ ℕ0 ↦ (𝑧 ∈ ℝ ↦ ((𝐹‘𝑧)‘𝑚))) |
26 | 25 | a1i 11 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑘 ∈ ℕ0 ∧ 𝑤 ∈ ℝ)) → (𝑚 ∈ ℕ0
↦ (𝑧 ∈ ℝ
↦ ((𝐹‘𝑧)‘𝑚))) = (𝑚 ∈ ℕ0 ↦ (𝑧 ∈ ℝ ↦ ((𝐹‘𝑧)‘𝑚)))) |
27 | | simpr 488 |
. . . . . . . 8
⊢ (((𝜑 ∧ (𝑘 ∈ ℕ0 ∧ 𝑤 ∈ ℝ)) ∧ 𝑚 = 𝑘) → 𝑚 = 𝑘) |
28 | 27 | fveq2d 6680 |
. . . . . . 7
⊢ (((𝜑 ∧ (𝑘 ∈ ℕ0 ∧ 𝑤 ∈ ℝ)) ∧ 𝑚 = 𝑘) → ((𝐹‘𝑧)‘𝑚) = ((𝐹‘𝑧)‘𝑘)) |
29 | 28 | mpteq2dv 5126 |
. . . . . 6
⊢ (((𝜑 ∧ (𝑘 ∈ ℕ0 ∧ 𝑤 ∈ ℝ)) ∧ 𝑚 = 𝑘) → (𝑧 ∈ ℝ ↦ ((𝐹‘𝑧)‘𝑚)) = (𝑧 ∈ ℝ ↦ ((𝐹‘𝑧)‘𝑘))) |
30 | 17 | adantrr 717 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑘 ∈ ℕ0 ∧ 𝑤 ∈ ℝ)) → 𝑘 ∈
ℕ0) |
31 | 3 | mptex 6998 |
. . . . . . 7
⊢ (𝑧 ∈ ℝ ↦ ((𝐹‘𝑧)‘𝑘)) ∈ V |
32 | 31 | a1i 11 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑘 ∈ ℕ0 ∧ 𝑤 ∈ ℝ)) → (𝑧 ∈ ℝ ↦ ((𝐹‘𝑧)‘𝑘)) ∈ V) |
33 | 26, 29, 30, 32 | fvmptd 6784 |
. . . . 5
⊢ ((𝜑 ∧ (𝑘 ∈ ℕ0 ∧ 𝑤 ∈ ℝ)) → ((𝑚 ∈ ℕ0
↦ (𝑧 ∈ ℝ
↦ ((𝐹‘𝑧)‘𝑚)))‘𝑘) = (𝑧 ∈ ℝ ↦ ((𝐹‘𝑧)‘𝑘))) |
34 | | simpr 488 |
. . . . . . 7
⊢ (((𝜑 ∧ (𝑘 ∈ ℕ0 ∧ 𝑤 ∈ ℝ)) ∧ 𝑧 = 𝑤) → 𝑧 = 𝑤) |
35 | 34 | fveq2d 6680 |
. . . . . 6
⊢ (((𝜑 ∧ (𝑘 ∈ ℕ0 ∧ 𝑤 ∈ ℝ)) ∧ 𝑧 = 𝑤) → (𝐹‘𝑧) = (𝐹‘𝑤)) |
36 | 35 | fveq1d 6678 |
. . . . 5
⊢ (((𝜑 ∧ (𝑘 ∈ ℕ0 ∧ 𝑤 ∈ ℝ)) ∧ 𝑧 = 𝑤) → ((𝐹‘𝑧)‘𝑘) = ((𝐹‘𝑤)‘𝑘)) |
37 | | simprr 773 |
. . . . 5
⊢ ((𝜑 ∧ (𝑘 ∈ ℕ0 ∧ 𝑤 ∈ ℝ)) → 𝑤 ∈
ℝ) |
38 | | fvexd 6691 |
. . . . 5
⊢ ((𝜑 ∧ (𝑘 ∈ ℕ0 ∧ 𝑤 ∈ ℝ)) → ((𝐹‘𝑤)‘𝑘) ∈ V) |
39 | 33, 36, 37, 38 | fvmptd 6784 |
. . . 4
⊢ ((𝜑 ∧ (𝑘 ∈ ℕ0 ∧ 𝑤 ∈ ℝ)) →
(((𝑚 ∈
ℕ0 ↦ (𝑧 ∈ ℝ ↦ ((𝐹‘𝑧)‘𝑚)))‘𝑘)‘𝑤) = ((𝐹‘𝑤)‘𝑘)) |
40 | 39 | fveq2d 6680 |
. . 3
⊢ ((𝜑 ∧ (𝑘 ∈ ℕ0 ∧ 𝑤 ∈ ℝ)) →
(abs‘(((𝑚 ∈
ℕ0 ↦ (𝑧 ∈ ℝ ↦ ((𝐹‘𝑧)‘𝑚)))‘𝑘)‘𝑤)) = (abs‘((𝐹‘𝑤)‘𝑘))) |
41 | 7 | adantr 484 |
. . . 4
⊢ ((𝜑 ∧ (𝑘 ∈ ℕ0 ∧ 𝑤 ∈ ℝ)) → 𝑁 ∈
ℕ) |
42 | 8 | adantr 484 |
. . . 4
⊢ ((𝜑 ∧ (𝑘 ∈ ℕ0 ∧ 𝑤 ∈ ℝ)) → 𝐶 ∈
ℝ) |
43 | 5, 6, 41, 42, 37, 30 | knoppcnlem4 34321 |
. . 3
⊢ ((𝜑 ∧ (𝑘 ∈ ℕ0 ∧ 𝑤 ∈ ℝ)) →
(abs‘((𝐹‘𝑤)‘𝑘)) ≤ ((𝑚 ∈ ℕ0 ↦
((abs‘𝐶)↑𝑚))‘𝑘)) |
44 | 40, 43 | eqbrtrd 5052 |
. 2
⊢ ((𝜑 ∧ (𝑘 ∈ ℕ0 ∧ 𝑤 ∈ ℝ)) →
(abs‘(((𝑚 ∈
ℕ0 ↦ (𝑧 ∈ ℝ ↦ ((𝐹‘𝑧)‘𝑚)))‘𝑘)‘𝑤)) ≤ ((𝑚 ∈ ℕ0 ↦
((abs‘𝐶)↑𝑚))‘𝑘)) |
45 | 21 | recnd 10749 |
. . . 4
⊢ (𝜑 → (abs‘𝐶) ∈
ℂ) |
46 | | absidm 14775 |
. . . . . 6
⊢ (𝐶 ∈ ℂ →
(abs‘(abs‘𝐶)) =
(abs‘𝐶)) |
47 | 20, 46 | syl 17 |
. . . . 5
⊢ (𝜑 →
(abs‘(abs‘𝐶)) =
(abs‘𝐶)) |
48 | | knoppcnlem6.2 |
. . . . 5
⊢ (𝜑 → (abs‘𝐶) < 1) |
49 | 47, 48 | eqbrtrd 5052 |
. . . 4
⊢ (𝜑 →
(abs‘(abs‘𝐶))
< 1) |
50 | 45, 49, 19 | geolim 15320 |
. . 3
⊢ (𝜑 → seq0( + , (𝑚 ∈ ℕ0
↦ ((abs‘𝐶)↑𝑚))) ⇝ (1 / (1 − (abs‘𝐶)))) |
51 | | seqex 13464 |
. . . 4
⊢ seq0( + ,
(𝑚 ∈
ℕ0 ↦ ((abs‘𝐶)↑𝑚))) ∈ V |
52 | | ovex 7205 |
. . . 4
⊢ (1 / (1
− (abs‘𝐶)))
∈ V |
53 | 51, 52 | breldm 5751 |
. . 3
⊢ (seq0( +
, (𝑚 ∈
ℕ0 ↦ ((abs‘𝐶)↑𝑚))) ⇝ (1 / (1 − (abs‘𝐶))) → seq0( + , (𝑚 ∈ ℕ0
↦ ((abs‘𝐶)↑𝑚))) ∈ dom ⇝ ) |
54 | 50, 53 | syl 17 |
. 2
⊢ (𝜑 → seq0( + , (𝑚 ∈ ℕ0
↦ ((abs‘𝐶)↑𝑚))) ∈ dom ⇝ ) |
55 | 1, 2, 4, 9, 12, 24, 44, 54 | mtest 25153 |
1
⊢ (𝜑 → seq0( ∘f
+ , (𝑚 ∈
ℕ0 ↦ (𝑧 ∈ ℝ ↦ ((𝐹‘𝑧)‘𝑚)))) ∈ dom
(⇝𝑢‘ℝ)) |