Metamath Proof Explorer

Theorem divcan5

Description: Cancellation of common factor in a ratio. (Contributed by NM, 9-Jan-2006)

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

Proof

Step Hyp Ref Expression
1 divid ⊢ C ∈ ℂ ∧ C ≠ 0 → C C = 1
2 1 oveq1d ⊢ C ∈ ℂ ∧ C ≠ 0 → C C ⁢ A B = 1 ⁢ A B
3 2 3ad2ant3 ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ B ≠ 0 ∧ C ∈ ℂ ∧ C ≠ 0 → C C ⁢ A B = 1 ⁢ A B
4 simp3l ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ B ≠ 0 ∧ C ∈ ℂ ∧ C ≠ 0 → C ∈ ℂ
5 simp1 ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ B ≠ 0 ∧ C ∈ ℂ ∧ C ≠ 0 → A ∈ ℂ
6 simp3 ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ B ≠ 0 ∧ C ∈ ℂ ∧ C ≠ 0 → C ∈ ℂ ∧ C ≠ 0
7 simp2 ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ B ≠ 0 ∧ C ∈ ℂ ∧ C ≠ 0 → B ∈ ℂ ∧ B ≠ 0
8 divmuldiv ⊢ C ∈ ℂ ∧ A ∈ ℂ ∧ C ∈ ℂ ∧ C ≠ 0 ∧ B ∈ ℂ ∧ B ≠ 0 → C C ⁢ A B = C ⁢ A C ⁢ B
9 4 5 6 7 8 syl22anc ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ B ≠ 0 ∧ C ∈ ℂ ∧ C ≠ 0 → C C ⁢ A B = C ⁢ A C ⁢ B
10 divcl ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ B ≠ 0 → A B ∈ ℂ
11 10 3expb ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ B ≠ 0 → A B ∈ ℂ
12 11 mulid2d ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ B ≠ 0 → 1 ⁢ A B = A B
13 12 3adant3 ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ B ≠ 0 ∧ C ∈ ℂ ∧ C ≠ 0 → 1 ⁢ A B = A B
14 3 9 13 3eqtr3d ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ B ≠ 0 ∧ C ∈ ℂ ∧ C ≠ 0 → C ⁢ A C ⁢ B = A B