Metamath Proof Explorer


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