Metamath Proof Explorer

Theorem coseq1

Description: A complex number whose cosine is one is an integer multiple of 2 _pi . (Contributed by Mario Carneiro, 12-May-2014)

Ref Expression
Assertion coseq1 ⊢A∈ℂ→cos⁡A=1↔A2⁢π∈ℤ

Proof

Step Hyp Ref Expression
1 2cn ⊢2∈ℂ
2 2ne0 ⊢2≠0
3 divcan2 ⊢A∈ℂ∧2∈ℂ∧2≠0→2⁢A2=A
4 1 2 3 mp3an23 ⊢A∈ℂ→2⁢A2=A
5 4 fveq2d ⊢A∈ℂ→cos⁡2⁢A2=cos⁡A
6 halfcl ⊢A∈ℂ→A2∈ℂ
7 cos2tsin ⊢A2∈ℂ→cos⁡2⁢A2=1−2⁢sin⁡A22
8 6 7 syl ⊢A∈ℂ→cos⁡2⁢A2=1−2⁢sin⁡A22
9 5 8 eqtr3d ⊢A∈ℂ→cos⁡A=1−2⁢sin⁡A22
10 9 eqeq1d ⊢A∈ℂ→cos⁡A=1↔1−2⁢sin⁡A22=1
11 6 sincld ⊢A∈ℂ→sin⁡A2∈ℂ
12 11 sqcld ⊢A∈ℂ→sin⁡A22∈ℂ
13 mulcl ⊢2∈ℂ∧sin⁡A22∈ℂ→2⁢sin⁡A22∈ℂ
14 1 12 13 sylancr ⊢A∈ℂ→2⁢sin⁡A22∈ℂ
15 ax-1cn ⊢1∈ℂ
16 subsub23 ⊢1∈ℂ∧2⁢sin⁡A22∈ℂ∧1∈ℂ→1−2⁢sin⁡A22=1↔1−1=2⁢sin⁡A22
17 15 15 16 mp3an13 ⊢2⁢sin⁡A22∈ℂ→1−2⁢sin⁡A22=1↔1−1=2⁢sin⁡A22
18 14 17 syl ⊢A∈ℂ→1−2⁢sin⁡A22=1↔1−1=2⁢sin⁡A22
19 eqcom ⊢1−1=2⁢sin⁡A22↔2⁢sin⁡A22=1−1
20 1m1e0 ⊢1−1=0
21 20 eqeq2i ⊢2⁢sin⁡A22=1−1↔2⁢sin⁡A22=0
22 19 21 bitri ⊢1−1=2⁢sin⁡A22↔2⁢sin⁡A22=0
23 18 22 bitrdi ⊢A∈ℂ→1−2⁢sin⁡A22=1↔2⁢sin⁡A22=0
24 10 23 bitrd ⊢A∈ℂ→cos⁡A=1↔2⁢sin⁡A22=0
25 mul0or ⊢2∈ℂ∧sin⁡A22∈ℂ→2⁢sin⁡A22=0↔2=0∨sin⁡A22=0
26 1 12 25 sylancr ⊢A∈ℂ→2⁢sin⁡A22=0↔2=0∨sin⁡A22=0
27 2 neii ⊢¬2=0
28 biorf ⊢¬2=0→sin⁡A22=0↔2=0∨sin⁡A22=0
29 27 28 ax-mp ⊢sin⁡A22=0↔2=0∨sin⁡A22=0
30 26 29 bitr4di ⊢A∈ℂ→2⁢sin⁡A22=0↔sin⁡A22=0
31 sqeq0 ⊢sin⁡A2∈ℂ→sin⁡A22=0↔sin⁡A2=0
32 11 31 syl ⊢A∈ℂ→sin⁡A22=0↔sin⁡A2=0
33 24 30 32 3bitrd ⊢A∈ℂ→cos⁡A=1↔sin⁡A2=0
34 sineq0 ⊢A2∈ℂ→sin⁡A2=0↔A2π∈ℤ
35 6 34 syl ⊢A∈ℂ→sin⁡A2=0↔A2π∈ℤ
36 1 2 pm3.2i ⊢2∈ℂ∧2≠0
37 picn ⊢π∈ℂ
38 pire ⊢π∈ℝ
39 pipos ⊢0<π
40 38 39 gt0ne0ii ⊢π≠0
41 37 40 pm3.2i ⊢π∈ℂ∧π≠0
42 divdiv1 ⊢A∈ℂ∧2∈ℂ∧2≠0∧π∈ℂ∧π≠0→A2π=A2⁢π
43 36 41 42 mp3an23 ⊢A∈ℂ→A2π=A2⁢π
44 43 eleq1d ⊢A∈ℂ→A2π∈ℤ↔A2⁢π∈ℤ
45 33 35 44 3bitrd ⊢A∈ℂ→cos⁡A=1↔A2⁢π∈ℤ