Metamath Proof Explorer

Theorem sqrtle

Description: Square root is monotonic. (Contributed by NM, 17-Mar-2005) (Proof shortened by Mario Carneiro, 29-May-2016)

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

Proof

Step Hyp Ref Expression
1 resqrtcl ⊢ A ∈ ℝ ∧ 0 ≤ A → A ∈ ℝ
2 sqrtge0 ⊢ A ∈ ℝ ∧ 0 ≤ A → 0 ≤ A
3 1 2 jca ⊢ A ∈ ℝ ∧ 0 ≤ A → A ∈ ℝ ∧ 0 ≤ A
4 resqrtcl ⊢ B ∈ ℝ ∧ 0 ≤ B → B ∈ ℝ
5 sqrtge0 ⊢ B ∈ ℝ ∧ 0 ≤ B → 0 ≤ B
6 4 5 jca ⊢ B ∈ ℝ ∧ 0 ≤ B → B ∈ ℝ ∧ 0 ≤ B
7 le2sq ⊢ A ∈ ℝ ∧ 0 ≤ A ∧ B ∈ ℝ ∧ 0 ≤ B → A ≤ B ↔ A 2 ≤ B 2
8 3 6 7 syl2an ⊢ A ∈ ℝ ∧ 0 ≤ A ∧ B ∈ ℝ ∧ 0 ≤ B → A ≤ B ↔ A 2 ≤ B 2
9 resqrtth ⊢ A ∈ ℝ ∧ 0 ≤ A → A 2 = A
10 resqrtth ⊢ B ∈ ℝ ∧ 0 ≤ B → B 2 = B
11 9 10 breqan12d ⊢ A ∈ ℝ ∧ 0 ≤ A ∧ B ∈ ℝ ∧ 0 ≤ B → A 2 ≤ B 2 ↔ A ≤ B
12 8 11 bitr2d ⊢ A ∈ ℝ ∧ 0 ≤ A ∧ B ∈ ℝ ∧ 0 ≤ B → A ≤ B ↔ A ≤ B