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 3 4 ax-mp 
 |-  ( 0 -R 1 ) e. RR
6 0re 
 |-  0 e. RR
7 resubdi 
 |-  ( ( ( 0 -R 1 ) e. RR /\ 0 e. RR /\ 1 e. RR ) -> ( ( 0 -R 1 ) x. ( 0 -R 1 ) ) = ( ( ( 0 -R 1 ) x. 0 ) -R ( ( 0 -R 1 ) x. 1 ) ) )
8 5 6 3 7 mp3an 
 |-  ( ( 0 -R 1 ) x. ( 0 -R 1 ) ) = ( ( ( 0 -R 1 ) x. 0 ) -R ( ( 0 -R 1 ) x. 1 ) )
9 remul01 
 |-  ( ( 0 -R 1 ) e. RR -> ( ( 0 -R 1 ) x. 0 ) = 0 )
10 5 9 ax-mp 
 |-  ( ( 0 -R 1 ) x. 0 ) = 0
11 ax-1rid 
 |-  ( ( 0 -R 1 ) e. RR -> ( ( 0 -R 1 ) x. 1 ) = ( 0 -R 1 ) )
12 5 11 ax-mp 
 |-  ( ( 0 -R 1 ) x. 1 ) = ( 0 -R 1 )
13 10 12 oveq12i 
 |-  ( ( ( 0 -R 1 ) x. 0 ) -R ( ( 0 -R 1 ) x. 1 ) ) = ( 0 -R ( 0 -R 1 ) )
14 renegneg 
 |-  ( 1 e. RR -> ( 0 -R ( 0 -R 1 ) ) = 1 )
15 3 14 ax-mp 
 |-  ( 0 -R ( 0 -R 1 ) ) = 1
16 8 13 15 3eqtri 
 |-  ( ( 0 -R 1 ) x. ( 0 -R 1 ) ) = 1
17 2 16 eqtri 
 |-  ( ( _i x. _i ) x. ( _i x. _i ) ) = 1