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 ∈ ℝ ∧ 0 ≤ A ∧ B ∈ ℝ ∧ 0 ≤ B → A < B ↔ A < B

Proof

Step Hyp Ref Expression
1 sqrtle ⊢ B ∈ ℝ ∧ 0 ≤ B ∧ A ∈ ℝ ∧ 0 ≤ A → B ≤ A ↔ B ≤ A
2 1 ancoms ⊢ A ∈ ℝ ∧ 0 ≤ A ∧ B ∈ ℝ ∧ 0 ≤ B → B ≤ A ↔ B ≤ A
3 2 notbid ⊢ A ∈ ℝ ∧ 0 ≤ A ∧ B ∈ ℝ ∧ 0 ≤ B → ¬ B ≤ A ↔ ¬ B ≤ A
4 simpll ⊢ A ∈ ℝ ∧ 0 ≤ A ∧ B ∈ ℝ ∧ 0 ≤ B → A ∈ ℝ
5 simprl ⊢ A ∈ ℝ ∧ 0 ≤ A ∧ B ∈ ℝ ∧ 0 ≤ B → B ∈ ℝ
6 4 5 ltnled ⊢ A ∈ ℝ ∧ 0 ≤ A ∧ B ∈ ℝ ∧ 0 ≤ B → A < B ↔ ¬ B ≤ A
7 resqrtcl ⊢ A ∈ ℝ ∧ 0 ≤ A → A ∈ ℝ
8 7 adantr ⊢ A ∈ ℝ ∧ 0 ≤ A ∧ B ∈ ℝ ∧ 0 ≤ B → A ∈ ℝ
9 resqrtcl ⊢ B ∈ ℝ ∧ 0 ≤ B → B ∈ ℝ
10 9 adantl ⊢ A ∈ ℝ ∧ 0 ≤ A ∧ B ∈ ℝ ∧ 0 ≤ B → B ∈ ℝ
11 8 10 ltnled ⊢ A ∈ ℝ ∧ 0 ≤ A ∧ B ∈ ℝ ∧ 0 ≤ B → A < B ↔ ¬ B ≤ A
12 3 6 11 3bitr4d ⊢ A ∈ ℝ ∧ 0 ≤ A ∧ B ∈ ℝ ∧ 0 ≤ B → A < B ↔ A < B