Metamath Proof Explorer


Theorem divmuldivd

Description: Multiplication of two ratios. Theorem I.14 of Apostol p. 18. (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 divmuldivd φ A B C D = A C B D

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 divmuldiv A C B B 0 D D 0 A B C D = A C B D
10 1 3 7 8 9 syl22anc φ A B C D = A C B D