Theorem muls1d

Description: Multiplication by one minus a number. (Contributed by Scott Fenton, 23-Dec-2017)

	Ref	Expression
Hypotheses	muls1d.1	⊢ ( 𝜑 → 𝐴 ∈ ℂ )
	muls1d.2	⊢ ( 𝜑 → 𝐵 ∈ ℂ )
Assertion	muls1d	⊢ ( 𝜑 → ( 𝐴 · ( 𝐵 − 1 ) ) = ( ( 𝐴 · 𝐵 ) − 𝐴 ) )

Proof

Step	Hyp	Ref	Expression
1		muls1d.1	⊢ ( 𝜑 → 𝐴 ∈ ℂ )
2		muls1d.2	⊢ ( 𝜑 → 𝐵 ∈ ℂ )
3		1cnd	⊢ ( 𝜑 → 1 ∈ ℂ )
4	1 2 3	subdid	⊢ ( 𝜑 → ( 𝐴 · ( 𝐵 − 1 ) ) = ( ( 𝐴 · 𝐵 ) − ( 𝐴 · 1 ) ) )
5	1	mulid1d	⊢ ( 𝜑 → ( 𝐴 · 1 ) = 𝐴 )
6	5	oveq2d	⊢ ( 𝜑 → ( ( 𝐴 · 𝐵 ) − ( 𝐴 · 1 ) ) = ( ( 𝐴 · 𝐵 ) − 𝐴 ) )
7	4 6	eqtrd	⊢ ( 𝜑 → ( 𝐴 · ( 𝐵 − 1 ) ) = ( ( 𝐴 · 𝐵 ) − 𝐴 ) )