Metamath Proof Explorer

Theorem coseq0

Description: A complex number whose cosine is zero. (Contributed by Glauco Siliprandi, 11-Dec-2019)

Ref Expression
Assertion coseq0 
|- ( A e. CC -> ( ( cos ` A ) = 0 <-> ( ( A / _pi ) + ( 1 / 2 ) ) e. ZZ ) )

Proof

Step Hyp Ref Expression
1 picn 
 |-  _pi e. CC
2 1 a1i 
 |-  ( A e. CC -> _pi e. CC )
3 2 halfcld 
 |-  ( A e. CC -> ( _pi / 2 ) e. CC )
4 id 
 |-  ( A e. CC -> A e. CC )
5 3 4 addcld 
 |-  ( A e. CC -> ( ( _pi / 2 ) + A ) e. CC )
6 sineq0 
 |-  ( ( ( _pi / 2 ) + A ) e. CC -> ( ( sin ` ( ( _pi / 2 ) + A ) ) = 0 <-> ( ( ( _pi / 2 ) + A ) / _pi ) e. ZZ ) )
7 5 6 syl 
 |-  ( A e. CC -> ( ( sin ` ( ( _pi / 2 ) + A ) ) = 0 <-> ( ( ( _pi / 2 ) + A ) / _pi ) e. ZZ ) )
8 sinhalfpip 
 |-  ( A e. CC -> ( sin ` ( ( _pi / 2 ) + A ) ) = ( cos ` A ) )
9 8 eqeq1d 
 |-  ( A e. CC -> ( ( sin ` ( ( _pi / 2 ) + A ) ) = 0 <-> ( cos ` A ) = 0 ) )
10 pire 
 |-  _pi e. RR
11 pipos 
 |-  0 < _pi
12 10 11 gt0ne0ii 
 |-  _pi =/= 0
13 12 a1i 
 |-  ( A e. CC -> _pi =/= 0 )
14 3 4 2 13 divdird 
 |-  ( A e. CC -> ( ( ( _pi / 2 ) + A ) / _pi ) = ( ( ( _pi / 2 ) / _pi ) + ( A / _pi ) ) )
15 2cnd 
 |-  ( A e. CC -> 2 e. CC )
16 2ne0 
 |-  2 =/= 0
17 16 a1i 
 |-  ( A e. CC -> 2 =/= 0 )
18 2 15 2 17 13 divdiv32d 
 |-  ( A e. CC -> ( ( _pi / 2 ) / _pi ) = ( ( _pi / _pi ) / 2 ) )
19 2 13 dividd 
 |-  ( A e. CC -> ( _pi / _pi ) = 1 )
20 19 oveq1d 
 |-  ( A e. CC -> ( ( _pi / _pi ) / 2 ) = ( 1 / 2 ) )
21 18 20 eqtrd 
 |-  ( A e. CC -> ( ( _pi / 2 ) / _pi ) = ( 1 / 2 ) )
22 21 oveq1d 
 |-  ( A e. CC -> ( ( ( _pi / 2 ) / _pi ) + ( A / _pi ) ) = ( ( 1 / 2 ) + ( A / _pi ) ) )
23 1cnd 
 |-  ( A e. CC -> 1 e. CC )
24 23 halfcld 
 |-  ( A e. CC -> ( 1 / 2 ) e. CC )
25 4 2 13 divcld 
 |-  ( A e. CC -> ( A / _pi ) e. CC )
26 24 25 addcomd 
 |-  ( A e. CC -> ( ( 1 / 2 ) + ( A / _pi ) ) = ( ( A / _pi ) + ( 1 / 2 ) ) )
27 14 22 26 3eqtrd 
 |-  ( A e. CC -> ( ( ( _pi / 2 ) + A ) / _pi ) = ( ( A / _pi ) + ( 1 / 2 ) ) )
28 27 eleq1d 
 |-  ( A e. CC -> ( ( ( ( _pi / 2 ) + A ) / _pi ) e. ZZ <-> ( ( A / _pi ) + ( 1 / 2 ) ) e. ZZ ) )
29 7 9 28 3bitr3d 
 |-  ( A e. CC -> ( ( cos ` A ) = 0 <-> ( ( A / _pi ) + ( 1 / 2 ) ) e. ZZ ) )