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 1 2

Proof

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