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
3 0re 0
4 2 3 lttri2i 1 0 1 < 0 0 < 1
5 1 4 mpbi 1 < 0 0 < 1
6 rernegcl 1 0 - 1
7 2 6 mp1i 1 < 0 0 - 1
8 relt0neg1 1 1 < 0 0 < 0 - 1
9 2 8 ax-mp 1 < 0 0 < 0 - 1
10 9 biimpi 1 < 0 0 < 0 - 1
11 7 7 10 10 mulgt0d 1 < 0 0 < 0 - 1 0 - 1
12 1red 1 1
13 6 12 remulneg2d 1 0 - 1 0 - 1 = 0 - 0 - 1 1
14 ax-1rid 0 - 1 0 - 1 1 = 0 - 1
15 6 14 syl 1 0 - 1 1 = 0 - 1
16 15 oveq2d 1 0 - 0 - 1 1 = 0 - 0 - 1
17 renegneg 1 0 - 0 - 1 = 1
18 13 16 17 3eqtrd 1 0 - 1 0 - 1 = 1
19 2 18 ax-mp 0 - 1 0 - 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