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	$$⊢\phi \to A\in ℂ$$
	absimnre.2	$$⊢\phi \to \neg A\in ℝ$$
Assertion	absimnre	$$⊢\phi \to \left|\Im \left(A\right)\right|\in {ℝ}^{+}$$

Proof

Step	Hyp	Ref	Expression
1		absimnre.1	$$⊢\phi \to A\in ℂ$$
2		absimnre.2	$$⊢\phi \to \neg A\in ℝ$$
3	1	imcld	$$⊢\phi \to \Im \left(A\right)\in ℝ$$
4	3	recnd	$$⊢\phi \to \Im \left(A\right)\in ℂ$$
5		reim0b	$$⊢A\in ℂ\to \left(A\in ℝ\leftrightarrow \Im \left(A\right)=0\right)$$
6	1 5	syl	$$⊢\phi \to \left(A\in ℝ\leftrightarrow \Im \left(A\right)=0\right)$$
7	2 6	mtbid	$$⊢\phi \to \neg \Im \left(A\right)=0$$
8	7	neqned	$$⊢\phi \to \Im \left(A\right)\ne 0$$
9	4 8	absrpcld	$$⊢\phi \to \left|\Im \left(A\right)\right|\in {ℝ}^{+}$$