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

Metamath Proof Explorer

Theorem absimnre

Description: The absolute value of the imaginary part of a non-real, complex number, is strictly positive. (Contributed by Glauco Siliprandi, 5-Feb-2022)

Ref Expression
Hypotheses absimnre.1 ⊢ ( 𝜑 → 𝐴 ∈ ℂ )
absimnre.2 ⊢ ( 𝜑 → ¬ 𝐴 ∈ ℝ )
Assertion absimnre ( 𝜑 → ( abs ‘ ( ℑ ‘ 𝐴 ) ) ∈ ℝ+ )

Proof

Step Hyp Ref Expression
1 absimnre.1 ⊢ ( 𝜑 → 𝐴 ∈ ℂ )
2 absimnre.2 ⊢ ( 𝜑 → ¬ 𝐴 ∈ ℝ )
3 1 imcld ⊢ ( 𝜑 → ( ℑ ‘ 𝐴 ) ∈ ℝ )
4 3 recnd ⊢ ( 𝜑 → ( ℑ ‘ 𝐴 ) ∈ ℂ )
5 reim0b ⊢ ( 𝐴 ∈ ℂ → ( 𝐴 ∈ ℝ ↔ ( ℑ ‘ 𝐴 ) = 0 ) )
6 1 5 syl ⊢ ( 𝜑 → ( 𝐴 ∈ ℝ ↔ ( ℑ ‘ 𝐴 ) = 0 ) )
7 2 6 mtbid ⊢ ( 𝜑 → ¬ ( ℑ ‘ 𝐴 ) = 0 )
8 7 neqned ⊢ ( 𝜑 → ( ℑ ‘ 𝐴 ) ≠ 0 )
9 4 8 absrpcld ⊢ ( 𝜑 → ( abs ‘ ( ℑ ‘ 𝐴 ) ) ∈ ℝ+ )