Description: The absolute values of two numbers compare as their squares. (Contributed by Paul Chapman, 7-Sep-2007)
Ref | Expression | ||
---|---|---|---|
Hypotheses | abs2sqlei.1 | |- A e. CC |
|
abs2sqlei.2 | |- B e. CC |
||
Assertion | abs2sqlei | |- ( ( abs ` A ) <_ ( abs ` B ) <-> ( ( abs ` A ) ^ 2 ) <_ ( ( abs ` B ) ^ 2 ) ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | abs2sqlei.1 | |- A e. CC |
|
2 | abs2sqlei.2 | |- B e. CC |
|
3 | 1 | absge0i | |- 0 <_ ( abs ` A ) |
4 | 2 | absge0i | |- 0 <_ ( abs ` B ) |
5 | 1 | abscli | |- ( abs ` A ) e. RR |
6 | 2 | abscli | |- ( abs ` B ) e. RR |
7 | 5 6 | le2sqi | |- ( ( 0 <_ ( abs ` A ) /\ 0 <_ ( abs ` B ) ) -> ( ( abs ` A ) <_ ( abs ` B ) <-> ( ( abs ` A ) ^ 2 ) <_ ( ( abs ` B ) ^ 2 ) ) ) |
8 | 3 4 7 | mp2an | |- ( ( abs ` A ) <_ ( abs ` B ) <-> ( ( abs ` A ) ^ 2 ) <_ ( ( abs ` B ) ^ 2 ) ) |