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