sn-itrere

Description: _i times a real is real iff the real is zero. (Contributed by SN, 27-Jun-2024)

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

Proof

Step	Hyp	Ref	Expression
1		ax-rrecex	$⊢ (R \in ℝ \land R \neq 0) \to \exists x \in ℝ R x = 1$
2		sn-inelr	$⊢ \neg i \in ℝ$
3		ax-icn	$⊢ i \in ℂ$
4	3	a1i	$⊢ (((R \in ℝ \land R \neq 0) \land (x \in ℝ \land R x = 1)) \land i R \in ℝ) \to i \in ℂ$
5		simplll	$⊢ (((R \in ℝ \land R \neq 0) \land (x \in ℝ \land R x = 1)) \land i R \in ℝ) \to R \in ℝ$
6	5	recnd	$⊢ (((R \in ℝ \land R \neq 0) \land (x \in ℝ \land R x = 1)) \land i R \in ℝ) \to R \in ℂ$
7		simplrl	$⊢ (((R \in ℝ \land R \neq 0) \land (x \in ℝ \land R x = 1)) \land i R \in ℝ) \to x \in ℝ$
8	7	recnd	$⊢ (((R \in ℝ \land R \neq 0) \land (x \in ℝ \land R x = 1)) \land i R \in ℝ) \to x \in ℂ$
9	4 6 8	mulassd	$⊢ (((R \in ℝ \land R \neq 0) \land (x \in ℝ \land R x = 1)) \land i R \in ℝ) \to i R x = i R x$
10		simplrr	$⊢ (((R \in ℝ \land R \neq 0) \land (x \in ℝ \land R x = 1)) \land i R \in ℝ) \to R x = 1$
11	10	oveq2d	$⊢ (((R \in ℝ \land R \neq 0) \land (x \in ℝ \land R x = 1)) \land i R \in ℝ) \to i R x = i \cdot 1$
12		sn-it1ei	$⊢ i \cdot 1 = i$
13	12	a1i	$⊢ (((R \in ℝ \land R \neq 0) \land (x \in ℝ \land R x = 1)) \land i R \in ℝ) \to i \cdot 1 = i$
14	9 11 13	3eqtrd	$⊢ (((R \in ℝ \land R \neq 0) \land (x \in ℝ \land R x = 1)) \land i R \in ℝ) \to i R x = i$
15		simpr	$⊢ (((R \in ℝ \land R \neq 0) \land (x \in ℝ \land R x = 1)) \land i R \in ℝ) \to i R \in ℝ$
16	15 7	remulcld	$⊢ (((R \in ℝ \land R \neq 0) \land (x \in ℝ \land R x = 1)) \land i R \in ℝ) \to i R x \in ℝ$
17	14 16	eqeltrrd	$⊢ (((R \in ℝ \land R \neq 0) \land (x \in ℝ \land R x = 1)) \land i R \in ℝ) \to i \in ℝ$
18	17	ex	$⊢ ((R \in ℝ \land R \neq 0) \land (x \in ℝ \land R x = 1)) \to (i R \in ℝ \to i \in ℝ)$
19	2 18	mtoi	$⊢ ((R \in ℝ \land R \neq 0) \land (x \in ℝ \land R x = 1)) \to \neg i R \in ℝ$
20	1 19	rexlimddv	$⊢ (R \in ℝ \land R \neq 0) \to \neg i R \in ℝ$
21	20	ex	$⊢ R \in ℝ \to (R \neq 0 \to \neg i R \in ℝ)$
22	21	necon4ad	$⊢ R \in ℝ \to (i R \in ℝ \to R = 0)$
23		oveq2	$⊢ R = 0 \to i R = i \cdot 0$
24		sn-it0e0	$⊢ i \cdot 0 = 0$
25		0re	$⊢ 0 \in ℝ$
26	24 25	eqeltri	$⊢ i \cdot 0 \in ℝ$
27	23 26	eqeltrdi	$⊢ R = 0 \to i R \in ℝ$
28	22 27	impbid1	$⊢ R \in ℝ \to (i R \in ℝ \leftrightarrow R = 0)$

Metamath Proof Explorer

Theorem sn-itrere

Proof