Step |
Hyp |
Ref |
Expression |
1 |
|
ltdivmul2 |
|- ( ( B e. RR /\ A e. RR /\ ( C e. RR /\ 0 < C ) ) -> ( ( B / C ) < A <-> B < ( A x. C ) ) ) |
2 |
1
|
3com12 |
|- ( ( A e. RR /\ B e. RR /\ ( C e. RR /\ 0 < C ) ) -> ( ( B / C ) < A <-> B < ( A x. C ) ) ) |
3 |
2
|
notbid |
|- ( ( A e. RR /\ B e. RR /\ ( C e. RR /\ 0 < C ) ) -> ( -. ( B / C ) < A <-> -. B < ( A x. C ) ) ) |
4 |
|
simp1 |
|- ( ( A e. RR /\ B e. RR /\ ( C e. RR /\ 0 < C ) ) -> A e. RR ) |
5 |
|
gt0ne0 |
|- ( ( C e. RR /\ 0 < C ) -> C =/= 0 ) |
6 |
5
|
3adant1 |
|- ( ( B e. RR /\ C e. RR /\ 0 < C ) -> C =/= 0 ) |
7 |
|
redivcl |
|- ( ( B e. RR /\ C e. RR /\ C =/= 0 ) -> ( B / C ) e. RR ) |
8 |
6 7
|
syld3an3 |
|- ( ( B e. RR /\ C e. RR /\ 0 < C ) -> ( B / C ) e. RR ) |
9 |
8
|
3expb |
|- ( ( B e. RR /\ ( C e. RR /\ 0 < C ) ) -> ( B / C ) e. RR ) |
10 |
9
|
3adant1 |
|- ( ( A e. RR /\ B e. RR /\ ( C e. RR /\ 0 < C ) ) -> ( B / C ) e. RR ) |
11 |
4 10
|
lenltd |
|- ( ( A e. RR /\ B e. RR /\ ( C e. RR /\ 0 < C ) ) -> ( A <_ ( B / C ) <-> -. ( B / C ) < A ) ) |
12 |
|
remulcl |
|- ( ( A e. RR /\ C e. RR ) -> ( A x. C ) e. RR ) |
13 |
12
|
3adant2 |
|- ( ( A e. RR /\ B e. RR /\ C e. RR ) -> ( A x. C ) e. RR ) |
14 |
|
simp2 |
|- ( ( A e. RR /\ B e. RR /\ C e. RR ) -> B e. RR ) |
15 |
13 14
|
lenltd |
|- ( ( A e. RR /\ B e. RR /\ C e. RR ) -> ( ( A x. C ) <_ B <-> -. B < ( A x. C ) ) ) |
16 |
15
|
3adant3r |
|- ( ( A e. RR /\ B e. RR /\ ( C e. RR /\ 0 < C ) ) -> ( ( A x. C ) <_ B <-> -. B < ( A x. C ) ) ) |
17 |
3 11 16
|
3bitr4rd |
|- ( ( A e. RR /\ B e. RR /\ ( C e. RR /\ 0 < C ) ) -> ( ( A x. C ) <_ B <-> A <_ ( B / C ) ) ) |