Theorem binom2subi

Description: Expand the square of a subtraction. (Contributed by Scott Fenton, 13-Jun-2013)

	Ref	Expression
Hypotheses	binom2subi.1	$$⊢A\in ℂ$$
	binom2subi.2	$$⊢B\in ℂ$$
Assertion	binom2subi	$$⊢{\left(A-B\right)}^2=A^2-2AB+B^2$$

Proof

Step	Hyp	Ref	Expression
1		binom2subi.1	$$⊢A\in ℂ$$
2		binom2subi.2	$$⊢B\in ℂ$$
3		binom2sub	$$⊢\left(A\in ℂ\wedge B\in ℂ\right)\to {\left(A-B\right)}^2=A^2-2AB+B^2$$
4	1 2 3	mp2an	$$⊢{\left(A-B\right)}^2=A^2-2AB+B^2$$