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