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