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 · π ) ) ∈ ℤ ) )