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