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	⊢ ( 𝜑 → 𝑋 ∈ ℂ )
	cosargd.2	⊢ ( 𝜑 → 𝑋 ≠ 0 )
Assertion	cosarg0d	⊢ ( 𝜑 → ( ( cos ‘ ( ℑ ‘ ( log ‘ 𝑋 ) ) ) = 0 ↔ ( ℜ ‘ 𝑋 ) = 0 ) )

Proof

Step	Hyp	Ref	Expression
1		cosargd.1	⊢ ( 𝜑 → 𝑋 ∈ ℂ )
2		cosargd.2	⊢ ( 𝜑 → 𝑋 ≠ 0 )
3	1 2	cosargd	⊢ ( 𝜑 → ( cos ‘ ( ℑ ‘ ( log ‘ 𝑋 ) ) ) = ( ( ℜ ‘ 𝑋 ) / ( abs ‘ 𝑋 ) ) )
4	3	eqeq1d	⊢ ( 𝜑 → ( ( cos ‘ ( ℑ ‘ ( log ‘ 𝑋 ) ) ) = 0 ↔ ( ( ℜ ‘ 𝑋 ) / ( abs ‘ 𝑋 ) ) = 0 ) )
5	1	recld	⊢ ( 𝜑 → ( ℜ ‘ 𝑋 ) ∈ ℝ )
6	5	recnd	⊢ ( 𝜑 → ( ℜ ‘ 𝑋 ) ∈ ℂ )
7	1	abscld	⊢ ( 𝜑 → ( abs ‘ 𝑋 ) ∈ ℝ )
8	7	recnd	⊢ ( 𝜑 → ( abs ‘ 𝑋 ) ∈ ℂ )
9	1 2	absne0d	⊢ ( 𝜑 → ( abs ‘ 𝑋 ) ≠ 0 )
10	6 8 9	diveq0ad	⊢ ( 𝜑 → ( ( ( ℜ ‘ 𝑋 ) / ( abs ‘ 𝑋 ) ) = 0 ↔ ( ℜ ‘ 𝑋 ) = 0 ) )
11	4 10	bitrd	⊢ ( 𝜑 → ( ( cos ‘ ( ℑ ‘ ( log ‘ 𝑋 ) ) ) = 0 ↔ ( ℜ ‘ 𝑋 ) = 0 ) )