retire

		Ref	Expression
	Assertion	retire	$⊢ R \in ℝ \to (R i \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		simplll	$⊢ (((R \in ℝ \land R \neq 0) \land (x \in ℝ \land R x = 1)) \land R i \in ℝ) \to R \in ℝ$
4		simplrl	$⊢ (((R \in ℝ \land R \neq 0) \land (x \in ℝ \land R x = 1)) \land R i \in ℝ) \to x \in ℝ$
5		simplrr	$⊢ (((R \in ℝ \land R \neq 0) \land (x \in ℝ \land R x = 1)) \land R i \in ℝ) \to R x = 1$
6	3 4 5	remulinvcom	$⊢ (((R \in ℝ \land R \neq 0) \land (x \in ℝ \land R x = 1)) \land R i \in ℝ) \to x R = 1$
7	6	oveq1d	$⊢ (((R \in ℝ \land R \neq 0) \land (x \in ℝ \land R x = 1)) \land R i \in ℝ) \to x R i = 1 i$
8	4	recnd	$⊢ (((R \in ℝ \land R \neq 0) \land (x \in ℝ \land R x = 1)) \land R i \in ℝ) \to x \in ℂ$
9	3	recnd	$⊢ (((R \in ℝ \land R \neq 0) \land (x \in ℝ \land R x = 1)) \land R i \in ℝ) \to R \in ℂ$
10		ax-icn	$⊢ i \in ℂ$
11	10	a1i	$⊢ (((R \in ℝ \land R \neq 0) \land (x \in ℝ \land R x = 1)) \land R i \in ℝ) \to i \in ℂ$
12	8 9 11	mulassd	$⊢ (((R \in ℝ \land R \neq 0) \land (x \in ℝ \land R x = 1)) \land R i \in ℝ) \to x R i = x R i$
13		sn-1ticom	$⊢ 1 i = i \cdot 1$
14		it1ei	$⊢ i \cdot 1 = i$
15	13 14	eqtri	$⊢ 1 i = i$
16	15	a1i	$⊢ (((R \in ℝ \land R \neq 0) \land (x \in ℝ \land R x = 1)) \land R i \in ℝ) \to 1 i = i$
17	7 12 16	3eqtr3d	$⊢ (((R \in ℝ \land R \neq 0) \land (x \in ℝ \land R x = 1)) \land R i \in ℝ) \to x R i = i$
18		simpr	$⊢ (((R \in ℝ \land R \neq 0) \land (x \in ℝ \land R x = 1)) \land R i \in ℝ) \to R i \in ℝ$
19	4 18	remulcld	$⊢ (((R \in ℝ \land R \neq 0) \land (x \in ℝ \land R x = 1)) \land R i \in ℝ) \to x R i \in ℝ$
20	17 19	eqeltrrd	$⊢ (((R \in ℝ \land R \neq 0) \land (x \in ℝ \land R x = 1)) \land R i \in ℝ) \to i \in ℝ$
21	20	ex	$⊢ ((R \in ℝ \land R \neq 0) \land (x \in ℝ \land R x = 1)) \to (R i \in ℝ \to i \in ℝ)$
22	2 21	mtoi	$⊢ ((R \in ℝ \land R \neq 0) \land (x \in ℝ \land R x = 1)) \to \neg R i \in ℝ$
23	1 22	rexlimddv	$⊢ (R \in ℝ \land R \neq 0) \to \neg R i \in ℝ$
24	23	ex	$⊢ R \in ℝ \to (R \neq 0 \to \neg R i \in ℝ)$
25	24	necon4ad	$⊢ R \in ℝ \to (R i \in ℝ \to R = 0)$
26		oveq1	$⊢ R = 0 \to R i = 0 \cdot i$
27		sn-0tie0	$⊢ 0 \cdot i = 0$
28		0re	$⊢ 0 \in ℝ$
29	27 28	eqeltri	$⊢ 0 \cdot i \in ℝ$
30	26 29	eqeltrdi	$⊢ R = 0 \to R i \in ℝ$
31	25 30	impbid1	$⊢ R \in ℝ \to (R i \in ℝ \leftrightarrow R = 0)$

Metamath Proof Explorer

Theorem retire

Proof