Metamath Proof Explorer


Theorem divmuleqd

Description: Cross-multiply in an equality of ratios. (Contributed by Mario Carneiro, 27-May-2016)

Ref Expression
Hypotheses div1d.1 φ A
divcld.2 φ B
divmuld.3 φ C
divmuldivd.4 φ D
divmuldivd.5 φ B 0
divmuldivd.6 φ D 0
Assertion divmuleqd φ A B = C D A D = C B

Proof

Step Hyp Ref Expression
1 div1d.1 φ A
2 divcld.2 φ B
3 divmuld.3 φ C
4 divmuldivd.4 φ D
5 divmuldivd.5 φ B 0
6 divmuldivd.6 φ D 0
7 2 5 jca φ B B 0
8 4 6 jca φ D D 0
9 divmuleq A C B B 0 D D 0 A B = C D A D = C B
10 1 3 7 8 9 syl22anc φ A B = C D A D = C B