Metamath Proof Explorer

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 syl5eq ⊢ ( ( 𝐴 ∈ ℂ ∧ ( 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 ‘ 𝐴 ) )