Metamath Proof Explorer

Theorem sqsumi

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

		Ref	Expression
	Hypotheses	sqsumi.1	$⊢ A \in ℂ$
		sqsumi.2	$⊢ B \in ℂ$
	Assertion	sqsumi	$⊢ (A + B) (A + B) = A A + B B + 2 A B$

Proof

Step	Hyp	Ref	Expression
1		sqsumi.1	$⊢ A \in ℂ$
2		sqsumi.2	$⊢ B \in ℂ$
3	1 2 1 2	muladdi	$⊢ (A + B) (A + B) = A A + B B + A B + A B$
4	1 2	mulcli	$⊢ A B \in ℂ$
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$