This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem cosarg0d

Description: The cosine of the argument is zero precisely on the imaginary axis. (Contributed by David Moews, 28-Feb-2017)

Ref Expression
Hypotheses cosargd.1 
|- ( ph -> X e. CC )
cosargd.2 
|- ( ph -> X =/= 0 )
Assertion cosarg0d 
|- ( ph -> ( ( cos ` ( Im ` ( log ` X ) ) ) = 0 <-> ( Re ` X ) = 0 ) )

Proof

Step Hyp Ref Expression
1 cosargd.1 
 |-  ( ph -> X e. CC )
2 cosargd.2 
 |-  ( ph -> X =/= 0 )
3 1 2 cosargd 
 |-  ( ph -> ( cos ` ( Im ` ( log ` X ) ) ) = ( ( Re ` X ) / ( abs ` X ) ) )
4 3 eqeq1d 
 |-  ( ph -> ( ( cos ` ( Im ` ( log ` X ) ) ) = 0 <-> ( ( Re ` X ) / ( abs ` X ) ) = 0 ) )
5 1 recld 
 |-  ( ph -> ( Re ` X ) e. RR )
6 5 recnd 
 |-  ( ph -> ( Re ` X ) e. CC )
7 1 abscld 
 |-  ( ph -> ( abs ` X ) e. RR )
8 7 recnd 
 |-  ( ph -> ( abs ` X ) e. CC )
9 1 2 absne0d 
 |-  ( ph -> ( abs ` X ) =/= 0 )
10 6 8 9 diveq0ad 
 |-  ( ph -> ( ( ( Re ` X ) / ( abs ` X ) ) = 0 <-> ( Re ` X ) = 0 ) )
11 4 10 bitrd 
 |-  ( ph -> ( ( cos ` ( Im ` ( log ` X ) ) ) = 0 <-> ( Re ` X ) = 0 ) )