Metamath Proof Explorer

Theorem binom2sub1

Description: Special case of binom2sub where B = 1 . (Contributed by AV, 2-Aug-2021)

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

Proof

Step Hyp Ref Expression
1 1cnd 
 |-  ( A e. CC -> 1 e. CC )
2 binom2sub 
 |-  ( ( A e. CC /\ 1 e. CC ) -> ( ( A - 1 ) ^ 2 ) = ( ( ( A ^ 2 ) - ( 2 x. ( A x. 1 ) ) ) + ( 1 ^ 2 ) ) )
3 1 2 mpdan 
 |-  ( 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 ) )