Theorem muls1d

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

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

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 2 3	subdid	|- ( ph -> ( A x. ( B - 1 ) ) = ( ( A x. B ) - ( A x. 1 ) ) )
5	1	mulid1d	|- ( ph -> ( A x. 1 ) = A )
6	5	oveq2d	|- ( ph -> ( ( A x. B ) - ( A x. 1 ) ) = ( ( A x. B ) - A ) )
7	4 6	eqtrd	|- ( ph -> ( A x. ( B - 1 ) ) = ( ( A x. B ) - A ) )