Metamath Proof Explorer

Theorem sn-0lt1

Description: 0lt1 without ax-mulcom . (Contributed by SN, 13-Feb-2024)

Ref Expression
Assertion sn-0lt1 
|- 0 < 1

Proof

Step Hyp Ref Expression
1 ax-1ne0 
 |-  1 =/= 0
2 1re 
 |-  1 e. RR
3 0re 
 |-  0 e. RR
4 2 3 lttri2i 
 |-  ( 1 =/= 0 <-> ( 1 < 0 \/ 0 < 1 ) )
5 1 4 mpbi 
 |-  ( 1 < 0 \/ 0 < 1 )
6 rernegcl 
 |-  ( 1 e. RR -> ( 0 -R 1 ) e. RR )
7 2 6 ax-mp 
 |-  ( 0 -R 1 ) e. RR
8 7 a1i 
 |-  ( 1 < 0 -> ( 0 -R 1 ) e. RR )
9 relt0neg1 
 |-  ( 1 e. RR -> ( 1 < 0 <-> 0 < ( 0 -R 1 ) ) )
10 2 9 ax-mp 
 |-  ( 1 < 0 <-> 0 < ( 0 -R 1 ) )
11 10 biimpi 
 |-  ( 1 < 0 -> 0 < ( 0 -R 1 ) )
12 8 8 11 11 mulgt0d 
 |-  ( 1 < 0 -> 0 < ( ( 0 -R 1 ) x. ( 0 -R 1 ) ) )
13 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 ) ) )
14 7 3 2 13 mp3an 
 |-  ( ( 0 -R 1 ) x. ( 0 -R 1 ) ) = ( ( ( 0 -R 1 ) x. 0 ) -R ( ( 0 -R 1 ) x. 1 ) )
15 remul01 
 |-  ( ( 0 -R 1 ) e. RR -> ( ( 0 -R 1 ) x. 0 ) = 0 )
16 7 15 ax-mp 
 |-  ( ( 0 -R 1 ) x. 0 ) = 0
17 ax-1rid 
 |-  ( ( 0 -R 1 ) e. RR -> ( ( 0 -R 1 ) x. 1 ) = ( 0 -R 1 ) )
18 7 17 ax-mp 
 |-  ( ( 0 -R 1 ) x. 1 ) = ( 0 -R 1 )
19 16 18 oveq12i 
 |-  ( ( ( 0 -R 1 ) x. 0 ) -R ( ( 0 -R 1 ) x. 1 ) ) = ( 0 -R ( 0 -R 1 ) )
20 renegneg 
 |-  ( 1 e. RR -> ( 0 -R ( 0 -R 1 ) ) = 1 )
21 2 20 ax-mp 
 |-  ( 0 -R ( 0 -R 1 ) ) = 1
22 14 19 21 3eqtri 
 |-  ( ( 0 -R 1 ) x. ( 0 -R 1 ) ) = 1
23 12 22 breqtrdi 
 |-  ( 1 < 0 -> 0 < 1 )
24 id 
 |-  ( 0 < 1 -> 0 < 1 )
25 23 24 jaoi 
 |-  ( ( 1 < 0 \/ 0 < 1 ) -> 0 < 1 )
26 5 25 ax-mp 
 |-  0 < 1