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 ⊢ ( 𝜑 → 𝑋 ∈ ℂ )
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 ) )