Step |
Hyp |
Ref |
Expression |
1 |
|
2cn |
|- 2 e. CC |
2 |
|
2ne0 |
|- 2 =/= 0 |
3 |
|
divcan2 |
|- ( ( A e. CC /\ 2 e. CC /\ 2 =/= 0 ) -> ( 2 x. ( A / 2 ) ) = A ) |
4 |
1 2 3
|
mp3an23 |
|- ( A e. CC -> ( 2 x. ( A / 2 ) ) = A ) |
5 |
4
|
fveq2d |
|- ( A e. CC -> ( cos ` ( 2 x. ( A / 2 ) ) ) = ( cos ` A ) ) |
6 |
|
halfcl |
|- ( A e. CC -> ( A / 2 ) e. CC ) |
7 |
|
cos2tsin |
|- ( ( A / 2 ) e. CC -> ( cos ` ( 2 x. ( A / 2 ) ) ) = ( 1 - ( 2 x. ( ( sin ` ( A / 2 ) ) ^ 2 ) ) ) ) |
8 |
6 7
|
syl |
|- ( A e. CC -> ( cos ` ( 2 x. ( A / 2 ) ) ) = ( 1 - ( 2 x. ( ( sin ` ( A / 2 ) ) ^ 2 ) ) ) ) |
9 |
5 8
|
eqtr3d |
|- ( A e. CC -> ( cos ` A ) = ( 1 - ( 2 x. ( ( sin ` ( A / 2 ) ) ^ 2 ) ) ) ) |
10 |
9
|
eqeq1d |
|- ( A e. CC -> ( ( cos ` A ) = 1 <-> ( 1 - ( 2 x. ( ( sin ` ( A / 2 ) ) ^ 2 ) ) ) = 1 ) ) |
11 |
6
|
sincld |
|- ( A e. CC -> ( sin ` ( A / 2 ) ) e. CC ) |
12 |
11
|
sqcld |
|- ( A e. CC -> ( ( sin ` ( A / 2 ) ) ^ 2 ) e. CC ) |
13 |
|
mulcl |
|- ( ( 2 e. CC /\ ( ( sin ` ( A / 2 ) ) ^ 2 ) e. CC ) -> ( 2 x. ( ( sin ` ( A / 2 ) ) ^ 2 ) ) e. CC ) |
14 |
1 12 13
|
sylancr |
|- ( A e. CC -> ( 2 x. ( ( sin ` ( A / 2 ) ) ^ 2 ) ) e. CC ) |
15 |
|
ax-1cn |
|- 1 e. CC |
16 |
|
subsub23 |
|- ( ( 1 e. CC /\ ( 2 x. ( ( sin ` ( A / 2 ) ) ^ 2 ) ) e. CC /\ 1 e. CC ) -> ( ( 1 - ( 2 x. ( ( sin ` ( A / 2 ) ) ^ 2 ) ) ) = 1 <-> ( 1 - 1 ) = ( 2 x. ( ( sin ` ( A / 2 ) ) ^ 2 ) ) ) ) |
17 |
15 15 16
|
mp3an13 |
|- ( ( 2 x. ( ( sin ` ( A / 2 ) ) ^ 2 ) ) e. CC -> ( ( 1 - ( 2 x. ( ( sin ` ( A / 2 ) ) ^ 2 ) ) ) = 1 <-> ( 1 - 1 ) = ( 2 x. ( ( sin ` ( A / 2 ) ) ^ 2 ) ) ) ) |
18 |
14 17
|
syl |
|- ( A e. CC -> ( ( 1 - ( 2 x. ( ( sin ` ( A / 2 ) ) ^ 2 ) ) ) = 1 <-> ( 1 - 1 ) = ( 2 x. ( ( sin ` ( A / 2 ) ) ^ 2 ) ) ) ) |
19 |
|
eqcom |
|- ( ( 1 - 1 ) = ( 2 x. ( ( sin ` ( A / 2 ) ) ^ 2 ) ) <-> ( 2 x. ( ( sin ` ( A / 2 ) ) ^ 2 ) ) = ( 1 - 1 ) ) |
20 |
|
1m1e0 |
|- ( 1 - 1 ) = 0 |
21 |
20
|
eqeq2i |
|- ( ( 2 x. ( ( sin ` ( A / 2 ) ) ^ 2 ) ) = ( 1 - 1 ) <-> ( 2 x. ( ( sin ` ( A / 2 ) ) ^ 2 ) ) = 0 ) |
22 |
19 21
|
bitri |
|- ( ( 1 - 1 ) = ( 2 x. ( ( sin ` ( A / 2 ) ) ^ 2 ) ) <-> ( 2 x. ( ( sin ` ( A / 2 ) ) ^ 2 ) ) = 0 ) |
23 |
18 22
|
bitrdi |
|- ( A e. CC -> ( ( 1 - ( 2 x. ( ( sin ` ( A / 2 ) ) ^ 2 ) ) ) = 1 <-> ( 2 x. ( ( sin ` ( A / 2 ) ) ^ 2 ) ) = 0 ) ) |
24 |
10 23
|
bitrd |
|- ( A e. CC -> ( ( cos ` A ) = 1 <-> ( 2 x. ( ( sin ` ( A / 2 ) ) ^ 2 ) ) = 0 ) ) |
25 |
|
mul0or |
|- ( ( 2 e. CC /\ ( ( sin ` ( A / 2 ) ) ^ 2 ) e. CC ) -> ( ( 2 x. ( ( sin ` ( A / 2 ) ) ^ 2 ) ) = 0 <-> ( 2 = 0 \/ ( ( sin ` ( A / 2 ) ) ^ 2 ) = 0 ) ) ) |
26 |
1 12 25
|
sylancr |
|- ( A e. CC -> ( ( 2 x. ( ( sin ` ( A / 2 ) ) ^ 2 ) ) = 0 <-> ( 2 = 0 \/ ( ( sin ` ( A / 2 ) ) ^ 2 ) = 0 ) ) ) |
27 |
2
|
neii |
|- -. 2 = 0 |
28 |
|
biorf |
|- ( -. 2 = 0 -> ( ( ( sin ` ( A / 2 ) ) ^ 2 ) = 0 <-> ( 2 = 0 \/ ( ( sin ` ( A / 2 ) ) ^ 2 ) = 0 ) ) ) |
29 |
27 28
|
ax-mp |
|- ( ( ( sin ` ( A / 2 ) ) ^ 2 ) = 0 <-> ( 2 = 0 \/ ( ( sin ` ( A / 2 ) ) ^ 2 ) = 0 ) ) |
30 |
26 29
|
bitr4di |
|- ( A e. CC -> ( ( 2 x. ( ( sin ` ( A / 2 ) ) ^ 2 ) ) = 0 <-> ( ( sin ` ( A / 2 ) ) ^ 2 ) = 0 ) ) |
31 |
|
sqeq0 |
|- ( ( sin ` ( A / 2 ) ) e. CC -> ( ( ( sin ` ( A / 2 ) ) ^ 2 ) = 0 <-> ( sin ` ( A / 2 ) ) = 0 ) ) |
32 |
11 31
|
syl |
|- ( A e. CC -> ( ( ( sin ` ( A / 2 ) ) ^ 2 ) = 0 <-> ( sin ` ( A / 2 ) ) = 0 ) ) |
33 |
24 30 32
|
3bitrd |
|- ( A e. CC -> ( ( cos ` A ) = 1 <-> ( sin ` ( A / 2 ) ) = 0 ) ) |
34 |
|
sineq0 |
|- ( ( A / 2 ) e. CC -> ( ( sin ` ( A / 2 ) ) = 0 <-> ( ( A / 2 ) / _pi ) e. ZZ ) ) |
35 |
6 34
|
syl |
|- ( A e. CC -> ( ( sin ` ( A / 2 ) ) = 0 <-> ( ( A / 2 ) / _pi ) e. ZZ ) ) |
36 |
1 2
|
pm3.2i |
|- ( 2 e. CC /\ 2 =/= 0 ) |
37 |
|
picn |
|- _pi e. CC |
38 |
|
pire |
|- _pi e. RR |
39 |
|
pipos |
|- 0 < _pi |
40 |
38 39
|
gt0ne0ii |
|- _pi =/= 0 |
41 |
37 40
|
pm3.2i |
|- ( _pi e. CC /\ _pi =/= 0 ) |
42 |
|
divdiv1 |
|- ( ( A e. CC /\ ( 2 e. CC /\ 2 =/= 0 ) /\ ( _pi e. CC /\ _pi =/= 0 ) ) -> ( ( A / 2 ) / _pi ) = ( A / ( 2 x. _pi ) ) ) |
43 |
36 41 42
|
mp3an23 |
|- ( A e. CC -> ( ( A / 2 ) / _pi ) = ( A / ( 2 x. _pi ) ) ) |
44 |
43
|
eleq1d |
|- ( A e. CC -> ( ( ( A / 2 ) / _pi ) e. ZZ <-> ( A / ( 2 x. _pi ) ) e. ZZ ) ) |
45 |
33 35 44
|
3bitrd |
|- ( A e. CC -> ( ( cos ` A ) = 1 <-> ( A / ( 2 x. _pi ) ) e. ZZ ) ) |