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 ↔ A 2 ≤ B 2

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 ↔ A 2 ≤ B 2
7 5 6 sylan ⊢ A ∈ ℝ ∧ B ∈ ℝ ∧ 0 ≤ B → A ≤ B ↔ A 2 ≤ B 2
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 ∈ ℝ → A 2 = A 2
16 15 breq1d ⊢ A ∈ ℝ → A 2 ≤ B 2 ↔ A 2 ≤ B 2
17 16 adantr ⊢ A ∈ ℝ ∧ B ∈ ℝ ∧ 0 ≤ B → A 2 ≤ B 2 ↔ A 2 ≤ B 2
18 7 14 17 3bitr3d ⊢ A ∈ ℝ ∧ B ∈ ℝ ∧ 0 ≤ B → A ≤ B ∧ − A ≤ B ↔ A 2 ≤ B 2
19 18 3impb ⊢ A ∈ ℝ ∧ B ∈ ℝ ∧ 0 ≤ B → A ≤ B ∧ − A ≤ B ↔ A 2 ≤ B 2