Proof of Theorem knoppcnlem10
Step | Hyp | Ref
| Expression |
1 | | knoppcnlem10.f |
. . . 4
⊢ 𝐹 = (𝑦 ∈ ℝ ↦ (𝑛 ∈ ℕ0 ↦ ((𝐶↑𝑛) · (𝑇‘(((2 · 𝑁)↑𝑛) · 𝑦))))) |
2 | | simpr 476 |
. . . 4
⊢ ((𝜑 ∧ 𝑧 ∈ ℝ) → 𝑧 ∈ ℝ) |
3 | | knoppcnlem10.2 |
. . . . 5
⊢ (𝜑 → 𝑀 ∈
ℕ0) |
4 | 3 | adantr 480 |
. . . 4
⊢ ((𝜑 ∧ 𝑧 ∈ ℝ) → 𝑀 ∈
ℕ0) |
5 | 1, 2, 4 | knoppcnlem1 31653 |
. . 3
⊢ ((𝜑 ∧ 𝑧 ∈ ℝ) → ((𝐹‘𝑧)‘𝑀) = ((𝐶↑𝑀) · (𝑇‘(((2 · 𝑁)↑𝑀) · 𝑧)))) |
6 | 5 | mpteq2dva 4672 |
. 2
⊢ (𝜑 → (𝑧 ∈ ℝ ↦ ((𝐹‘𝑧)‘𝑀)) = (𝑧 ∈ ℝ ↦ ((𝐶↑𝑀) · (𝑇‘(((2 · 𝑁)↑𝑀) · 𝑧))))) |
7 | | retopon 22377 |
. . . 4
⊢
(topGen‘ran (,)) ∈ (TopOn‘ℝ) |
8 | 7 | a1i 11 |
. . 3
⊢ (𝜑 → (topGen‘ran (,))
∈ (TopOn‘ℝ)) |
9 | | eqid 2610 |
. . . . . 6
⊢
(TopOpen‘ℂfld) =
(TopOpen‘ℂfld) |
10 | 9 | cnfldtopon 22396 |
. . . . 5
⊢
(TopOpen‘ℂfld) ∈
(TopOn‘ℂ) |
11 | 10 | a1i 11 |
. . . 4
⊢ (𝜑 →
(TopOpen‘ℂfld) ∈
(TopOn‘ℂ)) |
12 | | knoppcnlem10.1 |
. . . . . 6
⊢ (𝜑 → 𝐶 ∈ ℝ) |
13 | 12 | recnd 9947 |
. . . . 5
⊢ (𝜑 → 𝐶 ∈ ℂ) |
14 | 13, 3 | expcld 12870 |
. . . 4
⊢ (𝜑 → (𝐶↑𝑀) ∈ ℂ) |
15 | 8, 11, 14 | cnmptc 21275 |
. . 3
⊢ (𝜑 → (𝑧 ∈ ℝ ↦ (𝐶↑𝑀)) ∈ ((topGen‘ran (,)) Cn
(TopOpen‘ℂfld))) |
16 | | 2re 10967 |
. . . . . . . . . . . 12
⊢ 2 ∈
ℝ |
17 | 16 | a1i 11 |
. . . . . . . . . . 11
⊢ (𝜑 → 2 ∈
ℝ) |
18 | | knoppcnlem10.n |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝑁 ∈ ℕ) |
19 | | nnre 10904 |
. . . . . . . . . . . 12
⊢ (𝑁 ∈ ℕ → 𝑁 ∈
ℝ) |
20 | 18, 19 | syl 17 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝑁 ∈ ℝ) |
21 | 17, 20 | remulcld 9949 |
. . . . . . . . . 10
⊢ (𝜑 → (2 · 𝑁) ∈
ℝ) |
22 | 21, 3 | reexpcld 12887 |
. . . . . . . . 9
⊢ (𝜑 → ((2 · 𝑁)↑𝑀) ∈ ℝ) |
23 | 22 | recnd 9947 |
. . . . . . . 8
⊢ (𝜑 → ((2 · 𝑁)↑𝑀) ∈ ℂ) |
24 | 8, 11, 23 | cnmptc 21275 |
. . . . . . 7
⊢ (𝜑 → (𝑧 ∈ ℝ ↦ ((2 · 𝑁)↑𝑀)) ∈ ((topGen‘ran (,)) Cn
(TopOpen‘ℂfld))) |
25 | 9 | tgioo2 22414 |
. . . . . . . . . 10
⊢
(topGen‘ran (,)) = ((TopOpen‘ℂfld)
↾t ℝ) |
26 | 25 | oveq2i 6560 |
. . . . . . . . 9
⊢
((topGen‘ran (,)) Cn (topGen‘ran (,))) = ((topGen‘ran
(,)) Cn ((TopOpen‘ℂfld) ↾t
ℝ)) |
27 | 10 | topontopi 20546 |
. . . . . . . . . 10
⊢
(TopOpen‘ℂfld) ∈ Top |
28 | | cnrest2r 20901 |
. . . . . . . . . 10
⊢
((TopOpen‘ℂfld) ∈ Top →
((topGen‘ran (,)) Cn ((TopOpen‘ℂfld)
↾t ℝ)) ⊆ ((topGen‘ran (,)) Cn
(TopOpen‘ℂfld))) |
29 | 27, 28 | ax-mp 5 |
. . . . . . . . 9
⊢
((topGen‘ran (,)) Cn ((TopOpen‘ℂfld)
↾t ℝ)) ⊆ ((topGen‘ran (,)) Cn
(TopOpen‘ℂfld)) |
30 | 26, 29 | eqsstri 3598 |
. . . . . . . 8
⊢
((topGen‘ran (,)) Cn (topGen‘ran (,))) ⊆
((topGen‘ran (,)) Cn
(TopOpen‘ℂfld)) |
31 | 8 | cnmptid 21274 |
. . . . . . . 8
⊢ (𝜑 → (𝑧 ∈ ℝ ↦ 𝑧) ∈ ((topGen‘ran (,)) Cn
(topGen‘ran (,)))) |
32 | 30, 31 | sseldi 3566 |
. . . . . . 7
⊢ (𝜑 → (𝑧 ∈ ℝ ↦ 𝑧) ∈ ((topGen‘ran (,)) Cn
(TopOpen‘ℂfld))) |
33 | 9 | mulcn 22478 |
. . . . . . . 8
⊢ ·
∈ (((TopOpen‘ℂfld) ×t
(TopOpen‘ℂfld)) Cn
(TopOpen‘ℂfld)) |
34 | 33 | a1i 11 |
. . . . . . 7
⊢ (𝜑 → · ∈
(((TopOpen‘ℂfld) ×t
(TopOpen‘ℂfld)) Cn
(TopOpen‘ℂfld))) |
35 | 8, 24, 32, 34 | cnmpt12f 21279 |
. . . . . 6
⊢ (𝜑 → (𝑧 ∈ ℝ ↦ (((2 · 𝑁)↑𝑀) · 𝑧)) ∈ ((topGen‘ran (,)) Cn
(TopOpen‘ℂfld))) |
36 | 22 | adantr 480 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑧 ∈ ℝ) → ((2 · 𝑁)↑𝑀) ∈ ℝ) |
37 | 36, 2 | remulcld 9949 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑧 ∈ ℝ) → (((2 · 𝑁)↑𝑀) · 𝑧) ∈ ℝ) |
38 | | eqid 2610 |
. . . . . . . . . 10
⊢ (𝑧 ∈ ℝ ↦ (((2
· 𝑁)↑𝑀) · 𝑧)) = (𝑧 ∈ ℝ ↦ (((2 · 𝑁)↑𝑀) · 𝑧)) |
39 | 37, 38 | fmptd 6292 |
. . . . . . . . 9
⊢ (𝜑 → (𝑧 ∈ ℝ ↦ (((2 · 𝑁)↑𝑀) · 𝑧)):ℝ⟶ℝ) |
40 | | frn 5966 |
. . . . . . . . 9
⊢ ((𝑧 ∈ ℝ ↦ (((2
· 𝑁)↑𝑀) · 𝑧)):ℝ⟶ℝ → ran (𝑧 ∈ ℝ ↦ (((2
· 𝑁)↑𝑀) · 𝑧)) ⊆ ℝ) |
41 | 39, 40 | syl 17 |
. . . . . . . 8
⊢ (𝜑 → ran (𝑧 ∈ ℝ ↦ (((2 · 𝑁)↑𝑀) · 𝑧)) ⊆ ℝ) |
42 | | ax-resscn 9872 |
. . . . . . . . 9
⊢ ℝ
⊆ ℂ |
43 | 42 | a1i 11 |
. . . . . . . 8
⊢ (𝜑 → ℝ ⊆
ℂ) |
44 | 11, 41, 43 | 3jca 1235 |
. . . . . . 7
⊢ (𝜑 →
((TopOpen‘ℂfld) ∈ (TopOn‘ℂ) ∧ ran
(𝑧 ∈ ℝ ↦
(((2 · 𝑁)↑𝑀) · 𝑧)) ⊆ ℝ ∧ ℝ ⊆
ℂ)) |
45 | | cnrest2 20900 |
. . . . . . 7
⊢
(((TopOpen‘ℂfld) ∈ (TopOn‘ℂ)
∧ ran (𝑧 ∈ ℝ
↦ (((2 · 𝑁)↑𝑀) · 𝑧)) ⊆ ℝ ∧ ℝ ⊆
ℂ) → ((𝑧 ∈
ℝ ↦ (((2 · 𝑁)↑𝑀) · 𝑧)) ∈ ((topGen‘ran (,)) Cn
(TopOpen‘ℂfld)) ↔ (𝑧 ∈ ℝ ↦ (((2 · 𝑁)↑𝑀) · 𝑧)) ∈ ((topGen‘ran (,)) Cn
((TopOpen‘ℂfld) ↾t
ℝ)))) |
46 | 44, 45 | syl 17 |
. . . . . 6
⊢ (𝜑 → ((𝑧 ∈ ℝ ↦ (((2 · 𝑁)↑𝑀) · 𝑧)) ∈ ((topGen‘ran (,)) Cn
(TopOpen‘ℂfld)) ↔ (𝑧 ∈ ℝ ↦ (((2 · 𝑁)↑𝑀) · 𝑧)) ∈ ((topGen‘ran (,)) Cn
((TopOpen‘ℂfld) ↾t
ℝ)))) |
47 | 35, 46 | mpbid 221 |
. . . . 5
⊢ (𝜑 → (𝑧 ∈ ℝ ↦ (((2 · 𝑁)↑𝑀) · 𝑧)) ∈ ((topGen‘ran (,)) Cn
((TopOpen‘ℂfld) ↾t
ℝ))) |
48 | 47, 26 | syl6eleqr 2699 |
. . . 4
⊢ (𝜑 → (𝑧 ∈ ℝ ↦ (((2 · 𝑁)↑𝑀) · 𝑧)) ∈ ((topGen‘ran (,)) Cn
(topGen‘ran (,)))) |
49 | | ssid 3587 |
. . . . . . . 8
⊢ ℂ
⊆ ℂ |
50 | 42, 49 | pm3.2i 470 |
. . . . . . 7
⊢ (ℝ
⊆ ℂ ∧ ℂ ⊆ ℂ) |
51 | | cncfss 22510 |
. . . . . . 7
⊢ ((ℝ
⊆ ℂ ∧ ℂ ⊆ ℂ) → (ℝ–cn→ℝ) ⊆ (ℝ–cn→ℂ)) |
52 | 50, 51 | ax-mp 5 |
. . . . . 6
⊢
(ℝ–cn→ℝ)
⊆ (ℝ–cn→ℂ) |
53 | | knoppcnlem10.t |
. . . . . . . 8
⊢ 𝑇 = (𝑥 ∈ ℝ ↦
(abs‘((⌊‘(𝑥 + (1 / 2))) − 𝑥))) |
54 | 53 | dnicn 31652 |
. . . . . . 7
⊢ 𝑇 ∈ (ℝ–cn→ℝ) |
55 | 54 | a1i 11 |
. . . . . 6
⊢ (𝜑 → 𝑇 ∈ (ℝ–cn→ℝ)) |
56 | 52, 55 | sseldi 3566 |
. . . . 5
⊢ (𝜑 → 𝑇 ∈ (ℝ–cn→ℂ)) |
57 | | fvex 6113 |
. . . . . . . . 9
⊢
(TopOpen‘ℂfld) ∈ V |
58 | 10 | toponunii 20547 |
. . . . . . . . . 10
⊢ ℂ =
∪
(TopOpen‘ℂfld) |
59 | 58 | restid 15917 |
. . . . . . . . 9
⊢
((TopOpen‘ℂfld) ∈ V →
((TopOpen‘ℂfld) ↾t ℂ) =
(TopOpen‘ℂfld)) |
60 | 57, 59 | ax-mp 5 |
. . . . . . . 8
⊢
((TopOpen‘ℂfld) ↾t ℂ) =
(TopOpen‘ℂfld) |
61 | 60 | eqcomi 2619 |
. . . . . . 7
⊢
(TopOpen‘ℂfld) =
((TopOpen‘ℂfld) ↾t
ℂ) |
62 | 9, 25, 61 | cncfcn 22520 |
. . . . . 6
⊢ ((ℝ
⊆ ℂ ∧ ℂ ⊆ ℂ) → (ℝ–cn→ℂ) = ((topGen‘ran (,)) Cn
(TopOpen‘ℂfld))) |
63 | 50, 62 | ax-mp 5 |
. . . . 5
⊢
(ℝ–cn→ℂ) =
((topGen‘ran (,)) Cn
(TopOpen‘ℂfld)) |
64 | 56, 63 | syl6eleq 2698 |
. . . 4
⊢ (𝜑 → 𝑇 ∈ ((topGen‘ran (,)) Cn
(TopOpen‘ℂfld))) |
65 | 8, 48, 64 | cnmpt11f 21277 |
. . 3
⊢ (𝜑 → (𝑧 ∈ ℝ ↦ (𝑇‘(((2 · 𝑁)↑𝑀) · 𝑧))) ∈ ((topGen‘ran (,)) Cn
(TopOpen‘ℂfld))) |
66 | 8, 15, 65, 34 | cnmpt12f 21279 |
. 2
⊢ (𝜑 → (𝑧 ∈ ℝ ↦ ((𝐶↑𝑀) · (𝑇‘(((2 · 𝑁)↑𝑀) · 𝑧)))) ∈ ((topGen‘ran (,)) Cn
(TopOpen‘ℂfld))) |
67 | 6, 66 | eqeltrd 2688 |
1
⊢ (𝜑 → (𝑧 ∈ ℝ ↦ ((𝐹‘𝑧)‘𝑀)) ∈ ((topGen‘ran (,)) Cn
(TopOpen‘ℂfld))) |