This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 · ( 𝐴 · 𝐵 ) ) )