Metamath Proof Explorer


Theorem rei4

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

Ref Expression
Assertion rei4
|- ( ( _i x. _i ) x. ( _i x. _i ) ) = 1

Proof

Step Hyp Ref Expression
1 reixi
 |-  ( _i x. _i ) = ( 0 -R 1 )
2 1 1 oveq12i
 |-  ( ( _i x. _i ) x. ( _i x. _i ) ) = ( ( 0 -R 1 ) x. ( 0 -R 1 ) )
3 1re
 |-  1 e. RR
4 rernegcl
 |-  ( 1 e. RR -> ( 0 -R 1 ) e. RR )
5 1red
 |-  ( 1 e. RR -> 1 e. RR )
6 4 5 remulneg2d
 |-  ( 1 e. RR -> ( ( 0 -R 1 ) x. ( 0 -R 1 ) ) = ( 0 -R ( ( 0 -R 1 ) x. 1 ) ) )
7 ax-1rid
 |-  ( ( 0 -R 1 ) e. RR -> ( ( 0 -R 1 ) x. 1 ) = ( 0 -R 1 ) )
8 4 7 syl
 |-  ( 1 e. RR -> ( ( 0 -R 1 ) x. 1 ) = ( 0 -R 1 ) )
9 8 oveq2d
 |-  ( 1 e. RR -> ( 0 -R ( ( 0 -R 1 ) x. 1 ) ) = ( 0 -R ( 0 -R 1 ) ) )
10 renegneg
 |-  ( 1 e. RR -> ( 0 -R ( 0 -R 1 ) ) = 1 )
11 6 9 10 3eqtrd
 |-  ( 1 e. RR -> ( ( 0 -R 1 ) x. ( 0 -R 1 ) ) = 1 )
12 3 11 ax-mp
 |-  ( ( 0 -R 1 ) x. ( 0 -R 1 ) ) = 1
13 2 12 eqtri
 |-  ( ( _i x. _i ) x. ( _i x. _i ) ) = 1