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 e. CC
sqsumi.2 
|- B e. CC
Assertion sqsumi 
|- ( ( A + B ) x. ( A + B ) ) = ( ( ( A x. A ) + ( B x. B ) ) + ( 2 x. ( A x. B ) ) )

Proof

Step Hyp Ref Expression
1 sqsumi.1 
 |-  A e. CC
2 sqsumi.2 
 |-  B e. CC
3 1 2 1 2 muladdi 
 |-  ( ( A + B ) x. ( A + B ) ) = ( ( ( A x. A ) + ( B x. B ) ) + ( ( A x. B ) + ( A x. B ) ) )
4 1 2 mulcli 
 |-  ( A x. B ) e. CC
5 4 2timesi 
 |-  ( 2 x. ( A x. B ) ) = ( ( A x. B ) + ( A x. B ) )
6 5 eqcomi 
 |-  ( ( A x. B ) + ( A x. B ) ) = ( 2 x. ( A x. B ) )
7 6 oveq2i 
 |-  ( ( ( A x. A ) + ( B x. B ) ) + ( ( A x. B ) + ( A x. B ) ) ) = ( ( ( A x. A ) + ( B x. B ) ) + ( 2 x. ( A x. B ) ) )
8 3 7 eqtri 
 |-  ( ( A + B ) x. ( A + B ) ) = ( ( ( A x. A ) + ( B x. B ) ) + ( 2 x. ( A x. B ) ) )