cxpcn3lem

	Ref	Expression
Hypotheses	cxpcn3.d	$⊢ D = ℜ^{-1} [ℝ^{+}]$
	cxpcn3.j	$⊢ J = TopOpen (ℂ_{fld})$
	cxpcn3.k	$⊢ K = J ↾_{𝑡} [0, +∞)$
	cxpcn3.l	$⊢ L = J ↾_{𝑡} D$
	cxpcn3.u	$⊢ U = \frac{if (ℜ (A) \leq 1, ℜ (A), 1)}{2}$
	cxpcn3.t	$⊢ T = if (U \leq E^{\frac{1}{U}}, U, E^{\frac{1}{U}})$
Assertion	cxpcn3lem	$⊢ (A \in D \land E \in ℝ^{+}) \to \exists d \in ℝ^{+} \forall a \in [0, +∞) \forall b \in D ((\|a\| < d \land \|A - b\| < d) \to \|a^{b}\| < E)$

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		cxpcn3.u	$⊢ U = \frac{if (ℜ (A) \leq 1, ℜ (A), 1)}{2}$
6		cxpcn3.t	$⊢ T = if (U \leq E^{\frac{1}{U}}, U, E^{\frac{1}{U}})$
7	1	eleq2i	$⊢ A \in D \leftrightarrow A \in ℜ^{-1} [ℝ^{+}]$
8		ref	$⊢ ℜ : ℂ ⟶ ℝ$
9		ffn	$⊢ ℜ : ℂ ⟶ ℝ \to ℜ Fn ℂ$
10		elpreima	$⊢ ℜ Fn ℂ \to (A \in ℜ^{-1} [ℝ^{+}] \leftrightarrow (A \in ℂ \land ℜ (A) \in ℝ^{+}))$
11	8 9 10	mp2b	$⊢ A \in ℜ^{-1} [ℝ^{+}] \leftrightarrow (A \in ℂ \land ℜ (A) \in ℝ^{+})$
12	7 11	bitri	$⊢ A \in D \leftrightarrow (A \in ℂ \land ℜ (A) \in ℝ^{+})$
13	12	simprbi	$⊢ A \in D \to ℜ (A) \in ℝ^{+}$
14	13	adantr	$⊢ (A \in D \land E \in ℝ^{+}) \to ℜ (A) \in ℝ^{+}$
15		1rp	$⊢ 1 \in ℝ^{+}$
16		ifcl	$⊢ (ℜ (A) \in ℝ^{+} \land 1 \in ℝ^{+}) \to if (ℜ (A) \leq 1, ℜ (A), 1) \in ℝ^{+}$
17	14 15 16	sylancl	$⊢ (A \in D \land E \in ℝ^{+}) \to if (ℜ (A) \leq 1, ℜ (A), 1) \in ℝ^{+}$
18	17	rphalfcld	$⊢ (A \in D \land E \in ℝ^{+}) \to \frac{if (ℜ (A) \leq 1, ℜ (A), 1)}{2} \in ℝ^{+}$
19	5 18	eqeltrid	$⊢ (A \in D \land E \in ℝ^{+}) \to U \in ℝ^{+}$
20		simpr	$⊢ (A \in D \land E \in ℝ^{+}) \to E \in ℝ^{+}$
21	19	rpreccld	$⊢ (A \in D \land E \in ℝ^{+}) \to \frac{1}{U} \in ℝ^{+}$
22	21	rpred	$⊢ (A \in D \land E \in ℝ^{+}) \to \frac{1}{U} \in ℝ$
23	20 22	rpcxpcld	$⊢ (A \in D \land E \in ℝ^{+}) \to E^{\frac{1}{U}} \in ℝ^{+}$
24	19 23	ifcld	$⊢ (A \in D \land E \in ℝ^{+}) \to if (U \leq E^{\frac{1}{U}}, U, E^{\frac{1}{U}}) \in ℝ^{+}$
25	6 24	eqeltrid	$⊢ (A \in D \land E \in ℝ^{+}) \to T \in ℝ^{+}$
26		elrege0	$⊢ a \in [0, +∞) \leftrightarrow (a \in ℝ \land 0 \leq a)$
27		0red	$⊢ (A \in D \land E \in ℝ^{+}) \to 0 \in ℝ$
28		leloe	$⊢ (0 \in ℝ \land a \in ℝ) \to (0 \leq a \leftrightarrow (0 < a \lor 0 = a))$
29	27 28	sylan	$⊢ ((A \in D \land E \in ℝ^{+}) \land a \in ℝ) \to (0 \leq a \leftrightarrow (0 < a \lor 0 = a))$
30		elrp	$⊢ a \in ℝ^{+} \leftrightarrow (a \in ℝ \land 0 < a)$
31		simp2l	$⊢ ((A \in D \land E \in ℝ^{+}) \land (a \in ℝ^{+} \land b \in D) \land (\|a\| < T \land \|A - b\| < T)) \to a \in ℝ^{+}$
32		simp2r	$⊢ ((A \in D \land E \in ℝ^{+}) \land (a \in ℝ^{+} \land b \in D) \land (\|a\| < T \land \|A - b\| < T)) \to b \in D$
33		cnvimass	$⊢ ℜ^{-1} [ℝ^{+}] \subseteq dom ℜ$
34	8	fdmi	$⊢ dom ℜ = ℂ$
35	33 34	sseqtri	$⊢ ℜ^{-1} [ℝ^{+}] \subseteq ℂ$
36	1 35	eqsstri	$⊢ D \subseteq ℂ$
37	36	sseli	$⊢ b \in D \to b \in ℂ$
38	32 37	syl	$⊢ ((A \in D \land E \in ℝ^{+}) \land (a \in ℝ^{+} \land b \in D) \land (\|a\| < T \land \|A - b\| < T)) \to b \in ℂ$
39		abscxp	$⊢ (a \in ℝ^{+} \land b \in ℂ) \to \|a^{b}\| = a^{ℜ (b)}$
40	31 38 39	syl2anc	$⊢ ((A \in D \land E \in ℝ^{+}) \land (a \in ℝ^{+} \land b \in D) \land (\|a\| < T \land \|A - b\| < T)) \to \|a^{b}\| = a^{ℜ (b)}$
41	38	recld	$⊢ ((A \in D \land E \in ℝ^{+}) \land (a \in ℝ^{+} \land b \in D) \land (\|a\| < T \land \|A - b\| < T)) \to ℜ (b) \in ℝ$
42	31 41	rpcxpcld	$⊢ ((A \in D \land E \in ℝ^{+}) \land (a \in ℝ^{+} \land b \in D) \land (\|a\| < T \land \|A - b\| < T)) \to a^{ℜ (b)} \in ℝ^{+}$
43	42	rpred	$⊢ ((A \in D \land E \in ℝ^{+}) \land (a \in ℝ^{+} \land b \in D) \land (\|a\| < T \land \|A - b\| < T)) \to a^{ℜ (b)} \in ℝ$
44	19	3ad2ant1	$⊢ ((A \in D \land E \in ℝ^{+}) \land (a \in ℝ^{+} \land b \in D) \land (\|a\| < T \land \|A - b\| < T)) \to U \in ℝ^{+}$
45	44	rpred	$⊢ ((A \in D \land E \in ℝ^{+}) \land (a \in ℝ^{+} \land b \in D) \land (\|a\| < T \land \|A - b\| < T)) \to U \in ℝ$
46	31 45	rpcxpcld	$⊢ ((A \in D \land E \in ℝ^{+}) \land (a \in ℝ^{+} \land b \in D) \land (\|a\| < T \land \|A - b\| < T)) \to a^{U} \in ℝ^{+}$
47	46	rpred	$⊢ ((A \in D \land E \in ℝ^{+}) \land (a \in ℝ^{+} \land b \in D) \land (\|a\| < T \land \|A - b\| < T)) \to a^{U} \in ℝ$
48		simp1r	$⊢ ((A \in D \land E \in ℝ^{+}) \land (a \in ℝ^{+} \land b \in D) \land (\|a\| < T \land \|A - b\| < T)) \to E \in ℝ^{+}$
49	48	rpred	$⊢ ((A \in D \land E \in ℝ^{+}) \land (a \in ℝ^{+} \land b \in D) \land (\|a\| < T \land \|A - b\| < T)) \to E \in ℝ$
50		simp1l	$⊢ ((A \in D \land E \in ℝ^{+}) \land (a \in ℝ^{+} \land b \in D) \land (\|a\| < T \land \|A - b\| < T)) \to A \in D$
51	12	simplbi	$⊢ A \in D \to A \in ℂ$
52	50 51	syl	$⊢ ((A \in D \land E \in ℝ^{+}) \land (a \in ℝ^{+} \land b \in D) \land (\|a\| < T \land \|A - b\| < T)) \to A \in ℂ$
53	52	recld	$⊢ ((A \in D \land E \in ℝ^{+}) \land (a \in ℝ^{+} \land b \in D) \land (\|a\| < T \land \|A - b\| < T)) \to ℜ (A) \in ℝ$
54	53	rehalfcld	$⊢ ((A \in D \land E \in ℝ^{+}) \land (a \in ℝ^{+} \land b \in D) \land (\|a\| < T \land \|A - b\| < T)) \to \frac{ℜ (A)}{2} \in ℝ$
55		1re	$⊢ 1 \in ℝ$
56		min1	$⊢ (ℜ (A) \in ℝ \land 1 \in ℝ) \to if (ℜ (A) \leq 1, ℜ (A), 1) \leq ℜ (A)$
57	53 55 56	sylancl	$⊢ ((A \in D \land E \in ℝ^{+}) \land (a \in ℝ^{+} \land b \in D) \land (\|a\| < T \land \|A - b\| < T)) \to if (ℜ (A) \leq 1, ℜ (A), 1) \leq ℜ (A)$
58	17	3ad2ant1	$⊢ ((A \in D \land E \in ℝ^{+}) \land (a \in ℝ^{+} \land b \in D) \land (\|a\| < T \land \|A - b\| < T)) \to if (ℜ (A) \leq 1, ℜ (A), 1) \in ℝ^{+}$
59	58	rpred	$⊢ ((A \in D \land E \in ℝ^{+}) \land (a \in ℝ^{+} \land b \in D) \land (\|a\| < T \land \|A - b\| < T)) \to if (ℜ (A) \leq 1, ℜ (A), 1) \in ℝ$
60		2re	$⊢ 2 \in ℝ$
61	60	a1i	$⊢ ((A \in D \land E \in ℝ^{+}) \land (a \in ℝ^{+} \land b \in D) \land (\|a\| < T \land \|A - b\| < T)) \to 2 \in ℝ$
62		2pos	$⊢ 0 < 2$
63	62	a1i	$⊢ ((A \in D \land E \in ℝ^{+}) \land (a \in ℝ^{+} \land b \in D) \land (\|a\| < T \land \|A - b\| < T)) \to 0 < 2$
64		lediv1	$⊢ (if (ℜ (A) \leq 1, ℜ (A), 1) \in ℝ \land ℜ (A) \in ℝ \land (2 \in ℝ \land 0 < 2)) \to (if (ℜ (A) \leq 1, ℜ (A), 1) \leq ℜ (A) \leftrightarrow \frac{if (ℜ (A) \leq 1, ℜ (A), 1)}{2} \leq \frac{ℜ (A)}{2})$
65	59 53 61 63 64	syl112anc	$⊢ ((A \in D \land E \in ℝ^{+}) \land (a \in ℝ^{+} \land b \in D) \land (\|a\| < T \land \|A - b\| < T)) \to (if (ℜ (A) \leq 1, ℜ (A), 1) \leq ℜ (A) \leftrightarrow \frac{if (ℜ (A) \leq 1, ℜ (A), 1)}{2} \leq \frac{ℜ (A)}{2})$
66	57 65	mpbid	$⊢ ((A \in D \land E \in ℝ^{+}) \land (a \in ℝ^{+} \land b \in D) \land (\|a\| < T \land \|A - b\| < T)) \to \frac{if (ℜ (A) \leq 1, ℜ (A), 1)}{2} \leq \frac{ℜ (A)}{2}$
67	5 66	eqbrtrid	$⊢ ((A \in D \land E \in ℝ^{+}) \land (a \in ℝ^{+} \land b \in D) \land (\|a\| < T \land \|A - b\| < T)) \to U \leq \frac{ℜ (A)}{2}$
68	53	recnd	$⊢ ((A \in D \land E \in ℝ^{+}) \land (a \in ℝ^{+} \land b \in D) \land (\|a\| < T \land \|A - b\| < T)) \to ℜ (A) \in ℂ$
69	68	2halvesd	$⊢ ((A \in D \land E \in ℝ^{+}) \land (a \in ℝ^{+} \land b \in D) \land (\|a\| < T \land \|A - b\| < T)) \to (\frac{ℜ (A)}{2}) + (\frac{ℜ (A)}{2}) = ℜ (A)$
70	52 38	resubd	$⊢ ((A \in D \land E \in ℝ^{+}) \land (a \in ℝ^{+} \land b \in D) \land (\|a\| < T \land \|A - b\| < T)) \to ℜ (A - b) = ℜ (A) - ℜ (b)$
71	52 38	subcld	$⊢ ((A \in D \land E \in ℝ^{+}) \land (a \in ℝ^{+} \land b \in D) \land (\|a\| < T \land \|A - b\| < T)) \to A - b \in ℂ$
72	71	recld	$⊢ ((A \in D \land E \in ℝ^{+}) \land (a \in ℝ^{+} \land b \in D) \land (\|a\| < T \land \|A - b\| < T)) \to ℜ (A - b) \in ℝ$
73	71	abscld	$⊢ ((A \in D \land E \in ℝ^{+}) \land (a \in ℝ^{+} \land b \in D) \land (\|a\| < T \land \|A - b\| < T)) \to \|A - b\| \in ℝ$
74	71	releabsd	$⊢ ((A \in D \land E \in ℝ^{+}) \land (a \in ℝ^{+} \land b \in D) \land (\|a\| < T \land \|A - b\| < T)) \to ℜ (A - b) \leq \|A - b\|$
75		simp3r	$⊢ ((A \in D \land E \in ℝ^{+}) \land (a \in ℝ^{+} \land b \in D) \land (\|a\| < T \land \|A - b\| < T)) \to \|A - b\| < T$
76	75 6	breqtrdi	$⊢ ((A \in D \land E \in ℝ^{+}) \land (a \in ℝ^{+} \land b \in D) \land (\|a\| < T \land \|A - b\| < T)) \to \|A - b\| < if (U \leq E^{\frac{1}{U}}, U, E^{\frac{1}{U}})$
77	23	3ad2ant1	$⊢ ((A \in D \land E \in ℝ^{+}) \land (a \in ℝ^{+} \land b \in D) \land (\|a\| < T \land \|A - b\| < T)) \to E^{\frac{1}{U}} \in ℝ^{+}$
78	77	rpred	$⊢ ((A \in D \land E \in ℝ^{+}) \land (a \in ℝ^{+} \land b \in D) \land (\|a\| < T \land \|A - b\| < T)) \to E^{\frac{1}{U}} \in ℝ$
79		ltmin	$⊢ (\|A - b\| \in ℝ \land U \in ℝ \land E^{\frac{1}{U}} \in ℝ) \to (\|A - b\| < if (U \leq E^{\frac{1}{U}}, U, E^{\frac{1}{U}}) \leftrightarrow (\|A - b\| < U \land \|A - b\| < E^{\frac{1}{U}}))$
80	73 45 78 79	syl3anc	$⊢ ((A \in D \land E \in ℝ^{+}) \land (a \in ℝ^{+} \land b \in D) \land (\|a\| < T \land \|A - b\| < T)) \to (\|A - b\| < if (U \leq E^{\frac{1}{U}}, U, E^{\frac{1}{U}}) \leftrightarrow (\|A - b\| < U \land \|A - b\| < E^{\frac{1}{U}}))$
81	76 80	mpbid	$⊢ ((A \in D \land E \in ℝ^{+}) \land (a \in ℝ^{+} \land b \in D) \land (\|a\| < T \land \|A - b\| < T)) \to (\|A - b\| < U \land \|A - b\| < E^{\frac{1}{U}})$
82	81	simpld	$⊢ ((A \in D \land E \in ℝ^{+}) \land (a \in ℝ^{+} \land b \in D) \land (\|a\| < T \land \|A - b\| < T)) \to \|A - b\| < U$
83	72 73 45 74 82	lelttrd	$⊢ ((A \in D \land E \in ℝ^{+}) \land (a \in ℝ^{+} \land b \in D) \land (\|a\| < T \land \|A - b\| < T)) \to ℜ (A - b) < U$
84	72 45 54 83 67	ltletrd	$⊢ ((A \in D \land E \in ℝ^{+}) \land (a \in ℝ^{+} \land b \in D) \land (\|a\| < T \land \|A - b\| < T)) \to ℜ (A - b) < \frac{ℜ (A)}{2}$
85	70 84	eqbrtrrd	$⊢ ((A \in D \land E \in ℝ^{+}) \land (a \in ℝ^{+} \land b \in D) \land (\|a\| < T \land \|A - b\| < T)) \to ℜ (A) - ℜ (b) < \frac{ℜ (A)}{2}$
86	53 41 54	ltsubadd2d	$⊢ ((A \in D \land E \in ℝ^{+}) \land (a \in ℝ^{+} \land b \in D) \land (\|a\| < T \land \|A - b\| < T)) \to (ℜ (A) - ℜ (b) < \frac{ℜ (A)}{2} \leftrightarrow ℜ (A) < ℜ (b) + (\frac{ℜ (A)}{2}))$
87	85 86	mpbid	$⊢ ((A \in D \land E \in ℝ^{+}) \land (a \in ℝ^{+} \land b \in D) \land (\|a\| < T \land \|A - b\| < T)) \to ℜ (A) < ℜ (b) + (\frac{ℜ (A)}{2})$
88	69 87	eqbrtrd	$⊢ ((A \in D \land E \in ℝ^{+}) \land (a \in ℝ^{+} \land b \in D) \land (\|a\| < T \land \|A - b\| < T)) \to (\frac{ℜ (A)}{2}) + (\frac{ℜ (A)}{2}) < ℜ (b) + (\frac{ℜ (A)}{2})$
89	54 41 54	ltadd1d	$⊢ ((A \in D \land E \in ℝ^{+}) \land (a \in ℝ^{+} \land b \in D) \land (\|a\| < T \land \|A - b\| < T)) \to (\frac{ℜ (A)}{2} < ℜ (b) \leftrightarrow (\frac{ℜ (A)}{2}) + (\frac{ℜ (A)}{2}) < ℜ (b) + (\frac{ℜ (A)}{2}))$
90	88 89	mpbird	$⊢ ((A \in D \land E \in ℝ^{+}) \land (a \in ℝ^{+} \land b \in D) \land (\|a\| < T \land \|A - b\| < T)) \to \frac{ℜ (A)}{2} < ℜ (b)$
91	45 54 41 67 90	lelttrd	$⊢ ((A \in D \land E \in ℝ^{+}) \land (a \in ℝ^{+} \land b \in D) \land (\|a\| < T \land \|A - b\| < T)) \to U < ℜ (b)$
92	31	rpred	$⊢ ((A \in D \land E \in ℝ^{+}) \land (a \in ℝ^{+} \land b \in D) \land (\|a\| < T \land \|A - b\| < T)) \to a \in ℝ$
93	55	a1i	$⊢ ((A \in D \land E \in ℝ^{+}) \land (a \in ℝ^{+} \land b \in D) \land (\|a\| < T \land \|A - b\| < T)) \to 1 \in ℝ$
94	31	rprege0d	$⊢ ((A \in D \land E \in ℝ^{+}) \land (a \in ℝ^{+} \land b \in D) \land (\|a\| < T \land \|A - b\| < T)) \to (a \in ℝ \land 0 \leq a)$
95		absid	$⊢ (a \in ℝ \land 0 \leq a) \to \|a\| = a$
96	94 95	syl	$⊢ ((A \in D \land E \in ℝ^{+}) \land (a \in ℝ^{+} \land b \in D) \land (\|a\| < T \land \|A - b\| < T)) \to \|a\| = a$
97		simp3l	$⊢ ((A \in D \land E \in ℝ^{+}) \land (a \in ℝ^{+} \land b \in D) \land (\|a\| < T \land \|A - b\| < T)) \to \|a\| < T$
98	96 97	eqbrtrrd	$⊢ ((A \in D \land E \in ℝ^{+}) \land (a \in ℝ^{+} \land b \in D) \land (\|a\| < T \land \|A - b\| < T)) \to a < T$
99	98 6	breqtrdi	$⊢ ((A \in D \land E \in ℝ^{+}) \land (a \in ℝ^{+} \land b \in D) \land (\|a\| < T \land \|A - b\| < T)) \to a < if (U \leq E^{\frac{1}{U}}, U, E^{\frac{1}{U}})$
100		ltmin	$⊢ (a \in ℝ \land U \in ℝ \land E^{\frac{1}{U}} \in ℝ) \to (a < if (U \leq E^{\frac{1}{U}}, U, E^{\frac{1}{U}}) \leftrightarrow (a < U \land a < E^{\frac{1}{U}}))$
101	92 45 78 100	syl3anc	$⊢ ((A \in D \land E \in ℝ^{+}) \land (a \in ℝ^{+} \land b \in D) \land (\|a\| < T \land \|A - b\| < T)) \to (a < if (U \leq E^{\frac{1}{U}}, U, E^{\frac{1}{U}}) \leftrightarrow (a < U \land a < E^{\frac{1}{U}}))$
102	99 101	mpbid	$⊢ ((A \in D \land E \in ℝ^{+}) \land (a \in ℝ^{+} \land b \in D) \land (\|a\| < T \land \|A - b\| < T)) \to (a < U \land a < E^{\frac{1}{U}})$
103	102	simpld	$⊢ ((A \in D \land E \in ℝ^{+}) \land (a \in ℝ^{+} \land b \in D) \land (\|a\| < T \land \|A - b\| < T)) \to a < U$
104		rehalfcl	$⊢ 1 \in ℝ \to \frac{1}{2} \in ℝ$
105	55 104	mp1i	$⊢ ((A \in D \land E \in ℝ^{+}) \land (a \in ℝ^{+} \land b \in D) \land (\|a\| < T \land \|A - b\| < T)) \to \frac{1}{2} \in ℝ$
106		min2	$⊢ (ℜ (A) \in ℝ \land 1 \in ℝ) \to if (ℜ (A) \leq 1, ℜ (A), 1) \leq 1$
107	53 55 106	sylancl	$⊢ ((A \in D \land E \in ℝ^{+}) \land (a \in ℝ^{+} \land b \in D) \land (\|a\| < T \land \|A - b\| < T)) \to if (ℜ (A) \leq 1, ℜ (A), 1) \leq 1$
108		lediv1	$⊢ (if (ℜ (A) \leq 1, ℜ (A), 1) \in ℝ \land 1 \in ℝ \land (2 \in ℝ \land 0 < 2)) \to (if (ℜ (A) \leq 1, ℜ (A), 1) \leq 1 \leftrightarrow \frac{if (ℜ (A) \leq 1, ℜ (A), 1)}{2} \leq \frac{1}{2})$
109	59 93 61 63 108	syl112anc	$⊢ ((A \in D \land E \in ℝ^{+}) \land (a \in ℝ^{+} \land b \in D) \land (\|a\| < T \land \|A - b\| < T)) \to (if (ℜ (A) \leq 1, ℜ (A), 1) \leq 1 \leftrightarrow \frac{if (ℜ (A) \leq 1, ℜ (A), 1)}{2} \leq \frac{1}{2})$
110	107 109	mpbid	$⊢ ((A \in D \land E \in ℝ^{+}) \land (a \in ℝ^{+} \land b \in D) \land (\|a\| < T \land \|A - b\| < T)) \to \frac{if (ℜ (A) \leq 1, ℜ (A), 1)}{2} \leq \frac{1}{2}$
111	5 110	eqbrtrid	$⊢ ((A \in D \land E \in ℝ^{+}) \land (a \in ℝ^{+} \land b \in D) \land (\|a\| < T \land \|A - b\| < T)) \to U \leq \frac{1}{2}$
112		halflt1	$⊢ \frac{1}{2} < 1$
113	112	a1i	$⊢ ((A \in D \land E \in ℝ^{+}) \land (a \in ℝ^{+} \land b \in D) \land (\|a\| < T \land \|A - b\| < T)) \to \frac{1}{2} < 1$
114	45 105 93 111 113	lelttrd	$⊢ ((A \in D \land E \in ℝ^{+}) \land (a \in ℝ^{+} \land b \in D) \land (\|a\| < T \land \|A - b\| < T)) \to U < 1$
115	92 45 93 103 114	lttrd	$⊢ ((A \in D \land E \in ℝ^{+}) \land (a \in ℝ^{+} \land b \in D) \land (\|a\| < T \land \|A - b\| < T)) \to a < 1$
116	31 45 115 41	cxplt3d	$⊢ ((A \in D \land E \in ℝ^{+}) \land (a \in ℝ^{+} \land b \in D) \land (\|a\| < T \land \|A - b\| < T)) \to (U < ℜ (b) \leftrightarrow a^{ℜ (b)} < a^{U})$
117	91 116	mpbid	$⊢ ((A \in D \land E \in ℝ^{+}) \land (a \in ℝ^{+} \land b \in D) \land (\|a\| < T \land \|A - b\| < T)) \to a^{ℜ (b)} < a^{U}$
118	44	rpcnne0d	$⊢ ((A \in D \land E \in ℝ^{+}) \land (a \in ℝ^{+} \land b \in D) \land (\|a\| < T \land \|A - b\| < T)) \to (U \in ℂ \land U \neq 0)$
119		recid	$⊢ (U \in ℂ \land U \neq 0) \to U (\frac{1}{U}) = 1$
120	118 119	syl	$⊢ ((A \in D \land E \in ℝ^{+}) \land (a \in ℝ^{+} \land b \in D) \land (\|a\| < T \land \|A - b\| < T)) \to U (\frac{1}{U}) = 1$
121	120	oveq2d	$⊢ ((A \in D \land E \in ℝ^{+}) \land (a \in ℝ^{+} \land b \in D) \land (\|a\| < T \land \|A - b\| < T)) \to a^{U (\frac{1}{U})} = a^{1}$
122	44	rpreccld	$⊢ ((A \in D \land E \in ℝ^{+}) \land (a \in ℝ^{+} \land b \in D) \land (\|a\| < T \land \|A - b\| < T)) \to \frac{1}{U} \in ℝ^{+}$
123	122	rpcnd	$⊢ ((A \in D \land E \in ℝ^{+}) \land (a \in ℝ^{+} \land b \in D) \land (\|a\| < T \land \|A - b\| < T)) \to \frac{1}{U} \in ℂ$
124	31 45 123	cxpmuld	$⊢ ((A \in D \land E \in ℝ^{+}) \land (a \in ℝ^{+} \land b \in D) \land (\|a\| < T \land \|A - b\| < T)) \to a^{U (\frac{1}{U})} = {(a^{U})}^{\frac{1}{U}}$
125	31	rpcnd	$⊢ ((A \in D \land E \in ℝ^{+}) \land (a \in ℝ^{+} \land b \in D) \land (\|a\| < T \land \|A - b\| < T)) \to a \in ℂ$
126	125	cxp1d	$⊢ ((A \in D \land E \in ℝ^{+}) \land (a \in ℝ^{+} \land b \in D) \land (\|a\| < T \land \|A - b\| < T)) \to a^{1} = a$
127	121 124 126	3eqtr3d	$⊢ ((A \in D \land E \in ℝ^{+}) \land (a \in ℝ^{+} \land b \in D) \land (\|a\| < T \land \|A - b\| < T)) \to {(a^{U})}^{\frac{1}{U}} = a$
128	102	simprd	$⊢ ((A \in D \land E \in ℝ^{+}) \land (a \in ℝ^{+} \land b \in D) \land (\|a\| < T \land \|A - b\| < T)) \to a < E^{\frac{1}{U}}$
129	127 128	eqbrtrd	$⊢ ((A \in D \land E \in ℝ^{+}) \land (a \in ℝ^{+} \land b \in D) \land (\|a\| < T \land \|A - b\| < T)) \to {(a^{U})}^{\frac{1}{U}} < E^{\frac{1}{U}}$
130	46	rprege0d	$⊢ ((A \in D \land E \in ℝ^{+}) \land (a \in ℝ^{+} \land b \in D) \land (\|a\| < T \land \|A - b\| < T)) \to (a^{U} \in ℝ \land 0 \leq a^{U})$
131	48	rprege0d	$⊢ ((A \in D \land E \in ℝ^{+}) \land (a \in ℝ^{+} \land b \in D) \land (\|a\| < T \land \|A - b\| < T)) \to (E \in ℝ \land 0 \leq E)$
132		cxplt2	$⊢ ((a^{U} \in ℝ \land 0 \leq a^{U}) \land (E \in ℝ \land 0 \leq E) \land \frac{1}{U} \in ℝ^{+}) \to (a^{U} < E \leftrightarrow {(a^{U})}^{\frac{1}{U}} < E^{\frac{1}{U}})$
133	130 131 122 132	syl3anc	$⊢ ((A \in D \land E \in ℝ^{+}) \land (a \in ℝ^{+} \land b \in D) \land (\|a\| < T \land \|A - b\| < T)) \to (a^{U} < E \leftrightarrow {(a^{U})}^{\frac{1}{U}} < E^{\frac{1}{U}})$
134	129 133	mpbird	$⊢ ((A \in D \land E \in ℝ^{+}) \land (a \in ℝ^{+} \land b \in D) \land (\|a\| < T \land \|A - b\| < T)) \to a^{U} < E$
135	43 47 49 117 134	lttrd	$⊢ ((A \in D \land E \in ℝ^{+}) \land (a \in ℝ^{+} \land b \in D) \land (\|a\| < T \land \|A - b\| < T)) \to a^{ℜ (b)} < E$
136	40 135	eqbrtrd	$⊢ ((A \in D \land E \in ℝ^{+}) \land (a \in ℝ^{+} \land b \in D) \land (\|a\| < T \land \|A - b\| < T)) \to \|a^{b}\| < E$
137	136	3expia	$⊢ ((A \in D \land E \in ℝ^{+}) \land (a \in ℝ^{+} \land b \in D)) \to ((\|a\| < T \land \|A - b\| < T) \to \|a^{b}\| < E)$
138	137	anassrs	$⊢ (((A \in D \land E \in ℝ^{+}) \land a \in ℝ^{+}) \land b \in D) \to ((\|a\| < T \land \|A - b\| < T) \to \|a^{b}\| < E)$
139	138	ralrimiva	$⊢ ((A \in D \land E \in ℝ^{+}) \land a \in ℝ^{+}) \to \forall b \in D ((\|a\| < T \land \|A - b\| < T) \to \|a^{b}\| < E)$
140	30 139	sylan2br	$⊢ ((A \in D \land E \in ℝ^{+}) \land (a \in ℝ \land 0 < a)) \to \forall b \in D ((\|a\| < T \land \|A - b\| < T) \to \|a^{b}\| < E)$
141	140	expr	$⊢ ((A \in D \land E \in ℝ^{+}) \land a \in ℝ) \to (0 < a \to \forall b \in D ((\|a\| < T \land \|A - b\| < T) \to \|a^{b}\| < E))$
142		elpreima	$⊢ ℜ Fn ℂ \to (b \in ℜ^{-1} [ℝ^{+}] \leftrightarrow (b \in ℂ \land ℜ (b) \in ℝ^{+}))$
143	8 9 142	mp2b	$⊢ b \in ℜ^{-1} [ℝ^{+}] \leftrightarrow (b \in ℂ \land ℜ (b) \in ℝ^{+})$
144	143	simprbi	$⊢ b \in ℜ^{-1} [ℝ^{+}] \to ℜ (b) \in ℝ^{+}$
145	144 1	eleq2s	$⊢ b \in D \to ℜ (b) \in ℝ^{+}$
146	145	rpne0d	$⊢ b \in D \to ℜ (b) \neq 0$
147		fveq2	$⊢ b = 0 \to ℜ (b) = ℜ (0)$
148		re0	$⊢ ℜ (0) = 0$
149	147 148	eqtrdi	$⊢ b = 0 \to ℜ (b) = 0$
150	149	necon3i	$⊢ ℜ (b) \neq 0 \to b \neq 0$
151	146 150	syl	$⊢ b \in D \to b \neq 0$
152	37 151	0cxpd	$⊢ b \in D \to 0^{b} = 0$
153	152	adantl	$⊢ (((A \in D \land E \in ℝ^{+}) \land a \in ℝ) \land b \in D) \to 0^{b} = 0$
154	153	abs00bd	$⊢ (((A \in D \land E \in ℝ^{+}) \land a \in ℝ) \land b \in D) \to \|0^{b}\| = 0$
155		simpllr	$⊢ (((A \in D \land E \in ℝ^{+}) \land a \in ℝ) \land b \in D) \to E \in ℝ^{+}$
156	155	rpgt0d	$⊢ (((A \in D \land E \in ℝ^{+}) \land a \in ℝ) \land b \in D) \to 0 < E$
157	154 156	eqbrtrd	$⊢ (((A \in D \land E \in ℝ^{+}) \land a \in ℝ) \land b \in D) \to \|0^{b}\| < E$
158		fvoveq1	$⊢ 0 = a \to \|0^{b}\| = \|a^{b}\|$
159	158	breq1d	$⊢ 0 = a \to (\|0^{b}\| < E \leftrightarrow \|a^{b}\| < E)$
160	157 159	syl5ibcom	$⊢ (((A \in D \land E \in ℝ^{+}) \land a \in ℝ) \land b \in D) \to (0 = a \to \|a^{b}\| < E)$
161	160	a1dd	$⊢ (((A \in D \land E \in ℝ^{+}) \land a \in ℝ) \land b \in D) \to (0 = a \to ((\|a\| < T \land \|A - b\| < T) \to \|a^{b}\| < E))$
162	161	ralrimdva	$⊢ ((A \in D \land E \in ℝ^{+}) \land a \in ℝ) \to (0 = a \to \forall b \in D ((\|a\| < T \land \|A - b\| < T) \to \|a^{b}\| < E))$
163	141 162	jaod	$⊢ ((A \in D \land E \in ℝ^{+}) \land a \in ℝ) \to ((0 < a \lor 0 = a) \to \forall b \in D ((\|a\| < T \land \|A - b\| < T) \to \|a^{b}\| < E))$
164	29 163	sylbid	$⊢ ((A \in D \land E \in ℝ^{+}) \land a \in ℝ) \to (0 \leq a \to \forall b \in D ((\|a\| < T \land \|A - b\| < T) \to \|a^{b}\| < E))$
165	164	expimpd	$⊢ (A \in D \land E \in ℝ^{+}) \to ((a \in ℝ \land 0 \leq a) \to \forall b \in D ((\|a\| < T \land \|A - b\| < T) \to \|a^{b}\| < E))$
166	26 165	syl5bi	$⊢ (A \in D \land E \in ℝ^{+}) \to (a \in [0, +∞) \to \forall b \in D ((\|a\| < T \land \|A - b\| < T) \to \|a^{b}\| < E))$
167	166	ralrimiv	$⊢ (A \in D \land E \in ℝ^{+}) \to \forall a \in [0, +∞) \forall b \in D ((\|a\| < T \land \|A - b\| < T) \to \|a^{b}\| < E)$
168		breq2	$⊢ d = T \to (\|a\| < d \leftrightarrow \|a\| < T)$
169		breq2	$⊢ d = T \to (\|A - b\| < d \leftrightarrow \|A - b\| < T)$
170	168 169	anbi12d	$⊢ d = T \to ((\|a\| < d \land \|A - b\| < d) \leftrightarrow (\|a\| < T \land \|A - b\| < T))$
171	170	imbi1d	$⊢ d = T \to (((\|a\| < d \land \|A - b\| < d) \to \|a^{b}\| < E) \leftrightarrow ((\|a\| < T \land \|A - b\| < T) \to \|a^{b}\| < E))$
172	171	2ralbidv	$⊢ d = T \to (\forall a \in [0, +∞) \forall b \in D ((\|a\| < d \land \|A - b\| < d) \to \|a^{b}\| < E) \leftrightarrow \forall a \in [0, +∞) \forall b \in D ((\|a\| < T \land \|A - b\| < T) \to \|a^{b}\| < E))$
173	172	rspcev	$⊢ (T \in ℝ^{+} \land \forall a \in [0, +∞) \forall b \in D ((\|a\| < T \land \|A - b\| < T) \to \|a^{b}\| < E)) \to \exists d \in ℝ^{+} \forall a \in [0, +∞) \forall b \in D ((\|a\| < d \land \|A - b\| < d) \to \|a^{b}\| < E)$
174	25 167 173	syl2anc	$⊢ (A \in D \land E \in ℝ^{+}) \to \exists d \in ℝ^{+} \forall a \in [0, +∞) \forall b \in D ((\|a\| < d \land \|A - b\| < d) \to \|a^{b}\| < E)$

Metamath Proof Explorer

Theorem cxpcn3lem

Proof