Metamath Proof Explorer


Theorem sqrtltd

Description: Square root is strictly monotonic. (Contributed by Mario Carneiro, 29-May-2016)

Ref Expression
Hypotheses resqrcld.1 φ A
resqrcld.2 φ 0 A
sqr11d.3 φ B
sqr11d.4 φ 0 B
Assertion sqrtltd φ A < B A < B

Proof

Step Hyp Ref Expression
1 resqrcld.1 φ A
2 resqrcld.2 φ 0 A
3 sqr11d.3 φ B
4 sqr11d.4 φ 0 B
5 sqrtlt A 0 A B 0 B A < B A < B
6 1 2 3 4 5 syl22anc φ A < B A < B