Proof of Theorem cxpcn3lem
Step | Hyp | Ref
| Expression |
1 | | cxpcn3.t |
. . 3
⊢ 𝑇 = if(𝑈 ≤ (𝐸↑𝑐(1 / 𝑈)), 𝑈, (𝐸↑𝑐(1 / 𝑈))) |
2 | | cxpcn3.u |
. . . . 5
⊢ 𝑈 = (if((ℜ‘𝐴) ≤ 1, (ℜ‘𝐴), 1) / 2) |
3 | | cxpcn3.d |
. . . . . . . . . . 11
⊢ 𝐷 = (◡ℜ “
ℝ+) |
4 | 3 | eleq2i 2680 |
. . . . . . . . . 10
⊢ (𝐴 ∈ 𝐷 ↔ 𝐴 ∈ (◡ℜ “
ℝ+)) |
5 | | ref 13700 |
. . . . . . . . . . 11
⊢
ℜ:ℂ⟶ℝ |
6 | | ffn 5958 |
. . . . . . . . . . 11
⊢
(ℜ:ℂ⟶ℝ → ℜ Fn
ℂ) |
7 | | elpreima 6245 |
. . . . . . . . . . 11
⊢ (ℜ
Fn ℂ → (𝐴 ∈
(◡ℜ “ ℝ+)
↔ (𝐴 ∈ ℂ
∧ (ℜ‘𝐴)
∈ ℝ+))) |
8 | 5, 6, 7 | mp2b 10 |
. . . . . . . . . 10
⊢ (𝐴 ∈ (◡ℜ “ ℝ+) ↔
(𝐴 ∈ ℂ ∧
(ℜ‘𝐴) ∈
ℝ+)) |
9 | 4, 8 | bitri 263 |
. . . . . . . . 9
⊢ (𝐴 ∈ 𝐷 ↔ (𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ∈
ℝ+)) |
10 | 9 | simprbi 479 |
. . . . . . . 8
⊢ (𝐴 ∈ 𝐷 → (ℜ‘𝐴) ∈
ℝ+) |
11 | 10 | adantr 480 |
. . . . . . 7
⊢ ((𝐴 ∈ 𝐷 ∧ 𝐸 ∈ ℝ+) →
(ℜ‘𝐴) ∈
ℝ+) |
12 | | 1rp 11712 |
. . . . . . 7
⊢ 1 ∈
ℝ+ |
13 | | ifcl 4080 |
. . . . . . 7
⊢
(((ℜ‘𝐴)
∈ ℝ+ ∧ 1 ∈ ℝ+) →
if((ℜ‘𝐴) ≤ 1,
(ℜ‘𝐴), 1) ∈
ℝ+) |
14 | 11, 12, 13 | sylancl 693 |
. . . . . 6
⊢ ((𝐴 ∈ 𝐷 ∧ 𝐸 ∈ ℝ+) →
if((ℜ‘𝐴) ≤ 1,
(ℜ‘𝐴), 1) ∈
ℝ+) |
15 | 14 | rphalfcld 11760 |
. . . . 5
⊢ ((𝐴 ∈ 𝐷 ∧ 𝐸 ∈ ℝ+) →
(if((ℜ‘𝐴) ≤
1, (ℜ‘𝐴), 1) /
2) ∈ ℝ+) |
16 | 2, 15 | syl5eqel 2692 |
. . . 4
⊢ ((𝐴 ∈ 𝐷 ∧ 𝐸 ∈ ℝ+) → 𝑈 ∈
ℝ+) |
17 | | simpr 476 |
. . . . 5
⊢ ((𝐴 ∈ 𝐷 ∧ 𝐸 ∈ ℝ+) → 𝐸 ∈
ℝ+) |
18 | 16 | rpreccld 11758 |
. . . . . 6
⊢ ((𝐴 ∈ 𝐷 ∧ 𝐸 ∈ ℝ+) → (1 /
𝑈) ∈
ℝ+) |
19 | 18 | rpred 11748 |
. . . . 5
⊢ ((𝐴 ∈ 𝐷 ∧ 𝐸 ∈ ℝ+) → (1 /
𝑈) ∈
ℝ) |
20 | 17, 19 | rpcxpcld 24276 |
. . . 4
⊢ ((𝐴 ∈ 𝐷 ∧ 𝐸 ∈ ℝ+) → (𝐸↑𝑐(1 /
𝑈)) ∈
ℝ+) |
21 | 16, 20 | ifcld 4081 |
. . 3
⊢ ((𝐴 ∈ 𝐷 ∧ 𝐸 ∈ ℝ+) → if(𝑈 ≤ (𝐸↑𝑐(1 / 𝑈)), 𝑈, (𝐸↑𝑐(1 / 𝑈))) ∈
ℝ+) |
22 | 1, 21 | syl5eqel 2692 |
. 2
⊢ ((𝐴 ∈ 𝐷 ∧ 𝐸 ∈ ℝ+) → 𝑇 ∈
ℝ+) |
23 | | elrege0 12149 |
. . . 4
⊢ (𝑎 ∈ (0[,)+∞) ↔
(𝑎 ∈ ℝ ∧ 0
≤ 𝑎)) |
24 | | 0red 9920 |
. . . . . . 7
⊢ ((𝐴 ∈ 𝐷 ∧ 𝐸 ∈ ℝ+) → 0 ∈
ℝ) |
25 | | leloe 10003 |
. . . . . . 7
⊢ ((0
∈ ℝ ∧ 𝑎
∈ ℝ) → (0 ≤ 𝑎 ↔ (0 < 𝑎 ∨ 0 = 𝑎))) |
26 | 24, 25 | sylan 487 |
. . . . . 6
⊢ (((𝐴 ∈ 𝐷 ∧ 𝐸 ∈ ℝ+) ∧ 𝑎 ∈ ℝ) → (0 ≤
𝑎 ↔ (0 < 𝑎 ∨ 0 = 𝑎))) |
27 | | elrp 11710 |
. . . . . . . . 9
⊢ (𝑎 ∈ ℝ+
↔ (𝑎 ∈ ℝ
∧ 0 < 𝑎)) |
28 | | simp2l 1080 |
. . . . . . . . . . . . . 14
⊢ (((𝐴 ∈ 𝐷 ∧ 𝐸 ∈ ℝ+) ∧ (𝑎 ∈ ℝ+
∧ 𝑏 ∈ 𝐷) ∧ ((abs‘𝑎) < 𝑇 ∧ (abs‘(𝐴 − 𝑏)) < 𝑇)) → 𝑎 ∈ ℝ+) |
29 | | simp2r 1081 |
. . . . . . . . . . . . . . 15
⊢ (((𝐴 ∈ 𝐷 ∧ 𝐸 ∈ ℝ+) ∧ (𝑎 ∈ ℝ+
∧ 𝑏 ∈ 𝐷) ∧ ((abs‘𝑎) < 𝑇 ∧ (abs‘(𝐴 − 𝑏)) < 𝑇)) → 𝑏 ∈ 𝐷) |
30 | | cnvimass 5404 |
. . . . . . . . . . . . . . . . . 18
⊢ (◡ℜ “ ℝ+) ⊆
dom ℜ |
31 | 5 | fdmi 5965 |
. . . . . . . . . . . . . . . . . 18
⊢ dom
ℜ = ℂ |
32 | 30, 31 | sseqtri 3600 |
. . . . . . . . . . . . . . . . 17
⊢ (◡ℜ “ ℝ+) ⊆
ℂ |
33 | 3, 32 | eqsstri 3598 |
. . . . . . . . . . . . . . . 16
⊢ 𝐷 ⊆
ℂ |
34 | 33 | sseli 3564 |
. . . . . . . . . . . . . . 15
⊢ (𝑏 ∈ 𝐷 → 𝑏 ∈ ℂ) |
35 | 29, 34 | syl 17 |
. . . . . . . . . . . . . 14
⊢ (((𝐴 ∈ 𝐷 ∧ 𝐸 ∈ ℝ+) ∧ (𝑎 ∈ ℝ+
∧ 𝑏 ∈ 𝐷) ∧ ((abs‘𝑎) < 𝑇 ∧ (abs‘(𝐴 − 𝑏)) < 𝑇)) → 𝑏 ∈ ℂ) |
36 | | abscxp 24238 |
. . . . . . . . . . . . . 14
⊢ ((𝑎 ∈ ℝ+
∧ 𝑏 ∈ ℂ)
→ (abs‘(𝑎↑𝑐𝑏)) = (𝑎↑𝑐(ℜ‘𝑏))) |
37 | 28, 35, 36 | syl2anc 691 |
. . . . . . . . . . . . 13
⊢ (((𝐴 ∈ 𝐷 ∧ 𝐸 ∈ ℝ+) ∧ (𝑎 ∈ ℝ+
∧ 𝑏 ∈ 𝐷) ∧ ((abs‘𝑎) < 𝑇 ∧ (abs‘(𝐴 − 𝑏)) < 𝑇)) → (abs‘(𝑎↑𝑐𝑏)) = (𝑎↑𝑐(ℜ‘𝑏))) |
38 | 35 | recld 13782 |
. . . . . . . . . . . . . . . 16
⊢ (((𝐴 ∈ 𝐷 ∧ 𝐸 ∈ ℝ+) ∧ (𝑎 ∈ ℝ+
∧ 𝑏 ∈ 𝐷) ∧ ((abs‘𝑎) < 𝑇 ∧ (abs‘(𝐴 − 𝑏)) < 𝑇)) → (ℜ‘𝑏) ∈ ℝ) |
39 | 28, 38 | rpcxpcld 24276 |
. . . . . . . . . . . . . . 15
⊢ (((𝐴 ∈ 𝐷 ∧ 𝐸 ∈ ℝ+) ∧ (𝑎 ∈ ℝ+
∧ 𝑏 ∈ 𝐷) ∧ ((abs‘𝑎) < 𝑇 ∧ (abs‘(𝐴 − 𝑏)) < 𝑇)) → (𝑎↑𝑐(ℜ‘𝑏)) ∈
ℝ+) |
40 | 39 | rpred 11748 |
. . . . . . . . . . . . . 14
⊢ (((𝐴 ∈ 𝐷 ∧ 𝐸 ∈ ℝ+) ∧ (𝑎 ∈ ℝ+
∧ 𝑏 ∈ 𝐷) ∧ ((abs‘𝑎) < 𝑇 ∧ (abs‘(𝐴 − 𝑏)) < 𝑇)) → (𝑎↑𝑐(ℜ‘𝑏)) ∈
ℝ) |
41 | 16 | 3ad2ant1 1075 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝐴 ∈ 𝐷 ∧ 𝐸 ∈ ℝ+) ∧ (𝑎 ∈ ℝ+
∧ 𝑏 ∈ 𝐷) ∧ ((abs‘𝑎) < 𝑇 ∧ (abs‘(𝐴 − 𝑏)) < 𝑇)) → 𝑈 ∈
ℝ+) |
42 | 41 | rpred 11748 |
. . . . . . . . . . . . . . . 16
⊢ (((𝐴 ∈ 𝐷 ∧ 𝐸 ∈ ℝ+) ∧ (𝑎 ∈ ℝ+
∧ 𝑏 ∈ 𝐷) ∧ ((abs‘𝑎) < 𝑇 ∧ (abs‘(𝐴 − 𝑏)) < 𝑇)) → 𝑈 ∈ ℝ) |
43 | 28, 42 | rpcxpcld 24276 |
. . . . . . . . . . . . . . 15
⊢ (((𝐴 ∈ 𝐷 ∧ 𝐸 ∈ ℝ+) ∧ (𝑎 ∈ ℝ+
∧ 𝑏 ∈ 𝐷) ∧ ((abs‘𝑎) < 𝑇 ∧ (abs‘(𝐴 − 𝑏)) < 𝑇)) → (𝑎↑𝑐𝑈) ∈
ℝ+) |
44 | 43 | rpred 11748 |
. . . . . . . . . . . . . 14
⊢ (((𝐴 ∈ 𝐷 ∧ 𝐸 ∈ ℝ+) ∧ (𝑎 ∈ ℝ+
∧ 𝑏 ∈ 𝐷) ∧ ((abs‘𝑎) < 𝑇 ∧ (abs‘(𝐴 − 𝑏)) < 𝑇)) → (𝑎↑𝑐𝑈) ∈ ℝ) |
45 | | simp1r 1079 |
. . . . . . . . . . . . . . 15
⊢ (((𝐴 ∈ 𝐷 ∧ 𝐸 ∈ ℝ+) ∧ (𝑎 ∈ ℝ+
∧ 𝑏 ∈ 𝐷) ∧ ((abs‘𝑎) < 𝑇 ∧ (abs‘(𝐴 − 𝑏)) < 𝑇)) → 𝐸 ∈
ℝ+) |
46 | 45 | rpred 11748 |
. . . . . . . . . . . . . 14
⊢ (((𝐴 ∈ 𝐷 ∧ 𝐸 ∈ ℝ+) ∧ (𝑎 ∈ ℝ+
∧ 𝑏 ∈ 𝐷) ∧ ((abs‘𝑎) < 𝑇 ∧ (abs‘(𝐴 − 𝑏)) < 𝑇)) → 𝐸 ∈ ℝ) |
47 | | simp1l 1078 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝐴 ∈ 𝐷 ∧ 𝐸 ∈ ℝ+) ∧ (𝑎 ∈ ℝ+
∧ 𝑏 ∈ 𝐷) ∧ ((abs‘𝑎) < 𝑇 ∧ (abs‘(𝐴 − 𝑏)) < 𝑇)) → 𝐴 ∈ 𝐷) |
48 | 9 | simplbi 475 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝐴 ∈ 𝐷 → 𝐴 ∈ ℂ) |
49 | 47, 48 | syl 17 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝐴 ∈ 𝐷 ∧ 𝐸 ∈ ℝ+) ∧ (𝑎 ∈ ℝ+
∧ 𝑏 ∈ 𝐷) ∧ ((abs‘𝑎) < 𝑇 ∧ (abs‘(𝐴 − 𝑏)) < 𝑇)) → 𝐴 ∈ ℂ) |
50 | 49 | recld 13782 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝐴 ∈ 𝐷 ∧ 𝐸 ∈ ℝ+) ∧ (𝑎 ∈ ℝ+
∧ 𝑏 ∈ 𝐷) ∧ ((abs‘𝑎) < 𝑇 ∧ (abs‘(𝐴 − 𝑏)) < 𝑇)) → (ℜ‘𝐴) ∈ ℝ) |
51 | 50 | rehalfcld 11156 |
. . . . . . . . . . . . . . . 16
⊢ (((𝐴 ∈ 𝐷 ∧ 𝐸 ∈ ℝ+) ∧ (𝑎 ∈ ℝ+
∧ 𝑏 ∈ 𝐷) ∧ ((abs‘𝑎) < 𝑇 ∧ (abs‘(𝐴 − 𝑏)) < 𝑇)) → ((ℜ‘𝐴) / 2) ∈ ℝ) |
52 | | 1re 9918 |
. . . . . . . . . . . . . . . . . . 19
⊢ 1 ∈
ℝ |
53 | | min1 11894 |
. . . . . . . . . . . . . . . . . . 19
⊢
(((ℜ‘𝐴)
∈ ℝ ∧ 1 ∈ ℝ) → if((ℜ‘𝐴) ≤ 1, (ℜ‘𝐴), 1) ≤ (ℜ‘𝐴)) |
54 | 50, 52, 53 | sylancl 693 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝐴 ∈ 𝐷 ∧ 𝐸 ∈ ℝ+) ∧ (𝑎 ∈ ℝ+
∧ 𝑏 ∈ 𝐷) ∧ ((abs‘𝑎) < 𝑇 ∧ (abs‘(𝐴 − 𝑏)) < 𝑇)) → if((ℜ‘𝐴) ≤ 1, (ℜ‘𝐴), 1) ≤ (ℜ‘𝐴)) |
55 | 14 | 3ad2ant1 1075 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝐴 ∈ 𝐷 ∧ 𝐸 ∈ ℝ+) ∧ (𝑎 ∈ ℝ+
∧ 𝑏 ∈ 𝐷) ∧ ((abs‘𝑎) < 𝑇 ∧ (abs‘(𝐴 − 𝑏)) < 𝑇)) → if((ℜ‘𝐴) ≤ 1, (ℜ‘𝐴), 1) ∈
ℝ+) |
56 | 55 | rpred 11748 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝐴 ∈ 𝐷 ∧ 𝐸 ∈ ℝ+) ∧ (𝑎 ∈ ℝ+
∧ 𝑏 ∈ 𝐷) ∧ ((abs‘𝑎) < 𝑇 ∧ (abs‘(𝐴 − 𝑏)) < 𝑇)) → if((ℜ‘𝐴) ≤ 1, (ℜ‘𝐴), 1) ∈ ℝ) |
57 | | 2re 10967 |
. . . . . . . . . . . . . . . . . . . 20
⊢ 2 ∈
ℝ |
58 | 57 | a1i 11 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝐴 ∈ 𝐷 ∧ 𝐸 ∈ ℝ+) ∧ (𝑎 ∈ ℝ+
∧ 𝑏 ∈ 𝐷) ∧ ((abs‘𝑎) < 𝑇 ∧ (abs‘(𝐴 − 𝑏)) < 𝑇)) → 2 ∈ ℝ) |
59 | | 2pos 10989 |
. . . . . . . . . . . . . . . . . . . 20
⊢ 0 <
2 |
60 | 59 | a1i 11 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝐴 ∈ 𝐷 ∧ 𝐸 ∈ ℝ+) ∧ (𝑎 ∈ ℝ+
∧ 𝑏 ∈ 𝐷) ∧ ((abs‘𝑎) < 𝑇 ∧ (abs‘(𝐴 − 𝑏)) < 𝑇)) → 0 < 2) |
61 | | lediv1 10767 |
. . . . . . . . . . . . . . . . . . 19
⊢
((if((ℜ‘𝐴) ≤ 1, (ℜ‘𝐴), 1) ∈ ℝ ∧
(ℜ‘𝐴) ∈
ℝ ∧ (2 ∈ ℝ ∧ 0 < 2)) → (if((ℜ‘𝐴) ≤ 1, (ℜ‘𝐴), 1) ≤ (ℜ‘𝐴) ↔ (if((ℜ‘𝐴) ≤ 1, (ℜ‘𝐴), 1) / 2) ≤
((ℜ‘𝐴) /
2))) |
62 | 56, 50, 58, 60, 61 | syl112anc 1322 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝐴 ∈ 𝐷 ∧ 𝐸 ∈ ℝ+) ∧ (𝑎 ∈ ℝ+
∧ 𝑏 ∈ 𝐷) ∧ ((abs‘𝑎) < 𝑇 ∧ (abs‘(𝐴 − 𝑏)) < 𝑇)) → (if((ℜ‘𝐴) ≤ 1, (ℜ‘𝐴), 1) ≤ (ℜ‘𝐴) ↔ (if((ℜ‘𝐴) ≤ 1, (ℜ‘𝐴), 1) / 2) ≤
((ℜ‘𝐴) /
2))) |
63 | 54, 62 | mpbid 221 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝐴 ∈ 𝐷 ∧ 𝐸 ∈ ℝ+) ∧ (𝑎 ∈ ℝ+
∧ 𝑏 ∈ 𝐷) ∧ ((abs‘𝑎) < 𝑇 ∧ (abs‘(𝐴 − 𝑏)) < 𝑇)) → (if((ℜ‘𝐴) ≤ 1, (ℜ‘𝐴), 1) / 2) ≤
((ℜ‘𝐴) /
2)) |
64 | 2, 63 | syl5eqbr 4618 |
. . . . . . . . . . . . . . . 16
⊢ (((𝐴 ∈ 𝐷 ∧ 𝐸 ∈ ℝ+) ∧ (𝑎 ∈ ℝ+
∧ 𝑏 ∈ 𝐷) ∧ ((abs‘𝑎) < 𝑇 ∧ (abs‘(𝐴 − 𝑏)) < 𝑇)) → 𝑈 ≤ ((ℜ‘𝐴) / 2)) |
65 | 50 | recnd 9947 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝐴 ∈ 𝐷 ∧ 𝐸 ∈ ℝ+) ∧ (𝑎 ∈ ℝ+
∧ 𝑏 ∈ 𝐷) ∧ ((abs‘𝑎) < 𝑇 ∧ (abs‘(𝐴 − 𝑏)) < 𝑇)) → (ℜ‘𝐴) ∈ ℂ) |
66 | 65 | 2halvesd 11155 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝐴 ∈ 𝐷 ∧ 𝐸 ∈ ℝ+) ∧ (𝑎 ∈ ℝ+
∧ 𝑏 ∈ 𝐷) ∧ ((abs‘𝑎) < 𝑇 ∧ (abs‘(𝐴 − 𝑏)) < 𝑇)) → (((ℜ‘𝐴) / 2) + ((ℜ‘𝐴) / 2)) = (ℜ‘𝐴)) |
67 | 49, 35 | resubd 13804 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝐴 ∈ 𝐷 ∧ 𝐸 ∈ ℝ+) ∧ (𝑎 ∈ ℝ+
∧ 𝑏 ∈ 𝐷) ∧ ((abs‘𝑎) < 𝑇 ∧ (abs‘(𝐴 − 𝑏)) < 𝑇)) → (ℜ‘(𝐴 − 𝑏)) = ((ℜ‘𝐴) − (ℜ‘𝑏))) |
68 | 49, 35 | subcld 10271 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝐴 ∈ 𝐷 ∧ 𝐸 ∈ ℝ+) ∧ (𝑎 ∈ ℝ+
∧ 𝑏 ∈ 𝐷) ∧ ((abs‘𝑎) < 𝑇 ∧ (abs‘(𝐴 − 𝑏)) < 𝑇)) → (𝐴 − 𝑏) ∈ ℂ) |
69 | 68 | recld 13782 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝐴 ∈ 𝐷 ∧ 𝐸 ∈ ℝ+) ∧ (𝑎 ∈ ℝ+
∧ 𝑏 ∈ 𝐷) ∧ ((abs‘𝑎) < 𝑇 ∧ (abs‘(𝐴 − 𝑏)) < 𝑇)) → (ℜ‘(𝐴 − 𝑏)) ∈ ℝ) |
70 | 68 | abscld 14023 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝐴 ∈ 𝐷 ∧ 𝐸 ∈ ℝ+) ∧ (𝑎 ∈ ℝ+
∧ 𝑏 ∈ 𝐷) ∧ ((abs‘𝑎) < 𝑇 ∧ (abs‘(𝐴 − 𝑏)) < 𝑇)) → (abs‘(𝐴 − 𝑏)) ∈ ℝ) |
71 | 68 | releabsd 14038 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝐴 ∈ 𝐷 ∧ 𝐸 ∈ ℝ+) ∧ (𝑎 ∈ ℝ+
∧ 𝑏 ∈ 𝐷) ∧ ((abs‘𝑎) < 𝑇 ∧ (abs‘(𝐴 − 𝑏)) < 𝑇)) → (ℜ‘(𝐴 − 𝑏)) ≤ (abs‘(𝐴 − 𝑏))) |
72 | | simp3r 1083 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (((𝐴 ∈ 𝐷 ∧ 𝐸 ∈ ℝ+) ∧ (𝑎 ∈ ℝ+
∧ 𝑏 ∈ 𝐷) ∧ ((abs‘𝑎) < 𝑇 ∧ (abs‘(𝐴 − 𝑏)) < 𝑇)) → (abs‘(𝐴 − 𝑏)) < 𝑇) |
73 | 72, 1 | syl6breq 4624 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (((𝐴 ∈ 𝐷 ∧ 𝐸 ∈ ℝ+) ∧ (𝑎 ∈ ℝ+
∧ 𝑏 ∈ 𝐷) ∧ ((abs‘𝑎) < 𝑇 ∧ (abs‘(𝐴 − 𝑏)) < 𝑇)) → (abs‘(𝐴 − 𝑏)) < if(𝑈 ≤ (𝐸↑𝑐(1 / 𝑈)), 𝑈, (𝐸↑𝑐(1 / 𝑈)))) |
74 | 20 | 3ad2ant1 1075 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (((𝐴 ∈ 𝐷 ∧ 𝐸 ∈ ℝ+) ∧ (𝑎 ∈ ℝ+
∧ 𝑏 ∈ 𝐷) ∧ ((abs‘𝑎) < 𝑇 ∧ (abs‘(𝐴 − 𝑏)) < 𝑇)) → (𝐸↑𝑐(1 / 𝑈)) ∈
ℝ+) |
75 | 74 | rpred 11748 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (((𝐴 ∈ 𝐷 ∧ 𝐸 ∈ ℝ+) ∧ (𝑎 ∈ ℝ+
∧ 𝑏 ∈ 𝐷) ∧ ((abs‘𝑎) < 𝑇 ∧ (abs‘(𝐴 − 𝑏)) < 𝑇)) → (𝐸↑𝑐(1 / 𝑈)) ∈
ℝ) |
76 | | ltmin 11899 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢
(((abs‘(𝐴
− 𝑏)) ∈ ℝ
∧ 𝑈 ∈ ℝ
∧ (𝐸↑𝑐(1 / 𝑈)) ∈ ℝ) →
((abs‘(𝐴 −
𝑏)) < if(𝑈 ≤ (𝐸↑𝑐(1 / 𝑈)), 𝑈, (𝐸↑𝑐(1 / 𝑈))) ↔ ((abs‘(𝐴 − 𝑏)) < 𝑈 ∧ (abs‘(𝐴 − 𝑏)) < (𝐸↑𝑐(1 / 𝑈))))) |
77 | 70, 42, 75, 76 | syl3anc 1318 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (((𝐴 ∈ 𝐷 ∧ 𝐸 ∈ ℝ+) ∧ (𝑎 ∈ ℝ+
∧ 𝑏 ∈ 𝐷) ∧ ((abs‘𝑎) < 𝑇 ∧ (abs‘(𝐴 − 𝑏)) < 𝑇)) → ((abs‘(𝐴 − 𝑏)) < if(𝑈 ≤ (𝐸↑𝑐(1 / 𝑈)), 𝑈, (𝐸↑𝑐(1 / 𝑈))) ↔ ((abs‘(𝐴 − 𝑏)) < 𝑈 ∧ (abs‘(𝐴 − 𝑏)) < (𝐸↑𝑐(1 / 𝑈))))) |
78 | 73, 77 | mpbid 221 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝐴 ∈ 𝐷 ∧ 𝐸 ∈ ℝ+) ∧ (𝑎 ∈ ℝ+
∧ 𝑏 ∈ 𝐷) ∧ ((abs‘𝑎) < 𝑇 ∧ (abs‘(𝐴 − 𝑏)) < 𝑇)) → ((abs‘(𝐴 − 𝑏)) < 𝑈 ∧ (abs‘(𝐴 − 𝑏)) < (𝐸↑𝑐(1 / 𝑈)))) |
79 | 78 | simpld 474 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝐴 ∈ 𝐷 ∧ 𝐸 ∈ ℝ+) ∧ (𝑎 ∈ ℝ+
∧ 𝑏 ∈ 𝐷) ∧ ((abs‘𝑎) < 𝑇 ∧ (abs‘(𝐴 − 𝑏)) < 𝑇)) → (abs‘(𝐴 − 𝑏)) < 𝑈) |
80 | 69, 70, 42, 71, 79 | lelttrd 10074 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝐴 ∈ 𝐷 ∧ 𝐸 ∈ ℝ+) ∧ (𝑎 ∈ ℝ+
∧ 𝑏 ∈ 𝐷) ∧ ((abs‘𝑎) < 𝑇 ∧ (abs‘(𝐴 − 𝑏)) < 𝑇)) → (ℜ‘(𝐴 − 𝑏)) < 𝑈) |
81 | 69, 42, 51, 80, 64 | ltletrd 10076 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝐴 ∈ 𝐷 ∧ 𝐸 ∈ ℝ+) ∧ (𝑎 ∈ ℝ+
∧ 𝑏 ∈ 𝐷) ∧ ((abs‘𝑎) < 𝑇 ∧ (abs‘(𝐴 − 𝑏)) < 𝑇)) → (ℜ‘(𝐴 − 𝑏)) < ((ℜ‘𝐴) / 2)) |
82 | 67, 81 | eqbrtrrd 4607 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝐴 ∈ 𝐷 ∧ 𝐸 ∈ ℝ+) ∧ (𝑎 ∈ ℝ+
∧ 𝑏 ∈ 𝐷) ∧ ((abs‘𝑎) < 𝑇 ∧ (abs‘(𝐴 − 𝑏)) < 𝑇)) → ((ℜ‘𝐴) − (ℜ‘𝑏)) < ((ℜ‘𝐴) / 2)) |
83 | 50, 38, 51 | ltsubadd2d 10504 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝐴 ∈ 𝐷 ∧ 𝐸 ∈ ℝ+) ∧ (𝑎 ∈ ℝ+
∧ 𝑏 ∈ 𝐷) ∧ ((abs‘𝑎) < 𝑇 ∧ (abs‘(𝐴 − 𝑏)) < 𝑇)) → (((ℜ‘𝐴) − (ℜ‘𝑏)) < ((ℜ‘𝐴) / 2) ↔ (ℜ‘𝐴) < ((ℜ‘𝑏) + ((ℜ‘𝐴) / 2)))) |
84 | 82, 83 | mpbid 221 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝐴 ∈ 𝐷 ∧ 𝐸 ∈ ℝ+) ∧ (𝑎 ∈ ℝ+
∧ 𝑏 ∈ 𝐷) ∧ ((abs‘𝑎) < 𝑇 ∧ (abs‘(𝐴 − 𝑏)) < 𝑇)) → (ℜ‘𝐴) < ((ℜ‘𝑏) + ((ℜ‘𝐴) / 2))) |
85 | 66, 84 | eqbrtrd 4605 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝐴 ∈ 𝐷 ∧ 𝐸 ∈ ℝ+) ∧ (𝑎 ∈ ℝ+
∧ 𝑏 ∈ 𝐷) ∧ ((abs‘𝑎) < 𝑇 ∧ (abs‘(𝐴 − 𝑏)) < 𝑇)) → (((ℜ‘𝐴) / 2) + ((ℜ‘𝐴) / 2)) < ((ℜ‘𝑏) + ((ℜ‘𝐴) / 2))) |
86 | 51, 38, 51 | ltadd1d 10499 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝐴 ∈ 𝐷 ∧ 𝐸 ∈ ℝ+) ∧ (𝑎 ∈ ℝ+
∧ 𝑏 ∈ 𝐷) ∧ ((abs‘𝑎) < 𝑇 ∧ (abs‘(𝐴 − 𝑏)) < 𝑇)) → (((ℜ‘𝐴) / 2) < (ℜ‘𝑏) ↔ (((ℜ‘𝐴) / 2) + ((ℜ‘𝐴) / 2)) < ((ℜ‘𝑏) + ((ℜ‘𝐴) / 2)))) |
87 | 85, 86 | mpbird 246 |
. . . . . . . . . . . . . . . 16
⊢ (((𝐴 ∈ 𝐷 ∧ 𝐸 ∈ ℝ+) ∧ (𝑎 ∈ ℝ+
∧ 𝑏 ∈ 𝐷) ∧ ((abs‘𝑎) < 𝑇 ∧ (abs‘(𝐴 − 𝑏)) < 𝑇)) → ((ℜ‘𝐴) / 2) < (ℜ‘𝑏)) |
88 | 42, 51, 38, 64, 87 | lelttrd 10074 |
. . . . . . . . . . . . . . 15
⊢ (((𝐴 ∈ 𝐷 ∧ 𝐸 ∈ ℝ+) ∧ (𝑎 ∈ ℝ+
∧ 𝑏 ∈ 𝐷) ∧ ((abs‘𝑎) < 𝑇 ∧ (abs‘(𝐴 − 𝑏)) < 𝑇)) → 𝑈 < (ℜ‘𝑏)) |
89 | 28 | rpred 11748 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝐴 ∈ 𝐷 ∧ 𝐸 ∈ ℝ+) ∧ (𝑎 ∈ ℝ+
∧ 𝑏 ∈ 𝐷) ∧ ((abs‘𝑎) < 𝑇 ∧ (abs‘(𝐴 − 𝑏)) < 𝑇)) → 𝑎 ∈ ℝ) |
90 | 52 | a1i 11 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝐴 ∈ 𝐷 ∧ 𝐸 ∈ ℝ+) ∧ (𝑎 ∈ ℝ+
∧ 𝑏 ∈ 𝐷) ∧ ((abs‘𝑎) < 𝑇 ∧ (abs‘(𝐴 − 𝑏)) < 𝑇)) → 1 ∈ ℝ) |
91 | 28 | rprege0d 11755 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝐴 ∈ 𝐷 ∧ 𝐸 ∈ ℝ+) ∧ (𝑎 ∈ ℝ+
∧ 𝑏 ∈ 𝐷) ∧ ((abs‘𝑎) < 𝑇 ∧ (abs‘(𝐴 − 𝑏)) < 𝑇)) → (𝑎 ∈ ℝ ∧ 0 ≤ 𝑎)) |
92 | | absid 13884 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝑎 ∈ ℝ ∧ 0 ≤
𝑎) → (abs‘𝑎) = 𝑎) |
93 | 91, 92 | syl 17 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝐴 ∈ 𝐷 ∧ 𝐸 ∈ ℝ+) ∧ (𝑎 ∈ ℝ+
∧ 𝑏 ∈ 𝐷) ∧ ((abs‘𝑎) < 𝑇 ∧ (abs‘(𝐴 − 𝑏)) < 𝑇)) → (abs‘𝑎) = 𝑎) |
94 | | simp3l 1082 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝐴 ∈ 𝐷 ∧ 𝐸 ∈ ℝ+) ∧ (𝑎 ∈ ℝ+
∧ 𝑏 ∈ 𝐷) ∧ ((abs‘𝑎) < 𝑇 ∧ (abs‘(𝐴 − 𝑏)) < 𝑇)) → (abs‘𝑎) < 𝑇) |
95 | 93, 94 | eqbrtrrd 4607 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝐴 ∈ 𝐷 ∧ 𝐸 ∈ ℝ+) ∧ (𝑎 ∈ ℝ+
∧ 𝑏 ∈ 𝐷) ∧ ((abs‘𝑎) < 𝑇 ∧ (abs‘(𝐴 − 𝑏)) < 𝑇)) → 𝑎 < 𝑇) |
96 | 95, 1 | syl6breq 4624 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝐴 ∈ 𝐷 ∧ 𝐸 ∈ ℝ+) ∧ (𝑎 ∈ ℝ+
∧ 𝑏 ∈ 𝐷) ∧ ((abs‘𝑎) < 𝑇 ∧ (abs‘(𝐴 − 𝑏)) < 𝑇)) → 𝑎 < if(𝑈 ≤ (𝐸↑𝑐(1 / 𝑈)), 𝑈, (𝐸↑𝑐(1 / 𝑈)))) |
97 | | ltmin 11899 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑎 ∈ ℝ ∧ 𝑈 ∈ ℝ ∧ (𝐸↑𝑐(1 /
𝑈)) ∈ ℝ) →
(𝑎 < if(𝑈 ≤ (𝐸↑𝑐(1 / 𝑈)), 𝑈, (𝐸↑𝑐(1 / 𝑈))) ↔ (𝑎 < 𝑈 ∧ 𝑎 < (𝐸↑𝑐(1 / 𝑈))))) |
98 | 89, 42, 75, 97 | syl3anc 1318 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝐴 ∈ 𝐷 ∧ 𝐸 ∈ ℝ+) ∧ (𝑎 ∈ ℝ+
∧ 𝑏 ∈ 𝐷) ∧ ((abs‘𝑎) < 𝑇 ∧ (abs‘(𝐴 − 𝑏)) < 𝑇)) → (𝑎 < if(𝑈 ≤ (𝐸↑𝑐(1 / 𝑈)), 𝑈, (𝐸↑𝑐(1 / 𝑈))) ↔ (𝑎 < 𝑈 ∧ 𝑎 < (𝐸↑𝑐(1 / 𝑈))))) |
99 | 96, 98 | mpbid 221 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝐴 ∈ 𝐷 ∧ 𝐸 ∈ ℝ+) ∧ (𝑎 ∈ ℝ+
∧ 𝑏 ∈ 𝐷) ∧ ((abs‘𝑎) < 𝑇 ∧ (abs‘(𝐴 − 𝑏)) < 𝑇)) → (𝑎 < 𝑈 ∧ 𝑎 < (𝐸↑𝑐(1 / 𝑈)))) |
100 | 99 | simpld 474 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝐴 ∈ 𝐷 ∧ 𝐸 ∈ ℝ+) ∧ (𝑎 ∈ ℝ+
∧ 𝑏 ∈ 𝐷) ∧ ((abs‘𝑎) < 𝑇 ∧ (abs‘(𝐴 − 𝑏)) < 𝑇)) → 𝑎 < 𝑈) |
101 | | rehalfcl 11135 |
. . . . . . . . . . . . . . . . . . 19
⊢ (1 ∈
ℝ → (1 / 2) ∈ ℝ) |
102 | 52, 101 | mp1i 13 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝐴 ∈ 𝐷 ∧ 𝐸 ∈ ℝ+) ∧ (𝑎 ∈ ℝ+
∧ 𝑏 ∈ 𝐷) ∧ ((abs‘𝑎) < 𝑇 ∧ (abs‘(𝐴 − 𝑏)) < 𝑇)) → (1 / 2) ∈
ℝ) |
103 | | min2 11895 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
(((ℜ‘𝐴)
∈ ℝ ∧ 1 ∈ ℝ) → if((ℜ‘𝐴) ≤ 1, (ℜ‘𝐴), 1) ≤ 1) |
104 | 50, 52, 103 | sylancl 693 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝐴 ∈ 𝐷 ∧ 𝐸 ∈ ℝ+) ∧ (𝑎 ∈ ℝ+
∧ 𝑏 ∈ 𝐷) ∧ ((abs‘𝑎) < 𝑇 ∧ (abs‘(𝐴 − 𝑏)) < 𝑇)) → if((ℜ‘𝐴) ≤ 1, (ℜ‘𝐴), 1) ≤ 1) |
105 | | lediv1 10767 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
((if((ℜ‘𝐴) ≤ 1, (ℜ‘𝐴), 1) ∈ ℝ ∧ 1 ∈ ℝ
∧ (2 ∈ ℝ ∧ 0 < 2)) → (if((ℜ‘𝐴) ≤ 1, (ℜ‘𝐴), 1) ≤ 1 ↔
(if((ℜ‘𝐴) ≤
1, (ℜ‘𝐴), 1) /
2) ≤ (1 / 2))) |
106 | 56, 90, 58, 60, 105 | syl112anc 1322 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝐴 ∈ 𝐷 ∧ 𝐸 ∈ ℝ+) ∧ (𝑎 ∈ ℝ+
∧ 𝑏 ∈ 𝐷) ∧ ((abs‘𝑎) < 𝑇 ∧ (abs‘(𝐴 − 𝑏)) < 𝑇)) → (if((ℜ‘𝐴) ≤ 1, (ℜ‘𝐴), 1) ≤ 1 ↔
(if((ℜ‘𝐴) ≤
1, (ℜ‘𝐴), 1) /
2) ≤ (1 / 2))) |
107 | 104, 106 | mpbid 221 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝐴 ∈ 𝐷 ∧ 𝐸 ∈ ℝ+) ∧ (𝑎 ∈ ℝ+
∧ 𝑏 ∈ 𝐷) ∧ ((abs‘𝑎) < 𝑇 ∧ (abs‘(𝐴 − 𝑏)) < 𝑇)) → (if((ℜ‘𝐴) ≤ 1, (ℜ‘𝐴), 1) / 2) ≤ (1 /
2)) |
108 | 2, 107 | syl5eqbr 4618 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝐴 ∈ 𝐷 ∧ 𝐸 ∈ ℝ+) ∧ (𝑎 ∈ ℝ+
∧ 𝑏 ∈ 𝐷) ∧ ((abs‘𝑎) < 𝑇 ∧ (abs‘(𝐴 − 𝑏)) < 𝑇)) → 𝑈 ≤ (1 / 2)) |
109 | | halflt1 11127 |
. . . . . . . . . . . . . . . . . . 19
⊢ (1 / 2)
< 1 |
110 | 109 | a1i 11 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝐴 ∈ 𝐷 ∧ 𝐸 ∈ ℝ+) ∧ (𝑎 ∈ ℝ+
∧ 𝑏 ∈ 𝐷) ∧ ((abs‘𝑎) < 𝑇 ∧ (abs‘(𝐴 − 𝑏)) < 𝑇)) → (1 / 2) < 1) |
111 | 42, 102, 90, 108, 110 | lelttrd 10074 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝐴 ∈ 𝐷 ∧ 𝐸 ∈ ℝ+) ∧ (𝑎 ∈ ℝ+
∧ 𝑏 ∈ 𝐷) ∧ ((abs‘𝑎) < 𝑇 ∧ (abs‘(𝐴 − 𝑏)) < 𝑇)) → 𝑈 < 1) |
112 | 89, 42, 90, 100, 111 | lttrd 10077 |
. . . . . . . . . . . . . . . 16
⊢ (((𝐴 ∈ 𝐷 ∧ 𝐸 ∈ ℝ+) ∧ (𝑎 ∈ ℝ+
∧ 𝑏 ∈ 𝐷) ∧ ((abs‘𝑎) < 𝑇 ∧ (abs‘(𝐴 − 𝑏)) < 𝑇)) → 𝑎 < 1) |
113 | 28, 42, 112, 38 | cxplt3d 24278 |
. . . . . . . . . . . . . . 15
⊢ (((𝐴 ∈ 𝐷 ∧ 𝐸 ∈ ℝ+) ∧ (𝑎 ∈ ℝ+
∧ 𝑏 ∈ 𝐷) ∧ ((abs‘𝑎) < 𝑇 ∧ (abs‘(𝐴 − 𝑏)) < 𝑇)) → (𝑈 < (ℜ‘𝑏) ↔ (𝑎↑𝑐(ℜ‘𝑏)) < (𝑎↑𝑐𝑈))) |
114 | 88, 113 | mpbid 221 |
. . . . . . . . . . . . . 14
⊢ (((𝐴 ∈ 𝐷 ∧ 𝐸 ∈ ℝ+) ∧ (𝑎 ∈ ℝ+
∧ 𝑏 ∈ 𝐷) ∧ ((abs‘𝑎) < 𝑇 ∧ (abs‘(𝐴 − 𝑏)) < 𝑇)) → (𝑎↑𝑐(ℜ‘𝑏)) < (𝑎↑𝑐𝑈)) |
115 | 41 | rpcnne0d 11757 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝐴 ∈ 𝐷 ∧ 𝐸 ∈ ℝ+) ∧ (𝑎 ∈ ℝ+
∧ 𝑏 ∈ 𝐷) ∧ ((abs‘𝑎) < 𝑇 ∧ (abs‘(𝐴 − 𝑏)) < 𝑇)) → (𝑈 ∈ ℂ ∧ 𝑈 ≠ 0)) |
116 | | recid 10578 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑈 ∈ ℂ ∧ 𝑈 ≠ 0) → (𝑈 · (1 / 𝑈)) = 1) |
117 | 115, 116 | syl 17 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝐴 ∈ 𝐷 ∧ 𝐸 ∈ ℝ+) ∧ (𝑎 ∈ ℝ+
∧ 𝑏 ∈ 𝐷) ∧ ((abs‘𝑎) < 𝑇 ∧ (abs‘(𝐴 − 𝑏)) < 𝑇)) → (𝑈 · (1 / 𝑈)) = 1) |
118 | 117 | oveq2d 6565 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝐴 ∈ 𝐷 ∧ 𝐸 ∈ ℝ+) ∧ (𝑎 ∈ ℝ+
∧ 𝑏 ∈ 𝐷) ∧ ((abs‘𝑎) < 𝑇 ∧ (abs‘(𝐴 − 𝑏)) < 𝑇)) → (𝑎↑𝑐(𝑈 · (1 / 𝑈))) = (𝑎↑𝑐1)) |
119 | 41 | rpreccld 11758 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝐴 ∈ 𝐷 ∧ 𝐸 ∈ ℝ+) ∧ (𝑎 ∈ ℝ+
∧ 𝑏 ∈ 𝐷) ∧ ((abs‘𝑎) < 𝑇 ∧ (abs‘(𝐴 − 𝑏)) < 𝑇)) → (1 / 𝑈) ∈
ℝ+) |
120 | 119 | rpcnd 11750 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝐴 ∈ 𝐷 ∧ 𝐸 ∈ ℝ+) ∧ (𝑎 ∈ ℝ+
∧ 𝑏 ∈ 𝐷) ∧ ((abs‘𝑎) < 𝑇 ∧ (abs‘(𝐴 − 𝑏)) < 𝑇)) → (1 / 𝑈) ∈ ℂ) |
121 | 28, 42, 120 | cxpmuld 24280 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝐴 ∈ 𝐷 ∧ 𝐸 ∈ ℝ+) ∧ (𝑎 ∈ ℝ+
∧ 𝑏 ∈ 𝐷) ∧ ((abs‘𝑎) < 𝑇 ∧ (abs‘(𝐴 − 𝑏)) < 𝑇)) → (𝑎↑𝑐(𝑈 · (1 / 𝑈))) = ((𝑎↑𝑐𝑈)↑𝑐(1 / 𝑈))) |
122 | 28 | rpcnd 11750 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝐴 ∈ 𝐷 ∧ 𝐸 ∈ ℝ+) ∧ (𝑎 ∈ ℝ+
∧ 𝑏 ∈ 𝐷) ∧ ((abs‘𝑎) < 𝑇 ∧ (abs‘(𝐴 − 𝑏)) < 𝑇)) → 𝑎 ∈ ℂ) |
123 | 122 | cxp1d 24252 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝐴 ∈ 𝐷 ∧ 𝐸 ∈ ℝ+) ∧ (𝑎 ∈ ℝ+
∧ 𝑏 ∈ 𝐷) ∧ ((abs‘𝑎) < 𝑇 ∧ (abs‘(𝐴 − 𝑏)) < 𝑇)) → (𝑎↑𝑐1) = 𝑎) |
124 | 118, 121,
123 | 3eqtr3d 2652 |
. . . . . . . . . . . . . . . 16
⊢ (((𝐴 ∈ 𝐷 ∧ 𝐸 ∈ ℝ+) ∧ (𝑎 ∈ ℝ+
∧ 𝑏 ∈ 𝐷) ∧ ((abs‘𝑎) < 𝑇 ∧ (abs‘(𝐴 − 𝑏)) < 𝑇)) → ((𝑎↑𝑐𝑈)↑𝑐(1 / 𝑈)) = 𝑎) |
125 | 99 | simprd 478 |
. . . . . . . . . . . . . . . 16
⊢ (((𝐴 ∈ 𝐷 ∧ 𝐸 ∈ ℝ+) ∧ (𝑎 ∈ ℝ+
∧ 𝑏 ∈ 𝐷) ∧ ((abs‘𝑎) < 𝑇 ∧ (abs‘(𝐴 − 𝑏)) < 𝑇)) → 𝑎 < (𝐸↑𝑐(1 / 𝑈))) |
126 | 124, 125 | eqbrtrd 4605 |
. . . . . . . . . . . . . . 15
⊢ (((𝐴 ∈ 𝐷 ∧ 𝐸 ∈ ℝ+) ∧ (𝑎 ∈ ℝ+
∧ 𝑏 ∈ 𝐷) ∧ ((abs‘𝑎) < 𝑇 ∧ (abs‘(𝐴 − 𝑏)) < 𝑇)) → ((𝑎↑𝑐𝑈)↑𝑐(1 / 𝑈)) < (𝐸↑𝑐(1 / 𝑈))) |
127 | 43 | rprege0d 11755 |
. . . . . . . . . . . . . . . 16
⊢ (((𝐴 ∈ 𝐷 ∧ 𝐸 ∈ ℝ+) ∧ (𝑎 ∈ ℝ+
∧ 𝑏 ∈ 𝐷) ∧ ((abs‘𝑎) < 𝑇 ∧ (abs‘(𝐴 − 𝑏)) < 𝑇)) → ((𝑎↑𝑐𝑈) ∈ ℝ ∧ 0 ≤ (𝑎↑𝑐𝑈))) |
128 | 45 | rprege0d 11755 |
. . . . . . . . . . . . . . . 16
⊢ (((𝐴 ∈ 𝐷 ∧ 𝐸 ∈ ℝ+) ∧ (𝑎 ∈ ℝ+
∧ 𝑏 ∈ 𝐷) ∧ ((abs‘𝑎) < 𝑇 ∧ (abs‘(𝐴 − 𝑏)) < 𝑇)) → (𝐸 ∈ ℝ ∧ 0 ≤ 𝐸)) |
129 | | cxplt2 24244 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝑎↑𝑐𝑈) ∈ ℝ ∧ 0 ≤
(𝑎↑𝑐𝑈)) ∧ (𝐸 ∈ ℝ ∧ 0 ≤ 𝐸) ∧ (1 / 𝑈) ∈ ℝ+) → ((𝑎↑𝑐𝑈) < 𝐸 ↔ ((𝑎↑𝑐𝑈)↑𝑐(1 / 𝑈)) < (𝐸↑𝑐(1 / 𝑈)))) |
130 | 127, 128,
119, 129 | syl3anc 1318 |
. . . . . . . . . . . . . . 15
⊢ (((𝐴 ∈ 𝐷 ∧ 𝐸 ∈ ℝ+) ∧ (𝑎 ∈ ℝ+
∧ 𝑏 ∈ 𝐷) ∧ ((abs‘𝑎) < 𝑇 ∧ (abs‘(𝐴 − 𝑏)) < 𝑇)) → ((𝑎↑𝑐𝑈) < 𝐸 ↔ ((𝑎↑𝑐𝑈)↑𝑐(1 / 𝑈)) < (𝐸↑𝑐(1 / 𝑈)))) |
131 | 126, 130 | mpbird 246 |
. . . . . . . . . . . . . 14
⊢ (((𝐴 ∈ 𝐷 ∧ 𝐸 ∈ ℝ+) ∧ (𝑎 ∈ ℝ+
∧ 𝑏 ∈ 𝐷) ∧ ((abs‘𝑎) < 𝑇 ∧ (abs‘(𝐴 − 𝑏)) < 𝑇)) → (𝑎↑𝑐𝑈) < 𝐸) |
132 | 40, 44, 46, 114, 131 | lttrd 10077 |
. . . . . . . . . . . . 13
⊢ (((𝐴 ∈ 𝐷 ∧ 𝐸 ∈ ℝ+) ∧ (𝑎 ∈ ℝ+
∧ 𝑏 ∈ 𝐷) ∧ ((abs‘𝑎) < 𝑇 ∧ (abs‘(𝐴 − 𝑏)) < 𝑇)) → (𝑎↑𝑐(ℜ‘𝑏)) < 𝐸) |
133 | 37, 132 | eqbrtrd 4605 |
. . . . . . . . . . . 12
⊢ (((𝐴 ∈ 𝐷 ∧ 𝐸 ∈ ℝ+) ∧ (𝑎 ∈ ℝ+
∧ 𝑏 ∈ 𝐷) ∧ ((abs‘𝑎) < 𝑇 ∧ (abs‘(𝐴 − 𝑏)) < 𝑇)) → (abs‘(𝑎↑𝑐𝑏)) < 𝐸) |
134 | 133 | 3expia 1259 |
. . . . . . . . . . 11
⊢ (((𝐴 ∈ 𝐷 ∧ 𝐸 ∈ ℝ+) ∧ (𝑎 ∈ ℝ+
∧ 𝑏 ∈ 𝐷)) → (((abs‘𝑎) < 𝑇 ∧ (abs‘(𝐴 − 𝑏)) < 𝑇) → (abs‘(𝑎↑𝑐𝑏)) < 𝐸)) |
135 | 134 | anassrs 678 |
. . . . . . . . . 10
⊢ ((((𝐴 ∈ 𝐷 ∧ 𝐸 ∈ ℝ+) ∧ 𝑎 ∈ ℝ+)
∧ 𝑏 ∈ 𝐷) → (((abs‘𝑎) < 𝑇 ∧ (abs‘(𝐴 − 𝑏)) < 𝑇) → (abs‘(𝑎↑𝑐𝑏)) < 𝐸)) |
136 | 135 | ralrimiva 2949 |
. . . . . . . . 9
⊢ (((𝐴 ∈ 𝐷 ∧ 𝐸 ∈ ℝ+) ∧ 𝑎 ∈ ℝ+)
→ ∀𝑏 ∈
𝐷 (((abs‘𝑎) < 𝑇 ∧ (abs‘(𝐴 − 𝑏)) < 𝑇) → (abs‘(𝑎↑𝑐𝑏)) < 𝐸)) |
137 | 27, 136 | sylan2br 492 |
. . . . . . . 8
⊢ (((𝐴 ∈ 𝐷 ∧ 𝐸 ∈ ℝ+) ∧ (𝑎 ∈ ℝ ∧ 0 <
𝑎)) → ∀𝑏 ∈ 𝐷 (((abs‘𝑎) < 𝑇 ∧ (abs‘(𝐴 − 𝑏)) < 𝑇) → (abs‘(𝑎↑𝑐𝑏)) < 𝐸)) |
138 | 137 | expr 641 |
. . . . . . 7
⊢ (((𝐴 ∈ 𝐷 ∧ 𝐸 ∈ ℝ+) ∧ 𝑎 ∈ ℝ) → (0 <
𝑎 → ∀𝑏 ∈ 𝐷 (((abs‘𝑎) < 𝑇 ∧ (abs‘(𝐴 − 𝑏)) < 𝑇) → (abs‘(𝑎↑𝑐𝑏)) < 𝐸))) |
139 | | elpreima 6245 |
. . . . . . . . . . . . . . . . . . 19
⊢ (ℜ
Fn ℂ → (𝑏 ∈
(◡ℜ “ ℝ+)
↔ (𝑏 ∈ ℂ
∧ (ℜ‘𝑏)
∈ ℝ+))) |
140 | 5, 6, 139 | mp2b 10 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑏 ∈ (◡ℜ “ ℝ+) ↔
(𝑏 ∈ ℂ ∧
(ℜ‘𝑏) ∈
ℝ+)) |
141 | 140 | simprbi 479 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑏 ∈ (◡ℜ “ ℝ+) →
(ℜ‘𝑏) ∈
ℝ+) |
142 | 141, 3 | eleq2s 2706 |
. . . . . . . . . . . . . . . 16
⊢ (𝑏 ∈ 𝐷 → (ℜ‘𝑏) ∈
ℝ+) |
143 | 142 | rpne0d 11753 |
. . . . . . . . . . . . . . 15
⊢ (𝑏 ∈ 𝐷 → (ℜ‘𝑏) ≠ 0) |
144 | | fveq2 6103 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑏 = 0 → (ℜ‘𝑏) =
(ℜ‘0)) |
145 | | re0 13740 |
. . . . . . . . . . . . . . . . 17
⊢
(ℜ‘0) = 0 |
146 | 144, 145 | syl6eq 2660 |
. . . . . . . . . . . . . . . 16
⊢ (𝑏 = 0 → (ℜ‘𝑏) = 0) |
147 | 146 | necon3i 2814 |
. . . . . . . . . . . . . . 15
⊢
((ℜ‘𝑏)
≠ 0 → 𝑏 ≠
0) |
148 | 143, 147 | syl 17 |
. . . . . . . . . . . . . 14
⊢ (𝑏 ∈ 𝐷 → 𝑏 ≠ 0) |
149 | 34, 148 | 0cxpd 24256 |
. . . . . . . . . . . . 13
⊢ (𝑏 ∈ 𝐷 → (0↑𝑐𝑏) = 0) |
150 | 149 | adantl 481 |
. . . . . . . . . . . 12
⊢ ((((𝐴 ∈ 𝐷 ∧ 𝐸 ∈ ℝ+) ∧ 𝑎 ∈ ℝ) ∧ 𝑏 ∈ 𝐷) → (0↑𝑐𝑏) = 0) |
151 | 150 | abs00bd 13879 |
. . . . . . . . . . 11
⊢ ((((𝐴 ∈ 𝐷 ∧ 𝐸 ∈ ℝ+) ∧ 𝑎 ∈ ℝ) ∧ 𝑏 ∈ 𝐷) →
(abs‘(0↑𝑐𝑏)) = 0) |
152 | | simpllr 795 |
. . . . . . . . . . . 12
⊢ ((((𝐴 ∈ 𝐷 ∧ 𝐸 ∈ ℝ+) ∧ 𝑎 ∈ ℝ) ∧ 𝑏 ∈ 𝐷) → 𝐸 ∈
ℝ+) |
153 | 152 | rpgt0d 11751 |
. . . . . . . . . . 11
⊢ ((((𝐴 ∈ 𝐷 ∧ 𝐸 ∈ ℝ+) ∧ 𝑎 ∈ ℝ) ∧ 𝑏 ∈ 𝐷) → 0 < 𝐸) |
154 | 151, 153 | eqbrtrd 4605 |
. . . . . . . . . 10
⊢ ((((𝐴 ∈ 𝐷 ∧ 𝐸 ∈ ℝ+) ∧ 𝑎 ∈ ℝ) ∧ 𝑏 ∈ 𝐷) →
(abs‘(0↑𝑐𝑏)) < 𝐸) |
155 | | oveq1 6556 |
. . . . . . . . . . . 12
⊢ (0 =
𝑎 →
(0↑𝑐𝑏) = (𝑎↑𝑐𝑏)) |
156 | 155 | fveq2d 6107 |
. . . . . . . . . . 11
⊢ (0 =
𝑎 →
(abs‘(0↑𝑐𝑏)) = (abs‘(𝑎↑𝑐𝑏))) |
157 | 156 | breq1d 4593 |
. . . . . . . . . 10
⊢ (0 =
𝑎 →
((abs‘(0↑𝑐𝑏)) < 𝐸 ↔ (abs‘(𝑎↑𝑐𝑏)) < 𝐸)) |
158 | 154, 157 | syl5ibcom 234 |
. . . . . . . . 9
⊢ ((((𝐴 ∈ 𝐷 ∧ 𝐸 ∈ ℝ+) ∧ 𝑎 ∈ ℝ) ∧ 𝑏 ∈ 𝐷) → (0 = 𝑎 → (abs‘(𝑎↑𝑐𝑏)) < 𝐸)) |
159 | 158 | a1dd 48 |
. . . . . . . 8
⊢ ((((𝐴 ∈ 𝐷 ∧ 𝐸 ∈ ℝ+) ∧ 𝑎 ∈ ℝ) ∧ 𝑏 ∈ 𝐷) → (0 = 𝑎 → (((abs‘𝑎) < 𝑇 ∧ (abs‘(𝐴 − 𝑏)) < 𝑇) → (abs‘(𝑎↑𝑐𝑏)) < 𝐸))) |
160 | 159 | ralrimdva 2952 |
. . . . . . 7
⊢ (((𝐴 ∈ 𝐷 ∧ 𝐸 ∈ ℝ+) ∧ 𝑎 ∈ ℝ) → (0 =
𝑎 → ∀𝑏 ∈ 𝐷 (((abs‘𝑎) < 𝑇 ∧ (abs‘(𝐴 − 𝑏)) < 𝑇) → (abs‘(𝑎↑𝑐𝑏)) < 𝐸))) |
161 | 138, 160 | jaod 394 |
. . . . . 6
⊢ (((𝐴 ∈ 𝐷 ∧ 𝐸 ∈ ℝ+) ∧ 𝑎 ∈ ℝ) → ((0 <
𝑎 ∨ 0 = 𝑎) → ∀𝑏 ∈ 𝐷 (((abs‘𝑎) < 𝑇 ∧ (abs‘(𝐴 − 𝑏)) < 𝑇) → (abs‘(𝑎↑𝑐𝑏)) < 𝐸))) |
162 | 26, 161 | sylbid 229 |
. . . . 5
⊢ (((𝐴 ∈ 𝐷 ∧ 𝐸 ∈ ℝ+) ∧ 𝑎 ∈ ℝ) → (0 ≤
𝑎 → ∀𝑏 ∈ 𝐷 (((abs‘𝑎) < 𝑇 ∧ (abs‘(𝐴 − 𝑏)) < 𝑇) → (abs‘(𝑎↑𝑐𝑏)) < 𝐸))) |
163 | 162 | expimpd 627 |
. . . 4
⊢ ((𝐴 ∈ 𝐷 ∧ 𝐸 ∈ ℝ+) → ((𝑎 ∈ ℝ ∧ 0 ≤
𝑎) → ∀𝑏 ∈ 𝐷 (((abs‘𝑎) < 𝑇 ∧ (abs‘(𝐴 − 𝑏)) < 𝑇) → (abs‘(𝑎↑𝑐𝑏)) < 𝐸))) |
164 | 23, 163 | syl5bi 231 |
. . 3
⊢ ((𝐴 ∈ 𝐷 ∧ 𝐸 ∈ ℝ+) → (𝑎 ∈ (0[,)+∞) →
∀𝑏 ∈ 𝐷 (((abs‘𝑎) < 𝑇 ∧ (abs‘(𝐴 − 𝑏)) < 𝑇) → (abs‘(𝑎↑𝑐𝑏)) < 𝐸))) |
165 | 164 | ralrimiv 2948 |
. 2
⊢ ((𝐴 ∈ 𝐷 ∧ 𝐸 ∈ ℝ+) →
∀𝑎 ∈
(0[,)+∞)∀𝑏
∈ 𝐷 (((abs‘𝑎) < 𝑇 ∧ (abs‘(𝐴 − 𝑏)) < 𝑇) → (abs‘(𝑎↑𝑐𝑏)) < 𝐸)) |
166 | | breq2 4587 |
. . . . . 6
⊢ (𝑑 = 𝑇 → ((abs‘𝑎) < 𝑑 ↔ (abs‘𝑎) < 𝑇)) |
167 | | breq2 4587 |
. . . . . 6
⊢ (𝑑 = 𝑇 → ((abs‘(𝐴 − 𝑏)) < 𝑑 ↔ (abs‘(𝐴 − 𝑏)) < 𝑇)) |
168 | 166, 167 | anbi12d 743 |
. . . . 5
⊢ (𝑑 = 𝑇 → (((abs‘𝑎) < 𝑑 ∧ (abs‘(𝐴 − 𝑏)) < 𝑑) ↔ ((abs‘𝑎) < 𝑇 ∧ (abs‘(𝐴 − 𝑏)) < 𝑇))) |
169 | 168 | imbi1d 330 |
. . . 4
⊢ (𝑑 = 𝑇 → ((((abs‘𝑎) < 𝑑 ∧ (abs‘(𝐴 − 𝑏)) < 𝑑) → (abs‘(𝑎↑𝑐𝑏)) < 𝐸) ↔ (((abs‘𝑎) < 𝑇 ∧ (abs‘(𝐴 − 𝑏)) < 𝑇) → (abs‘(𝑎↑𝑐𝑏)) < 𝐸))) |
170 | 169 | 2ralbidv 2972 |
. . 3
⊢ (𝑑 = 𝑇 → (∀𝑎 ∈ (0[,)+∞)∀𝑏 ∈ 𝐷 (((abs‘𝑎) < 𝑑 ∧ (abs‘(𝐴 − 𝑏)) < 𝑑) → (abs‘(𝑎↑𝑐𝑏)) < 𝐸) ↔ ∀𝑎 ∈ (0[,)+∞)∀𝑏 ∈ 𝐷 (((abs‘𝑎) < 𝑇 ∧ (abs‘(𝐴 − 𝑏)) < 𝑇) → (abs‘(𝑎↑𝑐𝑏)) < 𝐸))) |
171 | 170 | rspcev 3282 |
. 2
⊢ ((𝑇 ∈ ℝ+
∧ ∀𝑎 ∈
(0[,)+∞)∀𝑏
∈ 𝐷 (((abs‘𝑎) < 𝑇 ∧ (abs‘(𝐴 − 𝑏)) < 𝑇) → (abs‘(𝑎↑𝑐𝑏)) < 𝐸)) → ∃𝑑 ∈ ℝ+ ∀𝑎 ∈
(0[,)+∞)∀𝑏
∈ 𝐷 (((abs‘𝑎) < 𝑑 ∧ (abs‘(𝐴 − 𝑏)) < 𝑑) → (abs‘(𝑎↑𝑐𝑏)) < 𝐸)) |
172 | 22, 165, 171 | syl2anc 691 |
1
⊢ ((𝐴 ∈ 𝐷 ∧ 𝐸 ∈ ℝ+) →
∃𝑑 ∈
ℝ+ ∀𝑎 ∈ (0[,)+∞)∀𝑏 ∈ 𝐷 (((abs‘𝑎) < 𝑑 ∧ (abs‘(𝐴 − 𝑏)) < 𝑑) → (abs‘(𝑎↑𝑐𝑏)) < 𝐸)) |