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 e. RR /\ 0 <_ A ) /\ ( B e. RR /\ 0 <_ B ) ) -> ( A < B <-> ( sqrt ` A ) < ( sqrt ` B ) ) )

Proof

Step Hyp Ref Expression
1 sqrtle
 |-  ( ( ( B e. RR /\ 0 <_ B ) /\ ( A e. RR /\ 0 <_ A ) ) -> ( B <_ A <-> ( sqrt ` B ) <_ ( sqrt ` A ) ) )
2 1 ancoms
 |-  ( ( ( A e. RR /\ 0 <_ A ) /\ ( B e. RR /\ 0 <_ B ) ) -> ( B <_ A <-> ( sqrt ` B ) <_ ( sqrt ` A ) ) )
3 2 notbid
 |-  ( ( ( A e. RR /\ 0 <_ A ) /\ ( B e. RR /\ 0 <_ B ) ) -> ( -. B <_ A <-> -. ( sqrt ` B ) <_ ( sqrt ` A ) ) )
4 simpll
 |-  ( ( ( A e. RR /\ 0 <_ A ) /\ ( B e. RR /\ 0 <_ B ) ) -> A e. RR )
5 simprl
 |-  ( ( ( A e. RR /\ 0 <_ A ) /\ ( B e. RR /\ 0 <_ B ) ) -> B e. RR )
6 4 5 ltnled
 |-  ( ( ( A e. RR /\ 0 <_ A ) /\ ( B e. RR /\ 0 <_ B ) ) -> ( A < B <-> -. B <_ A ) )
7 resqrtcl
 |-  ( ( A e. RR /\ 0 <_ A ) -> ( sqrt ` A ) e. RR )
8 7 adantr
 |-  ( ( ( A e. RR /\ 0 <_ A ) /\ ( B e. RR /\ 0 <_ B ) ) -> ( sqrt ` A ) e. RR )
9 resqrtcl
 |-  ( ( B e. RR /\ 0 <_ B ) -> ( sqrt ` B ) e. RR )
10 9 adantl
 |-  ( ( ( A e. RR /\ 0 <_ A ) /\ ( B e. RR /\ 0 <_ B ) ) -> ( sqrt ` B ) e. RR )
11 8 10 ltnled
 |-  ( ( ( A e. RR /\ 0 <_ A ) /\ ( B e. RR /\ 0 <_ B ) ) -> ( ( sqrt ` A ) < ( sqrt ` B ) <-> -. ( sqrt ` B ) <_ ( sqrt ` A ) ) )
12 3 6 11 3bitr4d
 |-  ( ( ( A e. RR /\ 0 <_ A ) /\ ( B e. RR /\ 0 <_ B ) ) -> ( A < B <-> ( sqrt ` A ) < ( sqrt ` B ) ) )