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	|- ( ph -> A e. CC )
	binom2subadd.2	|- ( ph -> B e. CC )
Assertion	binom2subadd	|- ( ph -> ( ( ( A + B ) ^ 2 ) - ( ( A - B ) ^ 2 ) ) = ( 4 x. ( A x. B ) ) )

Proof

Step	Hyp	Ref	Expression
1		binom2subadd.1	|- ( ph -> A e. CC )
2		binom2subadd.2	|- ( ph -> B e. CC )
3	1 2	addcld	|- ( ph -> ( A + B ) e. CC )
4	1 2	subcld	|- ( ph -> ( A - B ) e. CC )
5		subsq	|- ( ( ( A + B ) e. CC /\ ( A - B ) e. CC ) -> ( ( ( A + B ) ^ 2 ) - ( ( A - B ) ^ 2 ) ) = ( ( ( A + B ) + ( A - B ) ) x. ( ( A + B ) - ( A - B ) ) ) )
6	3 4 5	syl2anc	|- ( ph -> ( ( ( A + B ) ^ 2 ) - ( ( A - B ) ^ 2 ) ) = ( ( ( A + B ) + ( A - B ) ) x. ( ( A + B ) - ( A - B ) ) ) )
7	1 2 1	ppncand	|- ( ph -> ( ( A + B ) + ( A - B ) ) = ( A + A ) )
8	1	2timesd	|- ( ph -> ( 2 x. A ) = ( A + A ) )
9	7 8	eqtr4d	|- ( ph -> ( ( A + B ) + ( A - B ) ) = ( 2 x. A ) )
10	1 2 2	pnncand	|- ( ph -> ( ( A + B ) - ( A - B ) ) = ( B + B ) )
11	2	2timesd	|- ( ph -> ( 2 x. B ) = ( B + B ) )
12	10 11	eqtr4d	|- ( ph -> ( ( A + B ) - ( A - B ) ) = ( 2 x. B ) )
13	9 12	oveq12d	|- ( ph -> ( ( ( A + B ) + ( A - B ) ) x. ( ( A + B ) - ( A - B ) ) ) = ( ( 2 x. A ) x. ( 2 x. B ) ) )
14		2cnd	|- ( ph -> 2 e. CC )
15	14 1 14 2	mul4d	|- ( ph -> ( ( 2 x. A ) x. ( 2 x. B ) ) = ( ( 2 x. 2 ) x. ( A x. B ) ) )
16	6 13 15	3eqtrd	|- ( ph -> ( ( ( A + B ) ^ 2 ) - ( ( A - B ) ^ 2 ) ) = ( ( 2 x. 2 ) x. ( A x. B ) ) )
17		2t2e4	|- ( 2 x. 2 ) = 4
18	17	oveq1i	|- ( ( 2 x. 2 ) x. ( A x. B ) ) = ( 4 x. ( A x. B ) )
19	16 18	eqtrdi	|- ( ph -> ( ( ( A + B ) ^ 2 ) - ( ( A - B ) ^ 2 ) ) = ( 4 x. ( A x. B ) ) )