Metamath Proof Explorer

Theorem atantayl3

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

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

Proof

Step Hyp Ref Expression
1 atantayl3.1 
 |-  F = ( n e. NN0 |-> ( ( -u 1 ^ n ) x. ( ( A ^ ( ( 2 x. n ) + 1 ) ) / ( ( 2 x. n ) + 1 ) ) ) )
2 2nn0 
 |-  2 e. NN0
3 simpr 
 |-  ( ( ( A e. CC /\ ( abs ` A ) < 1 ) /\ n e. NN0 ) -> n e. NN0 )
4 nn0mulcl 
 |-  ( ( 2 e. NN0 /\ n e. NN0 ) -> ( 2 x. n ) e. NN0 )
5 2 3 4 sylancr 
 |-  ( ( ( A e. CC /\ ( abs ` A ) < 1 ) /\ n e. NN0 ) -> ( 2 x. n ) e. NN0 )
6 5 nn0cnd 
 |-  ( ( ( A e. CC /\ ( abs ` A ) < 1 ) /\ n e. NN0 ) -> ( 2 x. n ) e. CC )
7 ax-1cn 
 |-  1 e. CC
8 pncan 
 |-  ( ( ( 2 x. n ) e. CC /\ 1 e. CC ) -> ( ( ( 2 x. n ) + 1 ) - 1 ) = ( 2 x. n ) )
9 6 7 8 sylancl 
 |-  ( ( ( A e. CC /\ ( abs ` A ) < 1 ) /\ n e. NN0 ) -> ( ( ( 2 x. n ) + 1 ) - 1 ) = ( 2 x. n ) )
10 9 oveq1d 
 |-  ( ( ( A e. CC /\ ( abs ` A ) < 1 ) /\ n e. NN0 ) -> ( ( ( ( 2 x. n ) + 1 ) - 1 ) / 2 ) = ( ( 2 x. n ) / 2 ) )
11 nn0cn 
 |-  ( n e. NN0 -> n e. CC )
12 11 adantl 
 |-  ( ( ( A e. CC /\ ( abs ` A ) < 1 ) /\ n e. NN0 ) -> n e. CC )
13 2cnd 
 |-  ( ( ( A e. CC /\ ( abs ` A ) < 1 ) /\ n e. NN0 ) -> 2 e. CC )
14 2ne0 
 |-  2 =/= 0
15 14 a1i 
 |-  ( ( ( A e. CC /\ ( abs ` A ) < 1 ) /\ n e. NN0 ) -> 2 =/= 0 )
16 12 13 15 divcan3d 
 |-  ( ( ( A e. CC /\ ( abs ` A ) < 1 ) /\ n e. NN0 ) -> ( ( 2 x. n ) / 2 ) = n )
17 10 16 eqtr2d 
 |-  ( ( ( A e. CC /\ ( abs ` A ) < 1 ) /\ n e. NN0 ) -> n = ( ( ( ( 2 x. n ) + 1 ) - 1 ) / 2 ) )
18 17 oveq2d 
 |-  ( ( ( A e. CC /\ ( abs ` A ) < 1 ) /\ n e. NN0 ) -> ( -u 1 ^ n ) = ( -u 1 ^ ( ( ( ( 2 x. n ) + 1 ) - 1 ) / 2 ) ) )
19 18 oveq1d 
 |-  ( ( ( A e. CC /\ ( abs ` A ) < 1 ) /\ n e. NN0 ) -> ( ( -u 1 ^ n ) x. ( ( A ^ ( ( 2 x. n ) + 1 ) ) / ( ( 2 x. n ) + 1 ) ) ) = ( ( -u 1 ^ ( ( ( ( 2 x. n ) + 1 ) - 1 ) / 2 ) ) x. ( ( A ^ ( ( 2 x. n ) + 1 ) ) / ( ( 2 x. n ) + 1 ) ) ) )
