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 ax-mp 0 - 1
8 7 a1i 1 < 0 0 - 1
9 relt0neg1 1 1 < 0 0 < 0 - 1
10 2 9 ax-mp 1 < 0 0 < 0 - 1
11 10 biimpi 1 < 0 0 < 0 - 1
12 8 8 11 11 mulgt0d 1 < 0 0 < 0 - 1 0 - 1
13 resubdi 0 - 1 0 1 0 - 1 0 - 1 = 0 - 1 0 - 0 - 1 1
14 7 3 2 13 mp3an 0 - 1 0 - 1 = 0 - 1 0 - 0 - 1 1
15 remul01 0 - 1 0 - 1 0 = 0
16 7 15 ax-mp 0 - 1 0 = 0
17 ax-1rid 0 - 1 0 - 1 1 = 0 - 1
18 7 17 ax-mp 0 - 1 1 = 0 - 1
19 16 18 oveq12i 0 - 1 0 - 0 - 1 1 = 0 - 0 - 1
20 renegneg 1 0 - 0 - 1 = 1
21 2 20 ax-mp 0 - 0 - 1 = 1
22 14 19 21 3eqtri 0 - 1 0 - 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