| Step |
Hyp |
Ref |
Expression |
| 1 |
|
sn-ltmul2d.a |
|- ( ph -> A e. RR ) |
| 2 |
|
sn-ltmul2d.b |
|- ( ph -> B e. RR ) |
| 3 |
|
sn-ltmul2d.c |
|- ( ph -> C e. RR ) |
| 4 |
|
sn-ltmul2d.1 |
|- ( ph -> 0 < C ) |
| 5 |
|
rersubcl |
|- ( ( B e. RR /\ A e. RR ) -> ( B -R A ) e. RR ) |
| 6 |
2 1 5
|
syl2anc |
|- ( ph -> ( B -R A ) e. RR ) |
| 7 |
3 6 4
|
mulgt0b1d |
|- ( ph -> ( 0 < ( B -R A ) <-> 0 < ( C x. ( B -R A ) ) ) ) |
| 8 |
|
resubdi |
|- ( ( C e. RR /\ B e. RR /\ A e. RR ) -> ( C x. ( B -R A ) ) = ( ( C x. B ) -R ( C x. A ) ) ) |
| 9 |
3 2 1 8
|
syl3anc |
|- ( ph -> ( C x. ( B -R A ) ) = ( ( C x. B ) -R ( C x. A ) ) ) |
| 10 |
9
|
breq2d |
|- ( ph -> ( 0 < ( C x. ( B -R A ) ) <-> 0 < ( ( C x. B ) -R ( C x. A ) ) ) ) |
| 11 |
7 10
|
bitr2d |
|- ( ph -> ( 0 < ( ( C x. B ) -R ( C x. A ) ) <-> 0 < ( B -R A ) ) ) |
| 12 |
3 1
|
remulcld |
|- ( ph -> ( C x. A ) e. RR ) |
| 13 |
3 2
|
remulcld |
|- ( ph -> ( C x. B ) e. RR ) |
| 14 |
|
reposdif |
|- ( ( ( C x. A ) e. RR /\ ( C x. B ) e. RR ) -> ( ( C x. A ) < ( C x. B ) <-> 0 < ( ( C x. B ) -R ( C x. A ) ) ) ) |
| 15 |
12 13 14
|
syl2anc |
|- ( ph -> ( ( C x. A ) < ( C x. B ) <-> 0 < ( ( C x. B ) -R ( C x. A ) ) ) ) |
| 16 |
|
reposdif |
|- ( ( A e. RR /\ B e. RR ) -> ( A < B <-> 0 < ( B -R A ) ) ) |
| 17 |
1 2 16
|
syl2anc |
|- ( ph -> ( A < B <-> 0 < ( B -R A ) ) ) |
| 18 |
11 15 17
|
3bitr4d |
|- ( ph -> ( ( C x. A ) < ( C x. B ) <-> A < B ) ) |