Description: The absolute value of the cosine of an integer multiple of _pi is 1. (Contributed by NM, 19-Aug-2008)
Ref | Expression | ||
---|---|---|---|
Assertion | coskpi | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | zcn | |
|
2 | 2cn | |
|
3 | picn | |
|
4 | mul12 | |
|
5 | 2 3 4 | mp3an23 | |
6 | 1 5 | syl | |
7 | 6 | fveq2d | |
8 | cos2kpi | |
|
9 | zre | |
|
10 | pire | |
|
11 | remulcl | |
|
12 | 9 10 11 | sylancl | |
13 | 12 | recnd | |
14 | cos2t | |
|
15 | 13 14 | syl | |
16 | 7 8 15 | 3eqtr3rd | |
17 | 12 | recoscld | |
18 | 17 | recnd | |
19 | 18 | sqcld | |
20 | mulcl | |
|
21 | 2 19 20 | sylancr | |
22 | ax-1cn | |
|
23 | subadd | |
|
24 | 22 22 23 | mp3an23 | |
25 | 21 24 | syl | |
26 | 16 25 | mpbid | |
27 | 2t1e2 | |
|
28 | df-2 | |
|
29 | 27 28 | eqtr2i | |
30 | 26 29 | eqtr3di | |
31 | 2cnne0 | |
|
32 | mulcan | |
|
33 | 22 31 32 | mp3an23 | |
34 | 19 33 | syl | |
35 | 30 34 | mpbid | |
36 | sq1 | |
|
37 | 35 36 | eqtr4di | |
38 | 1re | |
|
39 | sqabs | |
|
40 | 17 38 39 | sylancl | |
41 | 37 40 | mpbid | |
42 | abs1 | |
|
43 | 41 42 | eqtrdi | |