| Step | Hyp | Ref
| Expression |
| 1 | | rge0ssre 13496 |
. . . . . . 7
⊢
(0[,)+∞) ⊆ ℝ |
| 2 | | ax-resscn 11212 |
. . . . . . 7
⊢ ℝ
⊆ ℂ |
| 3 | 1, 2 | sstri 3993 |
. . . . . 6
⊢
(0[,)+∞) ⊆ ℂ |
| 4 | 3 | sseli 3979 |
. . . . 5
⊢ (𝑥 ∈ (0[,)+∞) →
𝑥 ∈
ℂ) |
| 5 | | cxpcn3.d |
. . . . . . 7
⊢ 𝐷 = (◡ℜ “
ℝ+) |
| 6 | | cnvimass 6100 |
. . . . . . . 8
⊢ (◡ℜ “ ℝ+) ⊆
dom ℜ |
| 7 | | ref 15151 |
. . . . . . . . 9
⊢
ℜ:ℂ⟶ℝ |
| 8 | 7 | fdmi 6747 |
. . . . . . . 8
⊢ dom
ℜ = ℂ |
| 9 | 6, 8 | sseqtri 4032 |
. . . . . . 7
⊢ (◡ℜ “ ℝ+) ⊆
ℂ |
| 10 | 5, 9 | eqsstri 4030 |
. . . . . 6
⊢ 𝐷 ⊆
ℂ |
| 11 | 10 | sseli 3979 |
. . . . 5
⊢ (𝑦 ∈ 𝐷 → 𝑦 ∈ ℂ) |
| 12 | | cxpcl 26716 |
. . . . 5
⊢ ((𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ) → (𝑥↑𝑐𝑦) ∈
ℂ) |
| 13 | 4, 11, 12 | syl2an 596 |
. . . 4
⊢ ((𝑥 ∈ (0[,)+∞) ∧
𝑦 ∈ 𝐷) → (𝑥↑𝑐𝑦) ∈ ℂ) |
| 14 | 13 | rgen2 3199 |
. . 3
⊢
∀𝑥 ∈
(0[,)+∞)∀𝑦
∈ 𝐷 (𝑥↑𝑐𝑦) ∈
ℂ |
| 15 | | eqid 2737 |
. . . 4
⊢ (𝑥 ∈ (0[,)+∞), 𝑦 ∈ 𝐷 ↦ (𝑥↑𝑐𝑦)) = (𝑥 ∈ (0[,)+∞), 𝑦 ∈ 𝐷 ↦ (𝑥↑𝑐𝑦)) |
| 16 | 15 | fmpo 8093 |
. . 3
⊢
(∀𝑥 ∈
(0[,)+∞)∀𝑦
∈ 𝐷 (𝑥↑𝑐𝑦) ∈ ℂ ↔ (𝑥 ∈ (0[,)+∞), 𝑦 ∈ 𝐷 ↦ (𝑥↑𝑐𝑦)):((0[,)+∞) × 𝐷)⟶ℂ) |
| 17 | 14, 16 | mpbi 230 |
. 2
⊢ (𝑥 ∈ (0[,)+∞), 𝑦 ∈ 𝐷 ↦ (𝑥↑𝑐𝑦)):((0[,)+∞) × 𝐷)⟶ℂ |
| 18 | | cxpcn3.j |
. . . . . . . . . . . 12
⊢ 𝐽 =
(TopOpen‘ℂfld) |
| 19 | 18 | cnfldtopon 24803 |
. . . . . . . . . . 11
⊢ 𝐽 ∈
(TopOn‘ℂ) |
| 20 | | rpre 13043 |
. . . . . . . . . . . . . 14
⊢ (𝑥 ∈ ℝ+
→ 𝑥 ∈
ℝ) |
| 21 | | rpge0 13048 |
. . . . . . . . . . . . . 14
⊢ (𝑥 ∈ ℝ+
→ 0 ≤ 𝑥) |
| 22 | | elrege0 13494 |
. . . . . . . . . . . . . 14
⊢ (𝑥 ∈ (0[,)+∞) ↔
(𝑥 ∈ ℝ ∧ 0
≤ 𝑥)) |
| 23 | 20, 21, 22 | sylanbrc 583 |
. . . . . . . . . . . . 13
⊢ (𝑥 ∈ ℝ+
→ 𝑥 ∈
(0[,)+∞)) |
| 24 | 23 | ssriv 3987 |
. . . . . . . . . . . 12
⊢
ℝ+ ⊆ (0[,)+∞) |
| 25 | 24, 3 | sstri 3993 |
. . . . . . . . . . 11
⊢
ℝ+ ⊆ ℂ |
| 26 | | resttopon 23169 |
. . . . . . . . . . 11
⊢ ((𝐽 ∈ (TopOn‘ℂ)
∧ ℝ+ ⊆ ℂ) → (𝐽 ↾t ℝ+)
∈ (TopOn‘ℝ+)) |
| 27 | 19, 25, 26 | mp2an 692 |
. . . . . . . . . 10
⊢ (𝐽 ↾t
ℝ+) ∈ (TopOn‘ℝ+) |
| 28 | 27 | toponrestid 22927 |
. . . . . . . . 9
⊢ (𝐽 ↾t
ℝ+) = ((𝐽
↾t ℝ+) ↾t
ℝ+) |
| 29 | 27 | a1i 11 |
. . . . . . . . 9
⊢ (((𝑢 ∈ (0[,)+∞) ∧
𝑣 ∈ 𝐷) ∧ 0 < 𝑢) → (𝐽 ↾t ℝ+)
∈ (TopOn‘ℝ+)) |
| 30 | | ssid 4006 |
. . . . . . . . . 10
⊢
ℝ+ ⊆ ℝ+ |
| 31 | 30 | a1i 11 |
. . . . . . . . 9
⊢ (((𝑢 ∈ (0[,)+∞) ∧
𝑣 ∈ 𝐷) ∧ 0 < 𝑢) → ℝ+ ⊆
ℝ+) |
| 32 | | cxpcn3.l |
. . . . . . . . 9
⊢ 𝐿 = (𝐽 ↾t 𝐷) |
| 33 | 19 | a1i 11 |
. . . . . . . . 9
⊢ (((𝑢 ∈ (0[,)+∞) ∧
𝑣 ∈ 𝐷) ∧ 0 < 𝑢) → 𝐽 ∈
(TopOn‘ℂ)) |
| 34 | 10 | a1i 11 |
. . . . . . . . 9
⊢ (((𝑢 ∈ (0[,)+∞) ∧
𝑣 ∈ 𝐷) ∧ 0 < 𝑢) → 𝐷 ⊆ ℂ) |
| 35 | | eqid 2737 |
. . . . . . . . . . 11
⊢ (𝐽 ↾t
ℝ+) = (𝐽
↾t ℝ+) |
| 36 | 18, 35 | cxpcn2 26789 |
. . . . . . . . . 10
⊢ (𝑥 ∈ ℝ+,
𝑦 ∈ ℂ ↦
(𝑥↑𝑐𝑦)) ∈ (((𝐽 ↾t ℝ+)
×t 𝐽) Cn
𝐽) |
| 37 | 36 | a1i 11 |
. . . . . . . . 9
⊢ (((𝑢 ∈ (0[,)+∞) ∧
𝑣 ∈ 𝐷) ∧ 0 < 𝑢) → (𝑥 ∈ ℝ+, 𝑦 ∈ ℂ ↦ (𝑥↑𝑐𝑦)) ∈ (((𝐽 ↾t ℝ+)
×t 𝐽) Cn
𝐽)) |
| 38 | 28, 29, 31, 32, 33, 34, 37 | cnmpt2res 23685 |
. . . . . . . 8
⊢ (((𝑢 ∈ (0[,)+∞) ∧
𝑣 ∈ 𝐷) ∧ 0 < 𝑢) → (𝑥 ∈ ℝ+, 𝑦 ∈ 𝐷 ↦ (𝑥↑𝑐𝑦)) ∈ (((𝐽 ↾t ℝ+)
×t 𝐿) Cn
𝐽)) |
| 39 | | elrege0 13494 |
. . . . . . . . . . . . 13
⊢ (𝑢 ∈ (0[,)+∞) ↔
(𝑢 ∈ ℝ ∧ 0
≤ 𝑢)) |
| 40 | 39 | simplbi 497 |
. . . . . . . . . . . 12
⊢ (𝑢 ∈ (0[,)+∞) →
𝑢 ∈
ℝ) |
| 41 | 40 | adantr 480 |
. . . . . . . . . . 11
⊢ ((𝑢 ∈ (0[,)+∞) ∧
𝑣 ∈ 𝐷) → 𝑢 ∈ ℝ) |
| 42 | 41 | adantr 480 |
. . . . . . . . . 10
⊢ (((𝑢 ∈ (0[,)+∞) ∧
𝑣 ∈ 𝐷) ∧ 0 < 𝑢) → 𝑢 ∈ ℝ) |
| 43 | | simpr 484 |
. . . . . . . . . 10
⊢ (((𝑢 ∈ (0[,)+∞) ∧
𝑣 ∈ 𝐷) ∧ 0 < 𝑢) → 0 < 𝑢) |
| 44 | 42, 43 | elrpd 13074 |
. . . . . . . . 9
⊢ (((𝑢 ∈ (0[,)+∞) ∧
𝑣 ∈ 𝐷) ∧ 0 < 𝑢) → 𝑢 ∈ ℝ+) |
| 45 | | simplr 769 |
. . . . . . . . 9
⊢ (((𝑢 ∈ (0[,)+∞) ∧
𝑣 ∈ 𝐷) ∧ 0 < 𝑢) → 𝑣 ∈ 𝐷) |
| 46 | 44, 45 | opelxpd 5724 |
. . . . . . . 8
⊢ (((𝑢 ∈ (0[,)+∞) ∧
𝑣 ∈ 𝐷) ∧ 0 < 𝑢) → 〈𝑢, 𝑣〉 ∈ (ℝ+ ×
𝐷)) |
| 47 | | resttopon 23169 |
. . . . . . . . . . . . 13
⊢ ((𝐽 ∈ (TopOn‘ℂ)
∧ 𝐷 ⊆ ℂ)
→ (𝐽
↾t 𝐷)
∈ (TopOn‘𝐷)) |
| 48 | 19, 10, 47 | mp2an 692 |
. . . . . . . . . . . 12
⊢ (𝐽 ↾t 𝐷) ∈ (TopOn‘𝐷) |
| 49 | 32, 48 | eqeltri 2837 |
. . . . . . . . . . 11
⊢ 𝐿 ∈ (TopOn‘𝐷) |
| 50 | | txtopon 23599 |
. . . . . . . . . . 11
⊢ (((𝐽 ↾t
ℝ+) ∈ (TopOn‘ℝ+) ∧ 𝐿 ∈ (TopOn‘𝐷)) → ((𝐽 ↾t ℝ+)
×t 𝐿)
∈ (TopOn‘(ℝ+ × 𝐷))) |
| 51 | 27, 49, 50 | mp2an 692 |
. . . . . . . . . 10
⊢ ((𝐽 ↾t
ℝ+) ×t 𝐿) ∈ (TopOn‘(ℝ+
× 𝐷)) |
| 52 | 51 | toponunii 22922 |
. . . . . . . . 9
⊢
(ℝ+ × 𝐷) = ∪ ((𝐽 ↾t
ℝ+) ×t 𝐿) |
| 53 | 52 | cncnpi 23286 |
. . . . . . . 8
⊢ (((𝑥 ∈ ℝ+,
𝑦 ∈ 𝐷 ↦ (𝑥↑𝑐𝑦)) ∈ (((𝐽 ↾t ℝ+)
×t 𝐿) Cn
𝐽) ∧ 〈𝑢, 𝑣〉 ∈ (ℝ+ ×
𝐷)) → (𝑥 ∈ ℝ+,
𝑦 ∈ 𝐷 ↦ (𝑥↑𝑐𝑦)) ∈ ((((𝐽 ↾t ℝ+)
×t 𝐿) CnP
𝐽)‘〈𝑢, 𝑣〉)) |
| 54 | 38, 46, 53 | syl2anc 584 |
. . . . . . 7
⊢ (((𝑢 ∈ (0[,)+∞) ∧
𝑣 ∈ 𝐷) ∧ 0 < 𝑢) → (𝑥 ∈ ℝ+, 𝑦 ∈ 𝐷 ↦ (𝑥↑𝑐𝑦)) ∈ ((((𝐽 ↾t ℝ+)
×t 𝐿) CnP
𝐽)‘〈𝑢, 𝑣〉)) |
| 55 | | ssid 4006 |
. . . . . . . 8
⊢ 𝐷 ⊆ 𝐷 |
| 56 | | resmpo 7553 |
. . . . . . . 8
⊢
((ℝ+ ⊆ (0[,)+∞) ∧ 𝐷 ⊆ 𝐷) → ((𝑥 ∈ (0[,)+∞), 𝑦 ∈ 𝐷 ↦ (𝑥↑𝑐𝑦)) ↾ (ℝ+ × 𝐷)) = (𝑥 ∈ ℝ+, 𝑦 ∈ 𝐷 ↦ (𝑥↑𝑐𝑦))) |
| 57 | 24, 55, 56 | mp2an 692 |
. . . . . . 7
⊢ ((𝑥 ∈ (0[,)+∞), 𝑦 ∈ 𝐷 ↦ (𝑥↑𝑐𝑦)) ↾ (ℝ+ × 𝐷)) = (𝑥 ∈ ℝ+, 𝑦 ∈ 𝐷 ↦ (𝑥↑𝑐𝑦)) |
| 58 | | cxpcn3.k |
. . . . . . . . . . . 12
⊢ 𝐾 = (𝐽 ↾t
(0[,)+∞)) |
| 59 | | resttopon 23169 |
. . . . . . . . . . . . 13
⊢ ((𝐽 ∈ (TopOn‘ℂ)
∧ (0[,)+∞) ⊆ ℂ) → (𝐽 ↾t (0[,)+∞)) ∈
(TopOn‘(0[,)+∞))) |
| 60 | 19, 3, 59 | mp2an 692 |
. . . . . . . . . . . 12
⊢ (𝐽 ↾t
(0[,)+∞)) ∈ (TopOn‘(0[,)+∞)) |
| 61 | 58, 60 | eqeltri 2837 |
. . . . . . . . . . 11
⊢ 𝐾 ∈
(TopOn‘(0[,)+∞)) |
| 62 | | ioorp 13465 |
. . . . . . . . . . . . . 14
⊢
(0(,)+∞) = ℝ+ |
| 63 | | iooretop 24786 |
. . . . . . . . . . . . . 14
⊢
(0(,)+∞) ∈ (topGen‘ran (,)) |
| 64 | 62, 63 | eqeltrri 2838 |
. . . . . . . . . . . . 13
⊢
ℝ+ ∈ (topGen‘ran (,)) |
| 65 | | retop 24782 |
. . . . . . . . . . . . . . 15
⊢
(topGen‘ran (,)) ∈ Top |
| 66 | | ovex 7464 |
. . . . . . . . . . . . . . 15
⊢
(0[,)+∞) ∈ V |
| 67 | | restopnb 23183 |
. . . . . . . . . . . . . . 15
⊢
((((topGen‘ran (,)) ∈ Top ∧ (0[,)+∞) ∈ V)
∧ (ℝ+ ∈ (topGen‘ran (,)) ∧
ℝ+ ⊆ (0[,)+∞) ∧ ℝ+ ⊆
ℝ+)) → (ℝ+ ∈ (topGen‘ran (,))
↔ ℝ+ ∈ ((topGen‘ran (,)) ↾t
(0[,)+∞)))) |
| 68 | 65, 66, 67 | mpanl12 702 |
. . . . . . . . . . . . . 14
⊢
((ℝ+ ∈ (topGen‘ran (,)) ∧
ℝ+ ⊆ (0[,)+∞) ∧ ℝ+ ⊆
ℝ+) → (ℝ+ ∈ (topGen‘ran (,))
↔ ℝ+ ∈ ((topGen‘ran (,)) ↾t
(0[,)+∞)))) |
| 69 | 64, 24, 30, 68 | mp3an 1463 |
. . . . . . . . . . . . 13
⊢
(ℝ+ ∈ (topGen‘ran (,)) ↔
ℝ+ ∈ ((topGen‘ran (,)) ↾t
(0[,)+∞))) |
| 70 | 64, 69 | mpbi 230 |
. . . . . . . . . . . 12
⊢
ℝ+ ∈ ((topGen‘ran (,)) ↾t
(0[,)+∞)) |
| 71 | | eqid 2737 |
. . . . . . . . . . . . . . 15
⊢
(topGen‘ran (,)) = (topGen‘ran (,)) |
| 72 | 18, 71 | rerest 24825 |
. . . . . . . . . . . . . 14
⊢
((0[,)+∞) ⊆ ℝ → (𝐽 ↾t (0[,)+∞)) =
((topGen‘ran (,)) ↾t (0[,)+∞))) |
| 73 | 1, 72 | ax-mp 5 |
. . . . . . . . . . . . 13
⊢ (𝐽 ↾t
(0[,)+∞)) = ((topGen‘ran (,)) ↾t
(0[,)+∞)) |
| 74 | 58, 73 | eqtri 2765 |
. . . . . . . . . . . 12
⊢ 𝐾 = ((topGen‘ran (,))
↾t (0[,)+∞)) |
| 75 | 70, 74 | eleqtrri 2840 |
. . . . . . . . . . 11
⊢
ℝ+ ∈ 𝐾 |
| 76 | | toponmax 22932 |
. . . . . . . . . . . 12
⊢ (𝐿 ∈ (TopOn‘𝐷) → 𝐷 ∈ 𝐿) |
| 77 | 49, 76 | ax-mp 5 |
. . . . . . . . . . 11
⊢ 𝐷 ∈ 𝐿 |
| 78 | | txrest 23639 |
. . . . . . . . . . 11
⊢ (((𝐾 ∈
(TopOn‘(0[,)+∞)) ∧ 𝐿 ∈ (TopOn‘𝐷)) ∧ (ℝ+ ∈ 𝐾 ∧ 𝐷 ∈ 𝐿)) → ((𝐾 ×t 𝐿) ↾t (ℝ+
× 𝐷)) = ((𝐾 ↾t
ℝ+) ×t (𝐿 ↾t 𝐷))) |
| 79 | 61, 49, 75, 77, 78 | mp4an 693 |
. . . . . . . . . 10
⊢ ((𝐾 ×t 𝐿) ↾t
(ℝ+ × 𝐷)) = ((𝐾 ↾t ℝ+)
×t (𝐿
↾t 𝐷)) |
| 80 | 58 | oveq1i 7441 |
. . . . . . . . . . . 12
⊢ (𝐾 ↾t
ℝ+) = ((𝐽
↾t (0[,)+∞)) ↾t
ℝ+) |
| 81 | | restabs 23173 |
. . . . . . . . . . . . 13
⊢ ((𝐽 ∈ (TopOn‘ℂ)
∧ ℝ+ ⊆ (0[,)+∞) ∧ (0[,)+∞) ∈ V)
→ ((𝐽
↾t (0[,)+∞)) ↾t ℝ+) =
(𝐽 ↾t
ℝ+)) |
| 82 | 19, 24, 66, 81 | mp3an 1463 |
. . . . . . . . . . . 12
⊢ ((𝐽 ↾t
(0[,)+∞)) ↾t ℝ+) = (𝐽 ↾t
ℝ+) |
| 83 | 80, 82 | eqtri 2765 |
. . . . . . . . . . 11
⊢ (𝐾 ↾t
ℝ+) = (𝐽
↾t ℝ+) |
| 84 | 49 | toponunii 22922 |
. . . . . . . . . . . . 13
⊢ 𝐷 = ∪
𝐿 |
| 85 | 84 | restid 17478 |
. . . . . . . . . . . 12
⊢ (𝐿 ∈ (TopOn‘𝐷) → (𝐿 ↾t 𝐷) = 𝐿) |
| 86 | 49, 85 | ax-mp 5 |
. . . . . . . . . . 11
⊢ (𝐿 ↾t 𝐷) = 𝐿 |
| 87 | 83, 86 | oveq12i 7443 |
. . . . . . . . . 10
⊢ ((𝐾 ↾t
ℝ+) ×t (𝐿 ↾t 𝐷)) = ((𝐽 ↾t ℝ+)
×t 𝐿) |
| 88 | 79, 87 | eqtri 2765 |
. . . . . . . . 9
⊢ ((𝐾 ×t 𝐿) ↾t
(ℝ+ × 𝐷)) = ((𝐽 ↾t ℝ+)
×t 𝐿) |
| 89 | 88 | oveq1i 7441 |
. . . . . . . 8
⊢ (((𝐾 ×t 𝐿) ↾t
(ℝ+ × 𝐷)) CnP 𝐽) = (((𝐽 ↾t ℝ+)
×t 𝐿) CnP
𝐽) |
| 90 | 89 | fveq1i 6907 |
. . . . . . 7
⊢ ((((𝐾 ×t 𝐿) ↾t
(ℝ+ × 𝐷)) CnP 𝐽)‘〈𝑢, 𝑣〉) = ((((𝐽 ↾t ℝ+)
×t 𝐿) CnP
𝐽)‘〈𝑢, 𝑣〉) |
| 91 | 54, 57, 90 | 3eltr4g 2858 |
. . . . . 6
⊢ (((𝑢 ∈ (0[,)+∞) ∧
𝑣 ∈ 𝐷) ∧ 0 < 𝑢) → ((𝑥 ∈ (0[,)+∞), 𝑦 ∈ 𝐷 ↦ (𝑥↑𝑐𝑦)) ↾ (ℝ+ × 𝐷)) ∈ ((((𝐾 ×t 𝐿) ↾t (ℝ+
× 𝐷)) CnP 𝐽)‘〈𝑢, 𝑣〉)) |
| 92 | | txtopon 23599 |
. . . . . . . . . 10
⊢ ((𝐾 ∈
(TopOn‘(0[,)+∞)) ∧ 𝐿 ∈ (TopOn‘𝐷)) → (𝐾 ×t 𝐿) ∈ (TopOn‘((0[,)+∞)
× 𝐷))) |
| 93 | 61, 49, 92 | mp2an 692 |
. . . . . . . . 9
⊢ (𝐾 ×t 𝐿) ∈
(TopOn‘((0[,)+∞) × 𝐷)) |
| 94 | 93 | topontopi 22921 |
. . . . . . . 8
⊢ (𝐾 ×t 𝐿) ∈ Top |
| 95 | 94 | a1i 11 |
. . . . . . 7
⊢ (((𝑢 ∈ (0[,)+∞) ∧
𝑣 ∈ 𝐷) ∧ 0 < 𝑢) → (𝐾 ×t 𝐿) ∈ Top) |
| 96 | | xpss1 5704 |
. . . . . . . 8
⊢
(ℝ+ ⊆ (0[,)+∞) → (ℝ+
× 𝐷) ⊆
((0[,)+∞) × 𝐷)) |
| 97 | 24, 96 | mp1i 13 |
. . . . . . 7
⊢ (((𝑢 ∈ (0[,)+∞) ∧
𝑣 ∈ 𝐷) ∧ 0 < 𝑢) → (ℝ+ × 𝐷) ⊆ ((0[,)+∞)
× 𝐷)) |
| 98 | | txopn 23610 |
. . . . . . . . . 10
⊢ (((𝐾 ∈
(TopOn‘(0[,)+∞)) ∧ 𝐿 ∈ (TopOn‘𝐷)) ∧ (ℝ+ ∈ 𝐾 ∧ 𝐷 ∈ 𝐿)) → (ℝ+ × 𝐷) ∈ (𝐾 ×t 𝐿)) |
| 99 | 61, 49, 75, 77, 98 | mp4an 693 |
. . . . . . . . 9
⊢
(ℝ+ × 𝐷) ∈ (𝐾 ×t 𝐿) |
| 100 | | isopn3i 23090 |
. . . . . . . . 9
⊢ (((𝐾 ×t 𝐿) ∈ Top ∧
(ℝ+ × 𝐷) ∈ (𝐾 ×t 𝐿)) → ((int‘(𝐾 ×t 𝐿))‘(ℝ+ × 𝐷)) = (ℝ+
× 𝐷)) |
| 101 | 94, 99, 100 | mp2an 692 |
. . . . . . . 8
⊢
((int‘(𝐾
×t 𝐿))‘(ℝ+ × 𝐷)) = (ℝ+
× 𝐷) |
| 102 | 46, 101 | eleqtrrdi 2852 |
. . . . . . 7
⊢ (((𝑢 ∈ (0[,)+∞) ∧
𝑣 ∈ 𝐷) ∧ 0 < 𝑢) → 〈𝑢, 𝑣〉 ∈ ((int‘(𝐾 ×t 𝐿))‘(ℝ+ × 𝐷))) |
| 103 | 17 | a1i 11 |
. . . . . . 7
⊢ (((𝑢 ∈ (0[,)+∞) ∧
𝑣 ∈ 𝐷) ∧ 0 < 𝑢) → (𝑥 ∈ (0[,)+∞), 𝑦 ∈ 𝐷 ↦ (𝑥↑𝑐𝑦)):((0[,)+∞) × 𝐷)⟶ℂ) |
| 104 | 61 | topontopi 22921 |
. . . . . . . . 9
⊢ 𝐾 ∈ Top |
| 105 | 49 | topontopi 22921 |
. . . . . . . . 9
⊢ 𝐿 ∈ Top |
| 106 | 61 | toponunii 22922 |
. . . . . . . . 9
⊢
(0[,)+∞) = ∪ 𝐾 |
| 107 | 104, 105,
106, 84 | txunii 23601 |
. . . . . . . 8
⊢
((0[,)+∞) × 𝐷) = ∪ (𝐾 ×t 𝐿) |
| 108 | 19 | toponunii 22922 |
. . . . . . . 8
⊢ ℂ =
∪ 𝐽 |
| 109 | 107, 108 | cnprest 23297 |
. . . . . . 7
⊢ ((((𝐾 ×t 𝐿) ∈ Top ∧
(ℝ+ × 𝐷) ⊆ ((0[,)+∞) × 𝐷)) ∧ (〈𝑢, 𝑣〉 ∈ ((int‘(𝐾 ×t 𝐿))‘(ℝ+ × 𝐷)) ∧ (𝑥 ∈ (0[,)+∞), 𝑦 ∈ 𝐷 ↦ (𝑥↑𝑐𝑦)):((0[,)+∞) × 𝐷)⟶ℂ)) → ((𝑥 ∈ (0[,)+∞), 𝑦 ∈ 𝐷 ↦ (𝑥↑𝑐𝑦)) ∈ (((𝐾 ×t 𝐿) CnP 𝐽)‘〈𝑢, 𝑣〉) ↔ ((𝑥 ∈ (0[,)+∞), 𝑦 ∈ 𝐷 ↦ (𝑥↑𝑐𝑦)) ↾ (ℝ+ × 𝐷)) ∈ ((((𝐾 ×t 𝐿) ↾t (ℝ+
× 𝐷)) CnP 𝐽)‘〈𝑢, 𝑣〉))) |
| 110 | 95, 97, 102, 103, 109 | syl22anc 839 |
. . . . . 6
⊢ (((𝑢 ∈ (0[,)+∞) ∧
𝑣 ∈ 𝐷) ∧ 0 < 𝑢) → ((𝑥 ∈ (0[,)+∞), 𝑦 ∈ 𝐷 ↦ (𝑥↑𝑐𝑦)) ∈ (((𝐾 ×t 𝐿) CnP 𝐽)‘〈𝑢, 𝑣〉) ↔ ((𝑥 ∈ (0[,)+∞), 𝑦 ∈ 𝐷 ↦ (𝑥↑𝑐𝑦)) ↾ (ℝ+ × 𝐷)) ∈ ((((𝐾 ×t 𝐿) ↾t (ℝ+
× 𝐷)) CnP 𝐽)‘〈𝑢, 𝑣〉))) |
| 111 | 91, 110 | mpbird 257 |
. . . . 5
⊢ (((𝑢 ∈ (0[,)+∞) ∧
𝑣 ∈ 𝐷) ∧ 0 < 𝑢) → (𝑥 ∈ (0[,)+∞), 𝑦 ∈ 𝐷 ↦ (𝑥↑𝑐𝑦)) ∈ (((𝐾 ×t 𝐿) CnP 𝐽)‘〈𝑢, 𝑣〉)) |
| 112 | 17 | a1i 11 |
. . . . . . . 8
⊢ (𝑣 ∈ 𝐷 → (𝑥 ∈ (0[,)+∞), 𝑦 ∈ 𝐷 ↦ (𝑥↑𝑐𝑦)):((0[,)+∞) × 𝐷)⟶ℂ) |
| 113 | | eqid 2737 |
. . . . . . . . . . 11
⊢
(if((ℜ‘𝑣)
≤ 1, (ℜ‘𝑣),
1) / 2) = (if((ℜ‘𝑣) ≤ 1, (ℜ‘𝑣), 1) / 2) |
| 114 | | eqid 2737 |
. . . . . . . . . . 11
⊢
if((if((ℜ‘𝑣) ≤ 1, (ℜ‘𝑣), 1) / 2) ≤ (𝑒↑𝑐(1 /
(if((ℜ‘𝑣) ≤
1, (ℜ‘𝑣), 1) /
2))), (if((ℜ‘𝑣)
≤ 1, (ℜ‘𝑣),
1) / 2), (𝑒↑𝑐(1 /
(if((ℜ‘𝑣) ≤
1, (ℜ‘𝑣), 1) /
2)))) = if((if((ℜ‘𝑣) ≤ 1, (ℜ‘𝑣), 1) / 2) ≤ (𝑒↑𝑐(1 /
(if((ℜ‘𝑣) ≤
1, (ℜ‘𝑣), 1) /
2))), (if((ℜ‘𝑣)
≤ 1, (ℜ‘𝑣),
1) / 2), (𝑒↑𝑐(1 /
(if((ℜ‘𝑣) ≤
1, (ℜ‘𝑣), 1) /
2)))) |
| 115 | 5, 18, 58, 32, 113, 114 | cxpcn3lem 26790 |
. . . . . . . . . 10
⊢ ((𝑣 ∈ 𝐷 ∧ 𝑒 ∈ ℝ+) →
∃𝑑 ∈
ℝ+ ∀𝑎 ∈ (0[,)+∞)∀𝑏 ∈ 𝐷 (((abs‘𝑎) < 𝑑 ∧ (abs‘(𝑣 − 𝑏)) < 𝑑) → (abs‘(𝑎↑𝑐𝑏)) < 𝑒)) |
| 116 | 115 | ralrimiva 3146 |
. . . . . . . . 9
⊢ (𝑣 ∈ 𝐷 → ∀𝑒 ∈ ℝ+ ∃𝑑 ∈ ℝ+
∀𝑎 ∈
(0[,)+∞)∀𝑏
∈ 𝐷 (((abs‘𝑎) < 𝑑 ∧ (abs‘(𝑣 − 𝑏)) < 𝑑) → (abs‘(𝑎↑𝑐𝑏)) < 𝑒)) |
| 117 | | 0e0icopnf 13498 |
. . . . . . . . . . . . . . . . . 18
⊢ 0 ∈
(0[,)+∞) |
| 118 | 117 | a1i 11 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑣 ∈ 𝐷 ∧ (𝑎 ∈ (0[,)+∞) ∧ 𝑏 ∈ 𝐷)) → 0 ∈
(0[,)+∞)) |
| 119 | | simprl 771 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑣 ∈ 𝐷 ∧ (𝑎 ∈ (0[,)+∞) ∧ 𝑏 ∈ 𝐷)) → 𝑎 ∈ (0[,)+∞)) |
| 120 | 118, 119 | ovresd 7600 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑣 ∈ 𝐷 ∧ (𝑎 ∈ (0[,)+∞) ∧ 𝑏 ∈ 𝐷)) → (0((abs ∘ − ) ↾
((0[,)+∞) × (0[,)+∞)))𝑎) = (0(abs ∘ − )𝑎)) |
| 121 | | 0cn 11253 |
. . . . . . . . . . . . . . . . 17
⊢ 0 ∈
ℂ |
| 122 | 3, 119 | sselid 3981 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑣 ∈ 𝐷 ∧ (𝑎 ∈ (0[,)+∞) ∧ 𝑏 ∈ 𝐷)) → 𝑎 ∈ ℂ) |
| 123 | | eqid 2737 |
. . . . . . . . . . . . . . . . . 18
⊢ (abs
∘ − ) = (abs ∘ − ) |
| 124 | 123 | cnmetdval 24791 |
. . . . . . . . . . . . . . . . 17
⊢ ((0
∈ ℂ ∧ 𝑎
∈ ℂ) → (0(abs ∘ − )𝑎) = (abs‘(0 − 𝑎))) |
| 125 | 121, 122,
124 | sylancr 587 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑣 ∈ 𝐷 ∧ (𝑎 ∈ (0[,)+∞) ∧ 𝑏 ∈ 𝐷)) → (0(abs ∘ − )𝑎) = (abs‘(0 − 𝑎))) |
| 126 | | df-neg 11495 |
. . . . . . . . . . . . . . . . . 18
⊢ -𝑎 = (0 − 𝑎) |
| 127 | 126 | fveq2i 6909 |
. . . . . . . . . . . . . . . . 17
⊢
(abs‘-𝑎) =
(abs‘(0 − 𝑎)) |
| 128 | 122 | absnegd 15488 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑣 ∈ 𝐷 ∧ (𝑎 ∈ (0[,)+∞) ∧ 𝑏 ∈ 𝐷)) → (abs‘-𝑎) = (abs‘𝑎)) |
| 129 | 127, 128 | eqtr3id 2791 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑣 ∈ 𝐷 ∧ (𝑎 ∈ (0[,)+∞) ∧ 𝑏 ∈ 𝐷)) → (abs‘(0 − 𝑎)) = (abs‘𝑎)) |
| 130 | 120, 125,
129 | 3eqtrd 2781 |
. . . . . . . . . . . . . . 15
⊢ ((𝑣 ∈ 𝐷 ∧ (𝑎 ∈ (0[,)+∞) ∧ 𝑏 ∈ 𝐷)) → (0((abs ∘ − ) ↾
((0[,)+∞) × (0[,)+∞)))𝑎) = (abs‘𝑎)) |
| 131 | 130 | breq1d 5153 |
. . . . . . . . . . . . . 14
⊢ ((𝑣 ∈ 𝐷 ∧ (𝑎 ∈ (0[,)+∞) ∧ 𝑏 ∈ 𝐷)) → ((0((abs ∘ − ) ↾
((0[,)+∞) × (0[,)+∞)))𝑎) < 𝑑 ↔ (abs‘𝑎) < 𝑑)) |
| 132 | | simpl 482 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑣 ∈ 𝐷 ∧ (𝑎 ∈ (0[,)+∞) ∧ 𝑏 ∈ 𝐷)) → 𝑣 ∈ 𝐷) |
| 133 | | simprr 773 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑣 ∈ 𝐷 ∧ (𝑎 ∈ (0[,)+∞) ∧ 𝑏 ∈ 𝐷)) → 𝑏 ∈ 𝐷) |
| 134 | 132, 133 | ovresd 7600 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑣 ∈ 𝐷 ∧ (𝑎 ∈ (0[,)+∞) ∧ 𝑏 ∈ 𝐷)) → (𝑣((abs ∘ − ) ↾ (𝐷 × 𝐷))𝑏) = (𝑣(abs ∘ − )𝑏)) |
| 135 | 10, 132 | sselid 3981 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑣 ∈ 𝐷 ∧ (𝑎 ∈ (0[,)+∞) ∧ 𝑏 ∈ 𝐷)) → 𝑣 ∈ ℂ) |
| 136 | 10, 133 | sselid 3981 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑣 ∈ 𝐷 ∧ (𝑎 ∈ (0[,)+∞) ∧ 𝑏 ∈ 𝐷)) → 𝑏 ∈ ℂ) |
| 137 | 123 | cnmetdval 24791 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑣 ∈ ℂ ∧ 𝑏 ∈ ℂ) → (𝑣(abs ∘ − )𝑏) = (abs‘(𝑣 − 𝑏))) |
| 138 | 135, 136,
137 | syl2anc 584 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑣 ∈ 𝐷 ∧ (𝑎 ∈ (0[,)+∞) ∧ 𝑏 ∈ 𝐷)) → (𝑣(abs ∘ − )𝑏) = (abs‘(𝑣 − 𝑏))) |
| 139 | 134, 138 | eqtrd 2777 |
. . . . . . . . . . . . . . 15
⊢ ((𝑣 ∈ 𝐷 ∧ (𝑎 ∈ (0[,)+∞) ∧ 𝑏 ∈ 𝐷)) → (𝑣((abs ∘ − ) ↾ (𝐷 × 𝐷))𝑏) = (abs‘(𝑣 − 𝑏))) |
| 140 | 139 | breq1d 5153 |
. . . . . . . . . . . . . 14
⊢ ((𝑣 ∈ 𝐷 ∧ (𝑎 ∈ (0[,)+∞) ∧ 𝑏 ∈ 𝐷)) → ((𝑣((abs ∘ − ) ↾ (𝐷 × 𝐷))𝑏) < 𝑑 ↔ (abs‘(𝑣 − 𝑏)) < 𝑑)) |
| 141 | 131, 140 | anbi12d 632 |
. . . . . . . . . . . . 13
⊢ ((𝑣 ∈ 𝐷 ∧ (𝑎 ∈ (0[,)+∞) ∧ 𝑏 ∈ 𝐷)) → (((0((abs ∘ − )
↾ ((0[,)+∞) × (0[,)+∞)))𝑎) < 𝑑 ∧ (𝑣((abs ∘ − ) ↾ (𝐷 × 𝐷))𝑏) < 𝑑) ↔ ((abs‘𝑎) < 𝑑 ∧ (abs‘(𝑣 − 𝑏)) < 𝑑))) |
| 142 | | oveq12 7440 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑥 = 0 ∧ 𝑦 = 𝑣) → (𝑥↑𝑐𝑦) = (0↑𝑐𝑣)) |
| 143 | | ovex 7464 |
. . . . . . . . . . . . . . . . . . 19
⊢
(0↑𝑐𝑣) ∈ V |
| 144 | 142, 15, 143 | ovmpoa 7588 |
. . . . . . . . . . . . . . . . . 18
⊢ ((0
∈ (0[,)+∞) ∧ 𝑣 ∈ 𝐷) → (0(𝑥 ∈ (0[,)+∞), 𝑦 ∈ 𝐷 ↦ (𝑥↑𝑐𝑦))𝑣) = (0↑𝑐𝑣)) |
| 145 | 117, 132,
144 | sylancr 587 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑣 ∈ 𝐷 ∧ (𝑎 ∈ (0[,)+∞) ∧ 𝑏 ∈ 𝐷)) → (0(𝑥 ∈ (0[,)+∞), 𝑦 ∈ 𝐷 ↦ (𝑥↑𝑐𝑦))𝑣) = (0↑𝑐𝑣)) |
| 146 | 5 | eleq2i 2833 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑣 ∈ 𝐷 ↔ 𝑣 ∈ (◡ℜ “
ℝ+)) |
| 147 | | ffn 6736 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
(ℜ:ℂ⟶ℝ → ℜ Fn
ℂ) |
| 148 | | elpreima 7078 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (ℜ
Fn ℂ → (𝑣 ∈
(◡ℜ “ ℝ+)
↔ (𝑣 ∈ ℂ
∧ (ℜ‘𝑣)
∈ ℝ+))) |
| 149 | 7, 147, 148 | mp2b 10 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑣 ∈ (◡ℜ “ ℝ+) ↔
(𝑣 ∈ ℂ ∧
(ℜ‘𝑣) ∈
ℝ+)) |
| 150 | 146, 149 | bitri 275 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑣 ∈ 𝐷 ↔ (𝑣 ∈ ℂ ∧ (ℜ‘𝑣) ∈
ℝ+)) |
| 151 | 150 | simplbi 497 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑣 ∈ 𝐷 → 𝑣 ∈ ℂ) |
| 152 | 150 | simprbi 496 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑣 ∈ 𝐷 → (ℜ‘𝑣) ∈
ℝ+) |
| 153 | 152 | rpne0d 13082 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑣 ∈ 𝐷 → (ℜ‘𝑣) ≠ 0) |
| 154 | | fveq2 6906 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑣 = 0 → (ℜ‘𝑣) =
(ℜ‘0)) |
| 155 | | re0 15191 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
(ℜ‘0) = 0 |
| 156 | 154, 155 | eqtrdi 2793 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑣 = 0 → (ℜ‘𝑣) = 0) |
| 157 | 156 | necon3i 2973 |
. . . . . . . . . . . . . . . . . . . 20
⊢
((ℜ‘𝑣)
≠ 0 → 𝑣 ≠
0) |
| 158 | 153, 157 | syl 17 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑣 ∈ 𝐷 → 𝑣 ≠ 0) |
| 159 | 151, 158 | 0cxpd 26752 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑣 ∈ 𝐷 → (0↑𝑐𝑣) = 0) |
| 160 | 159 | adantr 480 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑣 ∈ 𝐷 ∧ (𝑎 ∈ (0[,)+∞) ∧ 𝑏 ∈ 𝐷)) → (0↑𝑐𝑣) = 0) |
| 161 | 145, 160 | eqtrd 2777 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑣 ∈ 𝐷 ∧ (𝑎 ∈ (0[,)+∞) ∧ 𝑏 ∈ 𝐷)) → (0(𝑥 ∈ (0[,)+∞), 𝑦 ∈ 𝐷 ↦ (𝑥↑𝑐𝑦))𝑣) = 0) |
| 162 | | oveq12 7440 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑥 = 𝑎 ∧ 𝑦 = 𝑏) → (𝑥↑𝑐𝑦) = (𝑎↑𝑐𝑏)) |
| 163 | | ovex 7464 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑎↑𝑐𝑏) ∈ V |
| 164 | 162, 15, 163 | ovmpoa 7588 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑎 ∈ (0[,)+∞) ∧
𝑏 ∈ 𝐷) → (𝑎(𝑥 ∈ (0[,)+∞), 𝑦 ∈ 𝐷 ↦ (𝑥↑𝑐𝑦))𝑏) = (𝑎↑𝑐𝑏)) |
| 165 | 164 | adantl 481 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑣 ∈ 𝐷 ∧ (𝑎 ∈ (0[,)+∞) ∧ 𝑏 ∈ 𝐷)) → (𝑎(𝑥 ∈ (0[,)+∞), 𝑦 ∈ 𝐷 ↦ (𝑥↑𝑐𝑦))𝑏) = (𝑎↑𝑐𝑏)) |
| 166 | 161, 165 | oveq12d 7449 |
. . . . . . . . . . . . . . 15
⊢ ((𝑣 ∈ 𝐷 ∧ (𝑎 ∈ (0[,)+∞) ∧ 𝑏 ∈ 𝐷)) → ((0(𝑥 ∈ (0[,)+∞), 𝑦 ∈ 𝐷 ↦ (𝑥↑𝑐𝑦))𝑣)(abs ∘ − )(𝑎(𝑥 ∈ (0[,)+∞), 𝑦 ∈ 𝐷 ↦ (𝑥↑𝑐𝑦))𝑏)) = (0(abs ∘ − )(𝑎↑𝑐𝑏))) |
| 167 | 122, 136 | cxpcld 26750 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑣 ∈ 𝐷 ∧ (𝑎 ∈ (0[,)+∞) ∧ 𝑏 ∈ 𝐷)) → (𝑎↑𝑐𝑏) ∈ ℂ) |
| 168 | 123 | cnmetdval 24791 |
. . . . . . . . . . . . . . . 16
⊢ ((0
∈ ℂ ∧ (𝑎↑𝑐𝑏) ∈ ℂ) → (0(abs ∘
− )(𝑎↑𝑐𝑏)) = (abs‘(0 − (𝑎↑𝑐𝑏)))) |
| 169 | 121, 167,
168 | sylancr 587 |
. . . . . . . . . . . . . . 15
⊢ ((𝑣 ∈ 𝐷 ∧ (𝑎 ∈ (0[,)+∞) ∧ 𝑏 ∈ 𝐷)) → (0(abs ∘ − )(𝑎↑𝑐𝑏)) = (abs‘(0 −
(𝑎↑𝑐𝑏)))) |
| 170 | | df-neg 11495 |
. . . . . . . . . . . . . . . . 17
⊢ -(𝑎↑𝑐𝑏) = (0 − (𝑎↑𝑐𝑏)) |
| 171 | 170 | fveq2i 6909 |
. . . . . . . . . . . . . . . 16
⊢
(abs‘-(𝑎↑𝑐𝑏)) = (abs‘(0 − (𝑎↑𝑐𝑏))) |
| 172 | 167 | absnegd 15488 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑣 ∈ 𝐷 ∧ (𝑎 ∈ (0[,)+∞) ∧ 𝑏 ∈ 𝐷)) → (abs‘-(𝑎↑𝑐𝑏)) = (abs‘(𝑎↑𝑐𝑏))) |
| 173 | 171, 172 | eqtr3id 2791 |
. . . . . . . . . . . . . . 15
⊢ ((𝑣 ∈ 𝐷 ∧ (𝑎 ∈ (0[,)+∞) ∧ 𝑏 ∈ 𝐷)) → (abs‘(0 − (𝑎↑𝑐𝑏))) = (abs‘(𝑎↑𝑐𝑏))) |
| 174 | 166, 169,
173 | 3eqtrd 2781 |
. . . . . . . . . . . . . 14
⊢ ((𝑣 ∈ 𝐷 ∧ (𝑎 ∈ (0[,)+∞) ∧ 𝑏 ∈ 𝐷)) → ((0(𝑥 ∈ (0[,)+∞), 𝑦 ∈ 𝐷 ↦ (𝑥↑𝑐𝑦))𝑣)(abs ∘ − )(𝑎(𝑥 ∈ (0[,)+∞), 𝑦 ∈ 𝐷 ↦ (𝑥↑𝑐𝑦))𝑏)) = (abs‘(𝑎↑𝑐𝑏))) |
| 175 | 174 | breq1d 5153 |
. . . . . . . . . . . . 13
⊢ ((𝑣 ∈ 𝐷 ∧ (𝑎 ∈ (0[,)+∞) ∧ 𝑏 ∈ 𝐷)) → (((0(𝑥 ∈ (0[,)+∞), 𝑦 ∈ 𝐷 ↦ (𝑥↑𝑐𝑦))𝑣)(abs ∘ − )(𝑎(𝑥 ∈ (0[,)+∞), 𝑦 ∈ 𝐷 ↦ (𝑥↑𝑐𝑦))𝑏)) < 𝑒 ↔ (abs‘(𝑎↑𝑐𝑏)) < 𝑒)) |
| 176 | 141, 175 | imbi12d 344 |
. . . . . . . . . . . 12
⊢ ((𝑣 ∈ 𝐷 ∧ (𝑎 ∈ (0[,)+∞) ∧ 𝑏 ∈ 𝐷)) → ((((0((abs ∘ − )
↾ ((0[,)+∞) × (0[,)+∞)))𝑎) < 𝑑 ∧ (𝑣((abs ∘ − ) ↾ (𝐷 × 𝐷))𝑏) < 𝑑) → ((0(𝑥 ∈ (0[,)+∞), 𝑦 ∈ 𝐷 ↦ (𝑥↑𝑐𝑦))𝑣)(abs ∘ − )(𝑎(𝑥 ∈ (0[,)+∞), 𝑦 ∈ 𝐷 ↦ (𝑥↑𝑐𝑦))𝑏)) < 𝑒) ↔ (((abs‘𝑎) < 𝑑 ∧ (abs‘(𝑣 − 𝑏)) < 𝑑) → (abs‘(𝑎↑𝑐𝑏)) < 𝑒))) |
| 177 | 176 | 2ralbidva 3219 |
. . . . . . . . . . 11
⊢ (𝑣 ∈ 𝐷 → (∀𝑎 ∈ (0[,)+∞)∀𝑏 ∈ 𝐷 (((0((abs ∘ − ) ↾
((0[,)+∞) × (0[,)+∞)))𝑎) < 𝑑 ∧ (𝑣((abs ∘ − ) ↾ (𝐷 × 𝐷))𝑏) < 𝑑) → ((0(𝑥 ∈ (0[,)+∞), 𝑦 ∈ 𝐷 ↦ (𝑥↑𝑐𝑦))𝑣)(abs ∘ − )(𝑎(𝑥 ∈ (0[,)+∞), 𝑦 ∈ 𝐷 ↦ (𝑥↑𝑐𝑦))𝑏)) < 𝑒) ↔ ∀𝑎 ∈ (0[,)+∞)∀𝑏 ∈ 𝐷 (((abs‘𝑎) < 𝑑 ∧ (abs‘(𝑣 − 𝑏)) < 𝑑) → (abs‘(𝑎↑𝑐𝑏)) < 𝑒))) |
| 178 | 177 | rexbidv 3179 |
. . . . . . . . . 10
⊢ (𝑣 ∈ 𝐷 → (∃𝑑 ∈ ℝ+ ∀𝑎 ∈
(0[,)+∞)∀𝑏
∈ 𝐷 (((0((abs ∘
− ) ↾ ((0[,)+∞) × (0[,)+∞)))𝑎) < 𝑑 ∧ (𝑣((abs ∘ − ) ↾ (𝐷 × 𝐷))𝑏) < 𝑑) → ((0(𝑥 ∈ (0[,)+∞), 𝑦 ∈ 𝐷 ↦ (𝑥↑𝑐𝑦))𝑣)(abs ∘ − )(𝑎(𝑥 ∈ (0[,)+∞), 𝑦 ∈ 𝐷 ↦ (𝑥↑𝑐𝑦))𝑏)) < 𝑒) ↔ ∃𝑑 ∈ ℝ+ ∀𝑎 ∈
(0[,)+∞)∀𝑏
∈ 𝐷 (((abs‘𝑎) < 𝑑 ∧ (abs‘(𝑣 − 𝑏)) < 𝑑) → (abs‘(𝑎↑𝑐𝑏)) < 𝑒))) |
| 179 | 178 | ralbidv 3178 |
. . . . . . . . 9
⊢ (𝑣 ∈ 𝐷 → (∀𝑒 ∈ ℝ+ ∃𝑑 ∈ ℝ+
∀𝑎 ∈
(0[,)+∞)∀𝑏
∈ 𝐷 (((0((abs ∘
− ) ↾ ((0[,)+∞) × (0[,)+∞)))𝑎) < 𝑑 ∧ (𝑣((abs ∘ − ) ↾ (𝐷 × 𝐷))𝑏) < 𝑑) → ((0(𝑥 ∈ (0[,)+∞), 𝑦 ∈ 𝐷 ↦ (𝑥↑𝑐𝑦))𝑣)(abs ∘ − )(𝑎(𝑥 ∈ (0[,)+∞), 𝑦 ∈ 𝐷 ↦ (𝑥↑𝑐𝑦))𝑏)) < 𝑒) ↔ ∀𝑒 ∈ ℝ+ ∃𝑑 ∈ ℝ+
∀𝑎 ∈
(0[,)+∞)∀𝑏
∈ 𝐷 (((abs‘𝑎) < 𝑑 ∧ (abs‘(𝑣 − 𝑏)) < 𝑑) → (abs‘(𝑎↑𝑐𝑏)) < 𝑒))) |
| 180 | 116, 179 | mpbird 257 |
. . . . . . . 8
⊢ (𝑣 ∈ 𝐷 → ∀𝑒 ∈ ℝ+ ∃𝑑 ∈ ℝ+
∀𝑎 ∈
(0[,)+∞)∀𝑏
∈ 𝐷 (((0((abs ∘
− ) ↾ ((0[,)+∞) × (0[,)+∞)))𝑎) < 𝑑 ∧ (𝑣((abs ∘ − ) ↾ (𝐷 × 𝐷))𝑏) < 𝑑) → ((0(𝑥 ∈ (0[,)+∞), 𝑦 ∈ 𝐷 ↦ (𝑥↑𝑐𝑦))𝑣)(abs ∘ − )(𝑎(𝑥 ∈ (0[,)+∞), 𝑦 ∈ 𝐷 ↦ (𝑥↑𝑐𝑦))𝑏)) < 𝑒)) |
| 181 | | cnxmet 24793 |
. . . . . . . . . . 11
⊢ (abs
∘ − ) ∈ (∞Met‘ℂ) |
| 182 | 181 | a1i 11 |
. . . . . . . . . 10
⊢ (𝑣 ∈ 𝐷 → (abs ∘ − ) ∈
(∞Met‘ℂ)) |
| 183 | | xmetres2 24371 |
. . . . . . . . . 10
⊢ (((abs
∘ − ) ∈ (∞Met‘ℂ) ∧ (0[,)+∞)
⊆ ℂ) → ((abs ∘ − ) ↾ ((0[,)+∞) ×
(0[,)+∞))) ∈ (∞Met‘(0[,)+∞))) |
| 184 | 182, 3, 183 | sylancl 586 |
. . . . . . . . 9
⊢ (𝑣 ∈ 𝐷 → ((abs ∘ − ) ↾
((0[,)+∞) × (0[,)+∞))) ∈
(∞Met‘(0[,)+∞))) |
| 185 | | xmetres2 24371 |
. . . . . . . . . 10
⊢ (((abs
∘ − ) ∈ (∞Met‘ℂ) ∧ 𝐷 ⊆ ℂ) → ((abs ∘
− ) ↾ (𝐷
× 𝐷)) ∈
(∞Met‘𝐷)) |
| 186 | 182, 10, 185 | sylancl 586 |
. . . . . . . . 9
⊢ (𝑣 ∈ 𝐷 → ((abs ∘ − ) ↾
(𝐷 × 𝐷)) ∈
(∞Met‘𝐷)) |
| 187 | 117 | a1i 11 |
. . . . . . . . 9
⊢ (𝑣 ∈ 𝐷 → 0 ∈
(0[,)+∞)) |
| 188 | | id 22 |
. . . . . . . . 9
⊢ (𝑣 ∈ 𝐷 → 𝑣 ∈ 𝐷) |
| 189 | | eqid 2737 |
. . . . . . . . . . . . 13
⊢ ((abs
∘ − ) ↾ ((0[,)+∞) × (0[,)+∞))) = ((abs
∘ − ) ↾ ((0[,)+∞) ×
(0[,)+∞))) |
| 190 | 18 | cnfldtopn 24802 |
. . . . . . . . . . . . 13
⊢ 𝐽 = (MetOpen‘(abs ∘
− )) |
| 191 | | eqid 2737 |
. . . . . . . . . . . . 13
⊢
(MetOpen‘((abs ∘ − ) ↾ ((0[,)+∞) ×
(0[,)+∞)))) = (MetOpen‘((abs ∘ − ) ↾
((0[,)+∞) × (0[,)+∞)))) |
| 192 | 189, 190,
191 | metrest 24537 |
. . . . . . . . . . . 12
⊢ (((abs
∘ − ) ∈ (∞Met‘ℂ) ∧ (0[,)+∞)
⊆ ℂ) → (𝐽
↾t (0[,)+∞)) = (MetOpen‘((abs ∘ − )
↾ ((0[,)+∞) × (0[,)+∞))))) |
| 193 | 181, 3, 192 | mp2an 692 |
. . . . . . . . . . 11
⊢ (𝐽 ↾t
(0[,)+∞)) = (MetOpen‘((abs ∘ − ) ↾
((0[,)+∞) × (0[,)+∞)))) |
| 194 | 58, 193 | eqtri 2765 |
. . . . . . . . . 10
⊢ 𝐾 = (MetOpen‘((abs ∘
− ) ↾ ((0[,)+∞) × (0[,)+∞)))) |
| 195 | | eqid 2737 |
. . . . . . . . . . . . 13
⊢ ((abs
∘ − ) ↾ (𝐷 × 𝐷)) = ((abs ∘ − ) ↾ (𝐷 × 𝐷)) |
| 196 | | eqid 2737 |
. . . . . . . . . . . . 13
⊢
(MetOpen‘((abs ∘ − ) ↾ (𝐷 × 𝐷))) = (MetOpen‘((abs ∘ − )
↾ (𝐷 × 𝐷))) |
| 197 | 195, 190,
196 | metrest 24537 |
. . . . . . . . . . . 12
⊢ (((abs
∘ − ) ∈ (∞Met‘ℂ) ∧ 𝐷 ⊆ ℂ) → (𝐽 ↾t 𝐷) = (MetOpen‘((abs ∘ − )
↾ (𝐷 × 𝐷)))) |
| 198 | 181, 10, 197 | mp2an 692 |
. . . . . . . . . . 11
⊢ (𝐽 ↾t 𝐷) = (MetOpen‘((abs ∘
− ) ↾ (𝐷
× 𝐷))) |
| 199 | 32, 198 | eqtri 2765 |
. . . . . . . . . 10
⊢ 𝐿 = (MetOpen‘((abs ∘
− ) ↾ (𝐷
× 𝐷))) |
| 200 | 194, 199,
190 | txmetcnp 24560 |
. . . . . . . . 9
⊢ (((((abs
∘ − ) ↾ ((0[,)+∞) × (0[,)+∞))) ∈
(∞Met‘(0[,)+∞)) ∧ ((abs ∘ − ) ↾ (𝐷 × 𝐷)) ∈ (∞Met‘𝐷) ∧ (abs ∘ − )
∈ (∞Met‘ℂ)) ∧ (0 ∈ (0[,)+∞) ∧ 𝑣 ∈ 𝐷)) → ((𝑥 ∈ (0[,)+∞), 𝑦 ∈ 𝐷 ↦ (𝑥↑𝑐𝑦)) ∈ (((𝐾 ×t 𝐿) CnP 𝐽)‘〈0, 𝑣〉) ↔ ((𝑥 ∈ (0[,)+∞), 𝑦 ∈ 𝐷 ↦ (𝑥↑𝑐𝑦)):((0[,)+∞) × 𝐷)⟶ℂ ∧ ∀𝑒 ∈ ℝ+
∃𝑑 ∈
ℝ+ ∀𝑎 ∈ (0[,)+∞)∀𝑏 ∈ 𝐷 (((0((abs ∘ − ) ↾
((0[,)+∞) × (0[,)+∞)))𝑎) < 𝑑 ∧ (𝑣((abs ∘ − ) ↾ (𝐷 × 𝐷))𝑏) < 𝑑) → ((0(𝑥 ∈ (0[,)+∞), 𝑦 ∈ 𝐷 ↦ (𝑥↑𝑐𝑦))𝑣)(abs ∘ − )(𝑎(𝑥 ∈ (0[,)+∞), 𝑦 ∈ 𝐷 ↦ (𝑥↑𝑐𝑦))𝑏)) < 𝑒)))) |
| 201 | 184, 186,
182, 187, 188, 200 | syl32anc 1380 |
. . . . . . . 8
⊢ (𝑣 ∈ 𝐷 → ((𝑥 ∈ (0[,)+∞), 𝑦 ∈ 𝐷 ↦ (𝑥↑𝑐𝑦)) ∈ (((𝐾 ×t 𝐿) CnP 𝐽)‘〈0, 𝑣〉) ↔ ((𝑥 ∈ (0[,)+∞), 𝑦 ∈ 𝐷 ↦ (𝑥↑𝑐𝑦)):((0[,)+∞) × 𝐷)⟶ℂ ∧ ∀𝑒 ∈ ℝ+
∃𝑑 ∈
ℝ+ ∀𝑎 ∈ (0[,)+∞)∀𝑏 ∈ 𝐷 (((0((abs ∘ − ) ↾
((0[,)+∞) × (0[,)+∞)))𝑎) < 𝑑 ∧ (𝑣((abs ∘ − ) ↾ (𝐷 × 𝐷))𝑏) < 𝑑) → ((0(𝑥 ∈ (0[,)+∞), 𝑦 ∈ 𝐷 ↦ (𝑥↑𝑐𝑦))𝑣)(abs ∘ − )(𝑎(𝑥 ∈ (0[,)+∞), 𝑦 ∈ 𝐷 ↦ (𝑥↑𝑐𝑦))𝑏)) < 𝑒)))) |
| 202 | 112, 180,
201 | mpbir2and 713 |
. . . . . . 7
⊢ (𝑣 ∈ 𝐷 → (𝑥 ∈ (0[,)+∞), 𝑦 ∈ 𝐷 ↦ (𝑥↑𝑐𝑦)) ∈ (((𝐾 ×t 𝐿) CnP 𝐽)‘〈0, 𝑣〉)) |
| 203 | 202 | ad2antlr 727 |
. . . . . 6
⊢ (((𝑢 ∈ (0[,)+∞) ∧
𝑣 ∈ 𝐷) ∧ 0 = 𝑢) → (𝑥 ∈ (0[,)+∞), 𝑦 ∈ 𝐷 ↦ (𝑥↑𝑐𝑦)) ∈ (((𝐾 ×t 𝐿) CnP 𝐽)‘〈0, 𝑣〉)) |
| 204 | | simpr 484 |
. . . . . . . 8
⊢ (((𝑢 ∈ (0[,)+∞) ∧
𝑣 ∈ 𝐷) ∧ 0 = 𝑢) → 0 = 𝑢) |
| 205 | 204 | opeq1d 4879 |
. . . . . . 7
⊢ (((𝑢 ∈ (0[,)+∞) ∧
𝑣 ∈ 𝐷) ∧ 0 = 𝑢) → 〈0, 𝑣〉 = 〈𝑢, 𝑣〉) |
| 206 | 205 | fveq2d 6910 |
. . . . . 6
⊢ (((𝑢 ∈ (0[,)+∞) ∧
𝑣 ∈ 𝐷) ∧ 0 = 𝑢) → (((𝐾 ×t 𝐿) CnP 𝐽)‘〈0, 𝑣〉) = (((𝐾 ×t 𝐿) CnP 𝐽)‘〈𝑢, 𝑣〉)) |
| 207 | 203, 206 | eleqtrd 2843 |
. . . . 5
⊢ (((𝑢 ∈ (0[,)+∞) ∧
𝑣 ∈ 𝐷) ∧ 0 = 𝑢) → (𝑥 ∈ (0[,)+∞), 𝑦 ∈ 𝐷 ↦ (𝑥↑𝑐𝑦)) ∈ (((𝐾 ×t 𝐿) CnP 𝐽)‘〈𝑢, 𝑣〉)) |
| 208 | 39 | simprbi 496 |
. . . . . . 7
⊢ (𝑢 ∈ (0[,)+∞) → 0
≤ 𝑢) |
| 209 | 208 | adantr 480 |
. . . . . 6
⊢ ((𝑢 ∈ (0[,)+∞) ∧
𝑣 ∈ 𝐷) → 0 ≤ 𝑢) |
| 210 | | 0re 11263 |
. . . . . . 7
⊢ 0 ∈
ℝ |
| 211 | | leloe 11347 |
. . . . . . 7
⊢ ((0
∈ ℝ ∧ 𝑢
∈ ℝ) → (0 ≤ 𝑢 ↔ (0 < 𝑢 ∨ 0 = 𝑢))) |
| 212 | 210, 41, 211 | sylancr 587 |
. . . . . 6
⊢ ((𝑢 ∈ (0[,)+∞) ∧
𝑣 ∈ 𝐷) → (0 ≤ 𝑢 ↔ (0 < 𝑢 ∨ 0 = 𝑢))) |
| 213 | 209, 212 | mpbid 232 |
. . . . 5
⊢ ((𝑢 ∈ (0[,)+∞) ∧
𝑣 ∈ 𝐷) → (0 < 𝑢 ∨ 0 = 𝑢)) |
| 214 | 111, 207,
213 | mpjaodan 961 |
. . . 4
⊢ ((𝑢 ∈ (0[,)+∞) ∧
𝑣 ∈ 𝐷) → (𝑥 ∈ (0[,)+∞), 𝑦 ∈ 𝐷 ↦ (𝑥↑𝑐𝑦)) ∈ (((𝐾 ×t 𝐿) CnP 𝐽)‘〈𝑢, 𝑣〉)) |
| 215 | 214 | rgen2 3199 |
. . 3
⊢
∀𝑢 ∈
(0[,)+∞)∀𝑣
∈ 𝐷 (𝑥 ∈ (0[,)+∞), 𝑦 ∈ 𝐷 ↦ (𝑥↑𝑐𝑦)) ∈ (((𝐾 ×t 𝐿) CnP 𝐽)‘〈𝑢, 𝑣〉) |
| 216 | | fveq2 6906 |
. . . . 5
⊢ (𝑧 = 〈𝑢, 𝑣〉 → (((𝐾 ×t 𝐿) CnP 𝐽)‘𝑧) = (((𝐾 ×t 𝐿) CnP 𝐽)‘〈𝑢, 𝑣〉)) |
| 217 | 216 | eleq2d 2827 |
. . . 4
⊢ (𝑧 = 〈𝑢, 𝑣〉 → ((𝑥 ∈ (0[,)+∞), 𝑦 ∈ 𝐷 ↦ (𝑥↑𝑐𝑦)) ∈ (((𝐾 ×t 𝐿) CnP 𝐽)‘𝑧) ↔ (𝑥 ∈ (0[,)+∞), 𝑦 ∈ 𝐷 ↦ (𝑥↑𝑐𝑦)) ∈ (((𝐾 ×t 𝐿) CnP 𝐽)‘〈𝑢, 𝑣〉))) |
| 218 | 217 | ralxp 5852 |
. . 3
⊢
(∀𝑧 ∈
((0[,)+∞) × 𝐷)(𝑥 ∈ (0[,)+∞), 𝑦 ∈ 𝐷 ↦ (𝑥↑𝑐𝑦)) ∈ (((𝐾 ×t 𝐿) CnP 𝐽)‘𝑧) ↔ ∀𝑢 ∈ (0[,)+∞)∀𝑣 ∈ 𝐷 (𝑥 ∈ (0[,)+∞), 𝑦 ∈ 𝐷 ↦ (𝑥↑𝑐𝑦)) ∈ (((𝐾 ×t 𝐿) CnP 𝐽)‘〈𝑢, 𝑣〉)) |
| 219 | 215, 218 | mpbir 231 |
. 2
⊢
∀𝑧 ∈
((0[,)+∞) × 𝐷)(𝑥 ∈ (0[,)+∞), 𝑦 ∈ 𝐷 ↦ (𝑥↑𝑐𝑦)) ∈ (((𝐾 ×t 𝐿) CnP 𝐽)‘𝑧) |
| 220 | | cncnp 23288 |
. . 3
⊢ (((𝐾 ×t 𝐿) ∈
(TopOn‘((0[,)+∞) × 𝐷)) ∧ 𝐽 ∈ (TopOn‘ℂ)) →
((𝑥 ∈ (0[,)+∞),
𝑦 ∈ 𝐷 ↦ (𝑥↑𝑐𝑦)) ∈ ((𝐾 ×t 𝐿) Cn 𝐽) ↔ ((𝑥 ∈ (0[,)+∞), 𝑦 ∈ 𝐷 ↦ (𝑥↑𝑐𝑦)):((0[,)+∞) × 𝐷)⟶ℂ ∧ ∀𝑧 ∈ ((0[,)+∞) ×
𝐷)(𝑥 ∈ (0[,)+∞), 𝑦 ∈ 𝐷 ↦ (𝑥↑𝑐𝑦)) ∈ (((𝐾 ×t 𝐿) CnP 𝐽)‘𝑧)))) |
| 221 | 93, 19, 220 | mp2an 692 |
. 2
⊢ ((𝑥 ∈ (0[,)+∞), 𝑦 ∈ 𝐷 ↦ (𝑥↑𝑐𝑦)) ∈ ((𝐾 ×t 𝐿) Cn 𝐽) ↔ ((𝑥 ∈ (0[,)+∞), 𝑦 ∈ 𝐷 ↦ (𝑥↑𝑐𝑦)):((0[,)+∞) × 𝐷)⟶ℂ ∧ ∀𝑧 ∈ ((0[,)+∞) ×
𝐷)(𝑥 ∈ (0[,)+∞), 𝑦 ∈ 𝐷 ↦ (𝑥↑𝑐𝑦)) ∈ (((𝐾 ×t 𝐿) CnP 𝐽)‘𝑧))) |
| 222 | 17, 219, 221 | mpbir2an 711 |
1
⊢ (𝑥 ∈ (0[,)+∞), 𝑦 ∈ 𝐷 ↦ (𝑥↑𝑐𝑦)) ∈ ((𝐾 ×t 𝐿) Cn 𝐽) |