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=n01nA2n+12n+1
Assertion atantayl3 AA<1seq0+FarctanA

Proof

Step Hyp Ref Expression
1 atantayl3.1 F=n01nA2n+12n+1
2 2nn0 20
3 simpr AA<1n0n0
4 nn0mulcl 20n02n0
5 2 3 4 sylancr AA<1n02n0
6 5 nn0cnd AA<1n02n
7 ax-1cn 1
8 pncan 2n12n+1-1=2n
9 6 7 8 sylancl AA<1n02n+1-1=2n
10 9 oveq1d AA<1n02n+1-12=2n2
11 nn0cn n0n
12 11 adantl AA<1n0n
13 2cnd AA<1n02
14 2ne0 20
15 14 a1i AA<1n020
16 12 13 15 divcan3d AA<1n02n2=n
17 10 16 eqtr2d AA<1n0n=2n+1-12
18 17 oveq2d AA<1n01n=12n+1-12
19 18 oveq1d AA<1n01nA2n+12n+1=12n+1-12A2n+12n+1
20 19 mpteq2dva AA<1n01nA2n+12n+1=n012n+1-12A2n+12n+1
21 1 20 eqtrid AA<1F=n012n+1-12A2n+12n+1
22 21 seqeq3d AA<1seq0+F=seq0+n012n+1-12A2n+12n+1
23 eqid kif2k01k12Akk=kif2k01k12Akk
24 23 atantayl2 AA<1seq1+kif2k01k12AkkarctanA
25 neg1cn 1
26 expcl 1n01n
27 25 3 26 sylancr AA<1n01n
28 simpll AA<1n0A
29 peano2nn0 2n02n+10
30 5 29 syl AA<1n02n+10
31 28 30 expcld AA<1n0A2n+1
32 nn0p1nn 2n02n+1
33 5 32 syl AA<1n02n+1
34 33 nncnd AA<1n02n+1
35 33 nnne0d AA<1n02n+10
36 31 34 35 divcld AA<1n0A2n+12n+1
37 27 36 mulcld AA<1n01nA2n+12n+1
38 19 37 eqeltrrd AA<1n012n+1-12A2n+12n+1
39 oveq1 k=2n+1k1=2n+1-1
40 39 oveq1d k=2n+1k12=2n+1-12
41 40 oveq2d k=2n+11k12=12n+1-12
42 oveq2 k=2n+1Ak=A2n+1
43 id k=2n+1k=2n+1
44 42 43 oveq12d k=2n+1Akk=A2n+12n+1
45 41 44 oveq12d k=2n+11k12Akk=12n+1-12A2n+12n+1
46 38 45 iserodd AA<1seq0+n012n+1-12A2n+12n+1arctanAseq1+kif2k01k12AkkarctanA
47 24 46 mpbird AA<1seq0+n012n+1-12A2n+12n+1arctanA
48 22 47 eqbrtrd AA<1seq0+FarctanA