This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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