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 e. CC -> ( ( cos ` A ) = 1 <-> ( A / ( 2 x. _pi ) ) e. ZZ ) )

Proof

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 ) )