Metamath Proof Explorer
Description: The absolute values of two numbers compare as their squares.
(Contributed by Paul Chapman, 7-Sep-2007)
|
|
Ref |
Expression |
|
Hypotheses |
abs2sqlei.1 |
|
|
|
abs2sqlei.2 |
|
|
Assertion |
abs2sqlei |
|
Proof
Step |
Hyp |
Ref |
Expression |
1 |
|
abs2sqlei.1 |
|
2 |
|
abs2sqlei.2 |
|
3 |
1
|
absge0i |
|
4 |
2
|
absge0i |
|
5 |
1
|
abscli |
|
6 |
2
|
abscli |
|
7 |
5 6
|
le2sqi |
|
8 |
3 4 7
|
mp2an |
|