Metamath Proof Explorer

Theorem binom2

Description: The square of a binomial. (Contributed by FL, 10-Dec-2006)

Ref Expression
Assertion binom2 
|- ( ( A e. CC /\ B e. CC ) -> ( ( A + B ) ^ 2 ) = ( ( ( A ^ 2 ) + ( 2 x. ( A x. B ) ) ) + ( B ^ 2 ) ) )

Proof

Step Hyp Ref Expression
1 oveq1 
 |-  ( A = if ( A e. CC , A , 0 ) -> ( A + B ) = ( if ( A e. CC , A , 0 ) + B ) )
2 1 oveq1d 
 |-  ( A = if ( A e. CC , A , 0 ) -> ( ( A + B ) ^ 2 ) = ( ( if ( A e. CC , A , 0 ) + B ) ^ 2 ) )
3 oveq1 
 |-  ( A = if ( A e. CC , A , 0 ) -> ( A ^ 2 ) = ( if ( A e. CC , A , 0 ) ^ 2 ) )
4 oveq1 
 |-  ( A = if ( A e. CC , A , 0 ) -> ( A x. B ) = ( if ( A e. CC , A , 0 ) x. B ) )
5 4 oveq2d 
 |-  ( A = if ( A e. CC , A , 0 ) -> ( 2 x. ( A x. B ) ) = ( 2 x. ( if ( A e. CC , A , 0 ) x. B ) ) )
6 3 5 oveq12d 
 |-  ( A = if ( A e. CC , A , 0 ) -> ( ( A ^ 2 ) + ( 2 x. ( A x. B ) ) ) = ( ( if ( A e. CC , A , 0 ) ^ 2 ) + ( 2 x. ( if ( A e. CC , A , 0 ) x. B ) ) ) )
7 6 oveq1d 
 |-  ( A = if ( A e. CC , A , 0 ) -> ( ( ( A ^ 2 ) + ( 2 x. ( A x. B ) ) ) + ( B ^ 2 ) ) = ( ( ( if ( A e. CC , A , 0 ) ^ 2 ) + ( 2 x. ( if ( A e. CC , A , 0 ) x. B ) ) ) + ( B ^ 2 ) ) )
8 2 7 eqeq12d 
 |-  ( A = if ( A e. CC , A , 0 ) -> ( ( ( A + B ) ^ 2 ) = ( ( ( A ^ 2 ) + ( 2 x. ( A x. B ) ) ) + ( B ^ 2 ) ) <-> ( ( if ( A e. CC , A , 0 ) + B ) ^ 2 ) = ( ( ( if ( A e. CC , A , 0 ) ^ 2 ) + ( 2 x. ( if ( A e. CC , A , 0 ) x. B ) ) ) + ( B ^ 2 ) ) ) )
9 oveq2 
 |-  ( B = if ( B e. CC , B , 0 ) -> ( if ( A e. CC , A , 0 ) + B ) = ( if ( A e. CC , A , 0 ) + if ( B e. CC , B , 0 ) ) )
10 9 oveq1d 
 |-  ( B = if ( B e. CC , B , 0 ) -> ( ( if ( A e. CC , A , 0 ) + B ) ^ 2 ) = ( ( if ( A e. CC , A , 0 ) + if ( B e. CC , B , 0 ) ) ^ 2 ) )
11 oveq2 
 |-  ( B = if ( B e. CC , B , 0 ) -> ( if ( A e. CC , A , 0 ) x. B ) = ( if ( A e. CC , A , 0 ) x. if ( B e. CC , B , 0 ) ) )
12 11 oveq2d 
 |-  ( B = if ( B e. CC , B , 0 ) -> ( 2 x. ( if ( A e. CC , A , 0 ) x. B ) ) = ( 2 x. ( if ( A e. CC , A , 0 ) x. if ( B e. CC , B , 0 ) ) ) )
13 12 oveq2d 
 |-  ( B = if ( B e. CC , B , 0 ) -> ( ( if ( A e. CC , A , 0 ) ^ 2 ) + ( 2 x. ( if ( A e. CC , A , 0 ) x. B ) ) ) = ( ( if ( A e. CC , A , 0 ) ^ 2 ) + ( 2 x. ( if ( A e. CC , A , 0 ) x. if ( B e. CC , B , 0 ) ) ) ) )
14 oveq1 
 |-  ( B = if ( B e. CC , B , 0 ) -> ( B ^ 2 ) = ( if ( B e. CC , B , 0 ) ^ 2 ) )
15 13 14 oveq12d 
 |-  ( B = if ( B e. CC , B , 0 ) -> ( ( ( if ( A e. CC , A , 0 ) ^ 2 ) + ( 2 x. ( if ( A e. CC , A , 0 ) x. B ) ) ) + ( B ^ 2 ) ) = ( ( ( if ( A e. CC , A , 0 ) ^ 2 ) + ( 2 x. ( if ( A e. CC , A , 0 ) x. if ( B e. CC , B , 0 ) ) ) ) + ( if ( B e. CC , B , 0 ) ^ 2 ) ) )
16 10 15 eqeq12d 
 |-  ( B = if ( B e. CC , B , 0 ) -> ( ( ( if ( A e. CC , A , 0 ) + B ) ^ 2 ) = ( ( ( if ( A e. CC , A , 0 ) ^ 2 ) + ( 2 x. ( if ( A e. CC , A , 0 ) x. B ) ) ) + ( B ^ 2 ) ) <-> ( ( if ( A e. CC , A , 0 ) + if ( B e. CC , B , 0 ) ) ^ 2 ) = ( ( ( if ( A e. CC , A , 0 ) ^ 2 ) + ( 2 x. ( if ( A e. CC , A , 0 ) x. if ( B e. CC , B , 0 ) ) ) ) + ( if ( B e. CC , B , 0 ) ^ 2 ) ) ) )
17 0cn 
 |-  0 e. CC
18 17 elimel 
 |-  if ( A e. CC , A , 0 ) e. CC
19 17 elimel 
 |-  if ( B e. CC , B , 0 ) e. CC
20 18 19 binom2i 
 |-  ( ( if ( A e. CC , A , 0 ) + if ( B e. CC , B , 0 ) ) ^ 2 ) = ( ( ( if ( A e. CC , A , 0 ) ^ 2 ) + ( 2 x. ( if ( A e. CC , A , 0 ) x. if ( B e. CC , B , 0 ) ) ) ) + ( if ( B e. CC , B , 0 ) ^ 2 ) )
21 8 16 20 dedth2h 
 |-  ( ( A e. CC /\ B e. CC ) -> ( ( A + B ) ^ 2 ) = ( ( ( A ^ 2 ) + ( 2 x. ( A x. B ) ) ) + ( B ^ 2 ) ) )