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