# Metamath Proof Explorer

## Theorem cxpcn3lem

Description: Lemma for cxpcn3 . (Contributed by Mario Carneiro, 2-May-2016)

Ref Expression
Hypotheses cxpcn3.d ${⊢}{D}={\Re }^{-1}\left[{ℝ}^{+}\right]$
cxpcn3.j ${⊢}{J}=\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)$
cxpcn3.k ${⊢}{K}={J}{↾}_{𝑡}\left[0,\mathrm{+\infty }\right)$
cxpcn3.l ${⊢}{L}={J}{↾}_{𝑡}{D}$
cxpcn3.u ${⊢}{U}=\frac{if\left(\Re \left({A}\right)\le 1,\Re \left({A}\right),1\right)}{2}$
cxpcn3.t ${⊢}{T}=if\left({U}\le {{E}}^{\frac{1}{{U}}},{U},{{E}}^{\frac{1}{{U}}}\right)$
Assertion cxpcn3lem ${⊢}\left({A}\in {D}\wedge {E}\in {ℝ}^{+}\right)\to \exists {d}\in {ℝ}^{+}\phantom{\rule{.4em}{0ex}}\forall {a}\in \left[0,\mathrm{+\infty }\right)\phantom{\rule{.4em}{0ex}}\forall {b}\in {D}\phantom{\rule{.4em}{0ex}}\left(\left(\left|{a}\right|<{d}\wedge \left|{A}-{b}\right|<{d}\right)\to \left|{{a}}^{{b}}\right|<{E}\right)$

### Proof

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