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 mp1i
 |-  ( 1 < 0 -> ( 0 -R 1 ) e. RR )
8 relt0neg1
 |-  ( 1 e. RR -> ( 1 < 0 <-> 0 < ( 0 -R 1 ) ) )
9 2 8 ax-mp
 |-  ( 1 < 0 <-> 0 < ( 0 -R 1 ) )
10 9 biimpi
 |-  ( 1 < 0 -> 0 < ( 0 -R 1 ) )
11 7 7 10 10 mulgt0d
 |-  ( 1 < 0 -> 0 < ( ( 0 -R 1 ) x. ( 0 -R 1 ) ) )
12 1red
 |-  ( 1 e. RR -> 1 e. RR )
13 6 12 remulneg2d
 |-  ( 1 e. RR -> ( ( 0 -R 1 ) x. ( 0 -R 1 ) ) = ( 0 -R ( ( 0 -R 1 ) x. 1 ) ) )
14 ax-1rid
 |-  ( ( 0 -R 1 ) e. RR -> ( ( 0 -R 1 ) x. 1 ) = ( 0 -R 1 ) )
15 6 14 syl
 |-  ( 1 e. RR -> ( ( 0 -R 1 ) x. 1 ) = ( 0 -R 1 ) )
16 15 oveq2d
 |-  ( 1 e. RR -> ( 0 -R ( ( 0 -R 1 ) x. 1 ) ) = ( 0 -R ( 0 -R 1 ) ) )
17 renegneg
 |-  ( 1 e. RR -> ( 0 -R ( 0 -R 1 ) ) = 1 )
18 13 16 17 3eqtrd
 |-  ( 1 e. RR -> ( ( 0 -R 1 ) x. ( 0 -R 1 ) ) = 1 )
19 2 18 ax-mp
 |-  ( ( 0 -R 1 ) x. ( 0 -R 1 ) ) = 1
20 11 19 breqtrdi
 |-  ( 1 < 0 -> 0 < 1 )
21 id
 |-  ( 0 < 1 -> 0 < 1 )
22 20 21 jaoi
 |-  ( ( 1 < 0 \/ 0 < 1 ) -> 0 < 1 )
23 5 22 ax-mp
 |-  0 < 1