atantayl2

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

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

Proof

Step	Hyp	Ref	Expression
1		atantayl2.1	$⊢ F = (n \in ℕ ⟼ if (2 ∥ n, 0, {(- 1)}^{\frac{n - 1}{2}} (\frac{A^{n}}{n})))$
2		ax-icn	$⊢ i \in ℂ$
3	2	negcli	$⊢ - i \in ℂ$
4	3	a1i	$⊢ (((A \in ℂ \land \|A\| < 1) \land n \in ℕ) \land 2 ∥ n) \to - i \in ℂ$
5		nnnn0	$⊢ n \in ℕ \to n \in ℕ_{0}$
6	5	ad2antlr	$⊢ (((A \in ℂ \land \|A\| < 1) \land n \in ℕ) \land 2 ∥ n) \to n \in ℕ_{0}$
7	4 6	expcld	$⊢ (((A \in ℂ \land \|A\| < 1) \land n \in ℕ) \land 2 ∥ n) \to {(- i)}^{n} \in ℂ$
8		sqneg	$⊢ i \in ℂ \to {(- i)}^{2} = i^{2}$
9	2 8	ax-mp	$⊢ {(- i)}^{2} = i^{2}$
10	9	oveq1i	$⊢ {({(- i)}^{2})}^{\frac{n}{2}} = {(i^{2})}^{\frac{n}{2}}$
11		ine0	$⊢ i \neq 0$
12	2 11	negne0i	$⊢ - i \neq 0$
13	12	a1i	$⊢ (((A \in ℂ \land \|A\| < 1) \land n \in ℕ) \land 2 ∥ n) \to - i \neq 0$
14		2z	$⊢ 2 \in ℤ$
15	14	a1i	$⊢ (((A \in ℂ \land \|A\| < 1) \land n \in ℕ) \land 2 ∥ n) \to 2 \in ℤ$
16		2ne0	$⊢ 2 \neq 0$
17		nnz	$⊢ n \in ℕ \to n \in ℤ$
18	17	adantl	$⊢ ((A \in ℂ \land \|A\| < 1) \land n \in ℕ) \to n \in ℤ$
19		dvdsval2	$⊢ (2 \in ℤ \land 2 \neq 0 \land n \in ℤ) \to (2 ∥ n \leftrightarrow \frac{n}{2} \in ℤ)$
20	14 16 18 19	mp3an12i	$⊢ ((A \in ℂ \land \|A\| < 1) \land n \in ℕ) \to (2 ∥ n \leftrightarrow \frac{n}{2} \in ℤ)$
21	20	biimpa	$⊢ (((A \in ℂ \land \|A\| < 1) \land n \in ℕ) \land 2 ∥ n) \to \frac{n}{2} \in ℤ$
22		expmulz	$⊢ ((- i \in ℂ \land - i \neq 0) \land (2 \in ℤ \land \frac{n}{2} \in ℤ)) \to {(- i)}^{2 (\frac{n}{2})} = {({(- i)}^{2})}^{\frac{n}{2}}$
23	4 13 15 21 22	syl22anc	$⊢ (((A \in ℂ \land \|A\| < 1) \land n \in ℕ) \land 2 ∥ n) \to {(- i)}^{2 (\frac{n}{2})} = {({(- i)}^{2})}^{\frac{n}{2}}$
24	2	a1i	$⊢ (((A \in ℂ \land \|A\| < 1) \land n \in ℕ) \land 2 ∥ n) \to i \in ℂ$
25	11	a1i	$⊢ (((A \in ℂ \land \|A\| < 1) \land n \in ℕ) \land 2 ∥ n) \to i \neq 0$
26		expmulz	$⊢ ((i \in ℂ \land i \neq 0) \land (2 \in ℤ \land \frac{n}{2} \in ℤ)) \to i^{2 (\frac{n}{2})} = {(i^{2})}^{\frac{n}{2}}$
27	24 25 15 21 26	syl22anc	$⊢ (((A \in ℂ \land \|A\| < 1) \land n \in ℕ) \land 2 ∥ n) \to i^{2 (\frac{n}{2})} = {(i^{2})}^{\frac{n}{2}}$
28	10 23 27	3eqtr4a	$⊢ (((A \in ℂ \land \|A\| < 1) \land n \in ℕ) \land 2 ∥ n) \to {(- i)}^{2 (\frac{n}{2})} = i^{2 (\frac{n}{2})}$
29		nncn	$⊢ n \in ℕ \to n \in ℂ$
30	29	ad2antlr	$⊢ (((A \in ℂ \land \|A\| < 1) \land n \in ℕ) \land 2 ∥ n) \to n \in ℂ$
31		2cnd	$⊢ (((A \in ℂ \land \|A\| < 1) \land n \in ℕ) \land 2 ∥ n) \to 2 \in ℂ$
32	16	a1i	$⊢ (((A \in ℂ \land \|A\| < 1) \land n \in ℕ) \land 2 ∥ n) \to 2 \neq 0$
33	30 31 32	divcan2d	$⊢ (((A \in ℂ \land \|A\| < 1) \land n \in ℕ) \land 2 ∥ n) \to 2 (\frac{n}{2}) = n$
34	33	oveq2d	$⊢ (((A \in ℂ \land \|A\| < 1) \land n \in ℕ) \land 2 ∥ n) \to {(- i)}^{2 (\frac{n}{2})} = {(- i)}^{n}$
35	33	oveq2d	$⊢ (((A \in ℂ \land \|A\| < 1) \land n \in ℕ) \land 2 ∥ n) \to i^{2 (\frac{n}{2})} = i^{n}$
36	28 34 35	3eqtr3d	$⊢ (((A \in ℂ \land \|A\| < 1) \land n \in ℕ) \land 2 ∥ n) \to {(- i)}^{n} = i^{n}$
37	7 36	subeq0bd	$⊢ (((A \in ℂ \land \|A\| < 1) \land n \in ℕ) \land 2 ∥ n) \to {(- i)}^{n} - i^{n} = 0$
38	37	oveq2d	$⊢ (((A \in ℂ \land \|A\| < 1) \land n \in ℕ) \land 2 ∥ n) \to i ({(- i)}^{n} - i^{n}) = i \cdot 0$
39		it0e0	$⊢ i \cdot 0 = 0$
40	38 39	eqtrdi	$⊢ (((A \in ℂ \land \|A\| < 1) \land n \in ℕ) \land 2 ∥ n) \to i ({(- i)}^{n} - i^{n}) = 0$
41	40	oveq1d	$⊢ (((A \in ℂ \land \|A\| < 1) \land n \in ℕ) \land 2 ∥ n) \to \frac{i ({(- i)}^{n} - i^{n})}{2} = \frac{0}{2}$
42		2cn	$⊢ 2 \in ℂ$
43	42 16	div0i	$⊢ \frac{0}{2} = 0$
44	41 43	eqtrdi	$⊢ (((A \in ℂ \land \|A\| < 1) \land n \in ℕ) \land 2 ∥ n) \to \frac{i ({(- i)}^{n} - i^{n})}{2} = 0$
45	44	oveq1d	$⊢ (((A \in ℂ \land \|A\| < 1) \land n \in ℕ) \land 2 ∥ n) \to (\frac{i ({(- i)}^{n} - i^{n})}{2}) (\frac{A^{n}}{n}) = 0 \cdot (\frac{A^{n}}{n})$
46		simplll	$⊢ (((A \in ℂ \land \|A\| < 1) \land n \in ℕ) \land 2 ∥ n) \to A \in ℂ$
47	46 6	expcld	$⊢ (((A \in ℂ \land \|A\| < 1) \land n \in ℕ) \land 2 ∥ n) \to A^{n} \in ℂ$
48		nnne0	$⊢ n \in ℕ \to n \neq 0$
49	48	ad2antlr	$⊢ (((A \in ℂ \land \|A\| < 1) \land n \in ℕ) \land 2 ∥ n) \to n \neq 0$
50	47 30 49	divcld	$⊢ (((A \in ℂ \land \|A\| < 1) \land n \in ℕ) \land 2 ∥ n) \to \frac{A^{n}}{n} \in ℂ$
51	50	mul02d	$⊢ (((A \in ℂ \land \|A\| < 1) \land n \in ℕ) \land 2 ∥ n) \to 0 \cdot (\frac{A^{n}}{n}) = 0$
52	45 51	eqtr2d	$⊢ (((A \in ℂ \land \|A\| < 1) \land n \in ℕ) \land 2 ∥ n) \to 0 = (\frac{i ({(- i)}^{n} - i^{n})}{2}) (\frac{A^{n}}{n})$
53		2cnd	$⊢ (((A \in ℂ \land \|A\| < 1) \land n \in ℕ) \land \neg 2 ∥ n) \to 2 \in ℂ$
54		ax-1cn	$⊢ 1 \in ℂ$
55	54	negcli	$⊢ - 1 \in ℂ$
56	55	a1i	$⊢ (((A \in ℂ \land \|A\| < 1) \land n \in ℕ) \land \neg 2 ∥ n) \to - 1 \in ℂ$
57		neg1ne0	$⊢ - 1 \neq 0$
58	57	a1i	$⊢ (((A \in ℂ \land \|A\| < 1) \land n \in ℕ) \land \neg 2 ∥ n) \to - 1 \neq 0$
59	29	ad2antlr	$⊢ (((A \in ℂ \land \|A\| < 1) \land n \in ℕ) \land \neg 2 ∥ n) \to n \in ℂ$
60		peano2cn	$⊢ n \in ℂ \to n + 1 \in ℂ$
61	59 60	syl	$⊢ (((A \in ℂ \land \|A\| < 1) \land n \in ℕ) \land \neg 2 ∥ n) \to n + 1 \in ℂ$
62	16	a1i	$⊢ (((A \in ℂ \land \|A\| < 1) \land n \in ℕ) \land \neg 2 ∥ n) \to 2 \neq 0$
63	61 53 53 62	divsubdird	$⊢ (((A \in ℂ \land \|A\| < 1) \land n \in ℕ) \land \neg 2 ∥ n) \to \frac{n + 1 - 2}{2} = (\frac{n + 1}{2}) - (\frac{2}{2})$
64		2div2e1	$⊢ \frac{2}{2} = 1$
65	64	oveq2i	$⊢ (\frac{n + 1}{2}) - (\frac{2}{2}) = (\frac{n + 1}{2}) - 1$
66	63 65	eqtrdi	$⊢ (((A \in ℂ \land \|A\| < 1) \land n \in ℕ) \land \neg 2 ∥ n) \to \frac{n + 1 - 2}{2} = (\frac{n + 1}{2}) - 1$
67		df-2	$⊢ 2 = 1 + 1$
68	67	oveq2i	$⊢ n + 1 - 2 = n + 1 - (1 + 1)$
69	54	a1i	$⊢ (((A \in ℂ \land \|A\| < 1) \land n \in ℕ) \land \neg 2 ∥ n) \to 1 \in ℂ$
70	59 69 69	pnpcan2d	$⊢ (((A \in ℂ \land \|A\| < 1) \land n \in ℕ) \land \neg 2 ∥ n) \to n + 1 - (1 + 1) = n - 1$
71	68 70	syl5eq	$⊢ (((A \in ℂ \land \|A\| < 1) \land n \in ℕ) \land \neg 2 ∥ n) \to n + 1 - 2 = n - 1$
72	71	oveq1d	$⊢ (((A \in ℂ \land \|A\| < 1) \land n \in ℕ) \land \neg 2 ∥ n) \to \frac{n + 1 - 2}{2} = \frac{n - 1}{2}$
73	66 72	eqtr3d	$⊢ (((A \in ℂ \land \|A\| < 1) \land n \in ℕ) \land \neg 2 ∥ n) \to (\frac{n + 1}{2}) - 1 = \frac{n - 1}{2}$
74	20	notbid	$⊢ ((A \in ℂ \land \|A\| < 1) \land n \in ℕ) \to (\neg 2 ∥ n \leftrightarrow \neg \frac{n}{2} \in ℤ)$
75		zeo	$⊢ n \in ℤ \to (\frac{n}{2} \in ℤ \lor \frac{n + 1}{2} \in ℤ)$
76	18 75	syl	$⊢ ((A \in ℂ \land \|A\| < 1) \land n \in ℕ) \to (\frac{n}{2} \in ℤ \lor \frac{n + 1}{2} \in ℤ)$
77	76	ord	$⊢ ((A \in ℂ \land \|A\| < 1) \land n \in ℕ) \to (\neg \frac{n}{2} \in ℤ \to \frac{n + 1}{2} \in ℤ)$
78	74 77	sylbid	$⊢ ((A \in ℂ \land \|A\| < 1) \land n \in ℕ) \to (\neg 2 ∥ n \to \frac{n + 1}{2} \in ℤ)$
79	78	imp	$⊢ (((A \in ℂ \land \|A\| < 1) \land n \in ℕ) \land \neg 2 ∥ n) \to \frac{n + 1}{2} \in ℤ$
80		peano2zm	$⊢ \frac{n + 1}{2} \in ℤ \to (\frac{n + 1}{2}) - 1 \in ℤ$
81	79 80	syl	$⊢ (((A \in ℂ \land \|A\| < 1) \land n \in ℕ) \land \neg 2 ∥ n) \to (\frac{n + 1}{2}) - 1 \in ℤ$
82	73 81	eqeltrrd	$⊢ (((A \in ℂ \land \|A\| < 1) \land n \in ℕ) \land \neg 2 ∥ n) \to \frac{n - 1}{2} \in ℤ$
83	56 58 82	expclzd	$⊢ (((A \in ℂ \land \|A\| < 1) \land n \in ℕ) \land \neg 2 ∥ n) \to {(- 1)}^{\frac{n - 1}{2}} \in ℂ$
84	83	2timesd	$⊢ (((A \in ℂ \land \|A\| < 1) \land n \in ℕ) \land \neg 2 ∥ n) \to 2 {(- 1)}^{\frac{n - 1}{2}} = {(- 1)}^{\frac{n - 1}{2}} + {(- 1)}^{\frac{n - 1}{2}}$
85		subcl	$⊢ (n \in ℂ \land 1 \in ℂ) \to n - 1 \in ℂ$
86	59 54 85	sylancl	$⊢ (((A \in ℂ \land \|A\| < 1) \land n \in ℕ) \land \neg 2 ∥ n) \to n - 1 \in ℂ$
87	86 53 62	divcan2d	$⊢ (((A \in ℂ \land \|A\| < 1) \land n \in ℕ) \land \neg 2 ∥ n) \to 2 (\frac{n - 1}{2}) = n - 1$
88	87	oveq2d	$⊢ (((A \in ℂ \land \|A\| < 1) \land n \in ℕ) \land \neg 2 ∥ n) \to {(- i)}^{2 (\frac{n - 1}{2})} = {(- i)}^{n - 1}$
89	3	a1i	$⊢ (((A \in ℂ \land \|A\| < 1) \land n \in ℕ) \land \neg 2 ∥ n) \to - i \in ℂ$
90	12	a1i	$⊢ (((A \in ℂ \land \|A\| < 1) \land n \in ℕ) \land \neg 2 ∥ n) \to - i \neq 0$
91	17	ad2antlr	$⊢ (((A \in ℂ \land \|A\| < 1) \land n \in ℕ) \land \neg 2 ∥ n) \to n \in ℤ$
92	89 90 91	expm1d	$⊢ (((A \in ℂ \land \|A\| < 1) \land n \in ℕ) \land \neg 2 ∥ n) \to {(- i)}^{n - 1} = \frac{{(- i)}^{n}}{- i}$
93	88 92	eqtrd	$⊢ (((A \in ℂ \land \|A\| < 1) \land n \in ℕ) \land \neg 2 ∥ n) \to {(- i)}^{2 (\frac{n - 1}{2})} = \frac{{(- i)}^{n}}{- i}$
94	14	a1i	$⊢ (((A \in ℂ \land \|A\| < 1) \land n \in ℕ) \land \neg 2 ∥ n) \to 2 \in ℤ$
95		expmulz	$⊢ ((- i \in ℂ \land - i \neq 0) \land (2 \in ℤ \land \frac{n - 1}{2} \in ℤ)) \to {(- i)}^{2 (\frac{n - 1}{2})} = {({(- i)}^{2})}^{\frac{n - 1}{2}}$
96	89 90 94 82 95	syl22anc	$⊢ (((A \in ℂ \land \|A\| < 1) \land n \in ℕ) \land \neg 2 ∥ n) \to {(- i)}^{2 (\frac{n - 1}{2})} = {({(- i)}^{2})}^{\frac{n - 1}{2}}$
97	5	ad2antlr	$⊢ (((A \in ℂ \land \|A\| < 1) \land n \in ℕ) \land \neg 2 ∥ n) \to n \in ℕ_{0}$
98		expcl	$⊢ (- i \in ℂ \land n \in ℕ_{0}) \to {(- i)}^{n} \in ℂ$
99	3 97 98	sylancr	$⊢ (((A \in ℂ \land \|A\| < 1) \land n \in ℕ) \land \neg 2 ∥ n) \to {(- i)}^{n} \in ℂ$
100	99 89 90	divrec2d	$⊢ (((A \in ℂ \land \|A\| < 1) \land n \in ℕ) \land \neg 2 ∥ n) \to \frac{{(- i)}^{n}}{- i} = (\frac{1}{- i}) {(- i)}^{n}$
101	93 96 100	3eqtr3d	$⊢ (((A \in ℂ \land \|A\| < 1) \land n \in ℕ) \land \neg 2 ∥ n) \to {({(- i)}^{2})}^{\frac{n - 1}{2}} = (\frac{1}{- i}) {(- i)}^{n}$
102		i2	$⊢ i^{2} = - 1$
103	9 102	eqtri	$⊢ {(- i)}^{2} = - 1$
104	103	oveq1i	$⊢ {({(- i)}^{2})}^{\frac{n - 1}{2}} = {(- 1)}^{\frac{n - 1}{2}}$
105		irec	$⊢ \frac{1}{i} = - i$
106	105	negeqi	$⊢ - \frac{1}{i} = - (- i)$
107		divneg2	$⊢ (1 \in ℂ \land i \in ℂ \land i \neq 0) \to - \frac{1}{i} = \frac{1}{- i}$
108	54 2 11 107	mp3an	$⊢ - \frac{1}{i} = \frac{1}{- i}$
109	2	negnegi	$⊢ - (- i) = i$
110	106 108 109	3eqtr3i	$⊢ \frac{1}{- i} = i$
111	110	oveq1i	$⊢ (\frac{1}{- i}) {(- i)}^{n} = i {(- i)}^{n}$
112	101 104 111	3eqtr3g	$⊢ (((A \in ℂ \land \|A\| < 1) \land n \in ℕ) \land \neg 2 ∥ n) \to {(- 1)}^{\frac{n - 1}{2}} = i {(- i)}^{n}$
113	87	oveq2d	$⊢ (((A \in ℂ \land \|A\| < 1) \land n \in ℕ) \land \neg 2 ∥ n) \to i^{2 (\frac{n - 1}{2})} = i^{n - 1}$
114	2	a1i	$⊢ (((A \in ℂ \land \|A\| < 1) \land n \in ℕ) \land \neg 2 ∥ n) \to i \in ℂ$
115	11	a1i	$⊢ (((A \in ℂ \land \|A\| < 1) \land n \in ℕ) \land \neg 2 ∥ n) \to i \neq 0$
116	114 115 91	expm1d	$⊢ (((A \in ℂ \land \|A\| < 1) \land n \in ℕ) \land \neg 2 ∥ n) \to i^{n - 1} = \frac{i^{n}}{i}$
117	113 116	eqtrd	$⊢ (((A \in ℂ \land \|A\| < 1) \land n \in ℕ) \land \neg 2 ∥ n) \to i^{2 (\frac{n - 1}{2})} = \frac{i^{n}}{i}$
118		expmulz	$⊢ ((i \in ℂ \land i \neq 0) \land (2 \in ℤ \land \frac{n - 1}{2} \in ℤ)) \to i^{2 (\frac{n - 1}{2})} = {(i^{2})}^{\frac{n - 1}{2}}$
119	114 115 94 82 118	syl22anc	$⊢ (((A \in ℂ \land \|A\| < 1) \land n \in ℕ) \land \neg 2 ∥ n) \to i^{2 (\frac{n - 1}{2})} = {(i^{2})}^{\frac{n - 1}{2}}$
120		expcl	$⊢ (i \in ℂ \land n \in ℕ_{0}) \to i^{n} \in ℂ$
121	2 97 120	sylancr	$⊢ (((A \in ℂ \land \|A\| < 1) \land n \in ℕ) \land \neg 2 ∥ n) \to i^{n} \in ℂ$
122	121 114 115	divrec2d	$⊢ (((A \in ℂ \land \|A\| < 1) \land n \in ℕ) \land \neg 2 ∥ n) \to \frac{i^{n}}{i} = (\frac{1}{i}) i^{n}$
123	117 119 122	3eqtr3d	$⊢ (((A \in ℂ \land \|A\| < 1) \land n \in ℕ) \land \neg 2 ∥ n) \to {(i^{2})}^{\frac{n - 1}{2}} = (\frac{1}{i}) i^{n}$
124	102	oveq1i	$⊢ {(i^{2})}^{\frac{n - 1}{2}} = {(- 1)}^{\frac{n - 1}{2}}$
125	105	oveq1i	$⊢ (\frac{1}{i}) i^{n} = (- i) i^{n}$
126	123 124 125	3eqtr3g	$⊢ (((A \in ℂ \land \|A\| < 1) \land n \in ℕ) \land \neg 2 ∥ n) \to {(- 1)}^{\frac{n - 1}{2}} = (- i) i^{n}$
127		mulneg1	$⊢ (i \in ℂ \land i^{n} \in ℂ) \to (- i) i^{n} = - i i^{n}$
128	2 121 127	sylancr	$⊢ (((A \in ℂ \land \|A\| < 1) \land n \in ℕ) \land \neg 2 ∥ n) \to (- i) i^{n} = - i i^{n}$
129	126 128	eqtrd	$⊢ (((A \in ℂ \land \|A\| < 1) \land n \in ℕ) \land \neg 2 ∥ n) \to {(- 1)}^{\frac{n - 1}{2}} = - i i^{n}$
130	112 129	oveq12d	$⊢ (((A \in ℂ \land \|A\| < 1) \land n \in ℕ) \land \neg 2 ∥ n) \to {(- 1)}^{\frac{n - 1}{2}} + {(- 1)}^{\frac{n - 1}{2}} = i {(- i)}^{n} + (- i i^{n})$
131		mulcl	$⊢ (i \in ℂ \land {(- i)}^{n} \in ℂ) \to i {(- i)}^{n} \in ℂ$
132	2 99 131	sylancr	$⊢ (((A \in ℂ \land \|A\| < 1) \land n \in ℕ) \land \neg 2 ∥ n) \to i {(- i)}^{n} \in ℂ$
133		mulcl	$⊢ (i \in ℂ \land i^{n} \in ℂ) \to i i^{n} \in ℂ$
134	2 121 133	sylancr	$⊢ (((A \in ℂ \land \|A\| < 1) \land n \in ℕ) \land \neg 2 ∥ n) \to i i^{n} \in ℂ$
135	132 134	negsubd	$⊢ (((A \in ℂ \land \|A\| < 1) \land n \in ℕ) \land \neg 2 ∥ n) \to i {(- i)}^{n} + (- i i^{n}) = i {(- i)}^{n} - i i^{n}$
136	114 99 121	subdid	$⊢ (((A \in ℂ \land \|A\| < 1) \land n \in ℕ) \land \neg 2 ∥ n) \to i ({(- i)}^{n} - i^{n}) = i {(- i)}^{n} - i i^{n}$
137	135 136	eqtr4d	$⊢ (((A \in ℂ \land \|A\| < 1) \land n \in ℕ) \land \neg 2 ∥ n) \to i {(- i)}^{n} + (- i i^{n}) = i ({(- i)}^{n} - i^{n})$
138	84 130 137	3eqtrd	$⊢ (((A \in ℂ \land \|A\| < 1) \land n \in ℕ) \land \neg 2 ∥ n) \to 2 {(- 1)}^{\frac{n - 1}{2}} = i ({(- i)}^{n} - i^{n})$
139	53 83 62 138	mvllmuld	$⊢ (((A \in ℂ \land \|A\| < 1) \land n \in ℕ) \land \neg 2 ∥ n) \to {(- 1)}^{\frac{n - 1}{2}} = \frac{i ({(- i)}^{n} - i^{n})}{2}$
140	139	oveq1d	$⊢ (((A \in ℂ \land \|A\| < 1) \land n \in ℕ) \land \neg 2 ∥ n) \to {(- 1)}^{\frac{n - 1}{2}} (\frac{A^{n}}{n}) = (\frac{i ({(- i)}^{n} - i^{n})}{2}) (\frac{A^{n}}{n})$
141	52 140	ifeqda	$⊢ ((A \in ℂ \land \|A\| < 1) \land n \in ℕ) \to if (2 ∥ n, 0, {(- 1)}^{\frac{n - 1}{2}} (\frac{A^{n}}{n})) = (\frac{i ({(- i)}^{n} - i^{n})}{2}) (\frac{A^{n}}{n})$
142	141	mpteq2dva	$⊢ (A \in ℂ \land \|A\| < 1) \to (n \in ℕ ⟼ if (2 ∥ n, 0, {(- 1)}^{\frac{n - 1}{2}} (\frac{A^{n}}{n}))) = (n \in ℕ ⟼ (\frac{i ({(- i)}^{n} - i^{n})}{2}) (\frac{A^{n}}{n}))$
143	1 142	syl5eq	$⊢ (A \in ℂ \land \|A\| < 1) \to F = (n \in ℕ ⟼ (\frac{i ({(- i)}^{n} - i^{n})}{2}) (\frac{A^{n}}{n}))$
144	143	seqeq3d	$⊢ (A \in ℂ \land \|A\| < 1) \to seq 1 (+ F) = seq 1 (+ (n \in ℕ ⟼ (\frac{i ({(- i)}^{n} - i^{n})}{2}) (\frac{A^{n}}{n})))$
145		eqid	$⊢ (n \in ℕ ⟼ (\frac{i ({(- i)}^{n} - i^{n})}{2}) (\frac{A^{n}}{n})) = (n \in ℕ ⟼ (\frac{i ({(- i)}^{n} - i^{n})}{2}) (\frac{A^{n}}{n}))$
146	145	atantayl	$⊢ (A \in ℂ \land \|A\| < 1) \to seq 1 (+ (n \in ℕ ⟼ (\frac{i ({(- i)}^{n} - i^{n})}{2}) (\frac{A^{n}}{n}))) ⇝ arctan (A)$
147	144 146	eqbrtrd	$⊢ (A \in ℂ \land \|A\| < 1) \to seq 1 (+ F) ⇝ arctan (A)$

Metamath Proof Explorer

Theorem atantayl2

Proof