Step |
Hyp |
Ref |
Expression |
1 |
|
simp1 |
|- ( ( A e. RR /\ B e. RR /\ ( C e. RR /\ 0 < C ) ) -> A e. RR ) |
2 |
|
simp3l |
|- ( ( A e. RR /\ B e. RR /\ ( C e. RR /\ 0 < C ) ) -> C e. RR ) |
3 |
1 2
|
remulcld |
|- ( ( A e. RR /\ B e. RR /\ ( C e. RR /\ 0 < C ) ) -> ( A x. C ) e. RR ) |
4 |
|
ltdiv1 |
|- ( ( ( A x. C ) e. RR /\ B e. RR /\ ( C e. RR /\ 0 < C ) ) -> ( ( A x. C ) < B <-> ( ( A x. C ) / C ) < ( B / C ) ) ) |
5 |
3 4
|
syld3an1 |
|- ( ( A e. RR /\ B e. RR /\ ( C e. RR /\ 0 < C ) ) -> ( ( A x. C ) < B <-> ( ( A x. C ) / C ) < ( B / C ) ) ) |
6 |
1
|
recnd |
|- ( ( A e. RR /\ B e. RR /\ ( C e. RR /\ 0 < C ) ) -> A e. CC ) |
7 |
2
|
recnd |
|- ( ( A e. RR /\ B e. RR /\ ( C e. RR /\ 0 < C ) ) -> C e. CC ) |
8 |
|
simp3r |
|- ( ( A e. RR /\ B e. RR /\ ( C e. RR /\ 0 < C ) ) -> 0 < C ) |
9 |
8
|
gt0ne0d |
|- ( ( A e. RR /\ B e. RR /\ ( C e. RR /\ 0 < C ) ) -> C =/= 0 ) |
10 |
6 7 9
|
divcan4d |
|- ( ( A e. RR /\ B e. RR /\ ( C e. RR /\ 0 < C ) ) -> ( ( A x. C ) / C ) = A ) |
11 |
10
|
breq1d |
|- ( ( A e. RR /\ B e. RR /\ ( C e. RR /\ 0 < C ) ) -> ( ( ( A x. C ) / C ) < ( B / C ) <-> A < ( B / C ) ) ) |
12 |
5 11
|
bitrd |
|- ( ( A e. RR /\ B e. RR /\ ( C e. RR /\ 0 < C ) ) -> ( ( A x. C ) < B <-> A < ( B / C ) ) ) |