Metamath Proof Explorer

Theorem le2msqi

Description: The square function on nonnegative reals is monotonic. (Contributed by NM, 2-Aug-1999)

Ref Expression
Hypotheses ltplus1.1 ⊢ A ∈ ℝ
prodgt0.2 ⊢ B ∈ ℝ
Assertion le2msqi ⊢ 0 ≤ A ∧ 0 ≤ B → A ≤ B ↔ A ⁢ A ≤ B ⁢ B

Proof

Step Hyp Ref Expression
1 ltplus1.1 ⊢ A ∈ ℝ
2 prodgt0.2 ⊢ B ∈ ℝ
3 le2msq ⊢ A ∈ ℝ ∧ 0 ≤ A ∧ B ∈ ℝ ∧ 0 ≤ B → A ≤ B ↔ A ⁢ A ≤ B ⁢ B
4 2 3 mpanr1 ⊢ A ∈ ℝ ∧ 0 ≤ A ∧ 0 ≤ B → A ≤ B ↔ A ⁢ A ≤ B ⁢ B
5 1 4 mpanl1 ⊢ 0 ≤ A ∧ 0 ≤ B → A ≤ B ↔ A ⁢ A ≤ B ⁢ B