This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem atantayl2

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

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

Proof

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