atantayl3

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

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

Proof

Step	Hyp	Ref	Expression
1		atantayl3.1	$⊢ F = (n \in ℕ_{0} ⟼ {(- 1)}^{n} (\frac{A^{2 n + 1}}{2 n + 1}))$
2		2nn0	$⊢ 2 \in ℕ_{0}$
3		simpr	$⊢ ((A \in ℂ \land \|A\| < 1) \land n \in ℕ_{0}) \to n \in ℕ_{0}$
4		nn0mulcl	$⊢ (2 \in ℕ_{0} \land n \in ℕ_{0}) \to 2 n \in ℕ_{0}$
5	2 3 4	sylancr	$⊢ ((A \in ℂ \land \|A\| < 1) \land n \in ℕ_{0}) \to 2 n \in ℕ_{0}$
6	5	nn0cnd	$⊢ ((A \in ℂ \land \|A\| < 1) \land n \in ℕ_{0}) \to 2 n \in ℂ$
7		ax-1cn	$⊢ 1 \in ℂ$
8		pncan	$⊢ (2 n \in ℂ \land 1 \in ℂ) \to 2 n + 1 - 1 = 2 n$
9	6 7 8	sylancl	$⊢ ((A \in ℂ \land \|A\| < 1) \land n \in ℕ_{0}) \to 2 n + 1 - 1 = 2 n$
10	9	oveq1d	$⊢ ((A \in ℂ \land \|A\| < 1) \land n \in ℕ_{0}) \to \frac{2 n + 1 - 1}{2} = \frac{2 n}{2}$
11		nn0cn	$⊢ n \in ℕ_{0} \to n \in ℂ$
12	11	adantl	$⊢ ((A \in ℂ \land \|A\| < 1) \land n \in ℕ_{0}) \to n \in ℂ$
13		2cnd	$⊢ ((A \in ℂ \land \|A\| < 1) \land n \in ℕ_{0}) \to 2 \in ℂ$
14		2ne0	$⊢ 2 \neq 0$
15	14	a1i	$⊢ ((A \in ℂ \land \|A\| < 1) \land n \in ℕ_{0}) \to 2 \neq 0$
16	12 13 15	divcan3d	$⊢ ((A \in ℂ \land \|A\| < 1) \land n \in ℕ_{0}) \to \frac{2 n}{2} = n$
17	10 16	eqtr2d	$⊢ ((A \in ℂ \land \|A\| < 1) \land n \in ℕ_{0}) \to n = \frac{2 n + 1 - 1}{2}$
18	17	oveq2d	$⊢ ((A \in ℂ \land \|A\| < 1) \land n \in ℕ_{0}) \to {(- 1)}^{n} = {(- 1)}^{\frac{2 n + 1 - 1}{2}}$
19	18	oveq1d	$⊢ ((A \in ℂ \land \|A\| < 1) \land n \in ℕ_{0}) \to {(- 1)}^{n} (\frac{A^{2 n + 1}}{2 n + 1}) = {(- 1)}^{\frac{2 n + 1 - 1}{2}} (\frac{A^{2 n + 1}}{2 n + 1})$
20	19	mpteq2dva	$⊢ (A \in ℂ \land \|A\| < 1) \to (n \in ℕ_{0} ⟼ {(- 1)}^{n} (\frac{A^{2 n + 1}}{2 n + 1})) = (n \in ℕ_{0} ⟼ {(- 1)}^{\frac{2 n + 1 - 1}{2}} (\frac{A^{2 n + 1}}{2 n + 1}))$
21	1 20	syl5eq	$⊢ (A \in ℂ \land \|A\| < 1) \to F = (n \in ℕ_{0} ⟼ {(- 1)}^{\frac{2 n + 1 - 1}{2}} (\frac{A^{2 n + 1}}{2 n + 1}))$
22	21	seqeq3d	$⊢ (A \in ℂ \land \|A\| < 1) \to seq 0 (+ F) = seq 0 (+ (n \in ℕ_{0} ⟼ {(- 1)}^{\frac{2 n + 1 - 1}{2}} (\frac{A^{2 n + 1}}{2 n + 1})))$
23		eqid	$⊢ (k \in ℕ ⟼ if (2 ∥ k, 0, {(- 1)}^{\frac{k - 1}{2}} (\frac{A^{k}}{k}))) = (k \in ℕ ⟼ if (2 ∥ k, 0, {(- 1)}^{\frac{k - 1}{2}} (\frac{A^{k}}{k})))$
24	23	atantayl2	$⊢ (A \in ℂ \land \|A\| < 1) \to seq 1 (+ (k \in ℕ ⟼ if (2 ∥ k, 0, {(- 1)}^{\frac{k - 1}{2}} (\frac{A^{k}}{k})))) ⇝ arctan (A)$
25		neg1cn	$⊢ - 1 \in ℂ$
26		expcl	$⊢ (- 1 \in ℂ \land n \in ℕ_{0}) \to {(- 1)}^{n} \in ℂ$
27	25 3 26	sylancr	$⊢ ((A \in ℂ \land \|A\| < 1) \land n \in ℕ_{0}) \to {(- 1)}^{n} \in ℂ$
28		simpll	$⊢ ((A \in ℂ \land \|A\| < 1) \land n \in ℕ_{0}) \to A \in ℂ$
29		peano2nn0	$⊢ 2 n \in ℕ_{0} \to 2 n + 1 \in ℕ_{0}$
30	5 29	syl	$⊢ ((A \in ℂ \land \|A\| < 1) \land n \in ℕ_{0}) \to 2 n + 1 \in ℕ_{0}$
31	28 30	expcld	$⊢ ((A \in ℂ \land \|A\| < 1) \land n \in ℕ_{0}) \to A^{2 n + 1} \in ℂ$
32		nn0p1nn	$⊢ 2 n \in ℕ_{0} \to 2 n + 1 \in ℕ$
33	5 32	syl	$⊢ ((A \in ℂ \land \|A\| < 1) \land n \in ℕ_{0}) \to 2 n + 1 \in ℕ$
34	33	nncnd	$⊢ ((A \in ℂ \land \|A\| < 1) \land n \in ℕ_{0}) \to 2 n + 1 \in ℂ$
35	33	nnne0d	$⊢ ((A \in ℂ \land \|A\| < 1) \land n \in ℕ_{0}) \to 2 n + 1 \neq 0$
36	31 34 35	divcld	$⊢ ((A \in ℂ \land \|A\| < 1) \land n \in ℕ_{0}) \to \frac{A^{2 n + 1}}{2 n + 1} \in ℂ$
37	27 36	mulcld	$⊢ ((A \in ℂ \land \|A\| < 1) \land n \in ℕ_{0}) \to {(- 1)}^{n} (\frac{A^{2 n + 1}}{2 n + 1}) \in ℂ$
38	19 37	eqeltrrd	$⊢ ((A \in ℂ \land \|A\| < 1) \land n \in ℕ_{0}) \to {(- 1)}^{\frac{2 n + 1 - 1}{2}} (\frac{A^{2 n + 1}}{2 n + 1}) \in ℂ$
39		oveq1	$⊢ k = 2 n + 1 \to k - 1 = 2 n + 1 - 1$
40	39	oveq1d	$⊢ k = 2 n + 1 \to \frac{k - 1}{2} = \frac{2 n + 1 - 1}{2}$
41	40	oveq2d	$⊢ k = 2 n + 1 \to {(- 1)}^{\frac{k - 1}{2}} = {(- 1)}^{\frac{2 n + 1 - 1}{2}}$
42		oveq2	$⊢ k = 2 n + 1 \to A^{k} = A^{2 n + 1}$
43		id	$⊢ k = 2 n + 1 \to k = 2 n + 1$
44	42 43	oveq12d	$⊢ k = 2 n + 1 \to \frac{A^{k}}{k} = \frac{A^{2 n + 1}}{2 n + 1}$
45	41 44	oveq12d	$⊢ k = 2 n + 1 \to {(- 1)}^{\frac{k - 1}{2}} (\frac{A^{k}}{k}) = {(- 1)}^{\frac{2 n + 1 - 1}{2}} (\frac{A^{2 n + 1}}{2 n + 1})$
46	38 45	iserodd	$⊢ (A \in ℂ \land \|A\| < 1) \to (seq 0 (+ (n \in ℕ_{0} ⟼ {(- 1)}^{\frac{2 n + 1 - 1}{2}} (\frac{A^{2 n + 1}}{2 n + 1}))) ⇝ arctan (A) \leftrightarrow seq 1 (+ (k \in ℕ ⟼ if (2 ∥ k, 0, {(- 1)}^{\frac{k - 1}{2}} (\frac{A^{k}}{k})))) ⇝ arctan (A))$
47	24 46	mpbird	$⊢ (A \in ℂ \land \|A\| < 1) \to seq 0 (+ (n \in ℕ_{0} ⟼ {(- 1)}^{\frac{2 n + 1 - 1}{2}} (\frac{A^{2 n + 1}}{2 n + 1}))) ⇝ arctan (A)$
48	22 47	eqbrtrd	$⊢ (A \in ℂ \land \|A\| < 1) \to seq 0 (+ F) ⇝ arctan (A)$

Metamath Proof Explorer

Theorem atantayl3

Proof