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

Metamath Proof Explorer

Theorem retire

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

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

Step	Hyp	Ref	Expression
1		recn	$⊢ R \in ℝ \to R \in ℂ$
2		ax-icn	$⊢ i \in ℂ$
3	2	a1i	$⊢ R \in ℝ \to i \in ℂ$
4	1 3	mulcomd	$⊢ R \in ℝ \to R i = i R$
5	4	eleq1d	$⊢ R \in ℝ \to (R i \in ℝ \leftrightarrow i R \in ℝ)$
6		itrere	$⊢ R \in ℝ \to (i R \in ℝ \leftrightarrow R = 0)$
7	5 6	bitrd	$⊢ R \in ℝ \to (R i \in ℝ \leftrightarrow R = 0)$