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→ACBC=AB

Proof

Step Hyp Ref Expression
1 divdivdiv ⊢A∈ℂ∧C∈ℂ∧C≠0∧B∈ℂ∧B≠0∧C∈ℂ∧C≠0→ACBC=A⁢CC⁢B
2 1 3impdir ⊢A∈ℂ∧B∈ℂ∧B≠0∧C∈ℂ∧C≠0→ACBC=A⁢CC⁢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⁢CC⁢B=C⁢AC⁢B
7 divcan5 ⊢A∈ℂ∧B∈ℂ∧B≠0∧C∈ℂ∧C≠0→C⁢AC⁢B=AB
8 2 6 7 3eqtrd ⊢A∈ℂ∧B∈ℂ∧B≠0∧C∈ℂ∧C≠0→ACBC=AB