Metamath Proof Explorer

Theorem atantayl

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

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

Proof

Step Hyp Ref Expression
1 atantayl.1 
 |-  F = ( n e. NN |-> ( ( ( _i x. ( ( -u _i ^ n ) - ( _i ^ n ) ) ) / 2 ) x. ( ( A ^ n ) / n ) ) )
2 nnuz 
 |-  NN = ( ZZ>= ` 1 )
3 1zzd 
 |-  ( ( A e. CC /\ ( abs ` A ) < 1 ) -> 1 e. ZZ )
4 ax-icn 
 |-  _i e. CC
5 halfcl 
 |-  ( _i e. CC -> ( _i / 2 ) e. CC )
6 4 5 mp1i 
 |-  ( ( A e. CC /\ ( abs ` A ) < 1 ) -> ( _i / 2 ) e. CC )
7 simpl 
 |-  ( ( A e. CC /\ ( abs ` A ) < 1 ) -> A e. CC )
8 mulcl 
 |-  ( ( _i e. CC /\ A e. CC ) -> ( _i x. A ) e. CC )
9 4 7 8 sylancr 
 |-  ( ( A e. CC /\ ( abs ` A ) < 1 ) -> ( _i x. A ) e. CC )
10 9 negcld 
 |-  ( ( A e. CC /\ ( abs ` A ) < 1 ) -> -u ( _i x. A ) e. CC )
11 9 absnegd 
 |-  ( ( A e. CC /\ ( abs ` A ) < 1 ) -> ( abs ` -u ( _i x. A ) ) = ( abs ` ( _i x. A ) ) )
12 absmul 
 |-  ( ( _i e. CC /\ A e. CC ) -> ( abs ` ( _i x. A ) ) = ( ( abs ` _i ) x. ( abs ` A ) ) )
13 4 7 12 sylancr 
 |-  ( ( A e. CC /\ ( abs ` A ) < 1 ) -> ( abs ` ( _i x. A ) ) = ( ( abs ` _i ) x. ( abs ` A ) ) )
14 absi 
 |-  ( abs ` _i ) = 1
15 14 oveq1i 
 |-  ( ( abs ` _i ) x. ( abs ` A ) ) = ( 1 x. ( abs ` A ) )
16 abscl 
 |-  ( A e. CC -> ( abs ` A ) e. RR )
17 16 adantr 
 |-  ( ( A e. CC /\ ( abs ` A ) < 1 ) -> ( abs ` A ) e. RR )
18 17 recnd 
 |-  ( ( A e. CC /\ ( abs ` A ) < 1 ) -> ( abs ` A ) e. CC )
19 18 mulid2d 
 |-  ( ( A e. CC /\ ( abs ` A ) < 1 ) -> ( 1 x. ( abs ` A ) ) = ( abs ` A ) )
20 15 19 syl5eq 
 |-  ( ( A e. CC /\ ( abs ` A ) < 1 ) -> ( ( abs ` _i ) x. ( abs ` A ) ) = ( abs ` A ) )
21 11 13 20 3eqtrd 
 |-  ( ( A e. CC /\ ( abs ` A ) < 1 ) -> ( abs ` -u ( _i x. A ) ) = ( abs ` A ) )
22 simpr 
 |-  ( ( A e. CC /\ ( abs ` A ) < 1 ) -> ( abs ` A ) < 1 )
23 21 22 eqbrtrd 
 |-  ( ( A e. CC /\ ( abs ` A ) < 1 ) -> ( abs ` -u ( _i x. A ) ) < 1 )
24 logtayl 
 |-  ( ( -u ( _i x. A ) e. CC /\ ( abs ` -u ( _i x. A ) ) < 1 ) -> seq 1 ( + , ( n e. NN |-> ( ( -u ( _i x. A ) ^ n ) / n ) ) ) ~~> -u ( log ` ( 1 - -u ( _i x. A ) ) ) )
25 10 23 24 syl2anc 
 |-  ( ( A e. CC /\ ( abs ` A ) < 1 ) -> seq 1 ( + , ( n e. NN |-> ( ( -u ( _i x. A ) ^ n ) / n ) ) ) ~~> -u ( log ` ( 1 - -u ( _i x. A ) ) ) )
26 ax-1cn 
 |-  1 e. CC
27 subneg 
 |-  ( ( 1 e. CC /\ ( _i x. A ) e. CC ) -> ( 1 - -u ( _i x. A ) ) = ( 1 + ( _i x. A ) ) )
28 26 9 27 sylancr 
 |-  ( ( A e. CC /\ ( abs ` A ) < 1 ) -> ( 1 - -u ( _i x. A ) ) = ( 1 + ( _i x. A ) ) )
