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 ( 𝐴 ∈ ℂ → ( ( cos ‘ 𝐴 ) = 1 ↔ ( 𝐴 / ( 2 · π ) ) ∈ ℤ ) )

Proof

Step Hyp Ref Expression
1 2cn ⊢ 2 ∈ ℂ
2 2ne0 ⊢ 2 ≠ 0
3 divcan2 ⊢ ( ( 𝐴 ∈ ℂ ∧ 2 ∈ ℂ ∧ 2 ≠ 0 ) → ( 2 · ( 𝐴 / 2 ) ) = 𝐴 )
4 1 2 3 mp3an23 ⊢ ( 𝐴 ∈ ℂ → ( 2 · ( 𝐴 / 2 ) ) = 𝐴 )
5 4 fveq2d ⊢ ( 𝐴 ∈ ℂ → ( cos ‘ ( 2 · ( 𝐴 / 2 ) ) ) = ( cos ‘ 𝐴 ) )
6 halfcl ⊢ ( 𝐴 ∈ ℂ → ( 𝐴 / 2 ) ∈ ℂ )
7 cos2tsin ⊢ ( ( 𝐴 / 2 ) ∈ ℂ → ( cos ‘ ( 2 · ( 𝐴 / 2 ) ) ) = ( 1 − ( 2 · ( ( sin ‘ ( 𝐴 / 2 ) ) ↑ 2 ) ) ) )
8 6 7 syl ⊢ ( 𝐴 ∈ ℂ → ( cos ‘ ( 2 · ( 𝐴 / 2 ) ) ) = ( 1 − ( 2 · ( ( sin ‘ ( 𝐴 / 2 ) ) ↑ 2 ) ) ) )
9 5 8 eqtr3d ⊢ ( 𝐴 ∈ ℂ → ( cos ‘ 𝐴 ) = ( 1 − ( 2 · ( ( sin ‘ ( 𝐴 / 2 ) ) ↑ 2 ) ) ) )
10 9 eqeq1d ⊢ ( 𝐴 ∈ ℂ → ( ( cos ‘ 𝐴 ) = 1 ↔ ( 1 − ( 2 · ( ( sin ‘ ( 𝐴 / 2 ) ) ↑ 2 ) ) ) = 1 ) )
11 6 sincld ⊢ ( 𝐴 ∈ ℂ → ( sin ‘ ( 𝐴 / 2 ) ) ∈ ℂ )
12 11 sqcld ⊢ ( 𝐴 ∈ ℂ → ( ( sin ‘ ( 𝐴 / 2 ) ) ↑ 2 ) ∈ ℂ )
13 mulcl ⊢ ( ( 2 ∈ ℂ ∧ ( ( sin ‘ ( 𝐴 / 2 ) ) ↑ 2 ) ∈ ℂ ) → ( 2 · ( ( sin ‘ ( 𝐴 / 2 ) ) ↑ 2 ) ) ∈ ℂ )
14 1 12 13 sylancr ⊢ ( 𝐴 ∈ ℂ → ( 2 · ( ( sin ‘ ( 𝐴 / 2 ) ) ↑ 2 ) ) ∈ ℂ )
15 ax-1cn ⊢ 1 ∈ ℂ
16 subsub23 ⊢ ( ( 1 ∈ ℂ ∧ ( 2 · ( ( sin ‘ ( 𝐴 / 2 ) ) ↑ 2 ) ) ∈ ℂ ∧ 1 ∈ ℂ ) → ( ( 1 − ( 2 · ( ( sin ‘ ( 𝐴 / 2 ) ) ↑ 2 ) ) ) = 1 ↔ ( 1 − 1 ) = ( 2 · ( ( sin ‘ ( 𝐴 / 2 ) ) ↑ 2 ) ) ) )
17 15 15 16 mp3an13 ⊢ ( ( 2 · ( ( sin ‘ ( 𝐴 / 2 ) ) ↑ 2 ) ) ∈ ℂ → ( ( 1 − ( 2 · ( ( sin ‘ ( 𝐴 / 2 ) ) ↑ 2 ) ) ) = 1 ↔ ( 1 − 1 ) = ( 2 · ( ( sin ‘ ( 𝐴 / 2 ) ) ↑ 2 ) ) ) )
18 14 17 syl ⊢ ( 𝐴 ∈ ℂ → ( ( 1 − ( 2 · ( ( sin ‘ ( 𝐴 / 2 ) ) ↑ 2 ) ) ) = 1 ↔ ( 1 − 1 ) = ( 2 · ( ( sin ‘ ( 𝐴 / 2 ) ) ↑ 2 ) ) ) )
19 eqcom ⊢ ( ( 1 − 1 ) = ( 2 · ( ( sin ‘ ( 𝐴 / 2 ) ) ↑ 2 ) ) ↔ ( 2 · ( ( sin ‘ ( 𝐴 / 2 ) ) ↑ 2 ) ) = ( 1 − 1 ) )
20 1m1e0 ⊢ ( 1 − 1 ) = 0
21 20 eqeq2i ⊢ ( ( 2 · ( ( sin ‘ ( 𝐴 / 2 ) ) ↑ 2 ) ) = ( 1 − 1 ) ↔ ( 2 · ( ( sin ‘ ( 𝐴 / 2 ) ) ↑ 2 ) ) = 0 )
22 19 21 bitri ⊢ ( ( 1 − 1 ) = ( 2 · ( ( sin ‘ ( 𝐴 / 2 ) ) ↑ 2 ) ) ↔ ( 2 · ( ( sin ‘ ( 𝐴 / 2 ) ) ↑ 2 ) ) = 0 )
23 18 22 bitrdi ⊢ ( 𝐴 ∈ ℂ → ( ( 1 − ( 2 · ( ( sin ‘ ( 𝐴 / 2 ) ) ↑ 2 ) ) ) = 1 ↔ ( 2 · ( ( sin ‘ ( 𝐴 / 2 ) ) ↑ 2 ) ) = 0 ) )
24 10 23 bitrd ⊢ ( 𝐴 ∈ ℂ → ( ( cos ‘ 𝐴 ) = 1 ↔ ( 2 · ( ( sin ‘ ( 𝐴 / 2 ) ) ↑ 2 ) ) = 0 ) )
25 mul0or ⊢ ( ( 2 ∈ ℂ ∧ ( ( sin ‘ ( 𝐴 / 2 ) ) ↑ 2 ) ∈ ℂ ) → ( ( 2 · ( ( sin ‘ ( 𝐴 / 2 ) ) ↑ 2 ) ) = 0 ↔ ( 2 = 0 ∨ ( ( sin ‘ ( 𝐴 / 2 ) ) ↑ 2 ) = 0 ) ) )
26 1 12 25 sylancr ⊢ ( 𝐴 ∈ ℂ → ( ( 2 · ( ( sin ‘ ( 𝐴 / 2 ) ) ↑ 2 ) ) = 0 ↔ ( 2 = 0 ∨ ( ( sin ‘ ( 𝐴 / 2 ) ) ↑ 2 ) = 0 ) ) )
27 2 neii ⊢ ¬ 2 = 0
28 biorf ⊢ ( ¬ 2 = 0 → ( ( ( sin ‘ ( 𝐴 / 2 ) ) ↑ 2 ) = 0 ↔ ( 2 = 0 ∨ ( ( sin ‘ ( 𝐴 / 2 ) ) ↑ 2 ) = 0 ) ) )
29 27 28 ax-mp ⊢ ( ( ( sin ‘ ( 𝐴 / 2 ) ) ↑ 2 ) = 0 ↔ ( 2 = 0 ∨ ( ( sin ‘ ( 𝐴 / 2 ) ) ↑ 2 ) = 0 ) )
30 26 29 bitr4di ⊢ ( 𝐴 ∈ ℂ → ( ( 2 · ( ( sin ‘ ( 𝐴 / 2 ) ) ↑ 2 ) ) = 0 ↔ ( ( sin ‘ ( 𝐴 / 2 ) ) ↑ 2 ) = 0 ) )
31 sqeq0 ⊢ ( ( sin ‘ ( 𝐴 / 2 ) ) ∈ ℂ → ( ( ( sin ‘ ( 𝐴 / 2 ) ) ↑ 2 ) = 0 ↔ ( sin ‘ ( 𝐴 / 2 ) ) = 0 ) )
32 11 31 syl ⊢ ( 𝐴 ∈ ℂ → ( ( ( sin ‘ ( 𝐴 / 2 ) ) ↑ 2 ) = 0 ↔ ( sin ‘ ( 𝐴 / 2 ) ) = 0 ) )
33 24 30 32 3bitrd ⊢ ( 𝐴 ∈ ℂ → ( ( cos ‘ 𝐴 ) = 1 ↔ ( sin ‘ ( 𝐴 / 2 ) ) = 0 ) )
34 sineq0 ⊢ ( ( 𝐴 / 2 ) ∈ ℂ → ( ( sin ‘ ( 𝐴 / 2 ) ) = 0 ↔ ( ( 𝐴 / 2 ) / π ) ∈ ℤ ) )
35 6 34 syl ⊢ ( 𝐴 ∈ ℂ → ( ( sin ‘ ( 𝐴 / 2 ) ) = 0 ↔ ( ( 𝐴 / 2 ) / π ) ∈ ℤ ) )
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 ⊢ ( ( 𝐴 ∈ ℂ ∧ ( 2 ∈ ℂ ∧ 2 ≠ 0 ) ∧ ( π ∈ ℂ ∧ π ≠ 0 ) ) → ( ( 𝐴 / 2 ) / π ) = ( 𝐴 / ( 2 · π ) ) )
43 36 41 42 mp3an23 ⊢ ( 𝐴 ∈ ℂ → ( ( 𝐴 / 2 ) / π ) = ( 𝐴 / ( 2 · π ) ) )
44 43 eleq1d ⊢ ( 𝐴 ∈ ℂ → ( ( ( 𝐴 / 2 ) / π ) ∈ ℤ ↔ ( 𝐴 / ( 2 · π ) ) ∈ ℤ ) )
45 33 35 44 3bitrd ⊢ ( 𝐴 ∈ ℂ → ( ( cos ‘ 𝐴 ) = 1 ↔ ( 𝐴 / ( 2 · π ) ) ∈ ℤ ) )