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	3 4	ax-mp	⊢ ( 0 −ℝ 1 ) ∈ ℝ
6		0re	⊢ 0 ∈ ℝ
7		resubdi	⊢ ( ( ( 0 −ℝ 1 ) ∈ ℝ ∧ 0 ∈ ℝ ∧ 1 ∈ ℝ ) → ( ( 0 −ℝ 1 ) · ( 0 −ℝ 1 ) ) = ( ( ( 0 −ℝ 1 ) · 0 ) −ℝ ( ( 0 −ℝ 1 ) · 1 ) ) )
8	5 6 3 7	mp3an	⊢ ( ( 0 −ℝ 1 ) · ( 0 −ℝ 1 ) ) = ( ( ( 0 −ℝ 1 ) · 0 ) −ℝ ( ( 0 −ℝ 1 ) · 1 ) )
9		remul01	⊢ ( ( 0 −ℝ 1 ) ∈ ℝ → ( ( 0 −ℝ 1 ) · 0 ) = 0 )
10	5 9	ax-mp	⊢ ( ( 0 −ℝ 1 ) · 0 ) = 0
11		ax-1rid	⊢ ( ( 0 −ℝ 1 ) ∈ ℝ → ( ( 0 −ℝ 1 ) · 1 ) = ( 0 −ℝ 1 ) )
12	5 11	ax-mp	⊢ ( ( 0 −ℝ 1 ) · 1 ) = ( 0 −ℝ 1 )
13	10 12	oveq12i	⊢ ( ( ( 0 −ℝ 1 ) · 0 ) −ℝ ( ( 0 −ℝ 1 ) · 1 ) ) = ( 0 −ℝ ( 0 −ℝ 1 ) )
14		renegneg	⊢ ( 1 ∈ ℝ → ( 0 −ℝ ( 0 −ℝ 1 ) ) = 1 )
15	3 14	ax-mp	⊢ ( 0 −ℝ ( 0 −ℝ 1 ) ) = 1
16	8 13 15	3eqtri	⊢ ( ( 0 −ℝ 1 ) · ( 0 −ℝ 1 ) ) = 1
17	2 16	eqtri	⊢ ( ( i · i ) · ( i · i ) ) = 1