This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem divcan5rd

Description: Cancellation of common factor in a ratio. (Contributed by Mario Carneiro, 1-Jan-2017)

Ref Expression
Hypotheses div1d.1 ⊢ φ → A ∈ ℂ
divcld.2 ⊢ φ → B ∈ ℂ
divmuld.3 ⊢ φ → C ∈ ℂ
divmuld.4 ⊢ φ → B ≠ 0
divdiv23d.5 ⊢ φ → C ≠ 0
Assertion divcan5rd ⊢ φ → A ⁢ C B ⁢ C = A B

Proof

Step Hyp Ref Expression
1 div1d.1 ⊢ φ → A ∈ ℂ
2 divcld.2 ⊢ φ → B ∈ ℂ
3 divmuld.3 ⊢ φ → C ∈ ℂ
4 divmuld.4 ⊢ φ → B ≠ 0
5 divdiv23d.5 ⊢ φ → C ≠ 0
6 1 3 mulcomd ⊢ φ → A ⁢ C = C ⁢ A
7 2 3 mulcomd ⊢ φ → B ⁢ C = C ⁢ B
8 6 7 oveq12d ⊢ φ → A ⁢ C B ⁢ C = C ⁢ A C ⁢ B
9 1 2 3 4 5 divcan5d ⊢ φ → C ⁢ A C ⁢ B = A B
10 8 9 eqtrd ⊢ φ → A ⁢ C B ⁢ C = A B