Metamath Proof Explorer

Theorem divcan7

Description: Cancel equal divisors in a division. (Contributed by Jeff Hankins, 29-Sep-2013)

Ref Expression
Assertion divcan7 ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ B ≠ 0 ∧ C ∈ ℂ ∧ C ≠ 0 → A C B C = A B

Proof

Step Hyp Ref Expression
1 divdivdiv ⊢ A ∈ ℂ ∧ C ∈ ℂ ∧ C ≠ 0 ∧ B ∈ ℂ ∧ B ≠ 0 ∧ C ∈ ℂ ∧ C ≠ 0 → A C B C = A ⁢ C C ⁢ B
2 1 3impdir ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ B ≠ 0 ∧ C ∈ ℂ ∧ C ≠ 0 → A C B C = A ⁢ C C ⁢ B
3 mulcom ⊢ A ∈ ℂ ∧ C ∈ ℂ → A ⁢ C = C ⁢ A
4 3 adantrr ⊢ A ∈ ℂ ∧ C ∈ ℂ ∧ C ≠ 0 → A ⁢ C = C ⁢ A
5 4 3adant2 ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ B ≠ 0 ∧ C ∈ ℂ ∧ C ≠ 0 → A ⁢ C = C ⁢ A
6 5 oveq1d ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ B ≠ 0 ∧ C ∈ ℂ ∧ C ≠ 0 → A ⁢ C C ⁢ B = C ⁢ A C ⁢ B
7 divcan5 ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ B ≠ 0 ∧ C ∈ ℂ ∧ C ≠ 0 → C ⁢ A C ⁢ B = A B
8 2 6 7 3eqtrd ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ B ≠ 0 ∧ C ∈ ℂ ∧ C ≠ 0 → A C B C = A B