ipiiie0

Description: The multiplicative inverse of _i (per i4 ) is also its additive inverse. (Contributed by SN, 30-Jun-2024)

		Ref	Expression
	Assertion	ipiiie0	$⊢ i + i i i = 0$

Step	Hyp	Ref	Expression
1		sn-it1ei	$⊢ i \cdot 1 = i$
2	1	eqcomi	$⊢ i = i \cdot 1$
3		reixi	$⊢ i i = 0 -_{ℝ} 1$
4	3	oveq2i	$⊢ i i i = i (0 -_{ℝ} 1)$
5	2 4	oveq12i	$⊢ i + i i i = i \cdot 1 + i (0 -_{ℝ} 1)$
6		ax-icn	$⊢ i \in ℂ$
7		ax-1cn	$⊢ 1 \in ℂ$
8		1re	$⊢ 1 \in ℝ$
9		rernegcl	$⊢ 1 \in ℝ \to 0 -_{ℝ} 1 \in ℝ$
10	8 9	ax-mp	$⊢ 0 -_{ℝ} 1 \in ℝ$
11	10	recni	$⊢ 0 -_{ℝ} 1 \in ℂ$
12	6 7 11	adddii	$⊢ i (1 + (0 -_{ℝ} 1)) = i \cdot 1 + i (0 -_{ℝ} 1)$
13		renegid	$⊢ 1 \in ℝ \to 1 + (0 -_{ℝ} 1) = 0$
14	8 13	ax-mp	$⊢ 1 + (0 -_{ℝ} 1) = 0$
15	14	oveq2i	$⊢ i (1 + (0 -_{ℝ} 1)) = i \cdot 0$
16		sn-it0e0	$⊢ i \cdot 0 = 0$
17	15 16	eqtri	$⊢ i (1 + (0 -_{ℝ} 1)) = 0$
18	5 12 17	3eqtr2i	$⊢ i + i i i = 0$

Metamath Proof Explorer