Theorem abs2sqlti

Description: The absolute values of two numbers compare as their squares. (Contributed by Paul Chapman, 7-Sep-2007)

	Ref	Expression
Hypotheses	abs2sqlti.1	$$⊢A\in ℂ$$
	abs2sqlti.2	$$⊢B\in ℂ$$
Assertion	abs2sqlti	$$⊢\left|A\right|<\left|B\right|\leftrightarrow {\left|A\right|}^2<{\left|B\right|}^2$$

Proof

Step	Hyp	Ref	Expression
1		abs2sqlti.1	$$⊢A\in ℂ$$
2		abs2sqlti.2	$$⊢B\in ℂ$$
3	1	absge0i	$$⊢0\le \left|A\right|$$
4	2	absge0i	$$⊢0\le \left|B\right|$$
5	1	abscli	$$⊢\left|A\right|\in ℝ$$
6	2	abscli	$$⊢\left|B\right|\in ℝ$$
7	5 6	lt2sqi	$$⊢\left(0\le \left|A\right|\wedge 0\le \left|B\right|\right)\to \left(\left|A\right|<\left|B\right|\leftrightarrow {\left|A\right|}^2<{\left|B\right|}^2\right)$$
8	3 4 7	mp2an	$$⊢\left|A\right|<\left|B\right|\leftrightarrow {\left|A\right|}^2<{\left|B\right|}^2$$