reixi

		Ref	Expression
	Assertion	reixi	$⊢ i i = 0 -_{ℝ} 1$

Step	Hyp	Ref	Expression
1		ax-i2m1	$⊢ i i + 1 = 0$
2		1re	$⊢ 1 \in ℝ$
3		renegid2	$⊢ 1 \in ℝ \to (0 -_{ℝ} 1) + 1 = 0$
4	2 3	ax-mp	$⊢ (0 -_{ℝ} 1) + 1 = 0$
5	1 4	eqtr4i	$⊢ i i + 1 = (0 -_{ℝ} 1) + 1$
6		ax-icn	$⊢ i \in ℂ$
7	6 6	mulcli	$⊢ i i \in ℂ$
8	7	a1i	$⊢ ⊤ \to i i \in ℂ$
9		rernegcl	$⊢ 1 \in ℝ \to 0 -_{ℝ} 1 \in ℝ$
10	9	recnd	$⊢ 1 \in ℝ \to 0 -_{ℝ} 1 \in ℂ$
11	2 10	mp1i	$⊢ ⊤ \to 0 -_{ℝ} 1 \in ℂ$
12		1cnd	$⊢ ⊤ \to 1 \in ℂ$
13	8 11 12	sn-addcan2d	$⊢ ⊤ \to (i i + 1 = (0 -_{ℝ} 1) + 1 \leftrightarrow i i = 0 -_{ℝ} 1)$
14	5 13	mpbii	$⊢ ⊤ \to i i = 0 -_{ℝ} 1$
15	14	mptru	$⊢ i i = 0 -_{ℝ} 1$

Metamath Proof Explorer