Theorem abs2sqlt

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

	Ref	Expression
Assertion	abs2sqlt	$$⊢\left(A\in ℂ\wedge B\in ℂ\right)\to \left(\left|A\right|<\left|B\right|\leftrightarrow {\left|A\right|}^2<{\left|B\right|}^2\right)$$

Proof

Step	Hyp	Ref	Expression
1		fveq2	$$⊢A=if\left(A\in ℂ,A,0\right)\to \left|A\right|=\left|if\left(A\in ℂ,A,0\right)\right|$$
2	1	breq1d	$$⊢A=if\left(A\in ℂ,A,0\right)\to \left(\left|A\right|<\left|B\right|\leftrightarrow \left|if\left(A\in ℂ,A,0\right)\right|<\left|B\right|\right)$$
3	1	oveq1d	$$⊢A=if\left(A\in ℂ,A,0\right)\to {\left|A\right|}^2={\left|if\left(A\in ℂ,A,0\right)\right|}^2$$
4	3	breq1d	$$⊢A=if\left(A\in ℂ,A,0\right)\to \left({\left|A\right|}^2<{\left|B\right|}^2\leftrightarrow {\left|if\left(A\in ℂ,A,0\right)\right|}^2<{\left|B\right|}^2\right)$$
5	2 4	bibi12d	$$⊢A=if\left(A\in ℂ,A,0\right)\to \left(\left(\left|A\right|<\left|B\right|\leftrightarrow {\left|A\right|}^2<{\left|B\right|}^2\right)\leftrightarrow \left(\left|if\left(A\in ℂ,A,0\right)\right|<\left|B\right|\leftrightarrow {\left|if\left(A\in ℂ,A,0\right)\right|}^2<{\left|B\right|}^2\right)\right)$$
6		fveq2	$$⊢B=if\left(B\in ℂ,B,0\right)\to \left|B\right|=\left|if\left(B\in ℂ,B,0\right)\right|$$
7	6	breq2d	$$⊢B=if\left(B\in ℂ,B,0\right)\to \left(\left|if\left(A\in ℂ,A,0\right)\right|<\left|B\right|\leftrightarrow \left|if\left(A\in ℂ,A,0\right)\right|<\left|if\left(B\in ℂ,B,0\right)\right|\right)$$
8		oveq1	$$⊢\left|B\right|=\left|if\left(B\in ℂ,B,0\right)\right|\to {\left|B\right|}^2={\left|if\left(B\in ℂ,B,0\right)\right|}^2$$
9	8	breq2d	$$⊢\left|B\right|=\left|if\left(B\in ℂ,B,0\right)\right|\to \left({\left|if\left(A\in ℂ,A,0\right)\right|}^2<{\left|B\right|}^2\leftrightarrow {\left|if\left(A\in ℂ,A,0\right)\right|}^2<{\left|if\left(B\in ℂ,B,0\right)\right|}^2\right)$$
10	6 9	syl	$$⊢B=if\left(B\in ℂ,B,0\right)\to \left({\left|if\left(A\in ℂ,A,0\right)\right|}^2<{\left|B\right|}^2\leftrightarrow {\left|if\left(A\in ℂ,A,0\right)\right|}^2<{\left|if\left(B\in ℂ,B,0\right)\right|}^2\right)$$
11	7 10	bibi12d	$$⊢B=if\left(B\in ℂ,B,0\right)\to \left(\left(\left|if\left(A\in ℂ,A,0\right)\right|<\left|B\right|\leftrightarrow {\left|if\left(A\in ℂ,A,0\right)\right|}^2<{\left|B\right|}^2\right)\leftrightarrow \left(\left|if\left(A\in ℂ,A,0\right)\right|<\left|if\left(B\in ℂ,B,0\right)\right|\leftrightarrow {\left|if\left(A\in ℂ,A,0\right)\right|}^2<{\left|if\left(B\in ℂ,B,0\right)\right|}^2\right)\right)$$
12		0cn	$$⊢0\in ℂ$$
13	12	elimel	$$⊢if\left(A\in ℂ,A,0\right)\in ℂ$$
14	12	elimel	$$⊢if\left(B\in ℂ,B,0\right)\in ℂ$$
15	13 14	abs2sqlti	$$⊢\left|if\left(A\in ℂ,A,0\right)\right|<\left|if\left(B\in ℂ,B,0\right)\right|\leftrightarrow {\left|if\left(A\in ℂ,A,0\right)\right|}^2<{\left|if\left(B\in ℂ,B,0\right)\right|}^2$$
16	5 11 15	dedth2h	$$⊢\left(A\in ℂ\wedge B\in ℂ\right)\to \left(\left|A\right|<\left|B\right|\leftrightarrow {\left|A\right|}^2<{\left|B\right|}^2\right)$$