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