Theorem rei4

Description: i4 without ax-mulcom . (Contributed by SN, 27-May-2024)

	Ref	Expression
Assertion	rei4	$$⊢\mathrm{i}\mathrm{i}\mathrm{i}\mathrm{i}=1$$

Proof

Step	Hyp	Ref	Expression
1		reixi	$$⊢\mathrm{i}\mathrm{i}=0{-}_{ℝ}1$$
2	1 1	oveq12i	$$⊢\mathrm{i}\mathrm{i}\mathrm{i}\mathrm{i}=\left(0{-}_{ℝ}1\right)\left(0{-}_{ℝ}1\right)$$
3		1re	$$⊢1\in ℝ$$
4		rernegcl	$$⊢1\in ℝ\to 0{-}_{ℝ}1\in ℝ$$
5	3 4	ax-mp	$$⊢0{-}_{ℝ}1\in ℝ$$
6		0re	$$⊢0\in ℝ$$
7		resubdi	$$⊢\left(0{-}_{ℝ}1\in ℝ\wedge 0\in ℝ\wedge 1\in ℝ\right)\to \left(0{-}_{ℝ}1\right)\left(0{-}_{ℝ}1\right)=\left(0{-}_{ℝ}1\right)\cdot 0{-}_{ℝ}\left(0{-}_{ℝ}1\right)\cdot 1$$
8	5 6 3 7	mp3an	$$⊢\left(0{-}_{ℝ}1\right)\left(0{-}_{ℝ}1\right)=\left(0{-}_{ℝ}1\right)\cdot 0{-}_{ℝ}\left(0{-}_{ℝ}1\right)\cdot 1$$
9		remul01	$$⊢0{-}_{ℝ}1\in ℝ\to \left(0{-}_{ℝ}1\right)\cdot 0=0$$
10	5 9	ax-mp	$$⊢\left(0{-}_{ℝ}1\right)\cdot 0=0$$
11		ax-1rid	$$⊢0{-}_{ℝ}1\in ℝ\to \left(0{-}_{ℝ}1\right)\cdot 1=0{-}_{ℝ}1$$
12	5 11	ax-mp	$$⊢\left(0{-}_{ℝ}1\right)\cdot 1=0{-}_{ℝ}1$$
13	10 12	oveq12i	$$⊢\left(0{-}_{ℝ}1\right)\cdot 0{-}_{ℝ}\left(0{-}_{ℝ}1\right)\cdot 1=0{-}_{ℝ}\left(0{-}_{ℝ}1\right)$$
14		renegneg	$$⊢1\in ℝ\to 0{-}_{ℝ}\left(0{-}_{ℝ}1\right)=1$$
15	3 14	ax-mp	$$⊢0{-}_{ℝ}\left(0{-}_{ℝ}1\right)=1$$
16	8 13 15	3eqtri	$$⊢\left(0{-}_{ℝ}1\right)\left(0{-}_{ℝ}1\right)=1$$
17	2 16	eqtri	$$⊢\mathrm{i}\mathrm{i}\mathrm{i}\mathrm{i}=1$$