# 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 ${⊢}{\phi }\to {A}\in ℂ$
divcld.2 ${⊢}{\phi }\to {B}\in ℂ$
divmuld.3 ${⊢}{\phi }\to {C}\in ℂ$
divmuldivd.4 ${⊢}{\phi }\to {D}\in ℂ$
divmuldivd.5 ${⊢}{\phi }\to {B}\ne 0$
divmuldivd.6 ${⊢}{\phi }\to {D}\ne 0$
Assertion divmuldivd ${⊢}{\phi }\to \left(\frac{{A}}{{B}}\right)\left(\frac{{C}}{{D}}\right)=\frac{{A}{C}}{{B}{D}}$

### Proof

Step Hyp Ref Expression
1 div1d.1 ${⊢}{\phi }\to {A}\in ℂ$
2 divcld.2 ${⊢}{\phi }\to {B}\in ℂ$
3 divmuld.3 ${⊢}{\phi }\to {C}\in ℂ$
4 divmuldivd.4 ${⊢}{\phi }\to {D}\in ℂ$
5 divmuldivd.5 ${⊢}{\phi }\to {B}\ne 0$
6 divmuldivd.6 ${⊢}{\phi }\to {D}\ne 0$
7 2 5 jca ${⊢}{\phi }\to \left({B}\in ℂ\wedge {B}\ne 0\right)$
8 4 6 jca ${⊢}{\phi }\to \left({D}\in ℂ\wedge {D}\ne 0\right)$
9 divmuldiv ${⊢}\left(\left({A}\in ℂ\wedge {C}\in ℂ\right)\wedge \left(\left({B}\in ℂ\wedge {B}\ne 0\right)\wedge \left({D}\in ℂ\wedge {D}\ne 0\right)\right)\right)\to \left(\frac{{A}}{{B}}\right)\left(\frac{{C}}{{D}}\right)=\frac{{A}{C}}{{B}{D}}$
10 1 3 7 8 9 syl22anc ${⊢}{\phi }\to \left(\frac{{A}}{{B}}\right)\left(\frac{{C}}{{D}}\right)=\frac{{A}{C}}{{B}{D}}$