Theorem abs2sqle

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

	Ref	Expression
Assertion	abs2sqle	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( ( abs ‘ 𝐴 ) ≤ ( abs ‘ 𝐵 ) ↔ ( ( abs ‘ 𝐴 ) ↑ 2 ) ≤ ( ( abs ‘ 𝐵 ) ↑ 2 ) ) )

Proof

Step	Hyp	Ref	Expression
1		fveq2	⊢ ( 𝐴 = if ( 𝐴 ∈ ℂ , 𝐴 , 0 ) → ( abs ‘ 𝐴 ) = ( abs ‘ if ( 𝐴 ∈ ℂ , 𝐴 , 0 ) ) )
2	1	breq1d	⊢ ( 𝐴 = if ( 𝐴 ∈ ℂ , 𝐴 , 0 ) → ( ( abs ‘ 𝐴 ) ≤ ( abs ‘ 𝐵 ) ↔ ( abs ‘ if ( 𝐴 ∈ ℂ , 𝐴 , 0 ) ) ≤ ( abs ‘ 𝐵 ) ) )
3	1	oveq1d	⊢ ( 𝐴 = if ( 𝐴 ∈ ℂ , 𝐴 , 0 ) → ( ( abs ‘ 𝐴 ) ↑ 2 ) = ( ( abs ‘ if ( 𝐴 ∈ ℂ , 𝐴 , 0 ) ) ↑ 2 ) )
4	3	breq1d	⊢ ( 𝐴 = if ( 𝐴 ∈ ℂ , 𝐴 , 0 ) → ( ( ( abs ‘ 𝐴 ) ↑ 2 ) ≤ ( ( abs ‘ 𝐵 ) ↑ 2 ) ↔ ( ( abs ‘ if ( 𝐴 ∈ ℂ , 𝐴 , 0 ) ) ↑ 2 ) ≤ ( ( abs ‘ 𝐵 ) ↑ 2 ) ) )
5	2 4	bibi12d	⊢ ( 𝐴 = if ( 𝐴 ∈ ℂ , 𝐴 , 0 ) → ( ( ( abs ‘ 𝐴 ) ≤ ( abs ‘ 𝐵 ) ↔ ( ( abs ‘ 𝐴 ) ↑ 2 ) ≤ ( ( abs ‘ 𝐵 ) ↑ 2 ) ) ↔ ( ( abs ‘ if ( 𝐴 ∈ ℂ , 𝐴 , 0 ) ) ≤ ( abs ‘ 𝐵 ) ↔ ( ( abs ‘ if ( 𝐴 ∈ ℂ , 𝐴 , 0 ) ) ↑ 2 ) ≤ ( ( abs ‘ 𝐵 ) ↑ 2 ) ) ) )
6		fveq2	⊢ ( 𝐵 = if ( 𝐵 ∈ ℂ , 𝐵 , 0 ) → ( abs ‘ 𝐵 ) = ( abs ‘ if ( 𝐵 ∈ ℂ , 𝐵 , 0 ) ) )
7	6	breq2d	⊢ ( 𝐵 = if ( 𝐵 ∈ ℂ , 𝐵 , 0 ) → ( ( abs ‘ if ( 𝐴 ∈ ℂ , 𝐴 , 0 ) ) ≤ ( abs ‘ 𝐵 ) ↔ ( abs ‘ if ( 𝐴 ∈ ℂ , 𝐴 , 0 ) ) ≤ ( abs ‘ if ( 𝐵 ∈ ℂ , 𝐵 , 0 ) ) ) )
8		oveq1	⊢ ( ( abs ‘ 𝐵 ) = ( abs ‘ if ( 𝐵 ∈ ℂ , 𝐵 , 0 ) ) → ( ( abs ‘ 𝐵 ) ↑ 2 ) = ( ( abs ‘ if ( 𝐵 ∈ ℂ , 𝐵 , 0 ) ) ↑ 2 ) )
9	8	breq2d	⊢ ( ( abs ‘ 𝐵 ) = ( abs ‘ if ( 𝐵 ∈ ℂ , 𝐵 , 0 ) ) → ( ( ( abs ‘ if ( 𝐴 ∈ ℂ , 𝐴 , 0 ) ) ↑ 2 ) ≤ ( ( abs ‘ 𝐵 ) ↑ 2 ) ↔ ( ( abs ‘ if ( 𝐴 ∈ ℂ , 𝐴 , 0 ) ) ↑ 2 ) ≤ ( ( abs ‘ if ( 𝐵 ∈ ℂ , 𝐵 , 0 ) ) ↑ 2 ) ) )
10	6 9	syl	⊢ ( 𝐵 = if ( 𝐵 ∈ ℂ , 𝐵 , 0 ) → ( ( ( abs ‘ if ( 𝐴 ∈ ℂ , 𝐴 , 0 ) ) ↑ 2 ) ≤ ( ( abs ‘ 𝐵 ) ↑ 2 ) ↔ ( ( abs ‘ if ( 𝐴 ∈ ℂ , 𝐴 , 0 ) ) ↑ 2 ) ≤ ( ( abs ‘ if ( 𝐵 ∈ ℂ , 𝐵 , 0 ) ) ↑ 2 ) ) )
11	7 10	bibi12d	⊢ ( 𝐵 = if ( 𝐵 ∈ ℂ , 𝐵 , 0 ) → ( ( ( abs ‘ if ( 𝐴 ∈ ℂ , 𝐴 , 0 ) ) ≤ ( abs ‘ 𝐵 ) ↔ ( ( abs ‘ if ( 𝐴 ∈ ℂ , 𝐴 , 0 ) ) ↑ 2 ) ≤ ( ( abs ‘ 𝐵 ) ↑ 2 ) ) ↔ ( ( abs ‘ if ( 𝐴 ∈ ℂ , 𝐴 , 0 ) ) ≤ ( abs ‘ if ( 𝐵 ∈ ℂ , 𝐵 , 0 ) ) ↔ ( ( abs ‘ if ( 𝐴 ∈ ℂ , 𝐴 , 0 ) ) ↑ 2 ) ≤ ( ( abs ‘ if ( 𝐵 ∈ ℂ , 𝐵 , 0 ) ) ↑ 2 ) ) ) )
12		0cn	⊢ 0 ∈ ℂ
13	12	elimel	⊢ if ( 𝐴 ∈ ℂ , 𝐴 , 0 ) ∈ ℂ
14	12	elimel	⊢ if ( 𝐵 ∈ ℂ , 𝐵 , 0 ) ∈ ℂ
15	13 14	abs2sqlei	⊢ ( ( abs ‘ if ( 𝐴 ∈ ℂ , 𝐴 , 0 ) ) ≤ ( abs ‘ if ( 𝐵 ∈ ℂ , 𝐵 , 0 ) ) ↔ ( ( abs ‘ if ( 𝐴 ∈ ℂ , 𝐴 , 0 ) ) ↑ 2 ) ≤ ( ( abs ‘ if ( 𝐵 ∈ ℂ , 𝐵 , 0 ) ) ↑ 2 ) )
16	5 11 15	dedth2h	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( ( abs ‘ 𝐴 ) ≤ ( abs ‘ 𝐵 ) ↔ ( ( abs ‘ 𝐴 ) ↑ 2 ) ≤ ( ( abs ‘ 𝐵 ) ↑ 2 ) ) )