Step | Hyp | Ref
| Expression |
1 | | sqrtf 13951 |
. . . . . . 7
⊢
√:ℂ⟶ℂ |
2 | 1 | a1i 11 |
. . . . . 6
⊢ (⊤
→ √:ℂ⟶ℂ) |
3 | 2 | feqmptd 6159 |
. . . . 5
⊢ (⊤
→ √ = (𝑥 ∈
ℂ ↦ (√‘𝑥))) |
4 | 3 | reseq1d 5316 |
. . . 4
⊢ (⊤
→ (√ ↾ (0[,)+∞)) = ((𝑥 ∈ ℂ ↦ (√‘𝑥)) ↾
(0[,)+∞))) |
5 | | elrege0 12149 |
. . . . . . . 8
⊢ (𝑥 ∈ (0[,)+∞) ↔
(𝑥 ∈ ℝ ∧ 0
≤ 𝑥)) |
6 | 5 | simplbi 475 |
. . . . . . 7
⊢ (𝑥 ∈ (0[,)+∞) →
𝑥 ∈
ℝ) |
7 | 6 | recnd 9947 |
. . . . . 6
⊢ (𝑥 ∈ (0[,)+∞) →
𝑥 ∈
ℂ) |
8 | 7 | ssriv 3572 |
. . . . 5
⊢
(0[,)+∞) ⊆ ℂ |
9 | | resmpt 5369 |
. . . . 5
⊢
((0[,)+∞) ⊆ ℂ → ((𝑥 ∈ ℂ ↦ (√‘𝑥)) ↾ (0[,)+∞)) =
(𝑥 ∈ (0[,)+∞)
↦ (√‘𝑥))) |
10 | 8, 9 | mp1i 13 |
. . . 4
⊢ (⊤
→ ((𝑥 ∈ ℂ
↦ (√‘𝑥))
↾ (0[,)+∞)) = (𝑥 ∈ (0[,)+∞) ↦
(√‘𝑥))) |
11 | 4, 10 | eqtrd 2644 |
. . 3
⊢ (⊤
→ (√ ↾ (0[,)+∞)) = (𝑥 ∈ (0[,)+∞) ↦
(√‘𝑥))) |
12 | 11 | trud 1484 |
. 2
⊢ (√
↾ (0[,)+∞)) = (𝑥 ∈ (0[,)+∞) ↦
(√‘𝑥)) |
13 | | eqid 2610 |
. . . 4
⊢ (𝑥 ∈ (0[,)+∞) ↦
(√‘𝑥)) = (𝑥 ∈ (0[,)+∞) ↦
(√‘𝑥)) |
14 | | resqrtcl 13842 |
. . . . 5
⊢ ((𝑥 ∈ ℝ ∧ 0 ≤
𝑥) →
(√‘𝑥) ∈
ℝ) |
15 | 5, 14 | sylbi 206 |
. . . 4
⊢ (𝑥 ∈ (0[,)+∞) →
(√‘𝑥) ∈
ℝ) |
16 | 13, 15 | fmpti 6291 |
. . 3
⊢ (𝑥 ∈ (0[,)+∞) ↦
(√‘𝑥)):(0[,)+∞)⟶ℝ |
17 | | ax-resscn 9872 |
. . . 4
⊢ ℝ
⊆ ℂ |
18 | | cxpsqrt 24249 |
. . . . . . . 8
⊢ (𝑥 ∈ ℂ → (𝑥↑𝑐(1 /
2)) = (√‘𝑥)) |
19 | 7, 18 | syl 17 |
. . . . . . 7
⊢ (𝑥 ∈ (0[,)+∞) →
(𝑥↑𝑐(1 / 2)) =
(√‘𝑥)) |
20 | 19 | mpteq2ia 4668 |
. . . . . 6
⊢ (𝑥 ∈ (0[,)+∞) ↦
(𝑥↑𝑐(1 / 2))) = (𝑥 ∈ (0[,)+∞) ↦
(√‘𝑥)) |
21 | | eqid 2610 |
. . . . . . . . . . 11
⊢
(TopOpen‘ℂfld) =
(TopOpen‘ℂfld) |
22 | 21 | cnfldtopon 22396 |
. . . . . . . . . 10
⊢
(TopOpen‘ℂfld) ∈
(TopOn‘ℂ) |
23 | 22 | a1i 11 |
. . . . . . . . 9
⊢ (⊤
→ (TopOpen‘ℂfld) ∈
(TopOn‘ℂ)) |
24 | | resttopon 20775 |
. . . . . . . . 9
⊢
(((TopOpen‘ℂfld) ∈ (TopOn‘ℂ)
∧ (0[,)+∞) ⊆ ℂ) →
((TopOpen‘ℂfld) ↾t (0[,)+∞))
∈ (TopOn‘(0[,)+∞))) |
25 | 23, 8, 24 | sylancl 693 |
. . . . . . . 8
⊢ (⊤
→ ((TopOpen‘ℂfld) ↾t
(0[,)+∞)) ∈ (TopOn‘(0[,)+∞))) |
26 | 25 | cnmptid 21274 |
. . . . . . . 8
⊢ (⊤
→ (𝑥 ∈
(0[,)+∞) ↦ 𝑥)
∈ (((TopOpen‘ℂfld) ↾t
(0[,)+∞)) Cn ((TopOpen‘ℂfld) ↾t
(0[,)+∞)))) |
27 | | cnvimass 5404 |
. . . . . . . . . . 11
⊢ (◡ℜ “ ℝ+) ⊆
dom ℜ |
28 | | ref 13700 |
. . . . . . . . . . . 12
⊢
ℜ:ℂ⟶ℝ |
29 | 28 | fdmi 5965 |
. . . . . . . . . . 11
⊢ dom
ℜ = ℂ |
30 | 27, 29 | sseqtri 3600 |
. . . . . . . . . 10
⊢ (◡ℜ “ ℝ+) ⊆
ℂ |
31 | | resttopon 20775 |
. . . . . . . . . 10
⊢
(((TopOpen‘ℂfld) ∈ (TopOn‘ℂ)
∧ (◡ℜ “
ℝ+) ⊆ ℂ) →
((TopOpen‘ℂfld) ↾t (◡ℜ “ ℝ+)) ∈
(TopOn‘(◡ℜ “
ℝ+))) |
32 | 23, 30, 31 | sylancl 693 |
. . . . . . . . 9
⊢ (⊤
→ ((TopOpen‘ℂfld) ↾t (◡ℜ “ ℝ+)) ∈
(TopOn‘(◡ℜ “
ℝ+))) |
33 | | halfcn 11124 |
. . . . . . . . . . 11
⊢ (1 / 2)
∈ ℂ |
34 | | 1rp 11712 |
. . . . . . . . . . . . . 14
⊢ 1 ∈
ℝ+ |
35 | | rphalfcl 11734 |
. . . . . . . . . . . . . 14
⊢ (1 ∈
ℝ+ → (1 / 2) ∈ ℝ+) |
36 | 34, 35 | ax-mp 5 |
. . . . . . . . . . . . 13
⊢ (1 / 2)
∈ ℝ+ |
37 | | rpre 11715 |
. . . . . . . . . . . . 13
⊢ ((1 / 2)
∈ ℝ+ → (1 / 2) ∈ ℝ) |
38 | | rere 13710 |
. . . . . . . . . . . . 13
⊢ ((1 / 2)
∈ ℝ → (ℜ‘(1 / 2)) = (1 / 2)) |
39 | 36, 37, 38 | mp2b 10 |
. . . . . . . . . . . 12
⊢
(ℜ‘(1 / 2)) = (1 / 2) |
40 | 39, 36 | eqeltri 2684 |
. . . . . . . . . . 11
⊢
(ℜ‘(1 / 2)) ∈ ℝ+ |
41 | | ffn 5958 |
. . . . . . . . . . . 12
⊢
(ℜ:ℂ⟶ℝ → ℜ Fn
ℂ) |
42 | | elpreima 6245 |
. . . . . . . . . . . 12
⊢ (ℜ
Fn ℂ → ((1 / 2) ∈ (◡ℜ “ ℝ+) ↔
((1 / 2) ∈ ℂ ∧ (ℜ‘(1 / 2)) ∈
ℝ+))) |
43 | 28, 41, 42 | mp2b 10 |
. . . . . . . . . . 11
⊢ ((1 / 2)
∈ (◡ℜ “
ℝ+) ↔ ((1 / 2) ∈ ℂ ∧ (ℜ‘(1 /
2)) ∈ ℝ+)) |
44 | 33, 40, 43 | mpbir2an 957 |
. . . . . . . . . 10
⊢ (1 / 2)
∈ (◡ℜ “
ℝ+) |
45 | 44 | a1i 11 |
. . . . . . . . 9
⊢ (⊤
→ (1 / 2) ∈ (◡ℜ “
ℝ+)) |
46 | 25, 32, 45 | cnmptc 21275 |
. . . . . . . 8
⊢ (⊤
→ (𝑥 ∈
(0[,)+∞) ↦ (1 / 2)) ∈ (((TopOpen‘ℂfld)
↾t (0[,)+∞)) Cn ((TopOpen‘ℂfld)
↾t (◡ℜ “
ℝ+)))) |
47 | | eqid 2610 |
. . . . . . . . . 10
⊢ (◡ℜ “ ℝ+) = (◡ℜ “
ℝ+) |
48 | | eqid 2610 |
. . . . . . . . . 10
⊢
((TopOpen‘ℂfld) ↾t
(0[,)+∞)) = ((TopOpen‘ℂfld) ↾t
(0[,)+∞)) |
49 | | eqid 2610 |
. . . . . . . . . 10
⊢
((TopOpen‘ℂfld) ↾t (◡ℜ “ ℝ+)) =
((TopOpen‘ℂfld) ↾t (◡ℜ “
ℝ+)) |
50 | 47, 21, 48, 49 | cxpcn3 24289 |
. . . . . . . . 9
⊢ (𝑦 ∈ (0[,)+∞), 𝑧 ∈ (◡ℜ “ ℝ+) ↦
(𝑦↑𝑐𝑧)) ∈
((((TopOpen‘ℂfld) ↾t (0[,)+∞))
×t ((TopOpen‘ℂfld) ↾t
(◡ℜ “ ℝ+)))
Cn (TopOpen‘ℂfld)) |
51 | 50 | a1i 11 |
. . . . . . . 8
⊢ (⊤
→ (𝑦 ∈
(0[,)+∞), 𝑧 ∈
(◡ℜ “ ℝ+)
↦ (𝑦↑𝑐𝑧)) ∈
((((TopOpen‘ℂfld) ↾t (0[,)+∞))
×t ((TopOpen‘ℂfld) ↾t
(◡ℜ “ ℝ+)))
Cn (TopOpen‘ℂfld))) |
52 | | oveq12 6558 |
. . . . . . . 8
⊢ ((𝑦 = 𝑥 ∧ 𝑧 = (1 / 2)) → (𝑦↑𝑐𝑧) = (𝑥↑𝑐(1 /
2))) |
53 | 25, 26, 46, 25, 32, 51, 52 | cnmpt12 21280 |
. . . . . . 7
⊢ (⊤
→ (𝑥 ∈
(0[,)+∞) ↦ (𝑥↑𝑐(1 / 2))) ∈
(((TopOpen‘ℂfld) ↾t (0[,)+∞)) Cn
(TopOpen‘ℂfld))) |
54 | | ssid 3587 |
. . . . . . . 8
⊢ ℂ
⊆ ℂ |
55 | 22 | toponunii 20547 |
. . . . . . . . . . . 12
⊢ ℂ =
∪
(TopOpen‘ℂfld) |
56 | 55 | restid 15917 |
. . . . . . . . . . 11
⊢
((TopOpen‘ℂfld) ∈ (TopOn‘ℂ)
→ ((TopOpen‘ℂfld) ↾t ℂ) =
(TopOpen‘ℂfld)) |
57 | 22, 56 | ax-mp 5 |
. . . . . . . . . 10
⊢
((TopOpen‘ℂfld) ↾t ℂ) =
(TopOpen‘ℂfld) |
58 | 57 | eqcomi 2619 |
. . . . . . . . 9
⊢
(TopOpen‘ℂfld) =
((TopOpen‘ℂfld) ↾t
ℂ) |
59 | 21, 48, 58 | cncfcn 22520 |
. . . . . . . 8
⊢
(((0[,)+∞) ⊆ ℂ ∧ ℂ ⊆ ℂ) →
((0[,)+∞)–cn→ℂ) =
(((TopOpen‘ℂfld) ↾t (0[,)+∞)) Cn
(TopOpen‘ℂfld))) |
60 | 8, 54, 59 | mp2an 704 |
. . . . . . 7
⊢
((0[,)+∞)–cn→ℂ) =
(((TopOpen‘ℂfld) ↾t (0[,)+∞)) Cn
(TopOpen‘ℂfld)) |
61 | 53, 60 | syl6eleqr 2699 |
. . . . . 6
⊢ (⊤
→ (𝑥 ∈
(0[,)+∞) ↦ (𝑥↑𝑐(1 / 2))) ∈
((0[,)+∞)–cn→ℂ)) |
62 | 20, 61 | syl5eqelr 2693 |
. . . . 5
⊢ (⊤
→ (𝑥 ∈
(0[,)+∞) ↦ (√‘𝑥)) ∈ ((0[,)+∞)–cn→ℂ)) |
63 | 62 | trud 1484 |
. . . 4
⊢ (𝑥 ∈ (0[,)+∞) ↦
(√‘𝑥)) ∈
((0[,)+∞)–cn→ℂ) |
64 | | cncffvrn 22509 |
. . . 4
⊢ ((ℝ
⊆ ℂ ∧ (𝑥
∈ (0[,)+∞) ↦ (√‘𝑥)) ∈ ((0[,)+∞)–cn→ℂ)) → ((𝑥 ∈ (0[,)+∞) ↦
(√‘𝑥)) ∈
((0[,)+∞)–cn→ℝ)
↔ (𝑥 ∈
(0[,)+∞) ↦ (√‘𝑥)):(0[,)+∞)⟶ℝ)) |
65 | 17, 63, 64 | mp2an 704 |
. . 3
⊢ ((𝑥 ∈ (0[,)+∞) ↦
(√‘𝑥)) ∈
((0[,)+∞)–cn→ℝ)
↔ (𝑥 ∈
(0[,)+∞) ↦ (√‘𝑥)):(0[,)+∞)⟶ℝ) |
66 | 16, 65 | mpbir 220 |
. 2
⊢ (𝑥 ∈ (0[,)+∞) ↦
(√‘𝑥)) ∈
((0[,)+∞)–cn→ℝ) |
67 | 12, 66 | eqeltri 2684 |
1
⊢ (√
↾ (0[,)+∞)) ∈ ((0[,)+∞)–cn→ℝ) |