Metamath Proof Explorer


Theorem sn-inelr

Description: inelr without ax-mulcom . (Contributed by SN, 1-Jun-2024)

Ref Expression
Assertion sn-inelr ¬ i

Proof

Step Hyp Ref Expression
1 0re 0
2 lttri4 i 0 i < 0 i = 0 0 < i
3 1 2 mpan2 i i < 0 i = 0 0 < i
4 reneg1lt0 0 - 1 < 0
5 1re 1
6 rernegcl 1 0 - 1
7 5 6 ax-mp 0 - 1
8 7 1 ltnsymi 0 - 1 < 0 ¬ 0 < 0 - 1
9 4 8 ax-mp ¬ 0 < 0 - 1
10 relt0neg1 i i < 0 0 < 0 - i
11 rernegcl i 0 - i
12 mulgt0 0 - i 0 < 0 - i 0 - i 0 < 0 - i 0 < 0 - i 0 - i
13 12 anidms 0 - i 0 < 0 - i 0 < 0 - i 0 - i
14 11 13 sylan i 0 < 0 - i 0 < 0 - i 0 - i
15 elre0re i 0
16 id i i
17 resubdi 0 - i 0 i 0 - i 0 - i = 0 - i 0 - 0 - i i
18 11 15 16 17 syl3anc i 0 - i 0 - i = 0 - i 0 - 0 - i i
19 remul01 0 - i 0 - i 0 = 0
20 11 19 syl i 0 - i 0 = 0
21 16 16 remulcld i i i
22 16 21 remulcld i i i i
23 ipiiie0 i + i i i = 0
24 renegadd i i i i 0 - i = i i i i + i i i = 0
25 23 24 mpbiri i i i i 0 - i = i i i
26 22 25 mpdan i 0 - i = i i i
27 26 oveq1d i 0 - i i = i i i i
28 ax-icn i
29 28 28 28 mulassi i i i = i i i
30 29 oveq1i i i i i = i i i i
31 28 28 mulcli i i
32 31 28 28 mulassi i i i i = i i i i
33 30 32 eqtr3i i i i i = i i i i
34 33 a1i i i i i i = i i i i
35 rei4 i i i i = 1
36 35 a1i i i i i i = 1
37 27 34 36 3eqtrd i 0 - i i = 1
38 20 37 oveq12d i 0 - i 0 - 0 - i i = 0 - 1
39 18 38 eqtrd i 0 - i 0 - i = 0 - 1
40 39 breq2d i 0 < 0 - i 0 - i 0 < 0 - 1
41 40 adantr i 0 < 0 - i 0 < 0 - i 0 - i 0 < 0 - 1
42 14 41 mpbid i 0 < 0 - i 0 < 0 - 1
43 42 ex i 0 < 0 - i 0 < 0 - 1
44 10 43 sylbid i i < 0 0 < 0 - 1
45 9 44 mtoi i ¬ i < 0
46 0ne1 0 1
47 46 neii ¬ 0 = 1
48 oveq12 i = 0 i = 0 i i = 0 0
49 48 anidms i = 0 i i = 0 0
50 49 oveq1d i = 0 i i + 1 = 0 0 + 1
51 ax-i2m1 i i + 1 = 0
52 remul02 0 0 0 = 0
53 1 52 ax-mp 0 0 = 0
54 53 oveq1i 0 0 + 1 = 0 + 1
55 readdid2 1 0 + 1 = 1
56 5 55 ax-mp 0 + 1 = 1
57 54 56 eqtri 0 0 + 1 = 1
58 50 51 57 3eqtr3g i = 0 0 = 1
59 47 58 mto ¬ i = 0
60 59 a1i i ¬ i = 0
61 mulgt0 i 0 < i i 0 < i 0 < i i
62 61 anidms i 0 < i 0 < i i
63 reixi i i = 0 - 1
64 62 63 breqtrdi i 0 < i 0 < 0 - 1
65 64 ex i 0 < i 0 < 0 - 1
66 9 65 mtoi i ¬ 0 < i
67 3ioran ¬ i < 0 i = 0 0 < i ¬ i < 0 ¬ i = 0 ¬ 0 < i
68 45 60 66 67 syl3anbrc i ¬ i < 0 i = 0 0 < i
69 3 68 pm2.65i ¬ i