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 readdlid 
 |-  ( 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