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

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