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 \left(R\mathrm{i}\in ℝ\leftrightarrow R=0\right)$$

Proof

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