Metamath Proof Explorer


Theorem sn-ltmul2d

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

Ref Expression
Hypotheses sn-ltmul2d.a φ A
sn-ltmul2d.b φ B
sn-ltmul2d.c φ C
sn-ltmul2d.1 φ 0 < C
Assertion sn-ltmul2d φ C A < C B A < B

Proof

Step Hyp Ref Expression
1 sn-ltmul2d.a φ A
2 sn-ltmul2d.b φ B
3 sn-ltmul2d.c φ C
4 sn-ltmul2d.1 φ 0 < C
5 rersubcl B A B - A
6 2 1 5 syl2anc φ B - A
7 3 6 4 mulgt0b2d φ 0 < B - A 0 < C B - A
8 resubdi C B A C B - A = C B - C A
9 3 2 1 8 syl3anc φ C B - A = C B - C A
10 9 breq2d φ 0 < C B - A 0 < C B - C A
11 7 10 bitr2d φ 0 < C B - C A 0 < B - A
12 3 1 remulcld φ C A
13 3 2 remulcld φ C B
14 reposdif C A C B C A < C B 0 < C B - C A
15 12 13 14 syl2anc φ C A < C B 0 < C B - C A
16 reposdif A B A < B 0 < B - A
17 1 2 16 syl2anc φ A < B 0 < B - A
18 11 15 17 3bitr4d φ C A < C B A < B