cxpcn3

Description: Extend continuity of the complex power function to a base of zero, as long as the exponent has strictly positive real part. (Contributed by Mario Carneiro, 2-May-2016)

	Ref	Expression
Hypotheses	cxpcn3.d	$⊢ D = ℜ^{-1} [ℝ^{+}]$
	cxpcn3.j	$⊢ J = TopOpen (ℂ_{fld})$
	cxpcn3.k	$⊢ K = J ↾_{𝑡} [0, +∞)$
	cxpcn3.l	$⊢ L = J ↾_{𝑡} D$
Assertion	cxpcn3	$⊢ (x \in [0, +∞), y \in D ⟼ x^{y}) \in ((K \times_{t} L) Cn J)$

Proof

Step	Hyp	Ref	Expression
1		cxpcn3.d	$⊢ D = ℜ^{-1} [ℝ^{+}]$
2		cxpcn3.j	$⊢ J = TopOpen (ℂ_{fld})$
3		cxpcn3.k	$⊢ K = J ↾_{𝑡} [0, +∞)$
4		cxpcn3.l	$⊢ L = J ↾_{𝑡} D$
5		rge0ssre	$⊢ [0, +∞) \subseteq ℝ$
6		ax-resscn	$⊢ ℝ \subseteq ℂ$
7	5 6	sstri	$⊢ [0, +∞) \subseteq ℂ$
8	7	sseli	$⊢ x \in [0, +∞) \to x \in ℂ$
9		cnvimass	$⊢ ℜ^{-1} [ℝ^{+}] \subseteq dom ℜ$
10		ref	$⊢ ℜ : ℂ ⟶ ℝ$
11	10	fdmi	$⊢ dom ℜ = ℂ$
12	9 11	sseqtri	$⊢ ℜ^{-1} [ℝ^{+}] \subseteq ℂ$
13	1 12	eqsstri	$⊢ D \subseteq ℂ$
14	13	sseli	$⊢ y \in D \to y \in ℂ$
15		cxpcl	$⊢ (x \in ℂ \land y \in ℂ) \to x^{y} \in ℂ$
16	8 14 15	syl2an	$⊢ (x \in [0, +∞) \land y \in D) \to x^{y} \in ℂ$
17	16	rgen2	$⊢ \forall x \in [0, +∞) \forall y \in D x^{y} \in ℂ$
18		eqid	$⊢ (x \in [0, +∞), y \in D ⟼ x^{y}) = (x \in [0, +∞), y \in D ⟼ x^{y})$
19	18	fmpo	$⊢ \forall x \in [0, +∞) \forall y \in D x^{y} \in ℂ \leftrightarrow (x \in [0, +∞), y \in D ⟼ x^{y}) : [0, +∞) \times D ⟶ ℂ$
20	17 19	mpbi	$⊢ (x \in [0, +∞), y \in D ⟼ x^{y}) : [0, +∞) \times D ⟶ ℂ$
21	2	cnfldtopon	$⊢ J \in TopOn (ℂ)$
22		rpre	$⊢ x \in ℝ^{+} \to x \in ℝ$
23		rpge0	$⊢ x \in ℝ^{+} \to 0 \leq x$
24		elrege0	$⊢ x \in [0, +∞) \leftrightarrow (x \in ℝ \land 0 \leq x)$
25	22 23 24	sylanbrc	$⊢ x \in ℝ^{+} \to x \in [0, +∞)$
26	25	ssriv	$⊢ ℝ^{+} \subseteq [0, +∞)$
27	26 7	sstri	$⊢ ℝ^{+} \subseteq ℂ$
28		resttopon	$⊢ (J \in TopOn (ℂ) \land ℝ^{+} \subseteq ℂ) \to J ↾_{𝑡} ℝ^{+} \in TopOn (ℝ^{+})$
29	21 27 28	mp2an	$⊢ J ↾_{𝑡} ℝ^{+} \in TopOn (ℝ^{+})$
30	29	toponrestid	$⊢ J ↾_{𝑡} ℝ^{+} = (J ↾_{𝑡} ℝ^{+}) ↾_{𝑡} ℝ^{+}$
31	29	a1i	$⊢ ((u \in [0, +∞) \land v \in D) \land 0 < u) \to J ↾_{𝑡} ℝ^{+} \in TopOn (ℝ^{+})$
32		ssid	$⊢ ℝ^{+} \subseteq ℝ^{+}$
33	32	a1i	$⊢ ((u \in [0, +∞) \land v \in D) \land 0 < u) \to ℝ^{+} \subseteq ℝ^{+}$
34	21	a1i	$⊢ ((u \in [0, +∞) \land v \in D) \land 0 < u) \to J \in TopOn (ℂ)$
35	13	a1i	$⊢ ((u \in [0, +∞) \land v \in D) \land 0 < u) \to D \subseteq ℂ$
36		eqid	$⊢ J ↾_{𝑡} ℝ^{+} = J ↾_{𝑡} ℝ^{+}$
37	2 36	cxpcn2	$⊢ (x \in ℝ^{+}, y \in ℂ ⟼ x^{y}) \in (((J ↾_{𝑡} ℝ^{+}) \times_{t} J) Cn J)$
38	37	a1i	$⊢ ((u \in [0, +∞) \land v \in D) \land 0 < u) \to (x \in ℝ^{+}, y \in ℂ ⟼ x^{y}) \in (((J ↾_{𝑡} ℝ^{+}) \times_{t} J) Cn J)$
39	30 31 33 4 34 35 38	cnmpt2res	$⊢ ((u \in [0, +∞) \land v \in D) \land 0 < u) \to (x \in ℝ^{+}, y \in D ⟼ x^{y}) \in (((J ↾_{𝑡} ℝ^{+}) \times_{t} L) Cn J)$
40		elrege0	$⊢ u \in [0, +∞) \leftrightarrow (u \in ℝ \land 0 \leq u)$
41	40	simplbi	$⊢ u \in [0, +∞) \to u \in ℝ$
42	41	adantr	$⊢ (u \in [0, +∞) \land v \in D) \to u \in ℝ$
43	42	adantr	$⊢ ((u \in [0, +∞) \land v \in D) \land 0 < u) \to u \in ℝ$
44		simpr	$⊢ ((u \in [0, +∞) \land v \in D) \land 0 < u) \to 0 < u$
45	43 44	elrpd	$⊢ ((u \in [0, +∞) \land v \in D) \land 0 < u) \to u \in ℝ^{+}$
46		simplr	$⊢ ((u \in [0, +∞) \land v \in D) \land 0 < u) \to v \in D$
47	45 46	opelxpd	$⊢ ((u \in [0, +∞) \land v \in D) \land 0 < u) \to ⟨u, v⟩ \in (ℝ^{+} \times D)$
48		resttopon	$⊢ (J \in TopOn (ℂ) \land D \subseteq ℂ) \to J ↾_{𝑡} D \in TopOn (D)$
49	21 13 48	mp2an	$⊢ J ↾_{𝑡} D \in TopOn (D)$
50	4 49	eqeltri	$⊢ L \in TopOn (D)$
51		txtopon	$⊢ (J ↾_{𝑡} ℝ^{+} \in TopOn (ℝ^{+}) \land L \in TopOn (D)) \to (J ↾_{𝑡} ℝ^{+}) \times_{t} L \in TopOn (ℝ^{+} \times D)$
52	29 50 51	mp2an	$⊢ (J ↾_{𝑡} ℝ^{+}) \times_{t} L \in TopOn (ℝ^{+} \times D)$
53	52	toponunii	$⊢ ℝ^{+} \times D = ⋃ ((J ↾_{𝑡} ℝ^{+}) \times_{t} L)$
54	53	cncnpi	$⊢ ((x \in ℝ^{+}, y \in D ⟼ x^{y}) \in (((J ↾_{𝑡} ℝ^{+}) \times_{t} L) Cn J) \land ⟨u, v⟩ \in (ℝ^{+} \times D)) \to (x \in ℝ^{+}, y \in D ⟼ x^{y}) \in (((J ↾_{𝑡} ℝ^{+}) \times_{t} L) CnP J) (⟨u, v⟩)$
55	39 47 54	syl2anc	$⊢ ((u \in [0, +∞) \land v \in D) \land 0 < u) \to (x \in ℝ^{+}, y \in D ⟼ x^{y}) \in (((J ↾_{𝑡} ℝ^{+}) \times_{t} L) CnP J) (⟨u, v⟩)$
56		ssid	$⊢ D \subseteq D$
57		resmpo	$⊢ (ℝ^{+} \subseteq [0, +∞) \land D \subseteq D) \to {(x \in [0, +∞), y \in D ⟼ x^{y}) ↾}_{(ℝ^{+} \times D)} = (x \in ℝ^{+}, y \in D ⟼ x^{y})$
58	26 56 57	mp2an	$⊢ {(x \in [0, +∞), y \in D ⟼ x^{y}) ↾}_{(ℝ^{+} \times D)} = (x \in ℝ^{+}, y \in D ⟼ x^{y})$
59		resttopon	$⊢ (J \in TopOn (ℂ) \land [0, +∞) \subseteq ℂ) \to J ↾_{𝑡} [0, +∞) \in TopOn ([0, +∞))$
60	21 7 59	mp2an	$⊢ J ↾_{𝑡} [0, +∞) \in TopOn ([0, +∞))$
61	3 60	eqeltri	$⊢ K \in TopOn ([0, +∞))$
62		ioorp	$⊢ (0, +∞) = ℝ^{+}$
63		iooretop	$⊢ (0, +∞) \in topGen (ran (.))$
64	62 63	eqeltrri	$⊢ ℝ^{+} \in topGen (ran (.))$
65		retop	$⊢ topGen (ran (.)) \in Top$
66		ovex	$⊢ [0, +∞) \in V$
67		restopnb	$⊢ ((topGen (ran (.)) \in Top \land [0, +∞) \in V) \land (ℝ^{+} \in topGen (ran (.)) \land ℝ^{+} \subseteq [0, +∞) \land ℝ^{+} \subseteq ℝ^{+})) \to (ℝ^{+} \in topGen (ran (.)) \leftrightarrow ℝ^{+} \in (topGen (ran (.)) ↾_{𝑡} [0, +∞)))$
68	65 66 67	mpanl12	$⊢ (ℝ^{+} \in topGen (ran (.)) \land ℝ^{+} \subseteq [0, +∞) \land ℝ^{+} \subseteq ℝ^{+}) \to (ℝ^{+} \in topGen (ran (.)) \leftrightarrow ℝ^{+} \in (topGen (ran (.)) ↾_{𝑡} [0, +∞)))$
69	64 26 32 68	mp3an	$⊢ ℝ^{+} \in topGen (ran (.)) \leftrightarrow ℝ^{+} \in (topGen (ran (.)) ↾_{𝑡} [0, +∞))$
70	64 69	mpbi	$⊢ ℝ^{+} \in (topGen (ran (.)) ↾_{𝑡} [0, +∞))$
71		eqid	$⊢ topGen (ran (.)) = topGen (ran (.))$
72	2 71	rerest	$⊢ [0, +∞) \subseteq ℝ \to J ↾_{𝑡} [0, +∞) = topGen (ran (.)) ↾_{𝑡} [0, +∞)$
73	5 72	ax-mp	$⊢ J ↾_{𝑡} [0, +∞) = topGen (ran (.)) ↾_{𝑡} [0, +∞)$
74	3 73	eqtri	$⊢ K = topGen (ran (.)) ↾_{𝑡} [0, +∞)$
75	70 74	eleqtrri	$⊢ ℝ^{+} \in K$
76		toponmax	$⊢ L \in TopOn (D) \to D \in L$
77	50 76	ax-mp	$⊢ D \in L$
78		txrest	$⊢ ((K \in TopOn ([0, +∞)) \land L \in TopOn (D)) \land (ℝ^{+} \in K \land D \in L)) \to (K \times_{t} L) ↾_{𝑡} (ℝ^{+} \times D) = (K ↾_{𝑡} ℝ^{+}) \times_{t} (L ↾_{𝑡} D)$
79	61 50 75 77 78	mp4an	$⊢ (K \times_{t} L) ↾_{𝑡} (ℝ^{+} \times D) = (K ↾_{𝑡} ℝ^{+}) \times_{t} (L ↾_{𝑡} D)$
80	3	oveq1i	$⊢ K ↾_{𝑡} ℝ^{+} = (J ↾_{𝑡} [0, +∞)) ↾_{𝑡} ℝ^{+}$
81		restabs	$⊢ (J \in TopOn (ℂ) \land ℝ^{+} \subseteq [0, +∞) \land [0, +∞) \in V) \to (J ↾_{𝑡} [0, +∞)) ↾_{𝑡} ℝ^{+} = J ↾_{𝑡} ℝ^{+}$
82	21 26 66 81	mp3an	$⊢ (J ↾_{𝑡} [0, +∞)) ↾_{𝑡} ℝ^{+} = J ↾_{𝑡} ℝ^{+}$
83	80 82	eqtri	$⊢ K ↾_{𝑡} ℝ^{+} = J ↾_{𝑡} ℝ^{+}$
84	50	toponunii	$⊢ D = ⋃ L$
85	84	restid	$⊢ L \in TopOn (D) \to L ↾_{𝑡} D = L$
86	50 85	ax-mp	$⊢ L ↾_{𝑡} D = L$
87	83 86	oveq12i	$⊢ (K ↾_{𝑡} ℝ^{+}) \times_{t} (L ↾_{𝑡} D) = (J ↾_{𝑡} ℝ^{+}) \times_{t} L$
88	79 87	eqtri	$⊢ (K \times_{t} L) ↾_{𝑡} (ℝ^{+} \times D) = (J ↾_{𝑡} ℝ^{+}) \times_{t} L$
89	88	oveq1i	$⊢ ((K \times_{t} L) ↾_{𝑡} (ℝ^{+} \times D)) CnP J = ((J ↾_{𝑡} ℝ^{+}) \times_{t} L) CnP J$
90	89	fveq1i	$⊢ (((K \times_{t} L) ↾_{𝑡} (ℝ^{+} \times D)) CnP J) (⟨u, v⟩) = (((J ↾_{𝑡} ℝ^{+}) \times_{t} L) CnP J) (⟨u, v⟩)$
91	55 58 90	3eltr4g	$⊢ ((u \in [0, +∞) \land v \in D) \land 0 < u) \to {(x \in [0, +∞), y \in D ⟼ x^{y}) ↾}_{(ℝ^{+} \times D)} \in (((K \times_{t} L) ↾_{𝑡} (ℝ^{+} \times D)) CnP J) (⟨u, v⟩)$
92		txtopon	$⊢ (K \in TopOn ([0, +∞)) \land L \in TopOn (D)) \to K \times_{t} L \in TopOn ([0, +∞) \times D)$
93	61 50 92	mp2an	$⊢ K \times_{t} L \in TopOn ([0, +∞) \times D)$
94	93	topontopi	$⊢ K \times_{t} L \in Top$
95	94	a1i	$⊢ ((u \in [0, +∞) \land v \in D) \land 0 < u) \to K \times_{t} L \in Top$
96		xpss1	$⊢ ℝ^{+} \subseteq [0, +∞) \to ℝ^{+} \times D \subseteq [0, +∞) \times D$
97	26 96	mp1i	$⊢ ((u \in [0, +∞) \land v \in D) \land 0 < u) \to ℝ^{+} \times D \subseteq [0, +∞) \times D$
98		txopn	$⊢ ((K \in TopOn ([0, +∞)) \land L \in TopOn (D)) \land (ℝ^{+} \in K \land D \in L)) \to ℝ^{+} \times D \in (K \times_{t} L)$
99	61 50 75 77 98	mp4an	$⊢ ℝ^{+} \times D \in (K \times_{t} L)$
100		isopn3i	$⊢ (K \times_{t} L \in Top \land ℝ^{+} \times D \in (K \times_{t} L)) \to int (K \times_{t} L) (ℝ^{+} \times D) = ℝ^{+} \times D$
101	94 99 100	mp2an	$⊢ int (K \times_{t} L) (ℝ^{+} \times D) = ℝ^{+} \times D$
102	47 101	eleqtrrdi	$⊢ ((u \in [0, +∞) \land v \in D) \land 0 < u) \to ⟨u, v⟩ \in int (K \times_{t} L) (ℝ^{+} \times D)$
103	20	a1i	$⊢ ((u \in [0, +∞) \land v \in D) \land 0 < u) \to (x \in [0, +∞), y \in D ⟼ x^{y}) : [0, +∞) \times D ⟶ ℂ$
104	61	topontopi	$⊢ K \in Top$
105	50	topontopi	$⊢ L \in Top$
106	61	toponunii	$⊢ [0, +∞) = ⋃ K$
107	104 105 106 84	txunii	$⊢ [0, +∞) \times D = ⋃ (K \times_{t} L)$
108	21	toponunii	$⊢ ℂ = ⋃ J$
109	107 108	cnprest	$⊢ ((K \times_{t} L \in Top \land ℝ^{+} \times D \subseteq [0, +∞) \times D) \land (⟨u, v⟩ \in int (K \times_{t} L) (ℝ^{+} \times D) \land (x \in [0, +∞), y \in D ⟼ x^{y}) : [0, +∞) \times D ⟶ ℂ)) \to ((x \in [0, +∞), y \in D ⟼ x^{y}) \in ((K \times_{t} L) CnP J) (⟨u, v⟩) \leftrightarrow {(x \in [0, +∞), y \in D ⟼ x^{y}) ↾}_{(ℝ^{+} \times D)} \in (((K \times_{t} L) ↾_{𝑡} (ℝ^{+} \times D)) CnP J) (⟨u, v⟩))$
110	95 97 102 103 109	syl22anc	$⊢ ((u \in [0, +∞) \land v \in D) \land 0 < u) \to ((x \in [0, +∞), y \in D ⟼ x^{y}) \in ((K \times_{t} L) CnP J) (⟨u, v⟩) \leftrightarrow {(x \in [0, +∞), y \in D ⟼ x^{y}) ↾}_{(ℝ^{+} \times D)} \in (((K \times_{t} L) ↾_{𝑡} (ℝ^{+} \times D)) CnP J) (⟨u, v⟩))$
111	91 110	mpbird	$⊢ ((u \in [0, +∞) \land v \in D) \land 0 < u) \to (x \in [0, +∞), y \in D ⟼ x^{y}) \in ((K \times_{t} L) CnP J) (⟨u, v⟩)$
112	20	a1i	$⊢ v \in D \to (x \in [0, +∞), y \in D ⟼ x^{y}) : [0, +∞) \times D ⟶ ℂ$
113		eqid	$⊢ \frac{if (ℜ (v) \leq 1, ℜ (v), 1)}{2} = \frac{if (ℜ (v) \leq 1, ℜ (v), 1)}{2}$
114		eqid	$⊢ if (\frac{if (ℜ (v) \leq 1, ℜ (v), 1)}{2} \leq e^{\frac{1}{\frac{if (ℜ (v) \leq 1, ℜ (v), 1)}{2}}}, \frac{if (ℜ (v) \leq 1, ℜ (v), 1)}{2}, e^{\frac{1}{\frac{if (ℜ (v) \leq 1, ℜ (v), 1)}{2}}}) = if (\frac{if (ℜ (v) \leq 1, ℜ (v), 1)}{2} \leq e^{\frac{1}{\frac{if (ℜ (v) \leq 1, ℜ (v), 1)}{2}}}, \frac{if (ℜ (v) \leq 1, ℜ (v), 1)}{2}, e^{\frac{1}{\frac{if (ℜ (v) \leq 1, ℜ (v), 1)}{2}}})$
115	1 2 3 4 113 114	cxpcn3lem	$⊢ (v \in D \land e \in ℝ^{+}) \to \exists d \in ℝ^{+} \forall a \in [0, +∞) \forall b \in D ((\|a\| < d \land \|v - b\| < d) \to \|a^{b}\| < e)$
116	115	ralrimiva	$⊢ v \in D \to \forall e \in ℝ^{+} \exists d \in ℝ^{+} \forall a \in [0, +∞) \forall b \in D ((\|a\| < d \land \|v - b\| < d) \to \|a^{b}\| < e)$
117		0e0icopnf	$⊢ 0 \in [0, +∞)$
118	117	a1i	$⊢ (v \in D \land (a \in [0, +∞) \land b \in D)) \to 0 \in [0, +∞)$
119		simprl	$⊢ (v \in D \land (a \in [0, +∞) \land b \in D)) \to a \in [0, +∞)$
120	118 119	ovresd	$⊢ (v \in D \land (a \in [0, +∞) \land b \in D)) \to 0 ({(abs \circ -) ↾}_{([0, +∞) \times [0, +∞))}) a = 0 (abs \circ -) a$
121		0cn	$⊢ 0 \in ℂ$
122	7 119	sselid	$⊢ (v \in D \land (a \in [0, +∞) \land b \in D)) \to a \in ℂ$
123		eqid	$⊢ abs \circ - = abs \circ -$
124	123	cnmetdval	$⊢ (0 \in ℂ \land a \in ℂ) \to 0 (abs \circ -) a = \|0 - a\|$
125	121 122 124	sylancr	$⊢ (v \in D \land (a \in [0, +∞) \land b \in D)) \to 0 (abs \circ -) a = \|0 - a\|$
126		df-neg	$⊢ - a = 0 - a$
127	126	fveq2i	$⊢ \|- a\| = \|0 - a\|$
128	122	absnegd	$⊢ (v \in D \land (a \in [0, +∞) \land b \in D)) \to \|- a\| = \|a\|$
129	127 128	eqtr3id	$⊢ (v \in D \land (a \in [0, +∞) \land b \in D)) \to \|0 - a\| = \|a\|$
130	120 125 129	3eqtrd	$⊢ (v \in D \land (a \in [0, +∞) \land b \in D)) \to 0 ({(abs \circ -) ↾}_{([0, +∞) \times [0, +∞))}) a = \|a\|$
131	130	breq1d	$⊢ (v \in D \land (a \in [0, +∞) \land b \in D)) \to (0 ({(abs \circ -) ↾}_{([0, +∞) \times [0, +∞))}) a < d \leftrightarrow \|a\| < d)$
132		simpl	$⊢ (v \in D \land (a \in [0, +∞) \land b \in D)) \to v \in D$
133		simprr	$⊢ (v \in D \land (a \in [0, +∞) \land b \in D)) \to b \in D$
134	132 133	ovresd	$⊢ (v \in D \land (a \in [0, +∞) \land b \in D)) \to v ({(abs \circ -) ↾}_{(D \times D)}) b = v (abs \circ -) b$
135	13 132	sselid	$⊢ (v \in D \land (a \in [0, +∞) \land b \in D)) \to v \in ℂ$
136	13 133	sselid	$⊢ (v \in D \land (a \in [0, +∞) \land b \in D)) \to b \in ℂ$
137	123	cnmetdval	$⊢ (v \in ℂ \land b \in ℂ) \to v (abs \circ -) b = \|v - b\|$
138	135 136 137	syl2anc	$⊢ (v \in D \land (a \in [0, +∞) \land b \in D)) \to v (abs \circ -) b = \|v - b\|$
139	134 138	eqtrd	$⊢ (v \in D \land (a \in [0, +∞) \land b \in D)) \to v ({(abs \circ -) ↾}_{(D \times D)}) b = \|v - b\|$
140	139	breq1d	$⊢ (v \in D \land (a \in [0, +∞) \land b \in D)) \to (v ({(abs \circ -) ↾}_{(D \times D)}) b < d \leftrightarrow \|v - b\| < d)$
141	131 140	anbi12d	$⊢ (v \in D \land (a \in [0, +∞) \land b \in D)) \to ((0 ({(abs \circ -) ↾}_{([0, +∞) \times [0, +∞))}) a < d \land v ({(abs \circ -) ↾}_{(D \times D)}) b < d) \leftrightarrow (\|a\| < d \land \|v - b\| < d))$
142		oveq12	$⊢ (x = 0 \land y = v) \to x^{y} = 0^{v}$
143		ovex	$⊢ 0^{v} \in V$
144	142 18 143	ovmpoa	$⊢ (0 \in [0, +∞) \land v \in D) \to 0 (x \in [0, +∞), y \in D ⟼ x^{y}) v = 0^{v}$
145	117 132 144	sylancr	$⊢ (v \in D \land (a \in [0, +∞) \land b \in D)) \to 0 (x \in [0, +∞), y \in D ⟼ x^{y}) v = 0^{v}$
146	1	eleq2i	$⊢ v \in D \leftrightarrow v \in ℜ^{-1} [ℝ^{+}]$
147		ffn	$⊢ ℜ : ℂ ⟶ ℝ \to ℜ Fn ℂ$
148		elpreima	$⊢ ℜ Fn ℂ \to (v \in ℜ^{-1} [ℝ^{+}] \leftrightarrow (v \in ℂ \land ℜ (v) \in ℝ^{+}))$
149	10 147 148	mp2b	$⊢ v \in ℜ^{-1} [ℝ^{+}] \leftrightarrow (v \in ℂ \land ℜ (v) \in ℝ^{+})$
150	146 149	bitri	$⊢ v \in D \leftrightarrow (v \in ℂ \land ℜ (v) \in ℝ^{+})$
151	150	simplbi	$⊢ v \in D \to v \in ℂ$
152	150	simprbi	$⊢ v \in D \to ℜ (v) \in ℝ^{+}$
153	152	rpne0d	$⊢ v \in D \to ℜ (v) \neq 0$
154		fveq2	$⊢ v = 0 \to ℜ (v) = ℜ (0)$
155		re0	$⊢ ℜ (0) = 0$
156	154 155	eqtrdi	$⊢ v = 0 \to ℜ (v) = 0$
157	156	necon3i	$⊢ ℜ (v) \neq 0 \to v \neq 0$
158	153 157	syl	$⊢ v \in D \to v \neq 0$
159	151 158	0cxpd	$⊢ v \in D \to 0^{v} = 0$
160	159	adantr	$⊢ (v \in D \land (a \in [0, +∞) \land b \in D)) \to 0^{v} = 0$
161	145 160	eqtrd	$⊢ (v \in D \land (a \in [0, +∞) \land b \in D)) \to 0 (x \in [0, +∞), y \in D ⟼ x^{y}) v = 0$
162		oveq12	$⊢ (x = a \land y = b) \to x^{y} = a^{b}$
163		ovex	$⊢ a^{b} \in V$
164	162 18 163	ovmpoa	$⊢ (a \in [0, +∞) \land b \in D) \to a (x \in [0, +∞), y \in D ⟼ x^{y}) b = a^{b}$
165	164	adantl	$⊢ (v \in D \land (a \in [0, +∞) \land b \in D)) \to a (x \in [0, +∞), y \in D ⟼ x^{y}) b = a^{b}$
166	161 165	oveq12d	$⊢ (v \in D \land (a \in [0, +∞) \land b \in D)) \to (0 (x \in [0, +∞), y \in D ⟼ x^{y}) v) (abs \circ -) (a (x \in [0, +∞), y \in D ⟼ x^{y}) b) = 0 (abs \circ -) a^{b}$
167	122 136	cxpcld	$⊢ (v \in D \land (a \in [0, +∞) \land b \in D)) \to a^{b} \in ℂ$
168	123	cnmetdval	$⊢ (0 \in ℂ \land a^{b} \in ℂ) \to 0 (abs \circ -) a^{b} = \|0 - a^{b}\|$
169	121 167 168	sylancr	$⊢ (v \in D \land (a \in [0, +∞) \land b \in D)) \to 0 (abs \circ -) a^{b} = \|0 - a^{b}\|$
170		df-neg	$⊢ - a^{b} = 0 - a^{b}$
171	170	fveq2i	$⊢ \|- a^{b}\| = \|0 - a^{b}\|$
172	167	absnegd	$⊢ (v \in D \land (a \in [0, +∞) \land b \in D)) \to \|- a^{b}\| = \|a^{b}\|$
173	171 172	eqtr3id	$⊢ (v \in D \land (a \in [0, +∞) \land b \in D)) \to \|0 - a^{b}\| = \|a^{b}\|$
174	166 169 173	3eqtrd	$⊢ (v \in D \land (a \in [0, +∞) \land b \in D)) \to (0 (x \in [0, +∞), y \in D ⟼ x^{y}) v) (abs \circ -) (a (x \in [0, +∞), y \in D ⟼ x^{y}) b) = \|a^{b}\|$
175	174	breq1d	$⊢ (v \in D \land (a \in [0, +∞) \land b \in D)) \to ((0 (x \in [0, +∞), y \in D ⟼ x^{y}) v) (abs \circ -) (a (x \in [0, +∞), y \in D ⟼ x^{y}) b) < e \leftrightarrow \|a^{b}\| < e)$
176	141 175	imbi12d	$⊢ (v \in D \land (a \in [0, +∞) \land b \in D)) \to (((0 ({(abs \circ -) ↾}_{([0, +∞) \times [0, +∞))}) a < d \land v ({(abs \circ -) ↾}_{(D \times D)}) b < d) \to (0 (x \in [0, +∞), y \in D ⟼ x^{y}) v) (abs \circ -) (a (x \in [0, +∞), y \in D ⟼ x^{y}) b) < e) \leftrightarrow ((\|a\| < d \land \|v - b\| < d) \to \|a^{b}\| < e))$
177	176	2ralbidva	$⊢ v \in D \to (\forall a \in [0, +∞) \forall b \in D ((0 ({(abs \circ -) ↾}_{([0, +∞) \times [0, +∞))}) a < d \land v ({(abs \circ -) ↾}_{(D \times D)}) b < d) \to (0 (x \in [0, +∞), y \in D ⟼ x^{y}) v) (abs \circ -) (a (x \in [0, +∞), y \in D ⟼ x^{y}) b) < e) \leftrightarrow \forall a \in [0, +∞) \forall b \in D ((\|a\| < d \land \|v - b\| < d) \to \|a^{b}\| < e))$
178	177	rexbidv	$⊢ v \in D \to (\exists d \in ℝ^{+} \forall a \in [0, +∞) \forall b \in D ((0 ({(abs \circ -) ↾}_{([0, +∞) \times [0, +∞))}) a < d \land v ({(abs \circ -) ↾}_{(D \times D)}) b < d) \to (0 (x \in [0, +∞), y \in D ⟼ x^{y}) v) (abs \circ -) (a (x \in [0, +∞), y \in D ⟼ x^{y}) b) < e) \leftrightarrow \exists d \in ℝ^{+} \forall a \in [0, +∞) \forall b \in D ((\|a\| < d \land \|v - b\| < d) \to \|a^{b}\| < e))$
179	178	ralbidv	$⊢ v \in D \to (\forall e \in ℝ^{+} \exists d \in ℝ^{+} \forall a \in [0, +∞) \forall b \in D ((0 ({(abs \circ -) ↾}_{([0, +∞) \times [0, +∞))}) a < d \land v ({(abs \circ -) ↾}_{(D \times D)}) b < d) \to (0 (x \in [0, +∞), y \in D ⟼ x^{y}) v) (abs \circ -) (a (x \in [0, +∞), y \in D ⟼ x^{y}) b) < e) \leftrightarrow \forall e \in ℝ^{+} \exists d \in ℝ^{+} \forall a \in [0, +∞) \forall b \in D ((\|a\| < d \land \|v - b\| < d) \to \|a^{b}\| < e))$
180	116 179	mpbird	$⊢ v \in D \to \forall e \in ℝ^{+} \exists d \in ℝ^{+} \forall a \in [0, +∞) \forall b \in D ((0 ({(abs \circ -) ↾}_{([0, +∞) \times [0, +∞))}) a < d \land v ({(abs \circ -) ↾}_{(D \times D)}) b < d) \to (0 (x \in [0, +∞), y \in D ⟼ x^{y}) v) (abs \circ -) (a (x \in [0, +∞), y \in D ⟼ x^{y}) b) < e)$
181		cnxmet	$⊢ abs \circ - \in ∞Met (ℂ)$
182	181	a1i	$⊢ v \in D \to abs \circ - \in ∞Met (ℂ)$
183		xmetres2	$⊢ (abs \circ - \in ∞Met (ℂ) \land [0, +∞) \subseteq ℂ) \to {(abs \circ -) ↾}_{([0, +∞) \times [0, +∞))} \in ∞Met ([0, +∞))$
184	182 7 183	sylancl	$⊢ v \in D \to {(abs \circ -) ↾}_{([0, +∞) \times [0, +∞))} \in ∞Met ([0, +∞))$
185		xmetres2	$⊢ (abs \circ - \in ∞Met (ℂ) \land D \subseteq ℂ) \to {(abs \circ -) ↾}_{(D \times D)} \in ∞Met (D)$
186	182 13 185	sylancl	$⊢ v \in D \to {(abs \circ -) ↾}_{(D \times D)} \in ∞Met (D)$
187	117	a1i	$⊢ v \in D \to 0 \in [0, +∞)$
188		id	$⊢ v \in D \to v \in D$
189		eqid	$⊢ {(abs \circ -) ↾}_{([0, +∞) \times [0, +∞))} = {(abs \circ -) ↾}_{([0, +∞) \times [0, +∞))}$
190	2	cnfldtopn	$⊢ J = MetOpen (abs \circ -)$
191		eqid	$⊢ MetOpen ({(abs \circ -) ↾}_{([0, +∞) \times [0, +∞))}) = MetOpen ({(abs \circ -) ↾}_{([0, +∞) \times [0, +∞))})$
192	189 190 191	metrest	$⊢ (abs \circ - \in ∞Met (ℂ) \land [0, +∞) \subseteq ℂ) \to J ↾_{𝑡} [0, +∞) = MetOpen ({(abs \circ -) ↾}_{([0, +∞) \times [0, +∞))})$
193	181 7 192	mp2an	$⊢ J ↾_{𝑡} [0, +∞) = MetOpen ({(abs \circ -) ↾}_{([0, +∞) \times [0, +∞))})$
194	3 193	eqtri	$⊢ K = MetOpen ({(abs \circ -) ↾}_{([0, +∞) \times [0, +∞))})$
195		eqid	$⊢ {(abs \circ -) ↾}_{(D \times D)} = {(abs \circ -) ↾}_{(D \times D)}$
196		eqid	$⊢ MetOpen ({(abs \circ -) ↾}_{(D \times D)}) = MetOpen ({(abs \circ -) ↾}_{(D \times D)})$
197	195 190 196	metrest	$⊢ (abs \circ - \in ∞Met (ℂ) \land D \subseteq ℂ) \to J ↾_{𝑡} D = MetOpen ({(abs \circ -) ↾}_{(D \times D)})$
198	181 13 197	mp2an	$⊢ J ↾_{𝑡} D = MetOpen ({(abs \circ -) ↾}_{(D \times D)})$
199	4 198	eqtri	$⊢ L = MetOpen ({(abs \circ -) ↾}_{(D \times D)})$
200	194 199 190	txmetcnp	$⊢ (({(abs \circ -) ↾}_{([0, +∞) \times [0, +∞))} \in ∞Met ([0, +∞)) \land {(abs \circ -) ↾}_{(D \times D)} \in ∞Met (D) \land abs \circ - \in ∞Met (ℂ)) \land (0 \in [0, +∞) \land v \in D)) \to ((x \in [0, +∞), y \in D ⟼ x^{y}) \in ((K \times_{t} L) CnP J) (⟨0, v⟩) \leftrightarrow ((x \in [0, +∞), y \in D ⟼ x^{y}) : [0, +∞) \times D ⟶ ℂ \land \forall e \in ℝ^{+} \exists d \in ℝ^{+} \forall a \in [0, +∞) \forall b \in D ((0 ({(abs \circ -) ↾}_{([0, +∞) \times [0, +∞))}) a < d \land v ({(abs \circ -) ↾}_{(D \times D)}) b < d) \to (0 (x \in [0, +∞), y \in D ⟼ x^{y}) v) (abs \circ -) (a (x \in [0, +∞), y \in D ⟼ x^{y}) b) < e)))$
201	184 186 182 187 188 200	syl32anc	$⊢ v \in D \to ((x \in [0, +∞), y \in D ⟼ x^{y}) \in ((K \times_{t} L) CnP J) (⟨0, v⟩) \leftrightarrow ((x \in [0, +∞), y \in D ⟼ x^{y}) : [0, +∞) \times D ⟶ ℂ \land \forall e \in ℝ^{+} \exists d \in ℝ^{+} \forall a \in [0, +∞) \forall b \in D ((0 ({(abs \circ -) ↾}_{([0, +∞) \times [0, +∞))}) a < d \land v ({(abs \circ -) ↾}_{(D \times D)}) b < d) \to (0 (x \in [0, +∞), y \in D ⟼ x^{y}) v) (abs \circ -) (a (x \in [0, +∞), y \in D ⟼ x^{y}) b) < e)))$
202	112 180 201	mpbir2and	$⊢ v \in D \to (x \in [0, +∞), y \in D ⟼ x^{y}) \in ((K \times_{t} L) CnP J) (⟨0, v⟩)$
203	202	ad2antlr	$⊢ ((u \in [0, +∞) \land v \in D) \land 0 = u) \to (x \in [0, +∞), y \in D ⟼ x^{y}) \in ((K \times_{t} L) CnP J) (⟨0, v⟩)$
204		simpr	$⊢ ((u \in [0, +∞) \land v \in D) \land 0 = u) \to 0 = u$
205	204	opeq1d	$⊢ ((u \in [0, +∞) \land v \in D) \land 0 = u) \to ⟨0, v⟩ = ⟨u, v⟩$
206	205	fveq2d	$⊢ ((u \in [0, +∞) \land v \in D) \land 0 = u) \to ((K \times_{t} L) CnP J) (⟨0, v⟩) = ((K \times_{t} L) CnP J) (⟨u, v⟩)$
207	203 206	eleqtrd	$⊢ ((u \in [0, +∞) \land v \in D) \land 0 = u) \to (x \in [0, +∞), y \in D ⟼ x^{y}) \in ((K \times_{t} L) CnP J) (⟨u, v⟩)$
208	40	simprbi	$⊢ u \in [0, +∞) \to 0 \leq u$
209	208	adantr	$⊢ (u \in [0, +∞) \land v \in D) \to 0 \leq u$
210		0re	$⊢ 0 \in ℝ$
211		leloe	$⊢ (0 \in ℝ \land u \in ℝ) \to (0 \leq u \leftrightarrow (0 < u \lor 0 = u))$
212	210 42 211	sylancr	$⊢ (u \in [0, +∞) \land v \in D) \to (0 \leq u \leftrightarrow (0 < u \lor 0 = u))$
213	209 212	mpbid	$⊢ (u \in [0, +∞) \land v \in D) \to (0 < u \lor 0 = u)$
214	111 207 213	mpjaodan	$⊢ (u \in [0, +∞) \land v \in D) \to (x \in [0, +∞), y \in D ⟼ x^{y}) \in ((K \times_{t} L) CnP J) (⟨u, v⟩)$
215	214	rgen2	$⊢ \forall u \in [0, +∞) \forall v \in D (x \in [0, +∞), y \in D ⟼ x^{y}) \in ((K \times_{t} L) CnP J) (⟨u, v⟩)$
216		fveq2	$⊢ z = ⟨u, v⟩ \to ((K \times_{t} L) CnP J) (z) = ((K \times_{t} L) CnP J) (⟨u, v⟩)$
217	216	eleq2d	$⊢ z = ⟨u, v⟩ \to ((x \in [0, +∞), y \in D ⟼ x^{y}) \in ((K \times_{t} L) CnP J) (z) \leftrightarrow (x \in [0, +∞), y \in D ⟼ x^{y}) \in ((K \times_{t} L) CnP J) (⟨u, v⟩))$
218	217	ralxp	$⊢ \forall z \in ([0, +∞) \times D) (x \in [0, +∞), y \in D ⟼ x^{y}) \in ((K \times_{t} L) CnP J) (z) \leftrightarrow \forall u \in [0, +∞) \forall v \in D (x \in [0, +∞), y \in D ⟼ x^{y}) \in ((K \times_{t} L) CnP J) (⟨u, v⟩)$
219	215 218	mpbir	$⊢ \forall z \in ([0, +∞) \times D) (x \in [0, +∞), y \in D ⟼ x^{y}) \in ((K \times_{t} L) CnP J) (z)$
220		cncnp	$⊢ (K \times_{t} L \in TopOn ([0, +∞) \times D) \land J \in TopOn (ℂ)) \to ((x \in [0, +∞), y \in D ⟼ x^{y}) \in ((K \times_{t} L) Cn J) \leftrightarrow ((x \in [0, +∞), y \in D ⟼ x^{y}) : [0, +∞) \times D ⟶ ℂ \land \forall z \in ([0, +∞) \times D) (x \in [0, +∞), y \in D ⟼ x^{y}) \in ((K \times_{t} L) CnP J) (z)))$
221	93 21 220	mp2an	$⊢ (x \in [0, +∞), y \in D ⟼ x^{y}) \in ((K \times_{t} L) Cn J) \leftrightarrow ((x \in [0, +∞), y \in D ⟼ x^{y}) : [0, +∞) \times D ⟶ ℂ \land \forall z \in ([0, +∞) \times D) (x \in [0, +∞), y \in D ⟼ x^{y}) \in ((K \times_{t} L) CnP J) (z))$
222	20 219 221	mpbir2an	$⊢ (x \in [0, +∞), y \in D ⟼ x^{y}) \in ((K \times_{t} L) Cn J)$

Metamath Proof Explorer

Theorem cxpcn3

Proof