Theorem binom2subadd

Description: The difference of the squares of the sum and difference of two complex numbers A and B . (Contributed by Thierry Arnoux, 5-Nov-2025)

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

Proof

Step	Hyp	Ref	Expression
1		binom2subadd.1	$$⊢\phi \to A\in ℂ$$
2		binom2subadd.2	$$⊢\phi \to B\in ℂ$$
3	1 2	addcld	$$⊢\phi \to A+B\in ℂ$$
4	1 2	subcld	$$⊢\phi \to A-B\in ℂ$$
5		subsq	$$⊢\left(A+B\in ℂ\wedge A-B\in ℂ\right)\to {\left(A+B\right)}^2-{\left(A-B\right)}^2=\left(A+B+\left(A-B\right)\right)\left(A+B-\left(A-B\right)\right)$$
6	3 4 5	syl2anc	$$⊢\phi \to {\left(A+B\right)}^2-{\left(A-B\right)}^2=\left(A+B+\left(A-B\right)\right)\left(A+B-\left(A-B\right)\right)$$
7	1 2 1	ppncand	$$⊢\phi \to A+B+\left(A-B\right)=A+A$$
8	1	2timesd	$$⊢\phi \to 2A=A+A$$
9	7 8	eqtr4d	$$⊢\phi \to A+B+\left(A-B\right)=2A$$
10	1 2 2	pnncand	$$⊢\phi \to A+B-\left(A-B\right)=B+B$$
11	2	2timesd	$$⊢\phi \to 2B=B+B$$
12	10 11	eqtr4d	$$⊢\phi \to A+B-\left(A-B\right)=2B$$
13	9 12	oveq12d	$$⊢\phi \to \left(A+B+\left(A-B\right)\right)\left(A+B-\left(A-B\right)\right)=2A2B$$
14		2cnd	$$⊢\phi \to 2\in ℂ$$
15	14 1 14 2	mul4d	$$⊢\phi \to 2A2B=2\cdot 2AB$$
16	6 13 15	3eqtrd	$$⊢\phi \to {\left(A+B\right)}^2-{\left(A-B\right)}^2=2\cdot 2AB$$
17		2t2e4	$$⊢2\cdot 2=4$$
18	17	oveq1i	$$⊢2\cdot 2AB=4AB$$
19	16 18	eqtrdi	$$⊢\phi \to {\left(A+B\right)}^2-{\left(A-B\right)}^2=4AB$$