Metamath Proof Explorer

Theorem atantayl2

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

Ref Expression
Hypothesis atantayl2.1 
|- F = ( n e. NN |-> if ( 2 || n , 0 , ( ( -u 1 ^ ( ( n - 1 ) / 2 ) ) x. ( ( A ^ n ) / n ) ) ) )
Assertion atantayl2 
|- ( ( A e. CC /\ ( abs ` A ) < 1 ) -> seq 1 ( + , F ) ~~> ( arctan ` A ) )

Proof

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