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		inelr	$⊢ \neg i \in ℝ$
2		ax-icn	$⊢ i \in ℂ$
3	2	a1i	$⊢ ((R \in ℝ \land R \neq 0) \land i R \in ℝ) \to i \in ℂ$
4		simpll	$⊢ ((R \in ℝ \land R \neq 0) \land i R \in ℝ) \to R \in ℝ$
5	4	recnd	$⊢ ((R \in ℝ \land R \neq 0) \land i R \in ℝ) \to R \in ℂ$
6		simplr	$⊢ ((R \in ℝ \land R \neq 0) \land i R \in ℝ) \to R \neq 0$
7	3 5 6	divcan4d	$⊢ ((R \in ℝ \land R \neq 0) \land i R \in ℝ) \to \frac{i R}{R} = i$
8		simpr	$⊢ ((R \in ℝ \land R \neq 0) \land i R \in ℝ) \to i R \in ℝ$
9	8 4 6	redivcld	$⊢ ((R \in ℝ \land R \neq 0) \land i R \in ℝ) \to \frac{i R}{R} \in ℝ$
10	7 9	eqeltrrd	$⊢ ((R \in ℝ \land R \neq 0) \land i R \in ℝ) \to i \in ℝ$
11	10	ex	$⊢ (R \in ℝ \land R \neq 0) \to (i R \in ℝ \to i \in ℝ)$
12	1 11	mtoi	$⊢ (R \in ℝ \land R \neq 0) \to \neg i R \in ℝ$
13	12	ex	$⊢ R \in ℝ \to (R \neq 0 \to \neg i R \in ℝ)$
14	13	necon4ad	$⊢ R \in ℝ \to (i R \in ℝ \to R = 0)$
15		oveq2	$⊢ R = 0 \to i R = i \cdot 0$
16		it0e0	$⊢ i \cdot 0 = 0$
17		0re	$⊢ 0 \in ℝ$
18	16 17	eqeltri	$⊢ i \cdot 0 \in ℝ$
19	15 18	eqeltrdi	$⊢ R = 0 \to i R \in ℝ$
20	14 19	impbid1	$⊢ R \in ℝ \to (i R \in ℝ \leftrightarrow R = 0)$

Metamath Proof Explorer