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