Description: The absolute values of two numbers compare as their squares. (Contributed by Paul Chapman, 7-Sep-2007)
Ref | Expression | ||
---|---|---|---|
Hypotheses | abs2sqlti.1 | |- A e. CC |
|
abs2sqlti.2 | |- B e. CC |
||
Assertion | abs2sqlti | |- ( ( abs ` A ) < ( abs ` B ) <-> ( ( abs ` A ) ^ 2 ) < ( ( abs ` B ) ^ 2 ) ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | abs2sqlti.1 | |- A e. CC |
|
2 | abs2sqlti.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 | lt2sqi | |- ( ( 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 ) ) |