Theorem ipiiie0

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

	Ref	Expression
Assertion	ipiiie0	$$⊢\mathrm{i}+\mathrm{i}\mathrm{i}\mathrm{i}=0$$

Proof

Step	Hyp	Ref	Expression
1		sn-it1ei	$$⊢\mathrm{i}\cdot 1=\mathrm{i}$$
2	1	eqcomi	$$⊢\mathrm{i}=\mathrm{i}\cdot 1$$
3		reixi	$$⊢\mathrm{i}\mathrm{i}=0{-}_{ℝ}1$$
4	3	oveq2i	$$⊢\mathrm{i}\mathrm{i}\mathrm{i}=\mathrm{i}\left(0{-}_{ℝ}1\right)$$
5	2 4	oveq12i	$$⊢\mathrm{i}+\mathrm{i}\mathrm{i}\mathrm{i}=\mathrm{i}\cdot 1+\mathrm{i}\left(0{-}_{ℝ}1\right)$$
6		ax-icn	$$⊢\mathrm{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	$$⊢\mathrm{i}\left(1+\left(0{-}_{ℝ}1\right)\right)=\mathrm{i}\cdot 1+\mathrm{i}\left(0{-}_{ℝ}1\right)$$
13		renegid	$$⊢1\in ℝ\to 1+\left(0{-}_{ℝ}1\right)=0$$
14	8 13	ax-mp	$$⊢1+\left(0{-}_{ℝ}1\right)=0$$
15	14	oveq2i	$$⊢\mathrm{i}\left(1+\left(0{-}_{ℝ}1\right)\right)=\mathrm{i}\cdot 0$$
16		sn-it0e0	$$⊢\mathrm{i}\cdot 0=0$$
17	15 16	eqtri	$$⊢\mathrm{i}\left(1+\left(0{-}_{ℝ}1\right)\right)=0$$
18	5 12 17	3eqtr2i	$$⊢\mathrm{i}+\mathrm{i}\mathrm{i}\mathrm{i}=0$$