atantayl

Description: The Taylor series for arctan ( A ) . (Contributed by Mario Carneiro, 1-Apr-2015)

		Ref	Expression
	Hypothesis	atantayl.1	$⊢ F = (n \in ℕ ⟼ (\frac{i ({(- i)}^{n} - i^{n})}{2}) (\frac{A^{n}}{n}))$
	Assertion	atantayl	$⊢ (A \in ℂ \land \|A\| < 1) \to seq 1 (+ F) ⇝ arctan (A)$

Proof

Step	Hyp	Ref	Expression
1		atantayl.1	$⊢ F = (n \in ℕ ⟼ (\frac{i ({(- i)}^{n} - i^{n})}{2}) (\frac{A^{n}}{n}))$
2		nnuz	$⊢ ℕ = ℤ_{\geq 1}$
3		1zzd	$⊢ (A \in ℂ \land \|A\| < 1) \to 1 \in ℤ$
4		ax-icn	$⊢ i \in ℂ$
5		halfcl	$⊢ i \in ℂ \to \frac{i}{2} \in ℂ$
6	4 5	mp1i	$⊢ (A \in ℂ \land \|A\| < 1) \to \frac{i}{2} \in ℂ$
7		simpl	$⊢ (A \in ℂ \land \|A\| < 1) \to A \in ℂ$
8		mulcl	$⊢ (i \in ℂ \land A \in ℂ) \to i A \in ℂ$
9	4 7 8	sylancr	$⊢ (A \in ℂ \land \|A\| < 1) \to i A \in ℂ$
10	9	negcld	$⊢ (A \in ℂ \land \|A\| < 1) \to - i A \in ℂ$
11	9	absnegd	$⊢ (A \in ℂ \land \|A\| < 1) \to \|- i A\| = \|i A\|$
12		absmul	$⊢ (i \in ℂ \land A \in ℂ) \to \|i A\| = \|i\| \|A\|$
13	4 7 12	sylancr	$⊢ (A \in ℂ \land \|A\| < 1) \to \|i A\| = \|i\| \|A\|$
14		absi	$⊢ \|i\| = 1$
15	14	oveq1i	$⊢ \|i\| \|A\| = 1 \|A\|$
16		abscl	$⊢ A \in ℂ \to \|A\| \in ℝ$
17	16	adantr	$⊢ (A \in ℂ \land \|A\| < 1) \to \|A\| \in ℝ$
18	17	recnd	$⊢ (A \in ℂ \land \|A\| < 1) \to \|A\| \in ℂ$
19	18	mulid2d	$⊢ (A \in ℂ \land \|A\| < 1) \to 1 \|A\| = \|A\|$
20	15 19	syl5eq	$⊢ (A \in ℂ \land \|A\| < 1) \to \|i\| \|A\| = \|A\|$
21	11 13 20	3eqtrd	$⊢ (A \in ℂ \land \|A\| < 1) \to \|- i A\| = \|A\|$
22		simpr	$⊢ (A \in ℂ \land \|A\| < 1) \to \|A\| < 1$
23	21 22	eqbrtrd	$⊢ (A \in ℂ \land \|A\| < 1) \to \|- i A\| < 1$
24		logtayl	$⊢ (- i A \in ℂ \land \|- i A\| < 1) \to seq 1 (+ (n \in ℕ ⟼ \frac{{(- i A)}^{n}}{n})) ⇝ (- \log (1 - (- i A)))$
25	10 23 24	syl2anc	$⊢ (A \in ℂ \land \|A\| < 1) \to seq 1 (+ (n \in ℕ ⟼ \frac{{(- i A)}^{n}}{n})) ⇝ (- \log (1 - (- i A)))$
26		ax-1cn	$⊢ 1 \in ℂ$
27		subneg	$⊢ (1 \in ℂ \land i A \in ℂ) \to 1 - (- i A) = 1 + i A$
28	26 9 27	sylancr	$⊢ (A \in ℂ \land \|A\| < 1) \to 1 - (- i A) = 1 + i A$
29	28	fveq2d	$⊢ (A \in ℂ \land \|A\| < 1) \to \log (1 - (- i A)) = \log (1 + i A)$
30	29	negeqd	$⊢ (A \in ℂ \land \|A\| < 1) \to - \log (1 - (- i A)) = - \log (1 + i A)$
31	25 30	breqtrd	$⊢ (A \in ℂ \land \|A\| < 1) \to seq 1 (+ (n \in ℕ ⟼ \frac{{(- i A)}^{n}}{n})) ⇝ (- \log (1 + i A))$
32		seqex	$⊢ seq 1 (+ (n \in ℕ ⟼ (\frac{{(- i A)}^{n}}{n}) - (\frac{{i A}^{n}}{n}))) \in V$
33	32	a1i	$⊢ (A \in ℂ \land \|A\| < 1) \to seq 1 (+ (n \in ℕ ⟼ (\frac{{(- i A)}^{n}}{n}) - (\frac{{i A}^{n}}{n}))) \in V$
34	11 23	eqbrtrrd	$⊢ (A \in ℂ \land \|A\| < 1) \to \|i A\| < 1$
35		logtayl	$⊢ (i A \in ℂ \land \|i A\| < 1) \to seq 1 (+ (n \in ℕ ⟼ \frac{{i A}^{n}}{n})) ⇝ (- \log (1 - i A))$
36	9 34 35	syl2anc	$⊢ (A \in ℂ \land \|A\| < 1) \to seq 1 (+ (n \in ℕ ⟼ \frac{{i A}^{n}}{n})) ⇝ (- \log (1 - i A))$
37		oveq2	$⊢ n = m \to {(- i A)}^{n} = {(- i A)}^{m}$
38		id	$⊢ n = m \to n = m$
39	37 38	oveq12d	$⊢ n = m \to \frac{{(- i A)}^{n}}{n} = \frac{{(- i A)}^{m}}{m}$
40		eqid	$⊢ (n \in ℕ ⟼ \frac{{(- i A)}^{n}}{n}) = (n \in ℕ ⟼ \frac{{(- i A)}^{n}}{n})$
41		ovex	$⊢ \frac{{(- i A)}^{m}}{m} \in V$
42	39 40 41	fvmpt	$⊢ m \in ℕ \to (n \in ℕ ⟼ \frac{{(- i A)}^{n}}{n}) (m) = \frac{{(- i A)}^{m}}{m}$
43	42	adantl	$⊢ ((A \in ℂ \land \|A\| < 1) \land m \in ℕ) \to (n \in ℕ ⟼ \frac{{(- i A)}^{n}}{n}) (m) = \frac{{(- i A)}^{m}}{m}$
44		nnnn0	$⊢ m \in ℕ \to m \in ℕ_{0}$
45		expcl	$⊢ (- i A \in ℂ \land m \in ℕ_{0}) \to {(- i A)}^{m} \in ℂ$
46	10 44 45	syl2an	$⊢ ((A \in ℂ \land \|A\| < 1) \land m \in ℕ) \to {(- i A)}^{m} \in ℂ$
47		nncn	$⊢ m \in ℕ \to m \in ℂ$
48	47	adantl	$⊢ ((A \in ℂ \land \|A\| < 1) \land m \in ℕ) \to m \in ℂ$
49		nnne0	$⊢ m \in ℕ \to m \neq 0$
50	49	adantl	$⊢ ((A \in ℂ \land \|A\| < 1) \land m \in ℕ) \to m \neq 0$
51	46 48 50	divcld	$⊢ ((A \in ℂ \land \|A\| < 1) \land m \in ℕ) \to \frac{{(- i A)}^{m}}{m} \in ℂ$
52	43 51	eqeltrd	$⊢ ((A \in ℂ \land \|A\| < 1) \land m \in ℕ) \to (n \in ℕ ⟼ \frac{{(- i A)}^{n}}{n}) (m) \in ℂ$
53	2 3 52	serf	$⊢ (A \in ℂ \land \|A\| < 1) \to seq 1 (+ (n \in ℕ ⟼ \frac{{(- i A)}^{n}}{n})) : ℕ ⟶ ℂ$
54	53	ffvelrnda	$⊢ ((A \in ℂ \land \|A\| < 1) \land k \in ℕ) \to seq 1 (+ (n \in ℕ ⟼ \frac{{(- i A)}^{n}}{n})) (k) \in ℂ$
55		oveq2	$⊢ n = m \to {i A}^{n} = {i A}^{m}$
56	55 38	oveq12d	$⊢ n = m \to \frac{{i A}^{n}}{n} = \frac{{i A}^{m}}{m}$
57		eqid	$⊢ (n \in ℕ ⟼ \frac{{i A}^{n}}{n}) = (n \in ℕ ⟼ \frac{{i A}^{n}}{n})$
58		ovex	$⊢ \frac{{i A}^{m}}{m} \in V$
59	56 57 58	fvmpt	$⊢ m \in ℕ \to (n \in ℕ ⟼ \frac{{i A}^{n}}{n}) (m) = \frac{{i A}^{m}}{m}$
60	59	adantl	$⊢ ((A \in ℂ \land \|A\| < 1) \land m \in ℕ) \to (n \in ℕ ⟼ \frac{{i A}^{n}}{n}) (m) = \frac{{i A}^{m}}{m}$
61		expcl	$⊢ (i A \in ℂ \land m \in ℕ_{0}) \to {i A}^{m} \in ℂ$
62	9 44 61	syl2an	$⊢ ((A \in ℂ \land \|A\| < 1) \land m \in ℕ) \to {i A}^{m} \in ℂ$
63	62 48 50	divcld	$⊢ ((A \in ℂ \land \|A\| < 1) \land m \in ℕ) \to \frac{{i A}^{m}}{m} \in ℂ$
64	60 63	eqeltrd	$⊢ ((A \in ℂ \land \|A\| < 1) \land m \in ℕ) \to (n \in ℕ ⟼ \frac{{i A}^{n}}{n}) (m) \in ℂ$
65	2 3 64	serf	$⊢ (A \in ℂ \land \|A\| < 1) \to seq 1 (+ (n \in ℕ ⟼ \frac{{i A}^{n}}{n})) : ℕ ⟶ ℂ$
66	65	ffvelrnda	$⊢ ((A \in ℂ \land \|A\| < 1) \land k \in ℕ) \to seq 1 (+ (n \in ℕ ⟼ \frac{{i A}^{n}}{n})) (k) \in ℂ$
67		simpr	$⊢ ((A \in ℂ \land \|A\| < 1) \land k \in ℕ) \to k \in ℕ$
68	67 2	eleqtrdi	$⊢ ((A \in ℂ \land \|A\| < 1) \land k \in ℕ) \to k \in ℤ_{\geq 1}$
69		simpl	$⊢ ((A \in ℂ \land \|A\| < 1) \land k \in ℕ) \to (A \in ℂ \land \|A\| < 1)$
70		elfznn	$⊢ m \in (1 \dots k) \to m \in ℕ$
71	69 70 52	syl2an	$⊢ (((A \in ℂ \land \|A\| < 1) \land k \in ℕ) \land m \in (1 \dots k)) \to (n \in ℕ ⟼ \frac{{(- i A)}^{n}}{n}) (m) \in ℂ$
72	69 70 64	syl2an	$⊢ (((A \in ℂ \land \|A\| < 1) \land k \in ℕ) \land m \in (1 \dots k)) \to (n \in ℕ ⟼ \frac{{i A}^{n}}{n}) (m) \in ℂ$
73	39 56	oveq12d	$⊢ n = m \to (\frac{{(- i A)}^{n}}{n}) - (\frac{{i A}^{n}}{n}) = (\frac{{(- i A)}^{m}}{m}) - (\frac{{i A}^{m}}{m})$
74		eqid	$⊢ (n \in ℕ ⟼ (\frac{{(- i A)}^{n}}{n}) - (\frac{{i A}^{n}}{n})) = (n \in ℕ ⟼ (\frac{{(- i A)}^{n}}{n}) - (\frac{{i A}^{n}}{n}))$
75		ovex	$⊢ (\frac{{(- i A)}^{m}}{m}) - (\frac{{i A}^{m}}{m}) \in V$
76	73 74 75	fvmpt	$⊢ m \in ℕ \to (n \in ℕ ⟼ (\frac{{(- i A)}^{n}}{n}) - (\frac{{i A}^{n}}{n})) (m) = (\frac{{(- i A)}^{m}}{m}) - (\frac{{i A}^{m}}{m})$
77	76	adantl	$⊢ ((A \in ℂ \land \|A\| < 1) \land m \in ℕ) \to (n \in ℕ ⟼ (\frac{{(- i A)}^{n}}{n}) - (\frac{{i A}^{n}}{n})) (m) = (\frac{{(- i A)}^{m}}{m}) - (\frac{{i A}^{m}}{m})$
78	43 60	oveq12d	$⊢ ((A \in ℂ \land \|A\| < 1) \land m \in ℕ) \to (n \in ℕ ⟼ \frac{{(- i A)}^{n}}{n}) (m) - (n \in ℕ ⟼ \frac{{i A}^{n}}{n}) (m) = (\frac{{(- i A)}^{m}}{m}) - (\frac{{i A}^{m}}{m})$
79	77 78	eqtr4d	$⊢ ((A \in ℂ \land \|A\| < 1) \land m \in ℕ) \to (n \in ℕ ⟼ (\frac{{(- i A)}^{n}}{n}) - (\frac{{i A}^{n}}{n})) (m) = (n \in ℕ ⟼ \frac{{(- i A)}^{n}}{n}) (m) - (n \in ℕ ⟼ \frac{{i A}^{n}}{n}) (m)$
80	69 70 79	syl2an	$⊢ (((A \in ℂ \land \|A\| < 1) \land k \in ℕ) \land m \in (1 \dots k)) \to (n \in ℕ ⟼ (\frac{{(- i A)}^{n}}{n}) - (\frac{{i A}^{n}}{n})) (m) = (n \in ℕ ⟼ \frac{{(- i A)}^{n}}{n}) (m) - (n \in ℕ ⟼ \frac{{i A}^{n}}{n}) (m)$
81	68 71 72 80	sersub	$⊢ ((A \in ℂ \land \|A\| < 1) \land k \in ℕ) \to seq 1 (+ (n \in ℕ ⟼ (\frac{{(- i A)}^{n}}{n}) - (\frac{{i A}^{n}}{n}))) (k) = seq 1 (+ (n \in ℕ ⟼ \frac{{(- i A)}^{n}}{n})) (k) - seq 1 (+ (n \in ℕ ⟼ \frac{{i A}^{n}}{n})) (k)$
82	2 3 31 33 36 54 66 81	climsub	$⊢ (A \in ℂ \land \|A\| < 1) \to seq 1 (+ (n \in ℕ ⟼ (\frac{{(- i A)}^{n}}{n}) - (\frac{{i A}^{n}}{n}))) ⇝ (- \log (1 + i A) - (- \log (1 - i A)))$
83		addcl	$⊢ (1 \in ℂ \land i A \in ℂ) \to 1 + i A \in ℂ$
84	26 9 83	sylancr	$⊢ (A \in ℂ \land \|A\| < 1) \to 1 + i A \in ℂ$
85		bndatandm	$⊢ (A \in ℂ \land \|A\| < 1) \to A \in dom arctan$
86		atandm2	$⊢ A \in dom arctan \leftrightarrow (A \in ℂ \land 1 - i A \neq 0 \land 1 + i A \neq 0)$
87	85 86	sylib	$⊢ (A \in ℂ \land \|A\| < 1) \to (A \in ℂ \land 1 - i A \neq 0 \land 1 + i A \neq 0)$
88	87	simp3d	$⊢ (A \in ℂ \land \|A\| < 1) \to 1 + i A \neq 0$
89	84 88	logcld	$⊢ (A \in ℂ \land \|A\| < 1) \to \log (1 + i A) \in ℂ$
90		subcl	$⊢ (1 \in ℂ \land i A \in ℂ) \to 1 - i A \in ℂ$
91	26 9 90	sylancr	$⊢ (A \in ℂ \land \|A\| < 1) \to 1 - i A \in ℂ$
92	87	simp2d	$⊢ (A \in ℂ \land \|A\| < 1) \to 1 - i A \neq 0$
93	91 92	logcld	$⊢ (A \in ℂ \land \|A\| < 1) \to \log (1 - i A) \in ℂ$
94	89 93	neg2subd	$⊢ (A \in ℂ \land \|A\| < 1) \to - \log (1 + i A) - (- \log (1 - i A)) = \log (1 - i A) - \log (1 + i A)$
95	82 94	breqtrd	$⊢ (A \in ℂ \land \|A\| < 1) \to seq 1 (+ (n \in ℕ ⟼ (\frac{{(- i A)}^{n}}{n}) - (\frac{{i A}^{n}}{n}))) ⇝ (\log (1 - i A) - \log (1 + i A))$
96	51 63	subcld	$⊢ ((A \in ℂ \land \|A\| < 1) \land m \in ℕ) \to (\frac{{(- i A)}^{m}}{m}) - (\frac{{i A}^{m}}{m}) \in ℂ$
97	77 96	eqeltrd	$⊢ ((A \in ℂ \land \|A\| < 1) \land m \in ℕ) \to (n \in ℕ ⟼ (\frac{{(- i A)}^{n}}{n}) - (\frac{{i A}^{n}}{n})) (m) \in ℂ$
98	4	a1i	$⊢ ((A \in ℂ \land \|A\| < 1) \land m \in ℕ) \to i \in ℂ$
99		negicn	$⊢ - i \in ℂ$
100	44	adantl	$⊢ ((A \in ℂ \land \|A\| < 1) \land m \in ℕ) \to m \in ℕ_{0}$
101		expcl	$⊢ (- i \in ℂ \land m \in ℕ_{0}) \to {(- i)}^{m} \in ℂ$
102	99 100 101	sylancr	$⊢ ((A \in ℂ \land \|A\| < 1) \land m \in ℕ) \to {(- i)}^{m} \in ℂ$
103		expcl	$⊢ (i \in ℂ \land m \in ℕ_{0}) \to i^{m} \in ℂ$
104	4 100 103	sylancr	$⊢ ((A \in ℂ \land \|A\| < 1) \land m \in ℕ) \to i^{m} \in ℂ$
105	102 104	subcld	$⊢ ((A \in ℂ \land \|A\| < 1) \land m \in ℕ) \to {(- i)}^{m} - i^{m} \in ℂ$
106		2cnd	$⊢ ((A \in ℂ \land \|A\| < 1) \land m \in ℕ) \to 2 \in ℂ$
107		2ne0	$⊢ 2 \neq 0$
108	107	a1i	$⊢ ((A \in ℂ \land \|A\| < 1) \land m \in ℕ) \to 2 \neq 0$
109	98 105 106 108	div23d	$⊢ ((A \in ℂ \land \|A\| < 1) \land m \in ℕ) \to \frac{i ({(- i)}^{m} - i^{m})}{2} = (\frac{i}{2}) ({(- i)}^{m} - i^{m})$
110	109	oveq1d	$⊢ ((A \in ℂ \land \|A\| < 1) \land m \in ℕ) \to (\frac{i ({(- i)}^{m} - i^{m})}{2}) (\frac{A^{m}}{m}) = (\frac{i}{2}) ({(- i)}^{m} - i^{m}) (\frac{A^{m}}{m})$
111	6	adantr	$⊢ ((A \in ℂ \land \|A\| < 1) \land m \in ℕ) \to \frac{i}{2} \in ℂ$
112		expcl	$⊢ (A \in ℂ \land m \in ℕ_{0}) \to A^{m} \in ℂ$
113	7 44 112	syl2an	$⊢ ((A \in ℂ \land \|A\| < 1) \land m \in ℕ) \to A^{m} \in ℂ$
114	113 48 50	divcld	$⊢ ((A \in ℂ \land \|A\| < 1) \land m \in ℕ) \to \frac{A^{m}}{m} \in ℂ$
115	111 105 114	mulassd	$⊢ ((A \in ℂ \land \|A\| < 1) \land m \in ℕ) \to (\frac{i}{2}) ({(- i)}^{m} - i^{m}) (\frac{A^{m}}{m}) = (\frac{i}{2}) ({(- i)}^{m} - i^{m}) (\frac{A^{m}}{m})$
116	102 104 113	subdird	$⊢ ((A \in ℂ \land \|A\| < 1) \land m \in ℕ) \to ({(- i)}^{m} - i^{m}) A^{m} = {(- i)}^{m} A^{m} - i^{m} A^{m}$
117	7	adantr	$⊢ ((A \in ℂ \land \|A\| < 1) \land m \in ℕ) \to A \in ℂ$
118		mulneg1	$⊢ (i \in ℂ \land A \in ℂ) \to (- i) A = - i A$
119	4 117 118	sylancr	$⊢ ((A \in ℂ \land \|A\| < 1) \land m \in ℕ) \to (- i) A = - i A$
120	119	oveq1d	$⊢ ((A \in ℂ \land \|A\| < 1) \land m \in ℕ) \to {(- i) A}^{m} = {(- i A)}^{m}$
121	99	a1i	$⊢ ((A \in ℂ \land \|A\| < 1) \land m \in ℕ) \to - i \in ℂ$
122	121 117 100	mulexpd	$⊢ ((A \in ℂ \land \|A\| < 1) \land m \in ℕ) \to {(- i) A}^{m} = {(- i)}^{m} A^{m}$
123	120 122	eqtr3d	$⊢ ((A \in ℂ \land \|A\| < 1) \land m \in ℕ) \to {(- i A)}^{m} = {(- i)}^{m} A^{m}$
124	98 117 100	mulexpd	$⊢ ((A \in ℂ \land \|A\| < 1) \land m \in ℕ) \to {i A}^{m} = i^{m} A^{m}$
125	123 124	oveq12d	$⊢ ((A \in ℂ \land \|A\| < 1) \land m \in ℕ) \to {(- i A)}^{m} - {i A}^{m} = {(- i)}^{m} A^{m} - i^{m} A^{m}$
126	116 125	eqtr4d	$⊢ ((A \in ℂ \land \|A\| < 1) \land m \in ℕ) \to ({(- i)}^{m} - i^{m}) A^{m} = {(- i A)}^{m} - {i A}^{m}$
127	126	oveq1d	$⊢ ((A \in ℂ \land \|A\| < 1) \land m \in ℕ) \to \frac{({(- i)}^{m} - i^{m}) A^{m}}{m} = \frac{{(- i A)}^{m} - {i A}^{m}}{m}$
128	105 113 48 50	divassd	$⊢ ((A \in ℂ \land \|A\| < 1) \land m \in ℕ) \to \frac{({(- i)}^{m} - i^{m}) A^{m}}{m} = ({(- i)}^{m} - i^{m}) (\frac{A^{m}}{m})$
129	46 62 48 50	divsubdird	$⊢ ((A \in ℂ \land \|A\| < 1) \land m \in ℕ) \to \frac{{(- i A)}^{m} - {i A}^{m}}{m} = (\frac{{(- i A)}^{m}}{m}) - (\frac{{i A}^{m}}{m})$
130	127 128 129	3eqtr3d	$⊢ ((A \in ℂ \land \|A\| < 1) \land m \in ℕ) \to ({(- i)}^{m} - i^{m}) (\frac{A^{m}}{m}) = (\frac{{(- i A)}^{m}}{m}) - (\frac{{i A}^{m}}{m})$
131	130	oveq2d	$⊢ ((A \in ℂ \land \|A\| < 1) \land m \in ℕ) \to (\frac{i}{2}) ({(- i)}^{m} - i^{m}) (\frac{A^{m}}{m}) = (\frac{i}{2}) ((\frac{{(- i A)}^{m}}{m}) - (\frac{{i A}^{m}}{m}))$
132	110 115 131	3eqtrd	$⊢ ((A \in ℂ \land \|A\| < 1) \land m \in ℕ) \to (\frac{i ({(- i)}^{m} - i^{m})}{2}) (\frac{A^{m}}{m}) = (\frac{i}{2}) ((\frac{{(- i A)}^{m}}{m}) - (\frac{{i A}^{m}}{m}))$
133		oveq2	$⊢ n = m \to {(- i)}^{n} = {(- i)}^{m}$
134		oveq2	$⊢ n = m \to i^{n} = i^{m}$
135	133 134	oveq12d	$⊢ n = m \to {(- i)}^{n} - i^{n} = {(- i)}^{m} - i^{m}$
136	135	oveq2d	$⊢ n = m \to i ({(- i)}^{n} - i^{n}) = i ({(- i)}^{m} - i^{m})$
137	136	oveq1d	$⊢ n = m \to \frac{i ({(- i)}^{n} - i^{n})}{2} = \frac{i ({(- i)}^{m} - i^{m})}{2}$
138		oveq2	$⊢ n = m \to A^{n} = A^{m}$
139	138 38	oveq12d	$⊢ n = m \to \frac{A^{n}}{n} = \frac{A^{m}}{m}$
140	137 139	oveq12d	$⊢ n = m \to (\frac{i ({(- i)}^{n} - i^{n})}{2}) (\frac{A^{n}}{n}) = (\frac{i ({(- i)}^{m} - i^{m})}{2}) (\frac{A^{m}}{m})$
141		ovex	$⊢ (\frac{i ({(- i)}^{m} - i^{m})}{2}) (\frac{A^{m}}{m}) \in V$
142	140 1 141	fvmpt	$⊢ m \in ℕ \to F (m) = (\frac{i ({(- i)}^{m} - i^{m})}{2}) (\frac{A^{m}}{m})$
143	142	adantl	$⊢ ((A \in ℂ \land \|A\| < 1) \land m \in ℕ) \to F (m) = (\frac{i ({(- i)}^{m} - i^{m})}{2}) (\frac{A^{m}}{m})$
144	77	oveq2d	$⊢ ((A \in ℂ \land \|A\| < 1) \land m \in ℕ) \to (\frac{i}{2}) (n \in ℕ ⟼ (\frac{{(- i A)}^{n}}{n}) - (\frac{{i A}^{n}}{n})) (m) = (\frac{i}{2}) ((\frac{{(- i A)}^{m}}{m}) - (\frac{{i A}^{m}}{m}))$
145	132 143 144	3eqtr4d	$⊢ ((A \in ℂ \land \|A\| < 1) \land m \in ℕ) \to F (m) = (\frac{i}{2}) (n \in ℕ ⟼ (\frac{{(- i A)}^{n}}{n}) - (\frac{{i A}^{n}}{n})) (m)$
146	2 3 6 95 97 145	isermulc2	$⊢ (A \in ℂ \land \|A\| < 1) \to seq 1 (+ F) ⇝ (\frac{i}{2}) (\log (1 - i A) - \log (1 + i A))$
147		atanval	$⊢ A \in dom arctan \to arctan (A) = (\frac{i}{2}) (\log (1 - i A) - \log (1 + i A))$
148	85 147	syl	$⊢ (A \in ℂ \land \|A\| < 1) \to arctan (A) = (\frac{i}{2}) (\log (1 - i A) - \log (1 + i A))$
149	146 148	breqtrrd	$⊢ (A \in ℂ \land \|A\| < 1) \to seq 1 (+ F) ⇝ arctan (A)$

Metamath Proof Explorer

Theorem atantayl

Proof