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 → A C ⁢ B D = A D ⁢ B C

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 ⁢ B C ⁢ D = A ⁢ B D ⁢ C
5 divmuldiv ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ C ∈ ℂ ∧ C ≠ 0 ∧ D ∈ ℂ ∧ D ≠ 0 → A C ⁢ B D = A ⁢ B C ⁢ D
6 divmuldiv ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ D ∈ ℂ ∧ D ≠ 0 ∧ C ∈ ℂ ∧ C ≠ 0 → A D ⁢ B C = A ⁢ B D ⁢ C
7 6 ancom2s ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ C ∈ ℂ ∧ C ≠ 0 ∧ D ∈ ℂ ∧ D ≠ 0 → A D ⁢ B C = A ⁢ B D ⁢ C
8 4 5 7 3eqtr4d ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ C ∈ ℂ ∧ C ≠ 0 ∧ D ∈ ℂ ∧ D ≠ 0 → A C ⁢ B D = A D ⁢ B C