This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem cxpcn3lem

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

Ref Expression
Hypotheses cxpcn3.d ⊢ 𝐷 = ( ◡ ℜ “ ℝ+ )
cxpcn3.j ⊢ 𝐽 = ( TopOpen ‘ ℂfld )
cxpcn3.k ⊢ 𝐾 = ( 𝐽 ↾t ( 0 [,) +∞ ) )
cxpcn3.l ⊢ 𝐿 = ( 𝐽 ↾t 𝐷 )
cxpcn3.u ⊢ 𝑈 = ( if ( ( ℜ ‘ 𝐴 ) ≤ 1 , ( ℜ ‘ 𝐴 ) , 1 ) / 2 )
cxpcn3.t ⊢ 𝑇 = if ( 𝑈 ≤ ( 𝐸 ↑𝑐 ( 1 / 𝑈 ) ) , 𝑈 , ( 𝐸 ↑𝑐 ( 1 / 𝑈 ) ) )
Assertion cxpcn3lem ( ( 𝐴 ∈ 𝐷 ∧ 𝐸 ∈ ℝ+ ) → ∃ 𝑑 ∈ ℝ+ ∀ 𝑎 ∈ ( 0 [,) +∞ ) ∀ 𝑏 ∈ 𝐷 ( ( ( abs ‘ 𝑎 ) < 𝑑 ∧ ( abs ‘ ( 𝐴 − 𝑏 ) ) < 𝑑 ) → ( abs ‘ ( 𝑎 ↑𝑐 𝑏 ) ) < 𝐸 ) )

Proof

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