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