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