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	⊢ ( 𝜑 → 𝐴 ∈ ℂ )
	binom2subadd.2	⊢ ( 𝜑 → 𝐵 ∈ ℂ )
Assertion	binom2subadd	⊢ ( 𝜑 → ( ( ( 𝐴 + 𝐵 ) ↑ 2 ) − ( ( 𝐴 − 𝐵 ) ↑ 2 ) ) = ( 4 · ( 𝐴 · 𝐵 ) ) )

Proof

Step	Hyp	Ref	Expression
1		binom2subadd.1	⊢ ( 𝜑 → 𝐴 ∈ ℂ )
2		binom2subadd.2	⊢ ( 𝜑 → 𝐵 ∈ ℂ )
3	1 2	addcld	⊢ ( 𝜑 → ( 𝐴 + 𝐵 ) ∈ ℂ )
4	1 2	subcld	⊢ ( 𝜑 → ( 𝐴 − 𝐵 ) ∈ ℂ )
5		subsq	⊢ ( ( ( 𝐴 + 𝐵 ) ∈ ℂ ∧ ( 𝐴 − 𝐵 ) ∈ ℂ ) → ( ( ( 𝐴 + 𝐵 ) ↑ 2 ) − ( ( 𝐴 − 𝐵 ) ↑ 2 ) ) = ( ( ( 𝐴 + 𝐵 ) + ( 𝐴 − 𝐵 ) ) · ( ( 𝐴 + 𝐵 ) − ( 𝐴 − 𝐵 ) ) ) )
6	3 4 5	syl2anc	⊢ ( 𝜑 → ( ( ( 𝐴 + 𝐵 ) ↑ 2 ) − ( ( 𝐴 − 𝐵 ) ↑ 2 ) ) = ( ( ( 𝐴 + 𝐵 ) + ( 𝐴 − 𝐵 ) ) · ( ( 𝐴 + 𝐵 ) − ( 𝐴 − 𝐵 ) ) ) )
7	1 2 1	ppncand	⊢ ( 𝜑 → ( ( 𝐴 + 𝐵 ) + ( 𝐴 − 𝐵 ) ) = ( 𝐴 + 𝐴 ) )
8	1	2timesd	⊢ ( 𝜑 → ( 2 · 𝐴 ) = ( 𝐴 + 𝐴 ) )
9	7 8	eqtr4d	⊢ ( 𝜑 → ( ( 𝐴 + 𝐵 ) + ( 𝐴 − 𝐵 ) ) = ( 2 · 𝐴 ) )
10	1 2 2	pnncand	⊢ ( 𝜑 → ( ( 𝐴 + 𝐵 ) − ( 𝐴 − 𝐵 ) ) = ( 𝐵 + 𝐵 ) )
11	2	2timesd	⊢ ( 𝜑 → ( 2 · 𝐵 ) = ( 𝐵 + 𝐵 ) )
12	10 11	eqtr4d	⊢ ( 𝜑 → ( ( 𝐴 + 𝐵 ) − ( 𝐴 − 𝐵 ) ) = ( 2 · 𝐵 ) )
13	9 12	oveq12d	⊢ ( 𝜑 → ( ( ( 𝐴 + 𝐵 ) + ( 𝐴 − 𝐵 ) ) · ( ( 𝐴 + 𝐵 ) − ( 𝐴 − 𝐵 ) ) ) = ( ( 2 · 𝐴 ) · ( 2 · 𝐵 ) ) )
14		2cnd	⊢ ( 𝜑 → 2 ∈ ℂ )
15	14 1 14 2	mul4d	⊢ ( 𝜑 → ( ( 2 · 𝐴 ) · ( 2 · 𝐵 ) ) = ( ( 2 · 2 ) · ( 𝐴 · 𝐵 ) ) )
16	6 13 15	3eqtrd	⊢ ( 𝜑 → ( ( ( 𝐴 + 𝐵 ) ↑ 2 ) − ( ( 𝐴 − 𝐵 ) ↑ 2 ) ) = ( ( 2 · 2 ) · ( 𝐴 · 𝐵 ) ) )
17		2t2e4	⊢ ( 2 · 2 ) = 4
18	17	oveq1i	⊢ ( ( 2 · 2 ) · ( 𝐴 · 𝐵 ) ) = ( 4 · ( 𝐴 · 𝐵 ) )
19	16 18	eqtrdi	⊢ ( 𝜑 → ( ( ( 𝐴 + 𝐵 ) ↑ 2 ) − ( ( 𝐴 − 𝐵 ) ↑ 2 ) ) = ( 4 · ( 𝐴 · 𝐵 ) ) )