Metamath Proof Explorer

Theorem le2msq

Description: The square function on nonnegative reals is monotonic. (Contributed by NM, 3-Aug-1999) (Proof shortened by Mario Carneiro, 27-May-2016)

Ref Expression
Assertion le2msq ⊢ A ∈ ℝ ∧ 0 ≤ A ∧ B ∈ ℝ ∧ 0 ≤ B → A ≤ B ↔ A ⁢ A ≤ B ⁢ B

Proof

Step Hyp Ref Expression
1 lt2msq ⊢ B ∈ ℝ ∧ 0 ≤ B ∧ A ∈ ℝ ∧ 0 ≤ A → B < A ↔ B ⁢ B < A ⁢ A
2 1 ancoms ⊢ A ∈ ℝ ∧ 0 ≤ A ∧ B ∈ ℝ ∧ 0 ≤ B → B < A ↔ B ⁢ B < A ⁢ A
3 2 notbid ⊢ A ∈ ℝ ∧ 0 ≤ A ∧ B ∈ ℝ ∧ 0 ≤ B → ¬ B < A ↔ ¬ B ⁢ B < A ⁢ A
4 simpll ⊢ A ∈ ℝ ∧ 0 ≤ A ∧ B ∈ ℝ ∧ 0 ≤ B → A ∈ ℝ
5 simprl ⊢ A ∈ ℝ ∧ 0 ≤ A ∧ B ∈ ℝ ∧ 0 ≤ B → B ∈ ℝ
6 4 5 lenltd ⊢ A ∈ ℝ ∧ 0 ≤ A ∧ B ∈ ℝ ∧ 0 ≤ B → A ≤ B ↔ ¬ B < A
7 4 4 remulcld ⊢ A ∈ ℝ ∧ 0 ≤ A ∧ B ∈ ℝ ∧ 0 ≤ B → A ⁢ A ∈ ℝ
8 5 5 remulcld ⊢ A ∈ ℝ ∧ 0 ≤ A ∧ B ∈ ℝ ∧ 0 ≤ B → B ⁢ B ∈ ℝ
9 7 8 lenltd ⊢ A ∈ ℝ ∧ 0 ≤ A ∧ B ∈ ℝ ∧ 0 ≤ B → A ⁢ A ≤ B ⁢ B ↔ ¬ B ⁢ B < A ⁢ A
10 3 6 9 3bitr4d ⊢ A ∈ ℝ ∧ 0 ≤ A ∧ B ∈ ℝ ∧ 0 ≤ B → A ≤ B ↔ A ⁢ A ≤ B ⁢ B