Database
SUPPLEMENTARY MATERIAL (USERS' MATHBOXES)
Mathbox for Steven Nguyen
Arithmetic theorems
sqsumi
Next ⟩
negn0nposznnd
Metamath Proof Explorer
Ascii
Unicode
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