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 ) )