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 A2B2=A+BAB

Proof

Step Hyp Ref Expression
1 binom2.1 A
2 binom2.2 B
3 subsq ABA2B2=A+BAB
4 1 2 3 mp2an A2B2=A+BAB