Theorem mulsubfacd

Description: Multiplication followed by the subtraction of a factor. (Contributed by Alexander van der Vekens, 28-Aug-2018)

	Ref	Expression
Hypotheses	muls1d.1	|- ( ph -> A e. CC )
	muls1d.2	|- ( ph -> B e. CC )
Assertion	mulsubfacd	|- ( ph -> ( ( A x. B ) - B ) = ( ( A - 1 ) x. B ) )

Proof

Step	Hyp	Ref	Expression
1		muls1d.1	|- ( ph -> A e. CC )
2		muls1d.2	|- ( ph -> B e. CC )
3		1cnd	|- ( ph -> 1 e. CC )
4	1 3 2	subdird	|- ( ph -> ( ( A - 1 ) x. B ) = ( ( A x. B ) - ( 1 x. B ) ) )
5	2	mulid2d	|- ( ph -> ( 1 x. B ) = B )
6	5	oveq2d	|- ( ph -> ( ( A x. B ) - ( 1 x. B ) ) = ( ( A x. B ) - B ) )
7	4 6	eqtr2d	|- ( ph -> ( ( A x. B ) - B ) = ( ( A - 1 ) x. B ) )