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 ) ) → ( ( 𝐶 · 𝐴 ) / ( 𝐶 · 𝐵 ) ) = ( 𝐴 / 𝐵 ) )