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 ‘ ( ℑ ‘ 𝐴 ) ) ∈ ℝ+ )