20 19 mpteq2dva 
 |-  ( ( A e. CC /\ ( abs ` A ) < 1 ) -> ( n e. NN0 |-> ( ( -u 1 ^ n ) x. ( ( A ^ ( ( 2 x. n ) + 1 ) ) / ( ( 2 x. n ) + 1 ) ) ) ) = ( n e. NN0 |-> ( ( -u 1 ^ ( ( ( ( 2 x. n ) + 1 ) - 1 ) / 2 ) ) x. ( ( A ^ ( ( 2 x. n ) + 1 ) ) / ( ( 2 x. n ) + 1 ) ) ) ) )
21 1 20 syl5eq 
 |-  ( ( A e. CC /\ ( abs ` A ) < 1 ) -> F = ( n e. NN0 |-> ( ( -u 1 ^ ( ( ( ( 2 x. n ) + 1 ) - 1 ) / 2 ) ) x. ( ( A ^ ( ( 2 x. n ) + 1 ) ) / ( ( 2 x. n ) + 1 ) ) ) ) )
22 21 seqeq3d 
 |-  ( ( A e. CC /\ ( abs ` A ) < 1 ) -> seq 0 ( + , F ) = seq 0 ( + , ( n e. NN0 |-> ( ( -u 1 ^ ( ( ( ( 2 x. n ) + 1 ) - 1 ) / 2 ) ) x. ( ( A ^ ( ( 2 x. n ) + 1 ) ) / ( ( 2 x. n ) + 1 ) ) ) ) ) )
23 eqid 
 |-  ( k e. NN |-> if ( 2 || k , 0 , ( ( -u 1 ^ ( ( k - 1 ) / 2 ) ) x. ( ( A ^ k ) / k ) ) ) ) = ( k e. NN |-> if ( 2 || k , 0 , ( ( -u 1 ^ ( ( k - 1 ) / 2 ) ) x. ( ( A ^ k ) / k ) ) ) )
24 23 atantayl2 
 |-  ( ( A e. CC /\ ( abs ` A ) < 1 ) -> seq 1 ( + , ( k e. NN |-> if ( 2 || k , 0 , ( ( -u 1 ^ ( ( k - 1 ) / 2 ) ) x. ( ( A ^ k ) / k ) ) ) ) ) ~~> ( arctan ` A ) )
25 neg1cn 
 |-  -u 1 e. CC
26 expcl 
 |-  ( ( -u 1 e. CC /\ n e. NN0 ) -> ( -u 1 ^ n ) e. CC )
27 25 3 26 sylancr 
 |-  ( ( ( A e. CC /\ ( abs ` A ) < 1 ) /\ n e. NN0 ) -> ( -u 1 ^ n ) e. CC )
28 simpll 
 |-  ( ( ( A e. CC /\ ( abs ` A ) < 1 ) /\ n e. NN0 ) -> A e. CC )
29 peano2nn0 
 |-  ( ( 2 x. n ) e. NN0 -> ( ( 2 x. n ) + 1 ) e. NN0 )
30 5 29 syl 
 |-  ( ( ( A e. CC /\ ( abs ` A ) < 1 ) /\ n e. NN0 ) -> ( ( 2 x. n ) + 1 ) e. NN0 )
31 28 30 expcld 
 |-  ( ( ( A e. CC /\ ( abs ` A ) < 1 ) /\ n e. NN0 ) -> ( A ^ ( ( 2 x. n ) + 1 ) ) e. CC )
32 nn0p1nn 
 |-  ( ( 2 x. n ) e. NN0 -> ( ( 2 x. n ) + 1 ) e. NN )
33 5 32 syl 
 |-  ( ( ( A e. CC /\ ( abs ` A ) < 1 ) /\ n e. NN0 ) -> ( ( 2 x. n ) + 1 ) e. NN )
34 33 nncnd 
 |-  ( ( ( A e. CC /\ ( abs ` A ) < 1 ) /\ n e. NN0 ) -> ( ( 2 x. n ) + 1 ) e. CC )
35 33 nnne0d 
 |-  ( ( ( A e. CC /\ ( abs ` A ) < 1 ) /\ n e. NN0 ) -> ( ( 2 x. n ) + 1 ) =/= 0 )
