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

Metamath Proof Explorer

Theorem subsqi

Description: Factor the difference of two squares. (Contributed by NM, 7-Feb-2005)

Ref Expression
Hypotheses binom2.1 ⊢ A ∈ ℂ
binom2.2 ⊢ B ∈ ℂ
Assertion subsqi ⊢ A 2 − B 2 = A + B ⁢ A − B

Proof

Step Hyp Ref Expression
1 binom2.1 ⊢ A ∈ ℂ
2 binom2.2 ⊢ B ∈ ℂ
3 subsq ⊢ A ∈ ℂ ∧ B ∈ ℂ → A 2 − B 2 = A + B ⁢ A − B
4 1 2 3 mp2an ⊢ A 2 − B 2 = A + B ⁢ A − B