Metamath Proof Explorer


Theorem sn-ltmul2d

Description: ltmul2d without ax-mulcom . (Contributed by SN, 26-Jun-2024)

Ref Expression
Hypotheses sn-ltmul2d.a
|- ( ph -> A e. RR )
sn-ltmul2d.b
|- ( ph -> B e. RR )
sn-ltmul2d.c
|- ( ph -> C e. RR )
sn-ltmul2d.1
|- ( ph -> 0 < C )
Assertion sn-ltmul2d
|- ( ph -> ( ( C x. A ) < ( C x. B ) <-> A < B ) )

Proof

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