36 31 34 35 divcld 
 |-  ( ( ( A e. CC /\ ( abs ` A ) < 1 ) /\ n e. NN0 ) -> ( ( A ^ ( ( 2 x. n ) + 1 ) ) / ( ( 2 x. n ) + 1 ) ) e. CC )
37 27 36 mulcld 
 |-  ( ( ( A e. CC /\ ( abs ` A ) < 1 ) /\ n e. NN0 ) -> ( ( -u 1 ^ n ) x. ( ( A ^ ( ( 2 x. n ) + 1 ) ) / ( ( 2 x. n ) + 1 ) ) ) e. CC )
38 19 37 eqeltrrd 
 |-  ( ( ( A e. CC /\ ( abs ` A ) < 1 ) /\ n e. NN0 ) -> ( ( -u 1 ^ ( ( ( ( 2 x. n ) + 1 ) - 1 ) / 2 ) ) x. ( ( A ^ ( ( 2 x. n ) + 1 ) ) / ( ( 2 x. n ) + 1 ) ) ) e. CC )
39 oveq1 
 |-  ( k = ( ( 2 x. n ) + 1 ) -> ( k - 1 ) = ( ( ( 2 x. n ) + 1 ) - 1 ) )
40 39 oveq1d 
 |-  ( k = ( ( 2 x. n ) + 1 ) -> ( ( k - 1 ) / 2 ) = ( ( ( ( 2 x. n ) + 1 ) - 1 ) / 2 ) )
41 40 oveq2d 
 |-  ( k = ( ( 2 x. n ) + 1 ) -> ( -u 1 ^ ( ( k - 1 ) / 2 ) ) = ( -u 1 ^ ( ( ( ( 2 x. n ) + 1 ) - 1 ) / 2 ) ) )
42 oveq2 
 |-  ( k = ( ( 2 x. n ) + 1 ) -> ( A ^ k ) = ( A ^ ( ( 2 x. n ) + 1 ) ) )
43 id 
 |-  ( k = ( ( 2 x. n ) + 1 ) -> k = ( ( 2 x. n ) + 1 ) )
44 42 43 oveq12d 
 |-  ( k = ( ( 2 x. n ) + 1 ) -> ( ( A ^ k ) / k ) = ( ( A ^ ( ( 2 x. n ) + 1 ) ) / ( ( 2 x. n ) + 1 ) ) )
45 41 44 oveq12d 
 |-  ( k = ( ( 2 x. n ) + 1 ) -> ( ( -u 1 ^ ( ( k - 1 ) / 2 ) ) x. ( ( A ^ k ) / k ) ) = ( ( -u 1 ^ ( ( ( ( 2 x. n ) + 1 ) - 1 ) / 2 ) ) x. ( ( A ^ ( ( 2 x. n ) + 1 ) ) / ( ( 2 x. n ) + 1 ) ) ) )
46 38 45 iserodd 
 |-  ( ( A e. CC /\ ( abs ` A ) < 1 ) -> ( seq 0 ( + , ( n e. NN0 |-> ( ( -u 1 ^ ( ( ( ( 2 x. n ) + 1 ) - 1 ) / 2 ) ) x. ( ( A ^ ( ( 2 x. n ) + 1 ) ) / ( ( 2 x. n ) + 1 ) ) ) ) ) ~~> ( arctan ` A ) <-> seq 1 ( + , ( k e. NN |-> if ( 2 || k , 0 , ( ( -u 1 ^ ( ( k - 1 ) / 2 ) ) x. ( ( A ^ k ) / k ) ) ) ) ) ~~> ( arctan ` A ) ) )
47 24 46 mpbird 
 |-  ( ( A e. CC /\ ( abs ` A ) < 1 ) -> seq 0 ( + , ( n e. NN0 |-> ( ( -u 1 ^ ( ( ( ( 2 x. n ) + 1 ) - 1 ) / 2 ) ) x. ( ( A ^ ( ( 2 x. n ) + 1 ) ) / ( ( 2 x. n ) + 1 ) ) ) ) ) ~~> ( arctan ` A ) )
48 22 47 eqbrtrd 
 |-  ( ( A e. CC /\ ( abs ` A ) < 1 ) -> seq 0 ( + , F ) ~~> ( arctan ` A ) )