Theorem binom2sub1

Description: Special case of binom2sub where B = 1 . (Contributed by AV, 2-Aug-2021)

	Ref	Expression
Assertion	binom2sub1	$$⊢A\in ℂ\to {\left(A-1\right)}^2=A^2-2A+1$$

Proof

Step	Hyp	Ref	Expression
1		1cnd	$$⊢A\in ℂ\to 1\in ℂ$$
2		binom2sub	$$⊢\left(A\in ℂ\wedge 1\in ℂ\right)\to {\left(A-1\right)}^2=A^2-2A\cdot 1+1^2$$
3	1 2	mpdan	$$⊢A\in ℂ\to {\left(A-1\right)}^2=A^2-2A\cdot 1+1^2$$
4		mulrid	$$⊢A\in ℂ\to A\cdot 1=A$$
5	4	oveq2d	$$⊢A\in ℂ\to 2A\cdot 1=2A$$
6	5	oveq2d	$$⊢A\in ℂ\to A^2-2A\cdot 1=A^2-2A$$
7		sq1	$$⊢1^2=1$$
8	7	a1i	$$⊢A\in ℂ\to 1^2=1$$
9	6 8	oveq12d	$$⊢A\in ℂ\to A^2-2A\cdot 1+1^2=A^2-2A+1$$
10	3 9	eqtrd	$$⊢A\in ℂ\to {\left(A-1\right)}^2=A^2-2A+1$$