Metamath Proof Explorer


Theorem coskpi

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 KcosKπ=1

Proof

Step Hyp Ref Expression
1 zcn KK
2 2cn 2
3 picn π
4 mul12 K2πK2π=2Kπ
5 2 3 4 mp3an23 KK2π=2Kπ
6 1 5 syl KK2π=2Kπ
7 6 fveq2d KcosK2π=cos2Kπ
8 cos2kpi KcosK2π=1
9 zre KK
10 pire π
11 remulcl KπKπ
12 9 10 11 sylancl KKπ
13 12 recnd KKπ
14 cos2t Kπcos2Kπ=2cosKπ21
15 13 14 syl Kcos2Kπ=2cosKπ21
16 7 8 15 3eqtr3rd K2cosKπ21=1
17 12 recoscld KcosKπ
18 17 recnd KcosKπ
19 18 sqcld KcosKπ2
20 mulcl 2cosKπ22cosKπ2
21 2 19 20 sylancr K2cosKπ2
22 ax-1cn 1
23 subadd 2cosKπ2112cosKπ21=11+1=2cosKπ2
24 22 22 23 mp3an23 2cosKπ22cosKπ21=11+1=2cosKπ2
25 21 24 syl K2cosKπ21=11+1=2cosKπ2
26 16 25 mpbid K1+1=2cosKπ2
27 2t1e2 21=2
28 df-2 2=1+1
29 27 28 eqtr2i 1+1=21
30 26 29 eqtr3di K2cosKπ2=21
31 2cnne0 220
32 mulcan cosKπ212202cosKπ2=21cosKπ2=1
33 22 31 32 mp3an23 cosKπ22cosKπ2=21cosKπ2=1
34 19 33 syl K2cosKπ2=21cosKπ2=1
35 30 34 mpbid KcosKπ2=1
36 sq1 12=1
37 35 36 eqtr4di KcosKπ2=12
38 1re 1
39 sqabs cosKπ1cosKπ2=12cosKπ=1
40 17 38 39 sylancl KcosKπ2=12cosKπ=1
41 37 40 mpbid KcosKπ=1
42 abs1 1=1
43 41 42 eqtrdi KcosKπ=1