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 e. RR
2 readdid2
 |-  ( 1 e. RR -> ( 0 + 1 ) = 1 )
3 1 2 ax-mp
 |-  ( 0 + 1 ) = 1
4 sn-1ne2
 |-  1 =/= 2
5 2re
 |-  2 e. RR
6 1 5 lttri2i
 |-  ( 1 =/= 2 <-> ( 1 < 2 \/ 2 < 1 ) )
7 4 6 mpbi
 |-  ( 1 < 2 \/ 2 < 1 )
8 1red
 |-  ( 1 < 2 -> 1 e. RR )
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 e. RR
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 e. RR )
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