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

Metamath Proof Explorer

Theorem binom2sub

Description: Expand the square of a subtraction. (Contributed by Scott Fenton, 10-Jun-2013)

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

Proof

Step Hyp Ref Expression
1 negcl 
 |-  ( B e. CC -> -u B e. CC )
2 binom2 
 |-  ( ( A e. CC /\ -u B e. CC ) -> ( ( A + -u B ) ^ 2 ) = ( ( ( A ^ 2 ) + ( 2 x. ( A x. -u B ) ) ) + ( -u B ^ 2 ) ) )
3 1 2 sylan2 
 |-  ( ( A e. CC /\ B e. CC ) -> ( ( A + -u B ) ^ 2 ) = ( ( ( A ^ 2 ) + ( 2 x. ( A x. -u B ) ) ) + ( -u B ^ 2 ) ) )
4 negsub 
 |-  ( ( A e. CC /\ B e. CC ) -> ( A + -u B ) = ( A - B ) )
5 4 oveq1d 
 |-  ( ( A e. CC /\ B e. CC ) -> ( ( A + -u B ) ^ 2 ) = ( ( A - B ) ^ 2 ) )
6 3 5 eqtr3d 
 |-  ( ( A e. CC /\ B e. CC ) -> ( ( ( A ^ 2 ) + ( 2 x. ( A x. -u B ) ) ) + ( -u B ^ 2 ) ) = ( ( A - B ) ^ 2 ) )
7 mulneg2 
 |-  ( ( A e. CC /\ B e. CC ) -> ( A x. -u B ) = -u ( A x. B ) )
8 7 oveq2d 
 |-  ( ( A e. CC /\ B e. CC ) -> ( 2 x. ( A x. -u B ) ) = ( 2 x. -u ( A x. B ) ) )
9 2cn 
 |-  2 e. CC
10 mulcl 
 |-  ( ( A e. CC /\ B e. CC ) -> ( A x. B ) e. CC )
11 mulneg2 
 |-  ( ( 2 e. CC /\ ( A x. B ) e. CC ) -> ( 2 x. -u ( A x. B ) ) = -u ( 2 x. ( A x. B ) ) )
12 9 10 11 sylancr 
 |-  ( ( A e. CC /\ B e. CC ) -> ( 2 x. -u ( A x. B ) ) = -u ( 2 x. ( A x. B ) ) )
13 8 12 eqtr2d 
 |-  ( ( A e. CC /\ B e. CC ) -> -u ( 2 x. ( A x. B ) ) = ( 2 x. ( A x. -u B ) ) )
14 13 oveq2d 
 |-  ( ( A e. CC /\ B e. CC ) -> ( ( A ^ 2 ) + -u ( 2 x. ( A x. B ) ) ) = ( ( A ^ 2 ) + ( 2 x. ( A x. -u B ) ) ) )
15 sqcl 
 |-  ( A e. CC -> ( A ^ 2 ) e. CC )
16 15 adantr 
 |-  ( ( A e. CC /\ B e. CC ) -> ( A ^ 2 ) e. CC )
17 mulcl 
 |-  ( ( 2 e. CC /\ ( A x. B ) e. CC ) -> ( 2 x. ( A x. B ) ) e. CC )
18 9 10 17 sylancr 
 |-  ( ( A e. CC /\ B e. CC ) -> ( 2 x. ( A x. B ) ) e. CC )
19 16 18 negsubd 
 |-  ( ( A e. CC /\ B e. CC ) -> ( ( A ^ 2 ) + -u ( 2 x. ( A x. B ) ) ) = ( ( A ^ 2 ) - ( 2 x. ( A x. B ) ) ) )
20 14 19 eqtr3d 
 |-  ( ( A e. CC /\ B e. CC ) -> ( ( A ^ 2 ) + ( 2 x. ( A x. -u B ) ) ) = ( ( A ^ 2 ) - ( 2 x. ( A x. B ) ) ) )
21 sqneg 
 |-  ( B e. CC -> ( -u B ^ 2 ) = ( B ^ 2 ) )
22 21 adantl 
 |-  ( ( A e. CC /\ B e. CC ) -> ( -u B ^ 2 ) = ( B ^ 2 ) )
23 20 22 oveq12d 
 |-  ( ( A e. CC /\ B e. CC ) -> ( ( ( A ^ 2 ) + ( 2 x. ( A x. -u B ) ) ) + ( -u B ^ 2 ) ) = ( ( ( A ^ 2 ) - ( 2 x. ( A x. B ) ) ) + ( B ^ 2 ) ) )
24 6 23 eqtr3d 
 |-  ( ( A e. CC /\ B e. CC ) -> ( ( A - B ) ^ 2 ) = ( ( ( A ^ 2 ) - ( 2 x. ( A x. B ) ) ) + ( B ^ 2 ) ) )