29 28 fveq2d 
 |-  ( ( A e. CC /\ ( abs ` A ) < 1 ) -> ( log ` ( 1 - -u ( _i x. A ) ) ) = ( log ` ( 1 + ( _i x. A ) ) ) )
30 29 negeqd 
 |-  ( ( A e. CC /\ ( abs ` A ) < 1 ) -> -u ( log ` ( 1 - -u ( _i x. A ) ) ) = -u ( log ` ( 1 + ( _i x. A ) ) ) )
31 25 30 breqtrd 
 |-  ( ( A e. CC /\ ( abs ` A ) < 1 ) -> seq 1 ( + , ( n e. NN |-> ( ( -u ( _i x. A ) ^ n ) / n ) ) ) ~~> -u ( log ` ( 1 + ( _i x. A ) ) ) )
32 seqex 
 |-  seq 1 ( + , ( n e. NN |-> ( ( ( -u ( _i x. A ) ^ n ) / n ) - ( ( ( _i x. A ) ^ n ) / n ) ) ) ) e. _V
33 32 a1i 
 |-  ( ( A e. CC /\ ( abs ` A ) < 1 ) -> seq 1 ( + , ( n e. NN |-> ( ( ( -u ( _i x. A ) ^ n ) / n ) - ( ( ( _i x. A ) ^ n ) / n ) ) ) ) e. _V )
34 11 23 eqbrtrrd 
 |-  ( ( A e. CC /\ ( abs ` A ) < 1 ) -> ( abs ` ( _i x. A ) ) < 1 )
35 logtayl 
 |-  ( ( ( _i x. A ) e. CC /\ ( abs ` ( _i x. A ) ) < 1 ) -> seq 1 ( + , ( n e. NN |-> ( ( ( _i x. A ) ^ n ) / n ) ) ) ~~> -u ( log ` ( 1 - ( _i x. A ) ) ) )
36 9 34 35 syl2anc 
 |-  ( ( A e. CC /\ ( abs ` A ) < 1 ) -> seq 1 ( + , ( n e. NN |-> ( ( ( _i x. A ) ^ n ) / n ) ) ) ~~> -u ( log ` ( 1 - ( _i x. A ) ) ) )
37 oveq2 
 |-  ( n = m -> ( -u ( _i x. A ) ^ n ) = ( -u ( _i x. A ) ^ m ) )
38 id 
 |-  ( n = m -> n = m )
39 37 38 oveq12d 
 |-  ( n = m -> ( ( -u ( _i x. A ) ^ n ) / n ) = ( ( -u ( _i x. A ) ^ m ) / m ) )
40 eqid 
 |-  ( n e. NN |-> ( ( -u ( _i x. A ) ^ n ) / n ) ) = ( n e. NN |-> ( ( -u ( _i x. A ) ^ n ) / n ) )
41 ovex 
 |-  ( ( -u ( _i x. A ) ^ m ) / m ) e. _V
42 39 40 41 fvmpt 
 |-  ( m e. NN -> ( ( n e. NN |-> ( ( -u ( _i x. A ) ^ n ) / n ) ) ` m ) = ( ( -u ( _i x. A ) ^ m ) / m ) )
