Metamath Proof Explorer

Theorem subsq2

Description: Express the difference of the squares of two numbers as a polynomial in the difference of the numbers. (Contributed by NM, 21-Feb-2008)

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

Proof

Step Hyp Ref Expression
1 2cn 
 |-  2 e. CC
2 mulcl 
 |-  ( ( 2 e. CC /\ B e. CC ) -> ( 2 x. B ) e. CC )
3 1 2 mpan 
 |-  ( B e. CC -> ( 2 x. B ) e. CC )
4 3 adantl 
 |-  ( ( A e. CC /\ B e. CC ) -> ( 2 x. B ) e. CC )
5 subadd23 
 |-  ( ( A e. CC /\ B e. CC /\ ( 2 x. B ) e. CC ) -> ( ( A - B ) + ( 2 x. B ) ) = ( A + ( ( 2 x. B ) - B ) ) )
6 4 5 mpd3an3 
 |-  ( ( A e. CC /\ B e. CC ) -> ( ( A - B ) + ( 2 x. B ) ) = ( A + ( ( 2 x. B ) - B ) ) )
7 2txmxeqx 
 |-  ( B e. CC -> ( ( 2 x. B ) - B ) = B )
8 7 adantl 
 |-  ( ( A e. CC /\ B e. CC ) -> ( ( 2 x. B ) - B ) = B )
9 8 oveq2d 
 |-  ( ( A e. CC /\ B e. CC ) -> ( A + ( ( 2 x. B ) - B ) ) = ( A + B ) )
10 6 9 eqtrd 
 |-  ( ( A e. CC /\ B e. CC ) -> ( ( A - B ) + ( 2 x. B ) ) = ( A + B ) )
11 10 oveq1d 
 |-  ( ( A e. CC /\ B e. CC ) -> ( ( ( A - B ) + ( 2 x. B ) ) x. ( A - B ) ) = ( ( A + B ) x. ( A - B ) ) )
12 subcl 
 |-  ( ( A e. CC /\ B e. CC ) -> ( A - B ) e. CC )
13 12 4 12 adddird 
 |-  ( ( A e. CC /\ B e. CC ) -> ( ( ( A - B ) + ( 2 x. B ) ) x. ( A - B ) ) = ( ( ( A - B ) x. ( A - B ) ) + ( ( 2 x. B ) x. ( A - B ) ) ) )
14 11 13 eqtr3d 
 |-  ( ( A e. CC /\ B e. CC ) -> ( ( A + B ) x. ( A - B ) ) = ( ( ( A - B ) x. ( A - B ) ) + ( ( 2 x. B ) x. ( A - B ) ) ) )
15 subsq 
 |-  ( ( A e. CC /\ B e. CC ) -> ( ( A ^ 2 ) - ( B ^ 2 ) ) = ( ( A + B ) x. ( A - B ) ) )
16 sqval 
 |-  ( ( A - B ) e. CC -> ( ( A - B ) ^ 2 ) = ( ( A - B ) x. ( A - B ) ) )
17 12 16 syl 
 |-  ( ( A e. CC /\ B e. CC ) -> ( ( A - B ) ^ 2 ) = ( ( A - B ) x. ( A - B ) ) )
18 17 oveq1d 
 |-  ( ( A e. CC /\ B e. CC ) -> ( ( ( A - B ) ^ 2 ) + ( ( 2 x. B ) x. ( A - B ) ) ) = ( ( ( A - B ) x. ( A - B ) ) + ( ( 2 x. B ) x. ( A - B ) ) ) )
19 14 15 18 3eqtr4d 
 |-  ( ( A e. CC /\ B e. CC ) -> ( ( A ^ 2 ) - ( B ^ 2 ) ) = ( ( ( A - B ) ^ 2 ) + ( ( 2 x. B ) x. ( A - B ) ) ) )