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		1red	$$⊢1\in ℝ\to 1\in ℝ$$
6	4 5	remulneg2d	$$⊢1\in ℝ\to \left(0{-}_{ℝ}1\right)\left(0{-}_{ℝ}1\right)=0{-}_{ℝ}\left(0{-}_{ℝ}1\right)\cdot 1$$
7		ax-1rid	$$⊢0{-}_{ℝ}1\in ℝ\to \left(0{-}_{ℝ}1\right)\cdot 1=0{-}_{ℝ}1$$
8	4 7	syl	$$⊢1\in ℝ\to \left(0{-}_{ℝ}1\right)\cdot 1=0{-}_{ℝ}1$$
9	8	oveq2d	$$⊢1\in ℝ\to 0{-}_{ℝ}\left(0{-}_{ℝ}1\right)\cdot 1=0{-}_{ℝ}\left(0{-}_{ℝ}1\right)$$
10		renegneg	$$⊢1\in ℝ\to 0{-}_{ℝ}\left(0{-}_{ℝ}1\right)=1$$
11	6 9 10	3eqtrd	$$⊢1\in ℝ\to \left(0{-}_{ℝ}1\right)\left(0{-}_{ℝ}1\right)=1$$
12	3 11	ax-mp	$$⊢\left(0{-}_{ℝ}1\right)\left(0{-}_{ℝ}1\right)=1$$
13	2 12	eqtri	$$⊢\mathrm{i}\mathrm{i}\mathrm{i}\mathrm{i}=1$$