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

Metamath Proof Explorer

Theorem binom2i

Description: The square of a binomial. (Contributed by NM, 11-Aug-1999)

Ref Expression
Hypotheses binom2.1 
|- A e. CC
binom2.2 
|- B e. CC
Assertion binom2i 
|- ( ( A + B ) ^ 2 ) = ( ( ( A ^ 2 ) + ( 2 x. ( A x. B ) ) ) + ( B ^ 2 ) )

Proof

Step Hyp Ref Expression
1 binom2.1 
 |-  A e. CC
2 binom2.2 
 |-  B e. CC
3 1 2 addcli 
 |-  ( A + B ) e. CC
4 3 1 2 adddii 
 |-  ( ( A + B ) x. ( A + B ) ) = ( ( ( A + B ) x. A ) + ( ( A + B ) x. B ) )
5 1 2 1 adddiri 
 |-  ( ( A + B ) x. A ) = ( ( A x. A ) + ( B x. A ) )
6 2 1 mulcomi 
 |-  ( B x. A ) = ( A x. B )
7 6 oveq2i 
 |-  ( ( A x. A ) + ( B x. A ) ) = ( ( A x. A ) + ( A x. B ) )
8 5 7 eqtri 
 |-  ( ( A + B ) x. A ) = ( ( A x. A ) + ( A x. B ) )
9 1 2 2 adddiri 
 |-  ( ( A + B ) x. B ) = ( ( A x. B ) + ( B x. B ) )
10 8 9 oveq12i 
 |-  ( ( ( A + B ) x. A ) + ( ( A + B ) x. B ) ) = ( ( ( A x. A ) + ( A x. B ) ) + ( ( A x. B ) + ( B x. B ) ) )
11 1 1 mulcli 
 |-  ( A x. A ) e. CC
12 1 2 mulcli 
 |-  ( A x. B ) e. CC
13 11 12 addcli 
 |-  ( ( A x. A ) + ( A x. B ) ) e. CC
14 2 2 mulcli 
 |-  ( B x. B ) e. CC
15 13 12 14 addassi 
 |-  ( ( ( ( A x. A ) + ( A x. B ) ) + ( A x. B ) ) + ( B x. B ) ) = ( ( ( A x. A ) + ( A x. B ) ) + ( ( A x. B ) + ( B x. B ) ) )
16 11 12 12 addassi 
 |-  ( ( ( A x. A ) + ( A x. B ) ) + ( A x. B ) ) = ( ( A x. A ) + ( ( A x. B ) + ( A x. B ) ) )
17 16 oveq1i 
 |-  ( ( ( ( A x. A ) + ( A x. B ) ) + ( A x. B ) ) + ( B x. B ) ) = ( ( ( A x. A ) + ( ( A x. B ) + ( A x. B ) ) ) + ( B x. B ) )
18 10 15 17 3eqtr2i 
 |-  ( ( ( A + B ) x. A ) + ( ( A + B ) x. B ) ) = ( ( ( A x. A ) + ( ( A x. B ) + ( A x. B ) ) ) + ( B x. B ) )
19 4 18 eqtri 
 |-  ( ( A + B ) x. ( A + B ) ) = ( ( ( A x. A ) + ( ( A x. B ) + ( A x. B ) ) ) + ( B x. B ) )
20 3 sqvali 
 |-  ( ( A + B ) ^ 2 ) = ( ( A + B ) x. ( A + B ) )
21 1 sqvali 
 |-  ( A ^ 2 ) = ( A x. A )
22 12 2timesi 
 |-  ( 2 x. ( A x. B ) ) = ( ( A x. B ) + ( A x. B ) )
23 21 22 oveq12i 
 |-  ( ( A ^ 2 ) + ( 2 x. ( A x. B ) ) ) = ( ( A x. A ) + ( ( A x. B ) + ( A x. B ) ) )
24 2 sqvali 
 |-  ( B ^ 2 ) = ( B x. B )
25 23 24 oveq12i 
 |-  ( ( ( A ^ 2 ) + ( 2 x. ( A x. B ) ) ) + ( B ^ 2 ) ) = ( ( ( A x. A ) + ( ( A x. B ) + ( A x. B ) ) ) + ( B x. B ) )
26 19 20 25 3eqtr4i 
 |-  ( ( A + B ) ^ 2 ) = ( ( ( A ^ 2 ) + ( 2 x. ( A x. B ) ) ) + ( B ^ 2 ) )