Description: The Taylor series for arctan ( A ) . (Contributed by Mario Carneiro, 7-Apr-2015)
Ref | Expression | ||
---|---|---|---|
Hypothesis | atantayl3.1 | |
|
Assertion | atantayl3 | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | atantayl3.1 | |
|
2 | 2nn0 | |
|
3 | simpr | |
|
4 | nn0mulcl | |
|
5 | 2 3 4 | sylancr | |
6 | 5 | nn0cnd | |
7 | ax-1cn | |
|
8 | pncan | |
|
9 | 6 7 8 | sylancl | |
10 | 9 | oveq1d | |
11 | nn0cn | |
|
12 | 11 | adantl | |
13 | 2cnd | |
|
14 | 2ne0 | |
|
15 | 14 | a1i | |
16 | 12 13 15 | divcan3d | |
17 | 10 16 | eqtr2d | |
18 | 17 | oveq2d | |
19 | 18 | oveq1d | |
20 | 19 | mpteq2dva | |
21 | 1 20 | eqtrid | |
22 | 21 | seqeq3d | |
23 | eqid | |
|
24 | 23 | atantayl2 | |
25 | neg1cn | |
|
26 | expcl | |
|
27 | 25 3 26 | sylancr | |
28 | simpll | |
|
29 | peano2nn0 | |
|
30 | 5 29 | syl | |
31 | 28 30 | expcld | |
32 | nn0p1nn | |
|
33 | 5 32 | syl | |
34 | 33 | nncnd | |
35 | 33 | nnne0d | |
36 | 31 34 35 | divcld | |
37 | 27 36 | mulcld | |
38 | 19 37 | eqeltrrd | |
39 | oveq1 | |
|
40 | 39 | oveq1d | |
41 | 40 | oveq2d | |
42 | oveq2 | |
|
43 | id | |
|
44 | 42 43 | oveq12d | |
45 | 41 44 | oveq12d | |
46 | 38 45 | iserodd | |
47 | 24 46 | mpbird | |
48 | 22 47 | eqbrtrd | |