Metamath Proof Explorer


Theorem sqsumi

Description: A sum squared. (Contributed by Steven Nguyen, 16-Sep-2022)

Ref Expression
Hypotheses sqsumi.1 A
sqsumi.2 B
Assertion sqsumi A + B A + B = A A + B B + 2 A B

Proof

Step Hyp Ref Expression
1 sqsumi.1 A
2 sqsumi.2 B
3 1 2 1 2 muladdi A + B A + B = A A + B B + A B + A B
4 1 2 mulcli A B
5 4 2timesi 2 A B = A B + A B
6 5 eqcomi A B + A B = 2 A B
7 6 oveq2i A A + B B + A B + A B = A A + B B + 2 A B
8 3 7 eqtri A + B A + B = A A + B B + 2 A B