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

Metamath Proof Explorer

Theorem itrere

Description: _i times a real is real iff the real is zero. (Contributed by SN, 25-Apr-2025)

		Ref	Expression
	Assertion	itrere	$⊢ R \in ℝ \to (i R \in ℝ \leftrightarrow R = 0)$

Step	Hyp	Ref	Expression
1		rimul	$⊢ (R \in ℝ \land i R \in ℝ) \to R = 0$
2	1	ex	$⊢ R \in ℝ \to (i R \in ℝ \to R = 0)$
3		oveq2	$⊢ R = 0 \to i R = i \cdot 0$
4		it0e0	$⊢ i \cdot 0 = 0$
5		0re	$⊢ 0 \in ℝ$
6	4 5	eqeltri	$⊢ i \cdot 0 \in ℝ$
7	3 6	eqeltrdi	$⊢ R = 0 \to i R \in ℝ$
8	2 7	impbid1	$⊢ R \in ℝ \to (i R \in ℝ \leftrightarrow R = 0)$