43 42 adantl 
 |-  ( ( ( A e. CC /\ ( abs ` A ) < 1 ) /\ m e. NN ) -> ( ( n e. NN |-> ( ( -u ( _i x. A ) ^ n ) / n ) ) ` m ) = ( ( -u ( _i x. A ) ^ m ) / m ) )
44 nnnn0 
 |-  ( m e. NN -> m e. NN0 )
45 expcl 
 |-  ( ( -u ( _i x. A ) e. CC /\ m e. NN0 ) -> ( -u ( _i x. A ) ^ m ) e. CC )
46 10 44 45 syl2an 
 |-  ( ( ( A e. CC /\ ( abs ` A ) < 1 ) /\ m e. NN ) -> ( -u ( _i x. A ) ^ m ) e. CC )
47 nncn 
 |-  ( m e. NN -> m e. CC )
48 47 adantl 
 |-  ( ( ( A e. CC /\ ( abs ` A ) < 1 ) /\ m e. NN ) -> m e. CC )
49 nnne0 
 |-  ( m e. NN -> m =/= 0 )
50 49 adantl 
 |-  ( ( ( A e. CC /\ ( abs ` A ) < 1 ) /\ m e. NN ) -> m =/= 0 )
51 46 48 50 divcld 
 |-  ( ( ( A e. CC /\ ( abs ` A ) < 1 ) /\ m e. NN ) -> ( ( -u ( _i x. A ) ^ m ) / m ) e. CC )
52 43 51 eqeltrd 
 |-  ( ( ( A e. CC /\ ( abs ` A ) < 1 ) /\ m e. NN ) -> ( ( n e. NN |-> ( ( -u ( _i x. A ) ^ n ) / n ) ) ` m ) e. CC )
53 2 3 52 serf 
 |-  ( ( A e. CC /\ ( abs ` A ) < 1 ) -> seq 1 ( + , ( n e. NN |-> ( ( -u ( _i x. A ) ^ n ) / n ) ) ) : NN --> CC )
54 53 ffvelrnda 
 |-  ( ( ( A e. CC /\ ( abs ` A ) < 1 ) /\ k e. NN ) -> ( seq 1 ( + , ( n e. NN |-> ( ( -u ( _i x. A ) ^ n ) / n ) ) ) ` k ) e. CC )
55 oveq2 
 |-  ( n = m -> ( ( _i x. A ) ^ n ) = ( ( _i x. A ) ^ m ) )
56 55 38 oveq12d 
 |-  ( n = m -> ( ( ( _i x. A ) ^ n ) / n ) = ( ( ( _i x. A ) ^ m ) / m ) )
57 eqid 
 |-  ( n e. NN |-> ( ( ( _i x. A ) ^ n ) / n ) ) = ( n e. NN |-> ( ( ( _i x. A ) ^ n ) / n ) )
58 ovex 
 |-  ( ( ( _i x. A ) ^ m ) / m ) e. _V
59 56 57 58 fvmpt 
 |-  ( m e. NN -> ( ( n e. NN |-> ( ( ( _i x. A ) ^ n ) / n ) ) ` m ) = ( ( ( _i x. A ) ^ m ) / m ) )
60 59 adantl 
 |-  ( ( ( A e. CC /\ ( abs ` A ) < 1 ) /\ m e. NN ) -> ( ( n e. NN |-> ( ( ( _i x. A ) ^ n ) / n ) ) ` m ) = ( ( ( _i x. A ) ^ m ) / m ) )
61 expcl 
 |-  ( ( ( _i x. A ) e. CC /\ m e. NN0 ) -> ( ( _i x. A ) ^ m ) e. CC )
62 9 44 61 syl2an 
 |-  ( ( ( A e. CC /\ ( abs ` A ) < 1 ) /\ m e. NN ) -> ( ( _i x. A ) ^ m ) e. CC )
63 62 48 50 divcld 
 |-  ( ( ( A e. CC /\ ( abs ` A ) < 1 ) /\ m e. NN ) -> ( ( ( _i x. A ) ^ m ) / m ) e. CC )
64 60 63 eqeltrd 
 |-  ( ( ( A e. CC /\ ( abs ` A ) < 1 ) /\ m e. NN ) -> ( ( n e. NN |-> ( ( ( _i x. A ) ^ n ) / n ) ) ` m ) e. CC )
65 2 3 64 serf 
 |-  ( ( A e. CC /\ ( abs ` A ) < 1 ) -> seq 1 ( + , ( n e. NN |-> ( ( ( _i x. A ) ^ n ) / n ) ) ) : NN --> CC )
66 65 ffvelrnda 
 |-  ( ( ( A e. CC /\ ( abs ` A ) < 1 ) /\ k e. NN ) -> ( seq 1 ( + , ( n e. NN |-> ( ( ( _i x. A ) ^ n ) / n ) ) ) ` k ) e. CC )
67 simpr 
 |-  ( ( ( A e. CC /\ ( abs ` A ) < 1 ) /\ k e. NN ) -> k e. NN )
68 67 2 eleqtrdi 
 |-  ( ( ( A e. CC /\ ( abs ` A ) < 1 ) /\ k e. NN ) -> k e. ( ZZ>= ` 1 ) )
69 simpl 
 |-  ( ( ( A e. CC /\ ( abs ` A ) < 1 ) /\ k e. NN ) -> ( A e. CC /\ ( abs ` A ) < 1 ) )
70 elfznn 
 |-  ( m e. ( 1 ... k ) -> m e. NN )
71 69 70 52 syl2an 
 |-  ( ( ( ( A e. CC /\ ( abs ` A ) < 1 ) /\ k e. NN ) /\ m e. ( 1 ... k ) ) -> ( ( n e. NN |-> ( ( -u ( _i x. A ) ^ n ) / n ) ) ` m ) e. CC )
72 69 70 64 syl2an 
 |-  ( ( ( ( A e. CC /\ ( abs ` A ) < 1 ) /\ k e. NN ) /\ m e. ( 1 ... k ) ) -> ( ( n e. NN |-> ( ( ( _i x. A ) ^ n ) / n ) ) ` m ) e. CC )
73 39 56 oveq12d 
 |-  ( n = m -> ( ( ( -u ( _i x. A ) ^ n ) / n ) - ( ( ( _i x. A ) ^ n ) / n ) ) = ( ( ( -u ( _i x. A ) ^ m ) / m ) - ( ( ( _i x. A ) ^ m ) / m ) ) )
74 eqid 
 |-  ( n e. NN |-> ( ( ( -u ( _i x. A ) ^ n ) / n ) - ( ( ( _i x. A ) ^ n ) / n ) ) ) = ( n e. NN |-> ( ( ( -u ( _i x. A ) ^ n ) / n ) - ( ( ( _i x. A ) ^ n ) / n ) ) )
75 ovex 
 |-  ( ( ( -u ( _i x. A ) ^ m ) / m ) - ( ( ( _i x. A ) ^ m ) / m ) ) e. _V
76 73 74 75 fvmpt 
 |-  ( m e. NN -> ( ( n e. NN |-> ( ( ( -u ( _i x. A ) ^ n ) / n ) - ( ( ( _i x. A ) ^ n ) / n ) ) ) ` m ) = ( ( ( -u ( _i x. A ) ^ m ) / m ) - ( ( ( _i x. A ) ^ m ) / m ) ) )
77 76 adantl 
 |-  ( ( ( A e. CC /\ ( abs ` A ) < 1 ) /\ m e. NN ) -> ( ( n e. NN |-> ( ( ( -u ( _i x. A ) ^ n ) / n ) - ( ( ( _i x. A ) ^ n ) / n ) ) ) ` m ) = ( ( ( -u ( _i x. A ) ^ m ) / m ) - ( ( ( _i x. A ) ^ m ) / m ) ) )
78 43 60 oveq12d 
 |-  ( ( ( A e. CC /\ ( abs ` A ) < 1 ) /\ m e. NN ) -> ( ( ( n e. NN |-> ( ( -u ( _i x. A ) ^ n ) / n ) ) ` m ) - ( ( n e. NN |-> ( ( ( _i x. A ) ^ n ) / n ) ) ` m ) ) = ( ( ( -u ( _i x. A ) ^ m ) / m ) - ( ( ( _i x. A ) ^ m ) / m ) ) )
79 77 78 eqtr4d 
 |-  ( ( ( A e. CC /\ ( abs ` A ) < 1 ) /\ m e. NN ) -> ( ( n e. NN |-> ( ( ( -u ( _i x. A ) ^ n ) / n ) - ( ( ( _i x. A ) ^ n ) / n ) ) ) ` m ) = ( ( ( n e. NN |-> ( ( -u ( _i x. A ) ^ n ) / n ) ) ` m ) - ( ( n e. NN |-> ( ( ( _i x. A ) ^ n ) / n ) ) ` m ) ) )
80 69 70 79 syl2an 
 |-  ( ( ( ( A e. CC /\ ( abs ` A ) < 1 ) /\ k e. NN ) /\ m e. ( 1 ... k ) ) -> ( ( n e. NN |-> ( ( ( -u ( _i x. A ) ^ n ) / n ) - ( ( ( _i x. A ) ^ n ) / n ) ) ) ` m ) = ( ( ( n e. NN |-> ( ( -u ( _i x. A ) ^ n ) / n ) ) ` m ) - ( ( n e. NN |-> ( ( ( _i x. A ) ^ n ) / n ) ) ` m ) ) )
81 68 71 72 80 sersub 
 |-  ( ( ( A e. CC /\ ( abs ` A ) < 1 ) /\ k e. NN ) -> ( seq 1 ( + , ( n e. NN |-> ( ( ( -u ( _i x. A ) ^ n ) / n ) - ( ( ( _i x. A ) ^ n ) / n ) ) ) ) ` k ) = ( ( seq 1 ( + , ( n e. NN |-> ( ( -u ( _i x. A ) ^ n ) / n ) ) ) ` k ) - ( seq 1 ( + , ( n e. NN |-> ( ( ( _i x. A ) ^ n ) / n ) ) ) ` k ) ) )
82 2 3 31 33 36 54 66 81 climsub 
 |-  ( ( A e. CC /\ ( abs ` A ) < 1 ) -> seq 1 ( + , ( n e. NN |-> ( ( ( -u ( _i x. A ) ^ n ) / n ) - ( ( ( _i x. A ) ^ n ) / n ) ) ) ) ~~> ( -u ( log ` ( 1 + ( _i x. A ) ) ) - -u ( log ` ( 1 - ( _i x. A ) ) ) ) )
83 addcl 
 |-  ( ( 1 e. CC /\ ( _i x. A ) e. CC ) -> ( 1 + ( _i x. A ) ) e. CC )
84 26 9 83 sylancr 
 |-  ( ( A e. CC /\ ( abs ` A ) < 1 ) -> ( 1 + ( _i x. A ) ) e. CC )
85 bndatandm 
 |-  ( ( A e. CC /\ ( abs ` A ) < 1 ) -> A e. dom arctan )
86 atandm2 
 |-  ( A e. dom arctan <-> ( A e. CC /\ ( 1 - ( _i x. A ) ) =/= 0 /\ ( 1 + ( _i x. A ) ) =/= 0 ) )
87 85 86 sylib 
 |-  ( ( A e. CC /\ ( abs ` A ) < 1 ) -> ( A e. CC /\ ( 1 - ( _i x. A ) ) =/= 0 /\ ( 1 + ( _i x. A ) ) =/= 0 ) )
88 87 simp3d 
 |-  ( ( A e. CC /\ ( abs ` A ) < 1 ) -> ( 1 + ( _i x. A ) ) =/= 0 )
89 84 88 logcld 
 |-  ( ( A e. CC /\ ( abs ` A ) < 1 ) -> ( log ` ( 1 + ( _i x. A ) ) ) e. CC )
90 subcl 
 |-  ( ( 1 e. CC /\ ( _i x. A ) e. CC ) -> ( 1 - ( _i x. A ) ) e. CC )
91 26 9 90 sylancr 
 |-  ( ( A e. CC /\ ( abs ` A ) < 1 ) -> ( 1 - ( _i x. A ) ) e. CC )
92 87 simp2d 
 |-  ( ( A e. CC /\ ( abs ` A ) < 1 ) -> ( 1 - ( _i x. A ) ) =/= 0 )
93 91 92 logcld 
 |-  ( ( A e. CC /\ ( abs ` A ) < 1 ) -> ( log ` ( 1 - ( _i x. A ) ) ) e. CC )
94 89 93 neg2subd 
 |-  ( ( A e. CC /\ ( abs ` A ) < 1 ) -> ( -u ( log ` ( 1 + ( _i x. A ) ) ) - -u ( log ` ( 1 - ( _i x. A ) ) ) ) = ( ( log ` ( 1 - ( _i x. A ) ) ) - ( log ` ( 1 + ( _i x. A ) ) ) ) )
95 82 94 breqtrd 
 |-  ( ( A e. CC /\ ( abs ` A ) < 1 ) -> seq 1 ( + , ( n e. NN |-> ( ( ( -u ( _i x. A ) ^ n ) / n ) - ( ( ( _i x. A ) ^ n ) / n ) ) ) ) ~~> ( ( log ` ( 1 - ( _i x. A ) ) ) - ( log ` ( 1 + ( _i x. A ) ) ) ) )
96 51 63 subcld 
 |-  ( ( ( A e. CC /\ ( abs ` A ) < 1 ) /\ m e. NN ) -> ( ( ( -u ( _i x. A ) ^ m ) / m ) - ( ( ( _i x. A ) ^ m ) / m ) ) e. CC )
97 77 96 eqeltrd 
 |-  ( ( ( A e. CC /\ ( abs ` A ) < 1 ) /\ m e. NN ) -> ( ( n e. NN |-> ( ( ( -u ( _i x. A ) ^ n ) / n ) - ( ( ( _i x. A ) ^ n ) / n ) ) ) ` m ) e. CC )
98 4 a1i 
 |-  ( ( ( A e. CC /\ ( abs ` A ) < 1 ) /\ m e. NN ) -> _i e. CC )
99 negicn 
 |-  -u _i e. CC
100 44 adantl 
 |-  ( ( ( A e. CC /\ ( abs ` A ) < 1 ) /\ m e. NN ) -> m e. NN0 )
101 expcl 
 |-  ( ( -u _i e. CC /\ m e. NN0 ) -> ( -u _i ^ m ) e. CC )
102 99 100 101 sylancr 
 |-  ( ( ( A e. CC /\ ( abs ` A ) < 1 ) /\ m e. NN ) -> ( -u _i ^ m ) e. CC )
103 expcl 
 |-  ( ( _i e. CC /\ m e. NN0 ) -> ( _i ^ m ) e. CC )
104 4 100 103 sylancr 
 |-  ( ( ( A e. CC /\ ( abs ` A ) < 1 ) /\ m e. NN ) -> ( _i ^ m ) e. CC )
105 102 104 subcld 
 |-  ( ( ( A e. CC /\ ( abs ` A ) < 1 ) /\ m e. NN ) -> ( ( -u _i ^ m ) - ( _i ^ m ) ) e. CC )
106 2cnd 
 |-  ( ( ( A e. CC /\ ( abs ` A ) < 1 ) /\ m e. NN ) -> 2 e. CC )
107 2ne0 
 |-  2 =/= 0
108 107 a1i 
 |-  ( ( ( A e. CC /\ ( abs ` A ) < 1 ) /\ m e. NN ) -> 2 =/= 0 )
109 98 105 106 108 div23d 
 |-  ( ( ( A e. CC /\ ( abs ` A ) < 1 ) /\ m e. NN ) -> ( ( _i x. ( ( -u _i ^ m ) - ( _i ^ m ) ) ) / 2 ) = ( ( _i / 2 ) x. ( ( -u _i ^ m ) - ( _i ^ m ) ) ) )
110 109 oveq1d 
 |-  ( ( ( A e. CC /\ ( abs ` A ) < 1 ) /\ m e. NN ) -> ( ( ( _i x. ( ( -u _i ^ m ) - ( _i ^ m ) ) ) / 2 ) x. ( ( A ^ m ) / m ) ) = ( ( ( _i / 2 ) x. ( ( -u _i ^ m ) - ( _i ^ m ) ) ) x. ( ( A ^ m ) / m ) ) )
111 6 adantr 
 |-  ( ( ( A e. CC /\ ( abs ` A ) < 1 ) /\ m e. NN ) -> ( _i / 2 ) e. CC )
112 expcl 
 |-  ( ( A e. CC /\ m e. NN0 ) -> ( A ^ m ) e. CC )
113 7 44 112 syl2an 
 |-  ( ( ( A e. CC /\ ( abs ` A ) < 1 ) /\ m e. NN ) -> ( A ^ m ) e. CC )
114 113 48 50 divcld 
 |-  ( ( ( A e. CC /\ ( abs ` A ) < 1 ) /\ m e. NN ) -> ( ( A ^ m ) / m ) e. CC )
115 111 105 114 mulassd 
 |-  ( ( ( A e. CC /\ ( abs ` A ) < 1 ) /\ m e. NN ) -> ( ( ( _i / 2 ) x. ( ( -u _i ^ m ) - ( _i ^ m ) ) ) x. ( ( A ^ m ) / m ) ) = ( ( _i / 2 ) x. ( ( ( -u _i ^ m ) - ( _i ^ m ) ) x. ( ( A ^ m ) / m ) ) ) )
116 102 104 113 subdird 
 |-  ( ( ( A e. CC /\ ( abs ` A ) < 1 ) /\ m e. NN ) -> ( ( ( -u _i ^ m ) - ( _i ^ m ) ) x. ( A ^ m ) ) = ( ( ( -u _i ^ m ) x. ( A ^ m ) ) - ( ( _i ^ m ) x. ( A ^ m ) ) ) )
117 7 adantr 
 |-  ( ( ( A e. CC /\ ( abs ` A ) < 1 ) /\ m e. NN ) -> A e. CC )
118 mulneg1 
 |-  ( ( _i e. CC /\ A e. CC ) -> ( -u _i x. A ) = -u ( _i x. A ) )
119 4 117 118 sylancr 
 |-  ( ( ( A e. CC /\ ( abs ` A ) < 1 ) /\ m e. NN ) -> ( -u _i x. A ) = -u ( _i x. A ) )
120 119 oveq1d 
 |-  ( ( ( A e. CC /\ ( abs ` A ) < 1 ) /\ m e. NN ) -> ( ( -u _i x. A ) ^ m ) = ( -u ( _i x. A ) ^ m ) )
121 99 a1i 
 |-  ( ( ( A e. CC /\ ( abs ` A ) < 1 ) /\ m e. NN ) -> -u _i e. CC )
122 121 117 100 mulexpd 
 |-  ( ( ( A e. CC /\ ( abs ` A ) < 1 ) /\ m e. NN ) -> ( ( -u _i x. A ) ^ m ) = ( ( -u _i ^ m ) x. ( A ^ m ) ) )
123 120 122 eqtr3d 
 |-  ( ( ( A e. CC /\ ( abs ` A ) < 1 ) /\ m e. NN ) -> ( -u ( _i x. A ) ^ m ) = ( ( -u _i ^ m ) x. ( A ^ m ) ) )
124 98 117 100 mulexpd 
 |-  ( ( ( A e. CC /\ ( abs ` A ) < 1 ) /\ m e. NN ) -> ( ( _i x. A ) ^ m ) = ( ( _i ^ m ) x. ( A ^ m ) ) )
125 123 124 oveq12d 
 |-  ( ( ( A e. CC /\ ( abs ` A ) < 1 ) /\ m e. NN ) -> ( ( -u ( _i x. A ) ^ m ) - ( ( _i x. A ) ^ m ) ) = ( ( ( -u _i ^ m ) x. ( A ^ m ) ) - ( ( _i ^ m ) x. ( A ^ m ) ) ) )
126 116 125 eqtr4d 
 |-  ( ( ( A e. CC /\ ( abs ` A ) < 1 ) /\ m e. NN ) -> ( ( ( -u _i ^ m ) - ( _i ^ m ) ) x. ( A ^ m ) ) = ( ( -u ( _i x. A ) ^ m ) - ( ( _i x. A ) ^ m ) ) )
127 126 oveq1d 
 |-  ( ( ( A e. CC /\ ( abs ` A ) < 1 ) /\ m e. NN ) -> ( ( ( ( -u _i ^ m ) - ( _i ^ m ) ) x. ( A ^ m ) ) / m ) = ( ( ( -u ( _i x. A ) ^ m ) - ( ( _i x. A ) ^ m ) ) / m ) )
128 105 113 48 50 divassd 
 |-  ( ( ( A e. CC /\ ( abs ` A ) < 1 ) /\ m e. NN ) -> ( ( ( ( -u _i ^ m ) - ( _i ^ m ) ) x. ( A ^ m ) ) / m ) = ( ( ( -u _i ^ m ) - ( _i ^ m ) ) x. ( ( A ^ m ) / m ) ) )
129 46 62 48 50 divsubdird 
 |-  ( ( ( A e. CC /\ ( abs ` A ) < 1 ) /\ m e. NN ) -> ( ( ( -u ( _i x. A ) ^ m ) - ( ( _i x. A ) ^ m ) ) / m ) = ( ( ( -u ( _i x. A ) ^ m ) / m ) - ( ( ( _i x. A ) ^ m ) / m ) ) )
130 127 128 129 3eqtr3d 
 |-  ( ( ( A e. CC /\ ( abs ` A ) < 1 ) /\ m e. NN ) -> ( ( ( -u _i ^ m ) - ( _i ^ m ) ) x. ( ( A ^ m ) / m ) ) = ( ( ( -u ( _i x. A ) ^ m ) / m ) - ( ( ( _i x. A ) ^ m ) / m ) ) )
131 130 oveq2d 
 |-  ( ( ( A e. CC /\ ( abs ` A ) < 1 ) /\ m e. NN ) -> ( ( _i / 2 ) x. ( ( ( -u _i ^ m ) - ( _i ^ m ) ) x. ( ( A ^ m ) / m ) ) ) = ( ( _i / 2 ) x. ( ( ( -u ( _i x. A ) ^ m ) / m ) - ( ( ( _i x. A ) ^ m ) / m ) ) ) )
132 110 115 131 3eqtrd 
 |-  ( ( ( A e. CC /\ ( abs ` A ) < 1 ) /\ m e. NN ) -> ( ( ( _i x. ( ( -u _i ^ m ) - ( _i ^ m ) ) ) / 2 ) x. ( ( A ^ m ) / m ) ) = ( ( _i / 2 ) x. ( ( ( -u ( _i x. A ) ^ m ) / m ) - ( ( ( _i x. A ) ^ m ) / m ) ) ) )
133 oveq2 
 |-  ( n = m -> ( -u _i ^ n ) = ( -u _i ^ m ) )
134 oveq2 
 |-  ( n = m -> ( _i ^ n ) = ( _i ^ m ) )
135 133 134 oveq12d 
 |-  ( n = m -> ( ( -u _i ^ n ) - ( _i ^ n ) ) = ( ( -u _i ^ m ) - ( _i ^ m ) ) )
136 135 oveq2d 
 |-  ( n = m -> ( _i x. ( ( -u _i ^ n ) - ( _i ^ n ) ) ) = ( _i x. ( ( -u _i ^ m ) - ( _i ^ m ) ) ) )
137 136 oveq1d 
 |-  ( n = m -> ( ( _i x. ( ( -u _i ^ n ) - ( _i ^ n ) ) ) / 2 ) = ( ( _i x. ( ( -u _i ^ m ) - ( _i ^ m ) ) ) / 2 ) )
138 oveq2 
 |-  ( n = m -> ( A ^ n ) = ( A ^ m ) )
139 138 38 oveq12d 
 |-  ( n = m -> ( ( A ^ n ) / n ) = ( ( A ^ m ) / m ) )
140 137 139 oveq12d 
 |-  ( n = m -> ( ( ( _i x. ( ( -u _i ^ n ) - ( _i ^ n ) ) ) / 2 ) x. ( ( A ^ n ) / n ) ) = ( ( ( _i x. ( ( -u _i ^ m ) - ( _i ^ m ) ) ) / 2 ) x. ( ( A ^ m ) / m ) ) )
141 ovex 
 |-  ( ( ( _i x. ( ( -u _i ^ m ) - ( _i ^ m ) ) ) / 2 ) x. ( ( A ^ m ) / m ) ) e. _V
142 140 1 141 fvmpt 
 |-  ( m e. NN -> ( F ` m ) = ( ( ( _i x. ( ( -u _i ^ m ) - ( _i ^ m ) ) ) / 2 ) x. ( ( A ^ m ) / m ) ) )
143 142 adantl 
 |-  ( ( ( A e. CC /\ ( abs ` A ) < 1 ) /\ m e. NN ) -> ( F ` m ) = ( ( ( _i x. ( ( -u _i ^ m ) - ( _i ^ m ) ) ) / 2 ) x. ( ( A ^ m ) / m ) ) )
144 77 oveq2d 
 |-  ( ( ( A e. CC /\ ( abs ` A ) < 1 ) /\ m e. NN ) -> ( ( _i / 2 ) x. ( ( n e. NN |-> ( ( ( -u ( _i x. A ) ^ n ) / n ) - ( ( ( _i x. A ) ^ n ) / n ) ) ) ` m ) ) = ( ( _i / 2 ) x. ( ( ( -u ( _i x. A ) ^ m ) / m ) - ( ( ( _i x. A ) ^ m ) / m ) ) ) )
145 132 143 144 3eqtr4d 
 |-  ( ( ( A e. CC /\ ( abs ` A ) < 1 ) /\ m e. NN ) -> ( F ` m ) = ( ( _i / 2 ) x. ( ( n e. NN |-> ( ( ( -u ( _i x. A ) ^ n ) / n ) - ( ( ( _i x. A ) ^ n ) / n ) ) ) ` m ) ) )
146 2 3 6 95 97 145 isermulc2 
 |-  ( ( A e. CC /\ ( abs ` A ) < 1 ) -> seq 1 ( + , F ) ~~> ( ( _i / 2 ) x. ( ( log ` ( 1 - ( _i x. A ) ) ) - ( log ` ( 1 + ( _i x. A ) ) ) ) ) )
147 atanval 
 |-  ( A e. dom arctan -> ( arctan ` A ) = ( ( _i / 2 ) x. ( ( log ` ( 1 - ( _i x. A ) ) ) - ( log ` ( 1 + ( _i x. A ) ) ) ) ) )
148 85 147 syl 
 |-  ( ( A e. CC /\ ( abs ` A ) < 1 ) -> ( arctan ` A ) = ( ( _i / 2 ) x. ( ( log ` ( 1 - ( _i x. A ) ) ) - ( log ` ( 1 + ( _i x. A ) ) ) ) ) )
149 146 148 breqtrrd 
 |-  ( ( A e. CC /\ ( abs ` A ) < 1 ) -> seq 1 ( + , F ) ~~> ( arctan ` A ) )