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 ) ) )