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

Metamath Proof Explorer

Theorem divcan5

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

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

Proof

Step Hyp Ref Expression
1 divid ⊢ ( ( 𝐶 ∈ ℂ ∧ 𝐶 ≠ 0 ) → ( 𝐶 / 𝐶 ) = 1 )
2 1 oveq1d ⊢ ( ( 𝐶 ∈ ℂ ∧ 𝐶 ≠ 0 ) → ( ( 𝐶 / 𝐶 ) · ( 𝐴 / 𝐵 ) ) = ( 1 · ( 𝐴 / 𝐵 ) ) )
3 2 3ad2ant3 ⊢ ( ( 𝐴 ∈ ℂ ∧ ( 𝐵 ∈ ℂ ∧ 𝐵 ≠ 0 ) ∧ ( 𝐶 ∈ ℂ ∧ 𝐶 ≠ 0 ) ) → ( ( 𝐶 / 𝐶 ) · ( 𝐴 / 𝐵 ) ) = ( 1 · ( 𝐴 / 𝐵 ) ) )
4 simp3l ⊢ ( ( 𝐴 ∈ ℂ ∧ ( 𝐵 ∈ ℂ ∧ 𝐵 ≠ 0 ) ∧ ( 𝐶 ∈ ℂ ∧ 𝐶 ≠ 0 ) ) → 𝐶 ∈ ℂ )
5 simp1 ⊢ ( ( 𝐴 ∈ ℂ ∧ ( 𝐵 ∈ ℂ ∧ 𝐵 ≠ 0 ) ∧ ( 𝐶 ∈ ℂ ∧ 𝐶 ≠ 0 ) ) → 𝐴 ∈ ℂ )
6 simp3 ⊢ ( ( 𝐴 ∈ ℂ ∧ ( 𝐵 ∈ ℂ ∧ 𝐵 ≠ 0 ) ∧ ( 𝐶 ∈ ℂ ∧ 𝐶 ≠ 0 ) ) → ( 𝐶 ∈ ℂ ∧ 𝐶 ≠ 0 ) )
7 simp2 ⊢ ( ( 𝐴 ∈ ℂ ∧ ( 𝐵 ∈ ℂ ∧ 𝐵 ≠ 0 ) ∧ ( 𝐶 ∈ ℂ ∧ 𝐶 ≠ 0 ) ) → ( 𝐵 ∈ ℂ ∧ 𝐵 ≠ 0 ) )
8 divmuldiv ⊢ ( ( ( 𝐶 ∈ ℂ ∧ 𝐴 ∈ ℂ ) ∧ ( ( 𝐶 ∈ ℂ ∧ 𝐶 ≠ 0 ) ∧ ( 𝐵 ∈ ℂ ∧ 𝐵 ≠ 0 ) ) ) → ( ( 𝐶 / 𝐶 ) · ( 𝐴 / 𝐵 ) ) = ( ( 𝐶 · 𝐴 ) / ( 𝐶 · 𝐵 ) ) )
9 4 5 6 7 8 syl22anc ⊢ ( ( 𝐴 ∈ ℂ ∧ ( 𝐵 ∈ ℂ ∧ 𝐵 ≠ 0 ) ∧ ( 𝐶 ∈ ℂ ∧ 𝐶 ≠ 0 ) ) → ( ( 𝐶 / 𝐶 ) · ( 𝐴 / 𝐵 ) ) = ( ( 𝐶 · 𝐴 ) / ( 𝐶 · 𝐵 ) ) )
10 divcl ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐵 ≠ 0 ) → ( 𝐴 / 𝐵 ) ∈ ℂ )
11 10 3expb ⊢ ( ( 𝐴 ∈ ℂ ∧ ( 𝐵 ∈ ℂ ∧ 𝐵 ≠ 0 ) ) → ( 𝐴 / 𝐵 ) ∈ ℂ )
12 11 mullidd ⊢ ( ( 𝐴 ∈ ℂ ∧ ( 𝐵 ∈ ℂ ∧ 𝐵 ≠ 0 ) ) → ( 1 · ( 𝐴 / 𝐵 ) ) = ( 𝐴 / 𝐵 ) )
13 12 3adant3 ⊢ ( ( 𝐴 ∈ ℂ ∧ ( 𝐵 ∈ ℂ ∧ 𝐵 ≠ 0 ) ∧ ( 𝐶 ∈ ℂ ∧ 𝐶 ≠ 0 ) ) → ( 1 · ( 𝐴 / 𝐵 ) ) = ( 𝐴 / 𝐵 ) )
14 3 9 13 3eqtr3d ⊢ ( ( 𝐴 ∈ ℂ ∧ ( 𝐵 ∈ ℂ ∧ 𝐵 ≠ 0 ) ∧ ( 𝐶 ∈ ℂ ∧ 𝐶 ≠ 0 ) ) → ( ( 𝐶 · 𝐴 ) / ( 𝐶 · 𝐵 ) ) = ( 𝐴 / 𝐵 ) )