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 \in ℝ \land 0 \leq A) \land (B \in ℝ \land 0 \leq B)) \to (A \leq B \leftrightarrow \sqrt{A} \leq \sqrt{B})$

Step	Hyp	Ref	Expression
1		resqrtcl	$⊢ (A \in ℝ \land 0 \leq A) \to \sqrt{A} \in ℝ$
2		sqrtge0	$⊢ (A \in ℝ \land 0 \leq A) \to 0 \leq \sqrt{A}$
3	1 2	jca	$⊢ (A \in ℝ \land 0 \leq A) \to (\sqrt{A} \in ℝ \land 0 \leq \sqrt{A})$
4		resqrtcl	$⊢ (B \in ℝ \land 0 \leq B) \to \sqrt{B} \in ℝ$
5		sqrtge0	$⊢ (B \in ℝ \land 0 \leq B) \to 0 \leq \sqrt{B}$
6	4 5	jca	$⊢ (B \in ℝ \land 0 \leq B) \to (\sqrt{B} \in ℝ \land 0 \leq \sqrt{B})$
7		le2sq	$⊢ ((\sqrt{A} \in ℝ \land 0 \leq \sqrt{A}) \land (\sqrt{B} \in ℝ \land 0 \leq \sqrt{B})) \to (\sqrt{A} \leq \sqrt{B} \leftrightarrow {\sqrt{A}}^{2} \leq {\sqrt{B}}^{2})$
8	3 6 7	syl2an	$⊢ ((A \in ℝ \land 0 \leq A) \land (B \in ℝ \land 0 \leq B)) \to (\sqrt{A} \leq \sqrt{B} \leftrightarrow {\sqrt{A}}^{2} \leq {\sqrt{B}}^{2})$
9		resqrtth	$⊢ (A \in ℝ \land 0 \leq A) \to {\sqrt{A}}^{2} = A$
10		resqrtth	$⊢ (B \in ℝ \land 0 \leq B) \to {\sqrt{B}}^{2} = B$
11	9 10	breqan12d	$⊢ ((A \in ℝ \land 0 \leq A) \land (B \in ℝ \land 0 \leq B)) \to ({\sqrt{A}}^{2} \leq {\sqrt{B}}^{2} \leftrightarrow A \leq B)$
12	8 11	bitr2d	$⊢ ((A \in ℝ \land 0 \leq A) \land (B \in ℝ \land 0 \leq B)) \to (A \leq B \leftrightarrow \sqrt{A} \leq \sqrt{B})$

Metamath Proof Explorer