Metamath Proof Explorer

Theorem lenegsq

Description: Comparison to a nonnegative number based on comparison to squares. (Contributed by NM, 16-Jan-2006)

Ref Expression
Assertion lenegsq ⊢A∈ℝ∧B∈ℝ∧0≤B→A≤B∧−A≤B↔A2≤B2

Proof

Step Hyp Ref Expression
1 recn ⊢A∈ℝ→A∈ℂ
2 abscl ⊢A∈ℂ→A∈ℝ
3 absge0 ⊢A∈ℂ→0≤A
4 2 3 jca ⊢A∈ℂ→A∈ℝ∧0≤A
5 1 4 syl ⊢A∈ℝ→A∈ℝ∧0≤A
6 le2sq ⊢A∈ℝ∧0≤A∧B∈ℝ∧0≤B→A≤B↔A2≤B2
7 5 6 sylan ⊢A∈ℝ∧B∈ℝ∧0≤B→A≤B↔A2≤B2
8 absle ⊢A∈ℝ∧B∈ℝ→A≤B↔−B≤A∧A≤B
9 lenegcon1 ⊢A∈ℝ∧B∈ℝ→−A≤B↔−B≤A
10 9 anbi1d ⊢A∈ℝ∧B∈ℝ→−A≤B∧A≤B↔−B≤A∧A≤B
11 ancom ⊢−A≤B∧A≤B↔A≤B∧−A≤B
12 10 11 bitr3di ⊢A∈ℝ∧B∈ℝ→−B≤A∧A≤B↔A≤B∧−A≤B
13 8 12 bitrd ⊢A∈ℝ∧B∈ℝ→A≤B↔A≤B∧−A≤B
14 13 adantrr ⊢A∈ℝ∧B∈ℝ∧0≤B→A≤B↔A≤B∧−A≤B
15 absresq ⊢A∈ℝ→A2=A2
16 15 breq1d ⊢A∈ℝ→A2≤B2↔A2≤B2
17 16 adantr ⊢A∈ℝ∧B∈ℝ∧0≤B→A2≤B2↔A2≤B2
18 7 14 17 3bitr3d ⊢A∈ℝ∧B∈ℝ∧0≤B→A≤B∧−A≤B↔A2≤B2
19 18 3impb ⊢A∈ℝ∧B∈ℝ∧0≤B→A≤B∧−A≤B↔A2≤B2