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

Metamath Proof Explorer

Theorem divcan7

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

Ref Expression
Assertion divcan7 ( ( 𝐴 ∈ ℂ ∧ ( 𝐵 ∈ ℂ ∧ 𝐵 ≠ 0 ) ∧ ( 𝐶 ∈ ℂ ∧ 𝐶 ≠ 0 ) ) → ( ( 𝐴 / 𝐶 ) / ( 𝐵 / 𝐶 ) ) = ( 𝐴 / 𝐵 ) )

Proof

Step Hyp Ref Expression
1 divdivdiv ⊢ ( ( ( 𝐴 ∈ ℂ ∧ ( 𝐶 ∈ ℂ ∧ 𝐶 ≠ 0 ) ) ∧ ( ( 𝐵 ∈ ℂ ∧ 𝐵 ≠ 0 ) ∧ ( 𝐶 ∈ ℂ ∧ 𝐶 ≠ 0 ) ) ) → ( ( 𝐴 / 𝐶 ) / ( 𝐵 / 𝐶 ) ) = ( ( 𝐴 · 𝐶 ) / ( 𝐶 · 𝐵 ) ) )
2 1 3impdir ⊢ ( ( 𝐴 ∈ ℂ ∧ ( 𝐵 ∈ ℂ ∧ 𝐵 ≠ 0 ) ∧ ( 𝐶 ∈ ℂ ∧ 𝐶 ≠ 0 ) ) → ( ( 𝐴 / 𝐶 ) / ( 𝐵 / 𝐶 ) ) = ( ( 𝐴 · 𝐶 ) / ( 𝐶 · 𝐵 ) ) )
3 mulcom ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐶 ∈ ℂ ) → ( 𝐴 · 𝐶 ) = ( 𝐶 · 𝐴 ) )
4 3 adantrr ⊢ ( ( 𝐴 ∈ ℂ ∧ ( 𝐶 ∈ ℂ ∧ 𝐶 ≠ 0 ) ) → ( 𝐴 · 𝐶 ) = ( 𝐶 · 𝐴 ) )
5 4 3adant2 ⊢ ( ( 𝐴 ∈ ℂ ∧ ( 𝐵 ∈ ℂ ∧ 𝐵 ≠ 0 ) ∧ ( 𝐶 ∈ ℂ ∧ 𝐶 ≠ 0 ) ) → ( 𝐴 · 𝐶 ) = ( 𝐶 · 𝐴 ) )
6 5 oveq1d ⊢ ( ( 𝐴 ∈ ℂ ∧ ( 𝐵 ∈ ℂ ∧ 𝐵 ≠ 0 ) ∧ ( 𝐶 ∈ ℂ ∧ 𝐶 ≠ 0 ) ) → ( ( 𝐴 · 𝐶 ) / ( 𝐶 · 𝐵 ) ) = ( ( 𝐶 · 𝐴 ) / ( 𝐶 · 𝐵 ) ) )
7 divcan5 ⊢ ( ( 𝐴 ∈ ℂ ∧ ( 𝐵 ∈ ℂ ∧ 𝐵 ≠ 0 ) ∧ ( 𝐶 ∈ ℂ ∧ 𝐶 ≠ 0 ) ) → ( ( 𝐶 · 𝐴 ) / ( 𝐶 · 𝐵 ) ) = ( 𝐴 / 𝐵 ) )
8 2 6 7 3eqtrd ⊢ ( ( 𝐴 ∈ ℂ ∧ ( 𝐵 ∈ ℂ ∧ 𝐵 ≠ 0 ) ∧ ( 𝐶 ∈ ℂ ∧ 𝐶 ≠ 0 ) ) → ( ( 𝐴 / 𝐶 ) / ( 𝐵 / 𝐶 ) ) = ( 𝐴 / 𝐵 ) )