Metamath Proof Explorer


Theorem sn-0ne2

Description: 0ne2 without ax-mulcom . (Contributed by SN, 23-Jan-2024)

Ref Expression
Assertion sn-0ne2 0 2

Proof

Step Hyp Ref Expression
1 1re 1
2 readdid2 1 0 + 1 = 1
3 1 2 ax-mp 0 + 1 = 1
4 sn-1ne2 1 2
5 2re 2
6 1 5 lttri2i 1 2 1 < 2 2 < 1
7 4 6 mpbi 1 < 2 2 < 1
8 1red 1 < 2 1
9 1 5 1 ltadd2i 1 < 2 1 + 1 < 1 + 2
10 9 biimpi 1 < 2 1 + 1 < 1 + 2
11 1p1e2 1 + 1 = 2
12 1p2e3 1 + 2 = 3
13 10 11 12 3brtr3g 1 < 2 2 < 3
14 3re 3
15 1 5 14 lttri 1 < 2 2 < 3 1 < 3
16 13 15 mpdan 1 < 2 1 < 3
17 8 16 ltned 1 < 2 1 3
18 14 a1i 2 < 1 3
19 5 1 1 ltadd2i 2 < 1 1 + 2 < 1 + 1
20 19 biimpi 2 < 1 1 + 2 < 1 + 1
21 20 12 11 3brtr3g 2 < 1 3 < 2
22 14 5 1 lttri 3 < 2 2 < 1 3 < 1
23 21 22 mpancom 2 < 1 3 < 1
24 18 23 gtned 2 < 1 1 3
25 17 24 jaoi 1 < 2 2 < 1 1 3
26 7 25 ax-mp 1 3
27 df-3 3 = 2 + 1
28 26 27 neeqtri 1 2 + 1
29 3 28 eqnetri 0 + 1 2 + 1
30 oveq1 0 = 2 0 + 1 = 2 + 1
31 30 necon3i 0 + 1 2 + 1 0 2
32 29 31 ax-mp 0 2