Metamath Proof Explorer


Theorem sn-1ne2

Description: A proof of 1ne2 without using ax-mulcom , ax-mulass , ax-pre-mulgt0 . Based on mul02lem2 . (Contributed by SN, 13-Dec-2023)

Ref Expression
Assertion sn-1ne2 12

Proof

Step Hyp Ref Expression
1 0ne1 01
2 ax-icn i
3 2 2 mulcli ii
4 ax-1cn 1
5 3 4 4 addassi ii+1+1=ii+1+1
6 5 a1i 0=0+01=1+1ii+1+1=ii+1+1
7 simpr 0=0+01=1+11=1+1
8 7 oveq2d 0=0+01=1+1ii+1=ii+1+1
9 ax-i2m1 ii+1=0
10 9 a1i 0=0+01=1+1ii+1=0
11 6 8 10 3eqtr2rd 0=0+01=1+10=ii+1+1
12 simpl 0=0+01=1+10=0+0
13 10 oveq1d 0=0+01=1+1ii+1+1=0+1
14 11 12 13 3eqtr3d 0=0+01=1+10+0=0+1
15 0red 0=0+01=1+10
16 1red 0=0+01=1+11
17 readdcan 0100+0=0+10=1
18 15 16 15 17 syl3anc 0=0+01=1+10+0=0+10=1
19 14 18 mpbid 0=0+01=1+10=1
20 19 ex 0=0+01=1+10=1
21 20 necon3d 0=0+00111+1
22 1 21 mpi 0=0+011+1
23 oveq2 1=1+101=01+1
24 0re 0
25 ax-1rid 001=0
26 24 25 ax-mp 01=0
27 0cn 0
28 27 4 4 adddii 01+1=01+01
29 26 26 oveq12i 01+01=0+0
30 28 29 eqtri 01+1=0+0
31 23 26 30 3eqtr3g 1=1+10=0+0
32 31 necon3i 00+011+1
33 22 32 pm2.61ine 11+1
34 df-2 2=1+1
35 33 34 neeqtrri 12