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