logtayl2

Description: Power series expression for the logarithm. (Contributed by Mario Carneiro, 31-Mar-2015)

		Ref	Expression
	Hypothesis	logtayl2.s	$⊢ S = 1 ball (abs \circ -) 1$
	Assertion	logtayl2	$⊢ A \in S \to seq 1 (+ (k \in ℕ ⟼ (\frac{{(- 1)}^{k - 1}}{k}) {(A - 1)}^{k})) ⇝ \log A$

Proof

Step	Hyp	Ref	Expression
1		logtayl2.s	$⊢ S = 1 ball (abs \circ -) 1$
2		nnuz	$⊢ ℕ = ℤ_{\geq 1}$
3		1zzd	$⊢ A \in S \to 1 \in ℤ$
4		neg1cn	$⊢ - 1 \in ℂ$
5	4	a1i	$⊢ A \in S \to - 1 \in ℂ$
6		ax-1cn	$⊢ 1 \in ℂ$
7	1	eleq2i	$⊢ A \in S \leftrightarrow A \in (1 ball (abs \circ -) 1)$
8		cnxmet	$⊢ abs \circ - \in ∞Met (ℂ)$
9		1xr	$⊢ 1 \in ℝ^{*}$
10		elbl	$⊢ (abs \circ - \in ∞Met (ℂ) \land 1 \in ℂ \land 1 \in ℝ^{*}) \to (A \in (1 ball (abs \circ -) 1) \leftrightarrow (A \in ℂ \land 1 (abs \circ -) A < 1))$
11	8 6 9 10	mp3an	$⊢ A \in (1 ball (abs \circ -) 1) \leftrightarrow (A \in ℂ \land 1 (abs \circ -) A < 1)$
12	7 11	bitri	$⊢ A \in S \leftrightarrow (A \in ℂ \land 1 (abs \circ -) A < 1)$
13	12	simplbi	$⊢ A \in S \to A \in ℂ$
14		subcl	$⊢ (1 \in ℂ \land A \in ℂ) \to 1 - A \in ℂ$
15	6 13 14	sylancr	$⊢ A \in S \to 1 - A \in ℂ$
16		eqid	$⊢ abs \circ - = abs \circ -$
17	16	cnmetdval	$⊢ (1 \in ℂ \land A \in ℂ) \to 1 (abs \circ -) A = \|1 - A\|$
18	6 13 17	sylancr	$⊢ A \in S \to 1 (abs \circ -) A = \|1 - A\|$
19	12	simprbi	$⊢ A \in S \to 1 (abs \circ -) A < 1$
20	18 19	eqbrtrrd	$⊢ A \in S \to \|1 - A\| < 1$
21		logtayl	$⊢ (1 - A \in ℂ \land \|1 - A\| < 1) \to seq 1 (+ (k \in ℕ ⟼ \frac{{(1 - A)}^{k}}{k})) ⇝ (- \log (1 - (1 - A)))$
22	15 20 21	syl2anc	$⊢ A \in S \to seq 1 (+ (k \in ℕ ⟼ \frac{{(1 - A)}^{k}}{k})) ⇝ (- \log (1 - (1 - A)))$
23		nncan	$⊢ (1 \in ℂ \land A \in ℂ) \to 1 - (1 - A) = A$
24	6 13 23	sylancr	$⊢ A \in S \to 1 - (1 - A) = A$
25	24	fveq2d	$⊢ A \in S \to \log (1 - (1 - A)) = \log A$
26	25	negeqd	$⊢ A \in S \to - \log (1 - (1 - A)) = - \log A$
27	22 26	breqtrd	$⊢ A \in S \to seq 1 (+ (k \in ℕ ⟼ \frac{{(1 - A)}^{k}}{k})) ⇝ (- \log A)$
28		oveq2	$⊢ k = n \to {(1 - A)}^{k} = {(1 - A)}^{n}$
29		id	$⊢ k = n \to k = n$
30	28 29	oveq12d	$⊢ k = n \to \frac{{(1 - A)}^{k}}{k} = \frac{{(1 - A)}^{n}}{n}$
31		eqid	$⊢ (k \in ℕ ⟼ \frac{{(1 - A)}^{k}}{k}) = (k \in ℕ ⟼ \frac{{(1 - A)}^{k}}{k})$
32		ovex	$⊢ \frac{{(1 - A)}^{n}}{n} \in V$
33	30 31 32	fvmpt	$⊢ n \in ℕ \to (k \in ℕ ⟼ \frac{{(1 - A)}^{k}}{k}) (n) = \frac{{(1 - A)}^{n}}{n}$
34	33	adantl	$⊢ (A \in S \land n \in ℕ) \to (k \in ℕ ⟼ \frac{{(1 - A)}^{k}}{k}) (n) = \frac{{(1 - A)}^{n}}{n}$
35		nnnn0	$⊢ n \in ℕ \to n \in ℕ_{0}$
36		expcl	$⊢ (1 - A \in ℂ \land n \in ℕ_{0}) \to {(1 - A)}^{n} \in ℂ$
37	15 35 36	syl2an	$⊢ (A \in S \land n \in ℕ) \to {(1 - A)}^{n} \in ℂ$
38		nncn	$⊢ n \in ℕ \to n \in ℂ$
39	38	adantl	$⊢ (A \in S \land n \in ℕ) \to n \in ℂ$
40		nnne0	$⊢ n \in ℕ \to n \neq 0$
41	40	adantl	$⊢ (A \in S \land n \in ℕ) \to n \neq 0$
42	37 39 41	divcld	$⊢ (A \in S \land n \in ℕ) \to \frac{{(1 - A)}^{n}}{n} \in ℂ$
43	34 42	eqeltrd	$⊢ (A \in S \land n \in ℕ) \to (k \in ℕ ⟼ \frac{{(1 - A)}^{k}}{k}) (n) \in ℂ$
44	37 39 41	divnegd	$⊢ (A \in S \land n \in ℕ) \to - \frac{{(1 - A)}^{n}}{n} = \frac{- {(1 - A)}^{n}}{n}$
45	42	mulm1d	$⊢ (A \in S \land n \in ℕ) \to -1 (\frac{{(1 - A)}^{n}}{n}) = - \frac{{(1 - A)}^{n}}{n}$
46	35	adantl	$⊢ (A \in S \land n \in ℕ) \to n \in ℕ_{0}$
47		expcl	$⊢ (- 1 \in ℂ \land n \in ℕ_{0}) \to {(- 1)}^{n} \in ℂ$
48	4 46 47	sylancr	$⊢ (A \in S \land n \in ℕ) \to {(- 1)}^{n} \in ℂ$
49		subcl	$⊢ (A \in ℂ \land 1 \in ℂ) \to A - 1 \in ℂ$
50	13 6 49	sylancl	$⊢ A \in S \to A - 1 \in ℂ$
51		expcl	$⊢ (A - 1 \in ℂ \land n \in ℕ_{0}) \to {(A - 1)}^{n} \in ℂ$
52	50 35 51	syl2an	$⊢ (A \in S \land n \in ℕ) \to {(A - 1)}^{n} \in ℂ$
53	48 52	mulneg1d	$⊢ (A \in S \land n \in ℕ) \to (- {(- 1)}^{n}) {(A - 1)}^{n} = - {(- 1)}^{n} {(A - 1)}^{n}$
54	4	a1i	$⊢ (A \in S \land n \in ℕ) \to - 1 \in ℂ$
55		neg1ne0	$⊢ - 1 \neq 0$
56	55	a1i	$⊢ (A \in S \land n \in ℕ) \to - 1 \neq 0$
57		nnz	$⊢ n \in ℕ \to n \in ℤ$
58	57	adantl	$⊢ (A \in S \land n \in ℕ) \to n \in ℤ$
59	54 56 58	expm1d	$⊢ (A \in S \land n \in ℕ) \to {(- 1)}^{n - 1} = \frac{{(- 1)}^{n}}{- 1}$
60	6	a1i	$⊢ (A \in S \land n \in ℕ) \to 1 \in ℂ$
61		ax-1ne0	$⊢ 1 \neq 0$
62	61	a1i	$⊢ (A \in S \land n \in ℕ) \to 1 \neq 0$
63	48 60 62	divneg2d	$⊢ (A \in S \land n \in ℕ) \to - \frac{{(- 1)}^{n}}{1} = \frac{{(- 1)}^{n}}{- 1}$
64	48	div1d	$⊢ (A \in S \land n \in ℕ) \to \frac{{(- 1)}^{n}}{1} = {(- 1)}^{n}$
65	64	negeqd	$⊢ (A \in S \land n \in ℕ) \to - \frac{{(- 1)}^{n}}{1} = - {(- 1)}^{n}$
66	59 63 65	3eqtr2d	$⊢ (A \in S \land n \in ℕ) \to {(- 1)}^{n - 1} = - {(- 1)}^{n}$
67	66	oveq1d	$⊢ (A \in S \land n \in ℕ) \to {(- 1)}^{n - 1} {(A - 1)}^{n} = (- {(- 1)}^{n}) {(A - 1)}^{n}$
68	50	mulm1d	$⊢ A \in S \to -1 (A - 1) = - (A - 1)$
69		negsubdi2	$⊢ (A \in ℂ \land 1 \in ℂ) \to - (A - 1) = 1 - A$
70	13 6 69	sylancl	$⊢ A \in S \to - (A - 1) = 1 - A$
71	68 70	eqtr2d	$⊢ A \in S \to 1 - A = -1 (A - 1)$
72	71	oveq1d	$⊢ A \in S \to {(1 - A)}^{n} = {-1 (A - 1)}^{n}$
73	72	adantr	$⊢ (A \in S \land n \in ℕ) \to {(1 - A)}^{n} = {-1 (A - 1)}^{n}$
74		mulexp	$⊢ (- 1 \in ℂ \land A - 1 \in ℂ \land n \in ℕ_{0}) \to {-1 (A - 1)}^{n} = {(- 1)}^{n} {(A - 1)}^{n}$
75	4 50 35 74	mp3an3an	$⊢ (A \in S \land n \in ℕ) \to {-1 (A - 1)}^{n} = {(- 1)}^{n} {(A - 1)}^{n}$
76	73 75	eqtrd	$⊢ (A \in S \land n \in ℕ) \to {(1 - A)}^{n} = {(- 1)}^{n} {(A - 1)}^{n}$
77	76	negeqd	$⊢ (A \in S \land n \in ℕ) \to - {(1 - A)}^{n} = - {(- 1)}^{n} {(A - 1)}^{n}$
78	53 67 77	3eqtr4d	$⊢ (A \in S \land n \in ℕ) \to {(- 1)}^{n - 1} {(A - 1)}^{n} = - {(1 - A)}^{n}$
79	78	oveq1d	$⊢ (A \in S \land n \in ℕ) \to \frac{{(- 1)}^{n - 1} {(A - 1)}^{n}}{n} = \frac{- {(1 - A)}^{n}}{n}$
80	44 45 79	3eqtr4d	$⊢ (A \in S \land n \in ℕ) \to -1 (\frac{{(1 - A)}^{n}}{n}) = \frac{{(- 1)}^{n - 1} {(A - 1)}^{n}}{n}$
81		nnm1nn0	$⊢ n \in ℕ \to n - 1 \in ℕ_{0}$
82	81	adantl	$⊢ (A \in S \land n \in ℕ) \to n - 1 \in ℕ_{0}$
83		expcl	$⊢ (- 1 \in ℂ \land n - 1 \in ℕ_{0}) \to {(- 1)}^{n - 1} \in ℂ$
84	4 82 83	sylancr	$⊢ (A \in S \land n \in ℕ) \to {(- 1)}^{n - 1} \in ℂ$
85	84 52 39 41	div23d	$⊢ (A \in S \land n \in ℕ) \to \frac{{(- 1)}^{n - 1} {(A - 1)}^{n}}{n} = (\frac{{(- 1)}^{n - 1}}{n}) {(A - 1)}^{n}$
86	80 85	eqtr2d	$⊢ (A \in S \land n \in ℕ) \to (\frac{{(- 1)}^{n - 1}}{n}) {(A - 1)}^{n} = -1 (\frac{{(1 - A)}^{n}}{n})$
87		oveq1	$⊢ k = n \to k - 1 = n - 1$
88	87	oveq2d	$⊢ k = n \to {(- 1)}^{k - 1} = {(- 1)}^{n - 1}$
89	88 29	oveq12d	$⊢ k = n \to \frac{{(- 1)}^{k - 1}}{k} = \frac{{(- 1)}^{n - 1}}{n}$
90		oveq2	$⊢ k = n \to {(A - 1)}^{k} = {(A - 1)}^{n}$
91	89 90	oveq12d	$⊢ k = n \to (\frac{{(- 1)}^{k - 1}}{k}) {(A - 1)}^{k} = (\frac{{(- 1)}^{n - 1}}{n}) {(A - 1)}^{n}$
92		eqid	$⊢ (k \in ℕ ⟼ (\frac{{(- 1)}^{k - 1}}{k}) {(A - 1)}^{k}) = (k \in ℕ ⟼ (\frac{{(- 1)}^{k - 1}}{k}) {(A - 1)}^{k})$
93		ovex	$⊢ (\frac{{(- 1)}^{n - 1}}{n}) {(A - 1)}^{n} \in V$
94	91 92 93	fvmpt	$⊢ n \in ℕ \to (k \in ℕ ⟼ (\frac{{(- 1)}^{k - 1}}{k}) {(A - 1)}^{k}) (n) = (\frac{{(- 1)}^{n - 1}}{n}) {(A - 1)}^{n}$
95	94	adantl	$⊢ (A \in S \land n \in ℕ) \to (k \in ℕ ⟼ (\frac{{(- 1)}^{k - 1}}{k}) {(A - 1)}^{k}) (n) = (\frac{{(- 1)}^{n - 1}}{n}) {(A - 1)}^{n}$
96	34	oveq2d	$⊢ (A \in S \land n \in ℕ) \to -1 (k \in ℕ ⟼ \frac{{(1 - A)}^{k}}{k}) (n) = -1 (\frac{{(1 - A)}^{n}}{n})$
97	86 95 96	3eqtr4d	$⊢ (A \in S \land n \in ℕ) \to (k \in ℕ ⟼ (\frac{{(- 1)}^{k - 1}}{k}) {(A - 1)}^{k}) (n) = -1 (k \in ℕ ⟼ \frac{{(1 - A)}^{k}}{k}) (n)$
98	2 3 5 27 43 97	isermulc2	$⊢ A \in S \to seq 1 (+ (k \in ℕ ⟼ (\frac{{(- 1)}^{k - 1}}{k}) {(A - 1)}^{k})) ⇝ -1 (- \log A)$
99	1	dvlog2lem	$⊢ S \subseteq ℂ ∖ (−∞, 0]$
100	99	sseli	$⊢ A \in S \to A \in (ℂ ∖ (−∞, 0])$
101		eqid	$⊢ ℂ ∖ (−∞, 0] = ℂ ∖ (−∞, 0]$
102	101	logdmn0	$⊢ A \in (ℂ ∖ (−∞, 0]) \to A \neq 0$
103	100 102	syl	$⊢ A \in S \to A \neq 0$
104	13 103	logcld	$⊢ A \in S \to \log A \in ℂ$
105	104	negcld	$⊢ A \in S \to - \log A \in ℂ$
106	105	mulm1d	$⊢ A \in S \to -1 (- \log A) = - (- \log A)$
107	104	negnegd	$⊢ A \in S \to - (- \log A) = \log A$
108	106 107	eqtrd	$⊢ A \in S \to -1 (- \log A) = \log A$
109	98 108	breqtrd	$⊢ A \in S \to seq 1 (+ (k \in ℕ ⟼ (\frac{{(- 1)}^{k - 1}}{k}) {(A - 1)}^{k})) ⇝ \log A$

Metamath Proof Explorer

Theorem logtayl2

Proof