Metamath Proof Explorer

Theorem divmul13

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

Ref Expression
Assertion divmul13 ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ C ∈ ℂ ∧ C ≠ 0 ∧ D ∈ ℂ ∧ D ≠ 0 → A C ⁢ B D = B C ⁢ A D

Proof

Step Hyp Ref Expression
1 mulcom ⊢ A ∈ ℂ ∧ B ∈ ℂ → A ⁢ B = B ⁢ A
2 1 adantr ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ C ∈ ℂ ∧ C ≠ 0 ∧ D ∈ ℂ ∧ D ≠ 0 → A ⁢ B = B ⁢ A
3 2 oveq1d ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ C ∈ ℂ ∧ C ≠ 0 ∧ D ∈ ℂ ∧ D ≠ 0 → A ⁢ B C ⁢ D = B ⁢ A C ⁢ D
4 divmuldiv ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ C ∈ ℂ ∧ C ≠ 0 ∧ D ∈ ℂ ∧ D ≠ 0 → A C ⁢ B D = A ⁢ B C ⁢ D
5 divmuldiv ⊢ B ∈ ℂ ∧ A ∈ ℂ ∧ C ∈ ℂ ∧ C ≠ 0 ∧ D ∈ ℂ ∧ D ≠ 0 → B C ⁢ A D = B ⁢ A C ⁢ D
6 5 ancom1s ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ C ∈ ℂ ∧ C ≠ 0 ∧ D ∈ ℂ ∧ D ≠ 0 → B C ⁢ A D = B ⁢ A C ⁢ D
7 3 4 6 3eqtr4d ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ C ∈ ℂ ∧ C ≠ 0 ∧ D ∈ ℂ ∧ D ≠ 0 → A C ⁢ B D = B C ⁢ A D