| Step | Hyp | Ref
| Expression |
| 1 | | nn0uz 12920 |
. 2
⊢
ℕ0 = (ℤ≥‘0) |
| 2 | | 0zd 12625 |
. 2
⊢ (𝜑 → 0 ∈
ℤ) |
| 3 | | reex 11246 |
. . 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 36498 |
. 2
⊢ (𝜑 → (𝑚 ∈ ℕ0 ↦ (𝑧 ∈ ℝ ↦ ((𝐹‘𝑧)‘𝑚))):ℕ0⟶(ℂ
↑m ℝ)) |
| 10 | | nn0ex 12532 |
. . . 4
⊢
ℕ0 ∈ V |
| 11 | 10 | mptex 7243 |
. . 3
⊢ (𝑚 ∈ ℕ0
↦ ((abs‘𝐶)↑𝑚)) ∈ V |
| 12 | 11 | a1i 11 |
. 2
⊢ (𝜑 → (𝑚 ∈ ℕ0 ↦
((abs‘𝐶)↑𝑚)) ∈ V) |
| 13 | | eqid 2737 |
. . . . 5
⊢ (𝑚 ∈ ℕ0
↦ ((abs‘𝐶)↑𝑚)) = (𝑚 ∈ ℕ0 ↦
((abs‘𝐶)↑𝑚)) |
| 14 | 13 | a1i 11 |
. . . 4
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → (𝑚 ∈ ℕ0
↦ ((abs‘𝐶)↑𝑚)) = (𝑚 ∈ ℕ0 ↦
((abs‘𝐶)↑𝑚))) |
| 15 | | simpr 484 |
. . . . 5
⊢ (((𝜑 ∧ 𝑘 ∈ ℕ0) ∧ 𝑚 = 𝑘) → 𝑚 = 𝑘) |
| 16 | 15 | oveq2d 7447 |
. . . 4
⊢ (((𝜑 ∧ 𝑘 ∈ ℕ0) ∧ 𝑚 = 𝑘) → ((abs‘𝐶)↑𝑚) = ((abs‘𝐶)↑𝑘)) |
| 17 | | simpr 484 |
. . . 4
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → 𝑘 ∈
ℕ0) |
| 18 | | ovexd 7466 |
. . . 4
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) →
((abs‘𝐶)↑𝑘) ∈ V) |
| 19 | 14, 16, 17, 18 | fvmptd 7023 |
. . 3
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → ((𝑚 ∈ ℕ0
↦ ((abs‘𝐶)↑𝑚))‘𝑘) = ((abs‘𝐶)↑𝑘)) |
| 20 | 8 | recnd 11289 |
. . . . . 6
⊢ (𝜑 → 𝐶 ∈ ℂ) |
| 21 | 20 | abscld 15475 |
. . . . 5
⊢ (𝜑 → (abs‘𝐶) ∈
ℝ) |
| 22 | 21 | adantr 480 |
. . . 4
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) →
(abs‘𝐶) ∈
ℝ) |
| 23 | 22, 17 | reexpcld 14203 |
. . 3
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) →
((abs‘𝐶)↑𝑘) ∈
ℝ) |
| 24 | 19, 23 | eqeltrd 2841 |
. 2
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → ((𝑚 ∈ ℕ0
↦ ((abs‘𝐶)↑𝑚))‘𝑘) ∈ ℝ) |
| 25 | | eqid 2737 |
. . . . . . 7
⊢ (𝑚 ∈ ℕ0
↦ (𝑧 ∈ ℝ
↦ ((𝐹‘𝑧)‘𝑚))) = (𝑚 ∈ ℕ0 ↦ (𝑧 ∈ ℝ ↦ ((𝐹‘𝑧)‘𝑚))) |
| 26 | 25 | a1i 11 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑘 ∈ ℕ0 ∧ 𝑤 ∈ ℝ)) → (𝑚 ∈ ℕ0
↦ (𝑧 ∈ ℝ
↦ ((𝐹‘𝑧)‘𝑚))) = (𝑚 ∈ ℕ0 ↦ (𝑧 ∈ ℝ ↦ ((𝐹‘𝑧)‘𝑚)))) |
| 27 | | simpr 484 |
. . . . . . . 8
⊢ (((𝜑 ∧ (𝑘 ∈ ℕ0 ∧ 𝑤 ∈ ℝ)) ∧ 𝑚 = 𝑘) → 𝑚 = 𝑘) |
| 28 | 27 | fveq2d 6910 |
. . . . . . 7
⊢ (((𝜑 ∧ (𝑘 ∈ ℕ0 ∧ 𝑤 ∈ ℝ)) ∧ 𝑚 = 𝑘) → ((𝐹‘𝑧)‘𝑚) = ((𝐹‘𝑧)‘𝑘)) |
| 29 | 28 | mpteq2dv 5244 |
. . . . . 6
⊢ (((𝜑 ∧ (𝑘 ∈ ℕ0 ∧ 𝑤 ∈ ℝ)) ∧ 𝑚 = 𝑘) → (𝑧 ∈ ℝ ↦ ((𝐹‘𝑧)‘𝑚)) = (𝑧 ∈ ℝ ↦ ((𝐹‘𝑧)‘𝑘))) |
| 30 | 17 | adantrr 717 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑘 ∈ ℕ0 ∧ 𝑤 ∈ ℝ)) → 𝑘 ∈
ℕ0) |
| 31 | 3 | mptex 7243 |
. . . . . . 7
⊢ (𝑧 ∈ ℝ ↦ ((𝐹‘𝑧)‘𝑘)) ∈ V |
| 32 | 31 | a1i 11 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑘 ∈ ℕ0 ∧ 𝑤 ∈ ℝ)) → (𝑧 ∈ ℝ ↦ ((𝐹‘𝑧)‘𝑘)) ∈ V) |
| 33 | 26, 29, 30, 32 | fvmptd 7023 |
. . . . 5
⊢ ((𝜑 ∧ (𝑘 ∈ ℕ0 ∧ 𝑤 ∈ ℝ)) → ((𝑚 ∈ ℕ0
↦ (𝑧 ∈ ℝ
↦ ((𝐹‘𝑧)‘𝑚)))‘𝑘) = (𝑧 ∈ ℝ ↦ ((𝐹‘𝑧)‘𝑘))) |
| 34 | | simpr 484 |
. . . . . . 7
⊢ (((𝜑 ∧ (𝑘 ∈ ℕ0 ∧ 𝑤 ∈ ℝ)) ∧ 𝑧 = 𝑤) → 𝑧 = 𝑤) |
| 35 | 34 | fveq2d 6910 |
. . . . . 6
⊢ (((𝜑 ∧ (𝑘 ∈ ℕ0 ∧ 𝑤 ∈ ℝ)) ∧ 𝑧 = 𝑤) → (𝐹‘𝑧) = (𝐹‘𝑤)) |
| 36 | 35 | fveq1d 6908 |
. . . . 5
⊢ (((𝜑 ∧ (𝑘 ∈ ℕ0 ∧ 𝑤 ∈ ℝ)) ∧ 𝑧 = 𝑤) → ((𝐹‘𝑧)‘𝑘) = ((𝐹‘𝑤)‘𝑘)) |
| 37 | | simprr 773 |
. . . . 5
⊢ ((𝜑 ∧ (𝑘 ∈ ℕ0 ∧ 𝑤 ∈ ℝ)) → 𝑤 ∈
ℝ) |
| 38 | | fvexd 6921 |
. . . . 5
⊢ ((𝜑 ∧ (𝑘 ∈ ℕ0 ∧ 𝑤 ∈ ℝ)) → ((𝐹‘𝑤)‘𝑘) ∈ V) |
| 39 | 33, 36, 37, 38 | fvmptd 7023 |
. . . 4
⊢ ((𝜑 ∧ (𝑘 ∈ ℕ0 ∧ 𝑤 ∈ ℝ)) →
(((𝑚 ∈
ℕ0 ↦ (𝑧 ∈ ℝ ↦ ((𝐹‘𝑧)‘𝑚)))‘𝑘)‘𝑤) = ((𝐹‘𝑤)‘𝑘)) |
| 40 | 39 | fveq2d 6910 |
. . 3
⊢ ((𝜑 ∧ (𝑘 ∈ ℕ0 ∧ 𝑤 ∈ ℝ)) →
(abs‘(((𝑚 ∈
ℕ0 ↦ (𝑧 ∈ ℝ ↦ ((𝐹‘𝑧)‘𝑚)))‘𝑘)‘𝑤)) = (abs‘((𝐹‘𝑤)‘𝑘))) |
| 41 | 7 | adantr 480 |
. . . 4
⊢ ((𝜑 ∧ (𝑘 ∈ ℕ0 ∧ 𝑤 ∈ ℝ)) → 𝑁 ∈
ℕ) |
| 42 | 8 | adantr 480 |
. . . 4
⊢ ((𝜑 ∧ (𝑘 ∈ ℕ0 ∧ 𝑤 ∈ ℝ)) → 𝐶 ∈
ℝ) |
| 43 | 5, 6, 41, 42, 37, 30 | knoppcnlem4 36497 |
. . 3
⊢ ((𝜑 ∧ (𝑘 ∈ ℕ0 ∧ 𝑤 ∈ ℝ)) →
(abs‘((𝐹‘𝑤)‘𝑘)) ≤ ((𝑚 ∈ ℕ0 ↦
((abs‘𝐶)↑𝑚))‘𝑘)) |
| 44 | 40, 43 | eqbrtrd 5165 |
. 2
⊢ ((𝜑 ∧ (𝑘 ∈ ℕ0 ∧ 𝑤 ∈ ℝ)) →
(abs‘(((𝑚 ∈
ℕ0 ↦ (𝑧 ∈ ℝ ↦ ((𝐹‘𝑧)‘𝑚)))‘𝑘)‘𝑤)) ≤ ((𝑚 ∈ ℕ0 ↦
((abs‘𝐶)↑𝑚))‘𝑘)) |
| 45 | 21 | recnd 11289 |
. . . 4
⊢ (𝜑 → (abs‘𝐶) ∈
ℂ) |
| 46 | | absidm 15362 |
. . . . . 6
⊢ (𝐶 ∈ ℂ →
(abs‘(abs‘𝐶)) =
(abs‘𝐶)) |
| 47 | 20, 46 | syl 17 |
. . . . 5
⊢ (𝜑 →
(abs‘(abs‘𝐶)) =
(abs‘𝐶)) |
| 48 | | knoppcnlem6.2 |
. . . . 5
⊢ (𝜑 → (abs‘𝐶) < 1) |
| 49 | 47, 48 | eqbrtrd 5165 |
. . . 4
⊢ (𝜑 →
(abs‘(abs‘𝐶))
< 1) |
| 50 | 45, 49, 19 | geolim 15906 |
. . 3
⊢ (𝜑 → seq0( + , (𝑚 ∈ ℕ0
↦ ((abs‘𝐶)↑𝑚))) ⇝ (1 / (1 − (abs‘𝐶)))) |
| 51 | | seqex 14044 |
. . . 4
⊢ seq0( + ,
(𝑚 ∈
ℕ0 ↦ ((abs‘𝐶)↑𝑚))) ∈ V |
| 52 | | ovex 7464 |
. . . 4
⊢ (1 / (1
− (abs‘𝐶)))
∈ V |
| 53 | 51, 52 | breldm 5919 |
. . 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 26447 |
1
⊢ (𝜑 → seq0( ∘f
+ , (𝑚 ∈
ℕ0 ↦ (𝑧 ∈ ℝ ↦ ((𝐹‘𝑧)‘𝑚)))) ∈ dom
(⇝𝑢‘ℝ)) |