Theorem abslt2sqd

Description: Comparison of the square of two numbers. (Contributed by Glauco Siliprandi, 24-Dec-2020)

	Ref	Expression
Hypotheses	abslt2sqd.a	$$⊢\phi \to A\in ℝ$$
	abslt2sqd.b	$$⊢\phi \to B\in ℝ$$
	abslt2sqd.l	$$⊢\phi \to \left|A\right|<\left|B\right|$$
Assertion	abslt2sqd	$$⊢\phi \to A^2<B^2$$

Proof

Step	Hyp	Ref	Expression
1		abslt2sqd.a	$$⊢\phi \to A\in ℝ$$
2		abslt2sqd.b	$$⊢\phi \to B\in ℝ$$
3		abslt2sqd.l	$$⊢\phi \to \left|A\right|<\left|B\right|$$
4	1	recnd	$$⊢\phi \to A\in ℂ$$
5	4	abscld	$$⊢\phi \to \left|A\right|\in ℝ$$
6	4	absge0d	$$⊢\phi \to 0\le \left|A\right|$$
7	2	recnd	$$⊢\phi \to B\in ℂ$$
8	7	abscld	$$⊢\phi \to \left|B\right|\in ℝ$$
9	7	absge0d	$$⊢\phi \to 0\le \left|B\right|$$
10		lt2sq	$$⊢\left(\left(\left|A\right|\in ℝ\wedge 0\le \left|A\right|\right)\wedge \left(\left|B\right|\in ℝ\wedge 0\le \left|B\right|\right)\right)\to \left(\left|A\right|<\left|B\right|\leftrightarrow {\left|A\right|}^2<{\left|B\right|}^2\right)$$
11	5 6 8 9 10	syl22anc	$$⊢\phi \to \left(\left|A\right|<\left|B\right|\leftrightarrow {\left|A\right|}^2<{\left|B\right|}^2\right)$$
12	3 11	mpbid	$$⊢\phi \to {\left|A\right|}^2<{\left|B\right|}^2$$
13		absresq	$$⊢A\in ℝ\to {\left|A\right|}^2=A^2$$
14	1 13	syl	$$⊢\phi \to {\left|A\right|}^2=A^2$$
15		absresq	$$⊢B\in ℝ\to {\left|B\right|}^2=B^2$$
16	2 15	syl	$$⊢\phi \to {\left|B\right|}^2=B^2$$
17	14 16	breq12d	$$⊢\phi \to \left({\left|A\right|}^2<{\left|B\right|}^2\leftrightarrow A^2<B^2\right)$$
18	12 17	mpbid	$$⊢\phi \to A^2<B^2$$