Metamath Proof Explorer

Theorem divmul24

Description: Swap the numerators in the product of two ratios. (Contributed by NM, 3-May-2005)

Ref Expression
Assertion divmul24 ⊢A∈ℂ∧B∈ℂ∧C∈ℂ∧C≠0∧D∈ℂ∧D≠0→AC⁢BD=AD⁢BC

Proof

Step Hyp Ref Expression
1 mulcom ⊢C∈ℂ∧D∈ℂ→C⁢D=D⁢C
2 1 ad2ant2r ⊢C∈ℂ∧C≠0∧D∈ℂ∧D≠0→C⁢D=D⁢C
3 2 adantl ⊢A∈ℂ∧B∈ℂ∧C∈ℂ∧C≠0∧D∈ℂ∧D≠0→C⁢D=D⁢C
4 3 oveq2d ⊢A∈ℂ∧B∈ℂ∧C∈ℂ∧C≠0∧D∈ℂ∧D≠0→A⁢BC⁢D=A⁢BD⁢C
5 divmuldiv ⊢A∈ℂ∧B∈ℂ∧C∈ℂ∧C≠0∧D∈ℂ∧D≠0→AC⁢BD=A⁢BC⁢D
6 divmuldiv ⊢A∈ℂ∧B∈ℂ∧D∈ℂ∧D≠0∧C∈ℂ∧C≠0→AD⁢BC=A⁢BD⁢C
7 6 ancom2s ⊢A∈ℂ∧B∈ℂ∧C∈ℂ∧C≠0∧D∈ℂ∧D≠0→AD⁢BC=A⁢BD⁢C
8 4 5 7 3eqtr4d ⊢A∈ℂ∧B∈ℂ∧C∈ℂ∧C≠0∧D∈ℂ∧D≠0→AC⁢BD=AD⁢BC