Database
BASIC REAL AND COMPLEX FUNCTIONS
Basic trigonometry
The natural logarithm on complex numbers
logtayl2
Next ⟩
logccv
Metamath Proof Explorer
Ascii
Unicode
Theorem
logtayl2
Description:
Power series expression for the logarithm.
(Contributed by
Mario Carneiro
, 31-Mar-2015)
Ref
Expression
Hypothesis
logtayl2.s
⊢
S
=
1
ball
abs
∘
−
1
Assertion
logtayl2
⊢
A
∈
S
→
seq
1
+
k
∈
ℕ
⟼
−
1
k
−
1
k
A
−
1
k
⇝
log
A
Proof
Step
Hyp
Ref
Expression
1
logtayl2.s
⊢
S
=
1
ball
abs
∘
−
1
2
nnuz
⊢
ℕ
=
ℤ
≥
1
3
1zzd
⊢
A
∈
S
→
1
∈
ℤ
4
neg1cn
⊢
−
1
∈
ℂ
5
4
a1i
⊢
A
∈
S
→
−
1
∈
ℂ
6
ax-1cn
⊢
1
∈
ℂ
7
1
eleq2i
⊢
A
∈
S
↔
A
∈
1
ball
abs
∘
−
1
8
cnxmet
⊢
abs
∘
−
∈
∞Met
ℂ
9
1xr
⊢
1
∈
ℝ
*
10
elbl
⊢
abs
∘
−
∈
∞Met
ℂ
∧
1
∈
ℂ
∧
1
∈
ℝ
*
→
A
∈
1
ball
abs
∘
−
1
↔
A
∈
ℂ
∧
1
abs
∘
−
A
<
1
11
8
6
9
10
mp3an
⊢
A
∈
1
ball
abs
∘
−
1
↔
A
∈
ℂ
∧
1
abs
∘
−
A
<
1
12
7
11
bitri
⊢
A
∈
S
↔
A
∈
ℂ
∧
1
abs
∘
−
A
<
1
13
12
simplbi
⊢
A
∈
S
→
A
∈
ℂ
14
subcl
⊢
1
∈
ℂ
∧
A
∈
ℂ
→
1
−
A
∈
ℂ
15
6
13
14
sylancr
⊢
A
∈
S
→
1
−
A
∈
ℂ
16
eqid
⊢
abs
∘
−
=
abs
∘
−
17
16
cnmetdval
⊢
1
∈
ℂ
∧
A
∈
ℂ
→
1
abs
∘
−
A
=
1
−
A
18
6
13
17
sylancr
⊢
A
∈
S
→
1
abs
∘
−
A
=
1
−
A
19
12
simprbi
⊢
A
∈
S
→
1
abs
∘
−
A
<
1
20
18
19
eqbrtrrd
⊢
A
∈
S
→
1
−
A
<
1
21
logtayl
⊢
1
−
A
∈
ℂ
∧
1
−
A
<
1
→
seq
1
+
k
∈
ℕ
⟼
1
−
A
k
k
⇝
−
log
1
−
1
−
A
22
15
20
21
syl2anc
⊢
A
∈
S
→
seq
1
+
k
∈
ℕ
⟼
1
−
A
k
k
⇝
−
log
1
−
1
−
A
23
nncan
⊢
1
∈
ℂ
∧
A
∈
ℂ
→
1
−
1
−
A
=
A
24
6
13
23
sylancr
⊢
A
∈
S
→
1
−
1
−
A
=
A
25
24
fveq2d
⊢
A
∈
S
→
log
1
−
1
−
A
=
log
A
26
25
negeqd
⊢
A
∈
S
→
−
log
1
−
1
−
A
=
−
log
A
27
22
26
breqtrd
⊢
A
∈
S
→
seq
1
+
k
∈
ℕ
⟼
1
−
A
k
k
⇝
−
log
A
28
oveq2
⊢
k
=
n
→
1
−
A
k
=
1
−
A
n
29
id
⊢
k
=
n
→
k
=
n
30
28
29
oveq12d
⊢
k
=
n
→
1
−
A
k
k
=
1
−
A
n
n
31
eqid
⊢
k
∈
ℕ
⟼
1
−
A
k
k
=
k
∈
ℕ
⟼
1
−
A
k
k
32
ovex
⊢
1
−
A
n
n
∈
V
33
30
31
32
fvmpt
⊢
n
∈
ℕ
→
k
∈
ℕ
⟼
1
−
A
k
k
n
=
1
−
A
n
n
34
33
adantl
⊢
A
∈
S
∧
n
∈
ℕ
→
k
∈
ℕ
⟼
1
−
A
k
k
n
=
1
−
A
n
n
35
nnnn0
⊢
n
∈
ℕ
→
n
∈
ℕ
0
36
expcl
⊢
1
−
A
∈
ℂ
∧
n
∈
ℕ
0
→
1
−
A
n
∈
ℂ
37
15
35
36
syl2an
⊢
A
∈
S
∧
n
∈
ℕ
→
1
−
A
n
∈
ℂ
38
nncn
⊢
n
∈
ℕ
→
n
∈
ℂ
39
38
adantl
⊢
A
∈
S
∧
n
∈
ℕ
→
n
∈
ℂ
40
nnne0
⊢
n
∈
ℕ
→
n
≠
0
41
40
adantl
⊢
A
∈
S
∧
n
∈
ℕ
→
n
≠
0
42
37
39
41
divcld
⊢
A
∈
S
∧
n
∈
ℕ
→
1
−
A
n
n
∈
ℂ
43
34
42
eqeltrd
⊢
A
∈
S
∧
n
∈
ℕ
→
k
∈
ℕ
⟼
1
−
A
k
k
n
∈
ℂ
44
37
39
41
divnegd
⊢
A
∈
S
∧
n
∈
ℕ
→
−
1
−
A
n
n
=
−
1
−
A
n
n
45
42
mulm1d
⊢
A
∈
S
∧
n
∈
ℕ
→
-1
1
−
A
n
n
=
−
1
−
A
n
n
46
35
adantl
⊢
A
∈
S
∧
n
∈
ℕ
→
n
∈
ℕ
0
47
expcl
⊢
−
1
∈
ℂ
∧
n
∈
ℕ
0
→
−
1
n
∈
ℂ
48
4
46
47
sylancr
⊢
A
∈
S
∧
n
∈
ℕ
→
−
1
n
∈
ℂ
49
subcl
⊢
A
∈
ℂ
∧
1
∈
ℂ
→
A
−
1
∈
ℂ
50
13
6
49
sylancl
⊢
A
∈
S
→
A
−
1
∈
ℂ
51
expcl
⊢
A
−
1
∈
ℂ
∧
n
∈
ℕ
0
→
A
−
1
n
∈
ℂ
52
50
35
51
syl2an
⊢
A
∈
S
∧
n
∈
ℕ
→
A
−
1
n
∈
ℂ
53
48
52
mulneg1d
⊢
A
∈
S
∧
n
∈
ℕ
→
−
−
1
n
A
−
1
n
=
−
−
1
n
A
−
1
n
54
4
a1i
⊢
A
∈
S
∧
n
∈
ℕ
→
−
1
∈
ℂ
55
neg1ne0
⊢
−
1
≠
0
56
55
a1i
⊢
A
∈
S
∧
n
∈
ℕ
→
−
1
≠
0
57
nnz
⊢
n
∈
ℕ
→
n
∈
ℤ
58
57
adantl
⊢
A
∈
S
∧
n
∈
ℕ
→
n
∈
ℤ
59
54
56
58
expm1d
⊢
A
∈
S
∧
n
∈
ℕ
→
−
1
n
−
1
=
−
1
n
−
1
60
6
a1i
⊢
A
∈
S
∧
n
∈
ℕ
→
1
∈
ℂ
61
ax-1ne0
⊢
1
≠
0
62
61
a1i
⊢
A
∈
S
∧
n
∈
ℕ
→
1
≠
0
63
48
60
62
divneg2d
⊢
A
∈
S
∧
n
∈
ℕ
→
−
−
1
n
1
=
−
1
n
−
1
64
48
div1d
⊢
A
∈
S
∧
n
∈
ℕ
→
−
1
n
1
=
−
1
n
65
64
negeqd
⊢
A
∈
S
∧
n
∈
ℕ
→
−
−
1
n
1
=
−
−
1
n
66
59
63
65
3eqtr2d
⊢
A
∈
S
∧
n
∈
ℕ
→
−
1
n
−
1
=
−
−
1
n
67
66
oveq1d
⊢
A
∈
S
∧
n
∈
ℕ
→
−
1
n
−
1
A
−
1
n
=
−
−
1
n
A
−
1
n
68
50
mulm1d
⊢
A
∈
S
→
-1
A
−
1
=
−
A
−
1
69
negsubdi2
⊢
A
∈
ℂ
∧
1
∈
ℂ
→
−
A
−
1
=
1
−
A
70
13
6
69
sylancl
⊢
A
∈
S
→
−
A
−
1
=
1
−
A
71
68
70
eqtr2d
⊢
A
∈
S
→
1
−
A
=
-1
A
−
1
72
71
oveq1d
⊢
A
∈
S
→
1
−
A
n
=
-1
A
−
1
n
73
72
adantr
⊢
A
∈
S
∧
n
∈
ℕ
→
1
−
A
n
=
-1
A
−
1
n
74
mulexp
⊢
−
1
∈
ℂ
∧
A
−
1
∈
ℂ
∧
n
∈
ℕ
0
→
-1
A
−
1
n
=
−
1
n
A
−
1
n
75
4
50
35
74
mp3an3an
⊢
A
∈
S
∧
n
∈
ℕ
→
-1
A
−
1
n
=
−
1
n
A
−
1
n
76
73
75
eqtrd
⊢
A
∈
S
∧
n
∈
ℕ
→
1
−
A
n
=
−
1
n
A
−
1
n
77
76
negeqd
⊢
A
∈
S
∧
n
∈
ℕ
→
−
1
−
A
n
=
−
−
1
n
A
−
1
n
78
53
67
77
3eqtr4d
⊢
A
∈
S
∧
n
∈
ℕ
→
−
1
n
−
1
A
−
1
n
=
−
1
−
A
n
79
78
oveq1d
⊢
A
∈
S
∧
n
∈
ℕ
→
−
1
n
−
1
A
−
1
n
n
=
−
1
−
A
n
n
80
44
45
79
3eqtr4d
⊢
A
∈
S
∧
n
∈
ℕ
→
-1
1
−
A
n
n
=
−
1
n
−
1
A
−
1
n
n
81
nnm1nn0
⊢
n
∈
ℕ
→
n
−
1
∈
ℕ
0
82
81
adantl
⊢
A
∈
S
∧
n
∈
ℕ
→
n
−
1
∈
ℕ
0
83
expcl
⊢
−
1
∈
ℂ
∧
n
−
1
∈
ℕ
0
→
−
1
n
−
1
∈
ℂ
84
4
82
83
sylancr
⊢
A
∈
S
∧
n
∈
ℕ
→
−
1
n
−
1
∈
ℂ
85
84
52
39
41
div23d
⊢
A
∈
S
∧
n
∈
ℕ
→
−
1
n
−
1
A
−
1
n
n
=
−
1
n
−
1
n
A
−
1
n
86
80
85
eqtr2d
⊢
A
∈
S
∧
n
∈
ℕ
→
−
1
n
−
1
n
A
−
1
n
=
-1
1
−
A
n
n
87
oveq1
⊢
k
=
n
→
k
−
1
=
n
−
1
88
87
oveq2d
⊢
k
=
n
→
−
1
k
−
1
=
−
1
n
−
1
89
88
29
oveq12d
⊢
k
=
n
→
−
1
k
−
1
k
=
−
1
n
−
1
n
90
oveq2
⊢
k
=
n
→
A
−
1
k
=
A
−
1
n
91
89
90
oveq12d
⊢
k
=
n
→
−
1
k
−
1
k
A
−
1
k
=
−
1
n
−
1
n
A
−
1
n
92
eqid
⊢
k
∈
ℕ
⟼
−
1
k
−
1
k
A
−
1
k
=
k
∈
ℕ
⟼
−
1
k
−
1
k
A
−
1
k
93
ovex
⊢
−
1
n
−
1
n
A
−
1
n
∈
V
94
91
92
93
fvmpt
⊢
n
∈
ℕ
→
k
∈
ℕ
⟼
−
1
k
−
1
k
A
−
1
k
n
=
−
1
n
−
1
n
A
−
1
n
95
94
adantl
⊢
A
∈
S
∧
n
∈
ℕ
→
k
∈
ℕ
⟼
−
1
k
−
1
k
A
−
1
k
n
=
−
1
n
−
1
n
A
−
1
n
96
34
oveq2d
⊢
A
∈
S
∧
n
∈
ℕ
→
-1
k
∈
ℕ
⟼
1
−
A
k
k
n
=
-1
1
−
A
n
n
97
86
95
96
3eqtr4d
⊢
A
∈
S
∧
n
∈
ℕ
→
k
∈
ℕ
⟼
−
1
k
−
1
k
A
−
1
k
n
=
-1
k
∈
ℕ
⟼
1
−
A
k
k
n
98
2
3
5
27
43
97
isermulc2
⊢
A
∈
S
→
seq
1
+
k
∈
ℕ
⟼
−
1
k
−
1
k
A
−
1
k
⇝
-1
−
log
A
99
1
dvlog2lem
⊢
S
⊆
ℂ
∖
−∞
0
100
99
sseli
⊢
A
∈
S
→
A
∈
ℂ
∖
−∞
0
101
eqid
⊢
ℂ
∖
−∞
0
=
ℂ
∖
−∞
0
102
101
logdmn0
⊢
A
∈
ℂ
∖
−∞
0
→
A
≠
0
103
100
102
syl
⊢
A
∈
S
→
A
≠
0
104
13
103
logcld
⊢
A
∈
S
→
log
A
∈
ℂ
105
104
negcld
⊢
A
∈
S
→
−
log
A
∈
ℂ
106
105
mulm1d
⊢
A
∈
S
→
-1
−
log
A
=
−
−
log
A
107
104
negnegd
⊢
A
∈
S
→
−
−
log
A
=
log
A
108
106
107
eqtrd
⊢
A
∈
S
→
-1
−
log
A
=
log
A
109
98
108
breqtrd
⊢
A
∈
S
→
seq
1
+
k
∈
ℕ
⟼
−
1
k
−
1
k
A
−
1
k
⇝
log
A