Theorem rei4

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

	Ref	Expression
Assertion	rei4	⊢ ( ( i · i ) · ( i · i ) ) = 1

Proof

Step	Hyp	Ref	Expression
1		reixi	⊢ ( i · i ) = ( 0 −ℝ 1 )
2	1 1	oveq12i	⊢ ( ( i · i ) · ( i · i ) ) = ( ( 0 −ℝ 1 ) · ( 0 −ℝ 1 ) )
3		1re	⊢ 1 ∈ ℝ
4		rernegcl	⊢ ( 1 ∈ ℝ → ( 0 −ℝ 1 ) ∈ ℝ )
5		1red	⊢ ( 1 ∈ ℝ → 1 ∈ ℝ )
6	4 5	remulneg2d	⊢ ( 1 ∈ ℝ → ( ( 0 −ℝ 1 ) · ( 0 −ℝ 1 ) ) = ( 0 −ℝ ( ( 0 −ℝ 1 ) · 1 ) ) )
7		ax-1rid	⊢ ( ( 0 −ℝ 1 ) ∈ ℝ → ( ( 0 −ℝ 1 ) · 1 ) = ( 0 −ℝ 1 ) )
8	4 7	syl	⊢ ( 1 ∈ ℝ → ( ( 0 −ℝ 1 ) · 1 ) = ( 0 −ℝ 1 ) )
9	8	oveq2d	⊢ ( 1 ∈ ℝ → ( 0 −ℝ ( ( 0 −ℝ 1 ) · 1 ) ) = ( 0 −ℝ ( 0 −ℝ 1 ) ) )
10		renegneg	⊢ ( 1 ∈ ℝ → ( 0 −ℝ ( 0 −ℝ 1 ) ) = 1 )
11	6 9 10	3eqtrd	⊢ ( 1 ∈ ℝ → ( ( 0 −ℝ 1 ) · ( 0 −ℝ 1 ) ) = 1 )
12	3 11	ax-mp	⊢ ( ( 0 −ℝ 1 ) · ( 0 −ℝ 1 ) ) = 1
13	2 12	eqtri	⊢ ( ( i · i ) · ( i · i ) ) = 1