Metamath Proof Explorer

Theorem binom21

Description: Special case of binom2 where B = 1 . (Contributed by Scott Fenton, 11-May-2014)

Ref Expression
Assertion binom21 
|- ( A e. CC -> ( ( A + 1 ) ^ 2 ) = ( ( ( A ^ 2 ) + ( 2 x. A ) ) + 1 ) )

Proof

Step Hyp Ref Expression
1 ax-1cn 
 |-  1 e. CC
2 binom2 
 |-  ( ( A e. CC /\ 1 e. CC ) -> ( ( A + 1 ) ^ 2 ) = ( ( ( A ^ 2 ) + ( 2 x. ( A x. 1 ) ) ) + ( 1 ^ 2 ) ) )
3 1 2 mpan2 
 |-  ( A e. CC -> ( ( A + 1 ) ^ 2 ) = ( ( ( A ^ 2 ) + ( 2 x. ( A x. 1 ) ) ) + ( 1 ^ 2 ) ) )
4 mulid1 
 |-  ( A e. CC -> ( A x. 1 ) = A )
5 4 oveq2d 
 |-  ( A e. CC -> ( 2 x. ( A x. 1 ) ) = ( 2 x. A ) )
6 5 oveq2d 
 |-  ( A e. CC -> ( ( A ^ 2 ) + ( 2 x. ( A x. 1 ) ) ) = ( ( A ^ 2 ) + ( 2 x. A ) ) )
7 sq1 
 |-  ( 1 ^ 2 ) = 1
8 7 a1i 
 |-  ( A e. CC -> ( 1 ^ 2 ) = 1 )
9 6 8 oveq12d 
 |-  ( A e. CC -> ( ( ( A ^ 2 ) + ( 2 x. ( A x. 1 ) ) ) + ( 1 ^ 2 ) ) = ( ( ( A ^ 2 ) + ( 2 x. A ) ) + 1 ) )
10 3 9 eqtrd 
 |-  ( A e. CC -> ( ( A + 1 ) ^ 2 ) = ( ( ( A ^ 2 ) + ( 2 x. A ) ) + 1 ) )