Metamath Proof Explorer

Theorem sqrtlt

Description: Square root is strictly monotonic. Closed form of sqrtlti . (Contributed by Scott Fenton, 17-Apr-2014) (Proof shortened by Mario Carneiro, 29-May-2016)

		Ref	Expression
	Assertion	sqrtlt	$⊢ ((A \in ℝ \land 0 \leq A) \land (B \in ℝ \land 0 \leq B)) \to (A < B \leftrightarrow \sqrt{A} < \sqrt{B})$

Proof

Step	Hyp	Ref	Expression
1		sqrtle	$⊢ ((B \in ℝ \land 0 \leq B) \land (A \in ℝ \land 0 \leq A)) \to (B \leq A \leftrightarrow \sqrt{B} \leq \sqrt{A})$
2	1	ancoms	$⊢ ((A \in ℝ \land 0 \leq A) \land (B \in ℝ \land 0 \leq B)) \to (B \leq A \leftrightarrow \sqrt{B} \leq \sqrt{A})$
3	2	notbid	$⊢ ((A \in ℝ \land 0 \leq A) \land (B \in ℝ \land 0 \leq B)) \to (\neg B \leq A \leftrightarrow \neg \sqrt{B} \leq \sqrt{A})$
4		simpll	$⊢ ((A \in ℝ \land 0 \leq A) \land (B \in ℝ \land 0 \leq B)) \to A \in ℝ$
5		simprl	$⊢ ((A \in ℝ \land 0 \leq A) \land (B \in ℝ \land 0 \leq B)) \to B \in ℝ$
6	4 5	ltnled	$⊢ ((A \in ℝ \land 0 \leq A) \land (B \in ℝ \land 0 \leq B)) \to (A < B \leftrightarrow \neg B \leq A)$
7		resqrtcl	$⊢ (A \in ℝ \land 0 \leq A) \to \sqrt{A} \in ℝ$
8	7	adantr	$⊢ ((A \in ℝ \land 0 \leq A) \land (B \in ℝ \land 0 \leq B)) \to \sqrt{A} \in ℝ$
9		resqrtcl	$⊢ (B \in ℝ \land 0 \leq B) \to \sqrt{B} \in ℝ$
10	9	adantl	$⊢ ((A \in ℝ \land 0 \leq A) \land (B \in ℝ \land 0 \leq B)) \to \sqrt{B} \in ℝ$
11	8 10	ltnled	$⊢ ((A \in ℝ \land 0 \leq A) \land (B \in ℝ \land 0 \leq B)) \to (\sqrt{A} < \sqrt{B} \leftrightarrow \neg \sqrt{B} \leq \sqrt{A})$
12	3 6 11	3bitr4d	$⊢ ((A \in ℝ \land 0 \leq A) \land (B \in ℝ \land 0 \leq B)) \to (A < B \leftrightarrow \sqrt{A} < \sqrt{B})$