Metamath Proof Explorer

Theorem sn-inelr

Description: inelr without ax-mulcom . (Contributed by SN, 1-Jun-2024)

Ref Expression
Assertion sn-inelr 
|- -. _i e. RR

Proof

Step Hyp Ref Expression
1 reneg1lt0 
 |-  ( 0 -R 1 ) < 0
2 1re 
 |-  1 e. RR
3 rernegcl 
 |-  ( 1 e. RR -> ( 0 -R 1 ) e. RR )
4 2 3 ax-mp 
 |-  ( 0 -R 1 ) e. RR
5 0re 
 |-  0 e. RR
6 4 5 ltnsymi 
 |-  ( ( 0 -R 1 ) < 0 -> -. 0 < ( 0 -R 1 ) )
7 1 6 ax-mp 
 |-  -. 0 < ( 0 -R 1 )
8 reixi 
 |-  ( _i x. _i ) = ( 0 -R 1 )
9 8 breq2i 
 |-  ( 0 < ( _i x. _i ) <-> 0 < ( 0 -R 1 ) )
10 7 9 mtbir 
 |-  -. 0 < ( _i x. _i )
11 id 
 |-  ( _i e. RR -> _i e. RR )
12 0ne1 
 |-  0 =/= 1
13 12 a1i 
 |-  ( _i e. RR -> 0 =/= 1 )
14 id 
 |-  ( _i = 0 -> _i = 0 )
15 14 14 oveq12d 
 |-  ( _i = 0 -> ( _i x. _i ) = ( 0 x. 0 ) )
16 15 oveq1d 
 |-  ( _i = 0 -> ( ( _i x. _i ) + 1 ) = ( ( 0 x. 0 ) + 1 ) )
17 ax-i2m1 
 |-  ( ( _i x. _i ) + 1 ) = 0
18 remul02 
 |-  ( 0 e. RR -> ( 0 x. 0 ) = 0 )
19 5 18 ax-mp 
 |-  ( 0 x. 0 ) = 0
20 19 oveq1i 
 |-  ( ( 0 x. 0 ) + 1 ) = ( 0 + 1 )
21 readdlid 
 |-  ( 1 e. RR -> ( 0 + 1 ) = 1 )
22 2 21 ax-mp 
 |-  ( 0 + 1 ) = 1
23 20 22 eqtri 
 |-  ( ( 0 x. 0 ) + 1 ) = 1
24 16 17 23 3eqtr3g 
 |-  ( _i = 0 -> 0 = 1 )
25 24 adantl 
 |-  ( ( _i e. RR /\ _i = 0 ) -> 0 = 1 )
26 13 25 mteqand 
 |-  ( _i e. RR -> _i =/= 0 )
27 11 26 sn-msqgt0d 
 |-  ( _i e. RR -> 0 < ( _i x. _i ) )
28 10 27 mto 
 |-  -. _i e. RR