Description: The absolute value of a negative is the same as that of the positive. (Contributed by Mario Carneiro, 8-Sep-2014)
Ref | Expression | ||
---|---|---|---|
Hypotheses | abv0.a | |
|
abvneg.b | |
||
abvneg.p | |
||
Assertion | abvneg | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | abv0.a | |
|
2 | abvneg.b | |
|
3 | abvneg.p | |
|
4 | 1 | abvrcl | |
5 | 4 | adantr | |
6 | ringgrp | |
|
7 | 4 6 | syl | |
8 | 2 3 | grpinvcl | |
9 | 7 8 | sylan | |
10 | simpr | |
|
11 | eqid | |
|
12 | eqid | |
|
13 | 2 11 12 | ring1eq0 | |
14 | 5 9 10 13 | syl3anc | |
15 | 14 | imp | |
16 | 15 | fveq2d | |
17 | 2 11 | ringidcl | |
18 | 4 17 | syl | |
19 | 2 3 | grpinvcl | |
20 | 7 18 19 | syl2anc | |
21 | 1 2 | abvcl | |
22 | 20 21 | mpdan | |
23 | 22 | recnd | |
24 | 23 | sqvald | |
25 | eqid | |
|
26 | 1 2 25 | abvmul | |
27 | 20 20 26 | mpd3an23 | |
28 | 2 25 3 4 20 18 | ringmneg2 | |
29 | 2 25 11 3 4 18 | ringnegl | |
30 | 29 | fveq2d | |
31 | 2 3 | grpinvinv | |
32 | 7 18 31 | syl2anc | |
33 | 28 30 32 | 3eqtrd | |
34 | 33 | fveq2d | |
35 | 24 27 34 | 3eqtr2d | |
36 | 35 | adantr | |
37 | 1 11 12 | abv1z | |
38 | 36 37 | eqtrd | |
39 | sq1 | |
|
40 | 38 39 | eqtr4di | |
41 | 1 2 | abvge0 | |
42 | 20 41 | mpdan | |
43 | 1re | |
|
44 | 0le1 | |
|
45 | sq11 | |
|
46 | 43 44 45 | mpanr12 | |
47 | 22 42 46 | syl2anc | |
48 | 47 | biimpa | |
49 | 40 48 | syldan | |
50 | 49 | adantlr | |
51 | 50 | oveq1d | |
52 | simpl | |
|
53 | 20 | adantr | |
54 | 1 2 25 | abvmul | |
55 | 52 53 10 54 | syl3anc | |
56 | 2 25 11 3 5 10 | ringnegl | |
57 | 56 | fveq2d | |
58 | 55 57 | eqtr3d | |
59 | 58 | adantr | |
60 | 51 59 | eqtr3d | |
61 | 1 2 | abvcl | |
62 | 61 | recnd | |
63 | 62 | mulid2d | |
64 | 63 | adantr | |
65 | 60 64 | eqtr3d | |
66 | 16 65 | pm2.61dane | |