Theorem atantayl3

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

	Ref	Expression
Hypothesis	atantayl3.1	⊢ 𝐹 = ( 𝑛 ∈ ℕ0 ↦ ( ( - 1 ↑ 𝑛 ) · ( ( 𝐴 ↑ ( ( 2 · 𝑛 ) + 1 ) ) / ( ( 2 · 𝑛 ) + 1 ) ) ) )
Assertion	atantayl3	⊢ ( ( 𝐴 ∈ ℂ ∧ ( abs ‘ 𝐴 ) < 1 ) → seq 0 ( + , 𝐹 ) ⇝ ( arctan ‘ 𝐴 ) )

Proof

Step	Hyp	Ref	Expression
1		atantayl3.1	⊢ 𝐹 = ( 𝑛 ∈ ℕ0 ↦ ( ( - 1 ↑ 𝑛 ) · ( ( 𝐴 ↑ ( ( 2 · 𝑛 ) + 1 ) ) / ( ( 2 · 𝑛 ) + 1 ) ) ) )
2		2nn0	⊢ 2 ∈ ℕ0
3		simpr	⊢ ( ( ( 𝐴 ∈ ℂ ∧ ( abs ‘ 𝐴 ) < 1 ) ∧ 𝑛 ∈ ℕ0 ) → 𝑛 ∈ ℕ0 )
4		nn0mulcl	⊢ ( ( 2 ∈ ℕ0 ∧ 𝑛 ∈ ℕ0 ) → ( 2 · 𝑛 ) ∈ ℕ0 )
5	2 3 4	sylancr	⊢ ( ( ( 𝐴 ∈ ℂ ∧ ( abs ‘ 𝐴 ) < 1 ) ∧ 𝑛 ∈ ℕ0 ) → ( 2 · 𝑛 ) ∈ ℕ0 )
6	5	nn0cnd	⊢ ( ( ( 𝐴 ∈ ℂ ∧ ( abs ‘ 𝐴 ) < 1 ) ∧ 𝑛 ∈ ℕ0 ) → ( 2 · 𝑛 ) ∈ ℂ )
7		ax-1cn	⊢ 1 ∈ ℂ
8		pncan	⊢ ( ( ( 2 · 𝑛 ) ∈ ℂ ∧ 1 ∈ ℂ ) → ( ( ( 2 · 𝑛 ) + 1 ) − 1 ) = ( 2 · 𝑛 ) )
9	6 7 8	sylancl	⊢ ( ( ( 𝐴 ∈ ℂ ∧ ( abs ‘ 𝐴 ) < 1 ) ∧ 𝑛 ∈ ℕ0 ) → ( ( ( 2 · 𝑛 ) + 1 ) − 1 ) = ( 2 · 𝑛 ) )
10	9	oveq1d	⊢ ( ( ( 𝐴 ∈ ℂ ∧ ( abs ‘ 𝐴 ) < 1 ) ∧ 𝑛 ∈ ℕ0 ) → ( ( ( ( 2 · 𝑛 ) + 1 ) − 1 ) / 2 ) = ( ( 2 · 𝑛 ) / 2 ) )
11		nn0cn	⊢ ( 𝑛 ∈ ℕ0 → 𝑛 ∈ ℂ )
12	11	adantl	⊢ ( ( ( 𝐴 ∈ ℂ ∧ ( abs ‘ 𝐴 ) < 1 ) ∧ 𝑛 ∈ ℕ0 ) → 𝑛 ∈ ℂ )
13		2cnd	⊢ ( ( ( 𝐴 ∈ ℂ ∧ ( abs ‘ 𝐴 ) < 1 ) ∧ 𝑛 ∈ ℕ0 ) → 2 ∈ ℂ )
14		2ne0	⊢ 2 ≠ 0
15	14	a1i	⊢ ( ( ( 𝐴 ∈ ℂ ∧ ( abs ‘ 𝐴 ) < 1 ) ∧ 𝑛 ∈ ℕ0 ) → 2 ≠ 0 )
16	12 13 15	divcan3d	⊢ ( ( ( 𝐴 ∈ ℂ ∧ ( abs ‘ 𝐴 ) < 1 ) ∧ 𝑛 ∈ ℕ0 ) → ( ( 2 · 𝑛 ) / 2 ) = 𝑛 )
17	10 16	eqtr2d	⊢ ( ( ( 𝐴 ∈ ℂ ∧ ( abs ‘ 𝐴 ) < 1 ) ∧ 𝑛 ∈ ℕ0 ) → 𝑛 = ( ( ( ( 2 · 𝑛 ) + 1 ) − 1 ) / 2 ) )
18	17	oveq2d	⊢ ( ( ( 𝐴 ∈ ℂ ∧ ( abs ‘ 𝐴 ) < 1 ) ∧ 𝑛 ∈ ℕ0 ) → ( - 1 ↑ 𝑛 ) = ( - 1 ↑ ( ( ( ( 2 · 𝑛 ) + 1 ) − 1 ) / 2 ) ) )
19	18	oveq1d	⊢ ( ( ( 𝐴 ∈ ℂ ∧ ( abs ‘ 𝐴 ) < 1 ) ∧ 𝑛 ∈ ℕ0 ) → ( ( - 1 ↑ 𝑛 ) · ( ( 𝐴 ↑ ( ( 2 · 𝑛 ) + 1 ) ) / ( ( 2 · 𝑛 ) + 1 ) ) ) = ( ( - 1 ↑ ( ( ( ( 2 · 𝑛 ) + 1 ) − 1 ) / 2 ) ) · ( ( 𝐴 ↑ ( ( 2 · 𝑛 ) + 1 ) ) / ( ( 2 · 𝑛 ) + 1 ) ) ) )
20	19	mpteq2dva	⊢ ( ( 𝐴 ∈ ℂ ∧ ( abs ‘ 𝐴 ) < 1 ) → ( 𝑛 ∈ ℕ0 ↦ ( ( - 1 ↑ 𝑛 ) · ( ( 𝐴 ↑ ( ( 2 · 𝑛 ) + 1 ) ) / ( ( 2 · 𝑛 ) + 1 ) ) ) ) = ( 𝑛 ∈ ℕ0 ↦ ( ( - 1 ↑ ( ( ( ( 2 · 𝑛 ) + 1 ) − 1 ) / 2 ) ) · ( ( 𝐴 ↑ ( ( 2 · 𝑛 ) + 1 ) ) / ( ( 2 · 𝑛 ) + 1 ) ) ) ) )
21	1 20	eqtrid	⊢ ( ( 𝐴 ∈ ℂ ∧ ( abs ‘ 𝐴 ) < 1 ) → 𝐹 = ( 𝑛 ∈ ℕ0 ↦ ( ( - 1 ↑ ( ( ( ( 2 · 𝑛 ) + 1 ) − 1 ) / 2 ) ) · ( ( 𝐴 ↑ ( ( 2 · 𝑛 ) + 1 ) ) / ( ( 2 · 𝑛 ) + 1 ) ) ) ) )
22	21	seqeq3d	⊢ ( ( 𝐴 ∈ ℂ ∧ ( abs ‘ 𝐴 ) < 1 ) → seq 0 ( + , 𝐹 ) = seq 0 ( + , ( 𝑛 ∈ ℕ0 ↦ ( ( - 1 ↑ ( ( ( ( 2 · 𝑛 ) + 1 ) − 1 ) / 2 ) ) · ( ( 𝐴 ↑ ( ( 2 · 𝑛 ) + 1 ) ) / ( ( 2 · 𝑛 ) + 1 ) ) ) ) ) )
23		eqid	⊢ ( 𝑘 ∈ ℕ ↦ if ( 2 ∥ 𝑘 , 0 , ( ( - 1 ↑ ( ( 𝑘 − 1 ) / 2 ) ) · ( ( 𝐴 ↑ 𝑘 ) / 𝑘 ) ) ) ) = ( 𝑘 ∈ ℕ ↦ if ( 2 ∥ 𝑘 , 0 , ( ( - 1 ↑ ( ( 𝑘 − 1 ) / 2 ) ) · ( ( 𝐴 ↑ 𝑘 ) / 𝑘 ) ) ) )
24	23	atantayl2	⊢ ( ( 𝐴 ∈ ℂ ∧ ( abs ‘ 𝐴 ) < 1 ) → seq 1 ( + , ( 𝑘 ∈ ℕ ↦ if ( 2 ∥ 𝑘 , 0 , ( ( - 1 ↑ ( ( 𝑘 − 1 ) / 2 ) ) · ( ( 𝐴 ↑ 𝑘 ) / 𝑘 ) ) ) ) ) ⇝ ( arctan ‘ 𝐴 ) )
25		neg1cn	⊢ - 1 ∈ ℂ
26		expcl	⊢ ( ( - 1 ∈ ℂ ∧ 𝑛 ∈ ℕ0 ) → ( - 1 ↑ 𝑛 ) ∈ ℂ )
27	25 3 26	sylancr	⊢ ( ( ( 𝐴 ∈ ℂ ∧ ( abs ‘ 𝐴 ) < 1 ) ∧ 𝑛 ∈ ℕ0 ) → ( - 1 ↑ 𝑛 ) ∈ ℂ )
28		simpll	⊢ ( ( ( 𝐴 ∈ ℂ ∧ ( abs ‘ 𝐴 ) < 1 ) ∧ 𝑛 ∈ ℕ0 ) → 𝐴 ∈ ℂ )
29		peano2nn0	⊢ ( ( 2 · 𝑛 ) ∈ ℕ0 → ( ( 2 · 𝑛 ) + 1 ) ∈ ℕ0 )
30	5 29	syl	⊢ ( ( ( 𝐴 ∈ ℂ ∧ ( abs ‘ 𝐴 ) < 1 ) ∧ 𝑛 ∈ ℕ0 ) → ( ( 2 · 𝑛 ) + 1 ) ∈ ℕ0 )
31	28 30	expcld	⊢ ( ( ( 𝐴 ∈ ℂ ∧ ( abs ‘ 𝐴 ) < 1 ) ∧ 𝑛 ∈ ℕ0 ) → ( 𝐴 ↑ ( ( 2 · 𝑛 ) + 1 ) ) ∈ ℂ )
32		nn0p1nn	⊢ ( ( 2 · 𝑛 ) ∈ ℕ0 → ( ( 2 · 𝑛 ) + 1 ) ∈ ℕ )
33	5 32	syl	⊢ ( ( ( 𝐴 ∈ ℂ ∧ ( abs ‘ 𝐴 ) < 1 ) ∧ 𝑛 ∈ ℕ0 ) → ( ( 2 · 𝑛 ) + 1 ) ∈ ℕ )
34	33	nncnd	⊢ ( ( ( 𝐴 ∈ ℂ ∧ ( abs ‘ 𝐴 ) < 1 ) ∧ 𝑛 ∈ ℕ0 ) → ( ( 2 · 𝑛 ) + 1 ) ∈ ℂ )
35	33	nnne0d	⊢ ( ( ( 𝐴 ∈ ℂ ∧ ( abs ‘ 𝐴 ) < 1 ) ∧ 𝑛 ∈ ℕ0 ) → ( ( 2 · 𝑛 ) + 1 ) ≠ 0 )
36	31 34 35	divcld	⊢ ( ( ( 𝐴 ∈ ℂ ∧ ( abs ‘ 𝐴 ) < 1 ) ∧ 𝑛 ∈ ℕ0 ) → ( ( 𝐴 ↑ ( ( 2 · 𝑛 ) + 1 ) ) / ( ( 2 · 𝑛 ) + 1 ) ) ∈ ℂ )
37	27 36	mulcld	⊢ ( ( ( 𝐴 ∈ ℂ ∧ ( abs ‘ 𝐴 ) < 1 ) ∧ 𝑛 ∈ ℕ0 ) → ( ( - 1 ↑ 𝑛 ) · ( ( 𝐴 ↑ ( ( 2 · 𝑛 ) + 1 ) ) / ( ( 2 · 𝑛 ) + 1 ) ) ) ∈ ℂ )
38	19 37	eqeltrrd	⊢ ( ( ( 𝐴 ∈ ℂ ∧ ( abs ‘ 𝐴 ) < 1 ) ∧ 𝑛 ∈ ℕ0 ) → ( ( - 1 ↑ ( ( ( ( 2 · 𝑛 ) + 1 ) − 1 ) / 2 ) ) · ( ( 𝐴 ↑ ( ( 2 · 𝑛 ) + 1 ) ) / ( ( 2 · 𝑛 ) + 1 ) ) ) ∈ ℂ )
39		oveq1	⊢ ( 𝑘 = ( ( 2 · 𝑛 ) + 1 ) → ( 𝑘 − 1 ) = ( ( ( 2 · 𝑛 ) + 1 ) − 1 ) )
40	39	oveq1d	⊢ ( 𝑘 = ( ( 2 · 𝑛 ) + 1 ) → ( ( 𝑘 − 1 ) / 2 ) = ( ( ( ( 2 · 𝑛 ) + 1 ) − 1 ) / 2 ) )
41	40	oveq2d	⊢ ( 𝑘 = ( ( 2 · 𝑛 ) + 1 ) → ( - 1 ↑ ( ( 𝑘 − 1 ) / 2 ) ) = ( - 1 ↑ ( ( ( ( 2 · 𝑛 ) + 1 ) − 1 ) / 2 ) ) )
42		oveq2	⊢ ( 𝑘 = ( ( 2 · 𝑛 ) + 1 ) → ( 𝐴 ↑ 𝑘 ) = ( 𝐴 ↑ ( ( 2 · 𝑛 ) + 1 ) ) )
43		id	⊢ ( 𝑘 = ( ( 2 · 𝑛 ) + 1 ) → 𝑘 = ( ( 2 · 𝑛 ) + 1 ) )
44	42 43	oveq12d	⊢ ( 𝑘 = ( ( 2 · 𝑛 ) + 1 ) → ( ( 𝐴 ↑ 𝑘 ) / 𝑘 ) = ( ( 𝐴 ↑ ( ( 2 · 𝑛 ) + 1 ) ) / ( ( 2 · 𝑛 ) + 1 ) ) )
45	41 44	oveq12d	⊢ ( 𝑘 = ( ( 2 · 𝑛 ) + 1 ) → ( ( - 1 ↑ ( ( 𝑘 − 1 ) / 2 ) ) · ( ( 𝐴 ↑ 𝑘 ) / 𝑘 ) ) = ( ( - 1 ↑ ( ( ( ( 2 · 𝑛 ) + 1 ) − 1 ) / 2 ) ) · ( ( 𝐴 ↑ ( ( 2 · 𝑛 ) + 1 ) ) / ( ( 2 · 𝑛 ) + 1 ) ) ) )
46	38 45	iserodd	⊢ ( ( 𝐴 ∈ ℂ ∧ ( abs ‘ 𝐴 ) < 1 ) → ( seq 0 ( + , ( 𝑛 ∈ ℕ0 ↦ ( ( - 1 ↑ ( ( ( ( 2 · 𝑛 ) + 1 ) − 1 ) / 2 ) ) · ( ( 𝐴 ↑ ( ( 2 · 𝑛 ) + 1 ) ) / ( ( 2 · 𝑛 ) + 1 ) ) ) ) ) ⇝ ( arctan ‘ 𝐴 ) ↔ seq 1 ( + , ( 𝑘 ∈ ℕ ↦ if ( 2 ∥ 𝑘 , 0 , ( ( - 1 ↑ ( ( 𝑘 − 1 ) / 2 ) ) · ( ( 𝐴 ↑ 𝑘 ) / 𝑘 ) ) ) ) ) ⇝ ( arctan ‘ 𝐴 ) ) )
47	24 46	mpbird	⊢ ( ( 𝐴 ∈ ℂ ∧ ( abs ‘ 𝐴 ) < 1 ) → seq 0 ( + , ( 𝑛 ∈ ℕ0 ↦ ( ( - 1 ↑ ( ( ( ( 2 · 𝑛 ) + 1 ) − 1 ) / 2 ) ) · ( ( 𝐴 ↑ ( ( 2 · 𝑛 ) + 1 ) ) / ( ( 2 · 𝑛 ) + 1 ) ) ) ) ) ⇝ ( arctan ‘ 𝐴 ) )
48	22 47	eqbrtrd	⊢ ( ( 𝐴 ∈ ℂ ∧ ( abs ‘ 𝐴 ) < 1 ) → seq 0 ( + , 𝐹 ) ⇝ ( arctan ‘ 𝐴 ) )