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