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

Metamath Proof Explorer

Theorem subsq

Description: Factor the difference of two squares. (Contributed by NM, 21-Feb-2008)

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

Proof

Step Hyp Ref Expression
1 simpl 
 |-  ( ( A e. CC /\ B e. CC ) -> A e. CC )
2 simpr 
 |-  ( ( A e. CC /\ B e. CC ) -> B e. CC )
3 subcl 
 |-  ( ( A e. CC /\ B e. CC ) -> ( A - B ) e. CC )
4 1 2 3 adddird 
 |-  ( ( A e. CC /\ B e. CC ) -> ( ( A + B ) x. ( A - B ) ) = ( ( A x. ( A - B ) ) + ( B x. ( A - B ) ) ) )
5 subdi 
 |-  ( ( A e. CC /\ A e. CC /\ B e. CC ) -> ( A x. ( A - B ) ) = ( ( A x. A ) - ( A x. B ) ) )
6 5 3anidm12 
 |-  ( ( A e. CC /\ B e. CC ) -> ( A x. ( A - B ) ) = ( ( A x. A ) - ( A x. B ) ) )
7 sqval 
 |-  ( A e. CC -> ( A ^ 2 ) = ( A x. A ) )
8 7 adantr 
 |-  ( ( A e. CC /\ B e. CC ) -> ( A ^ 2 ) = ( A x. A ) )
9 8 oveq1d 
 |-  ( ( A e. CC /\ B e. CC ) -> ( ( A ^ 2 ) - ( A x. B ) ) = ( ( A x. A ) - ( A x. B ) ) )
10 6 9 eqtr4d 
 |-  ( ( A e. CC /\ B e. CC ) -> ( A x. ( A - B ) ) = ( ( A ^ 2 ) - ( A x. B ) ) )
11 2 1 2 subdid 
 |-  ( ( A e. CC /\ B e. CC ) -> ( B x. ( A - B ) ) = ( ( B x. A ) - ( B x. B ) ) )
12 mulcom 
 |-  ( ( A e. CC /\ B e. CC ) -> ( A x. B ) = ( B x. A ) )
13 sqval 
 |-  ( B e. CC -> ( B ^ 2 ) = ( B x. B ) )
14 13 adantl 
 |-  ( ( A e. CC /\ B e. CC ) -> ( B ^ 2 ) = ( B x. B ) )
15 12 14 oveq12d 
 |-  ( ( A e. CC /\ B e. CC ) -> ( ( A x. B ) - ( B ^ 2 ) ) = ( ( B x. A ) - ( B x. B ) ) )
16 11 15 eqtr4d 
 |-  ( ( A e. CC /\ B e. CC ) -> ( B x. ( A - B ) ) = ( ( A x. B ) - ( B ^ 2 ) ) )
17 10 16 oveq12d 
 |-  ( ( A e. CC /\ B e. CC ) -> ( ( A x. ( A - B ) ) + ( B x. ( A - B ) ) ) = ( ( ( A ^ 2 ) - ( A x. B ) ) + ( ( A x. B ) - ( B ^ 2 ) ) ) )
18 sqcl 
 |-  ( A e. CC -> ( A ^ 2 ) e. CC )
19 18 adantr 
 |-  ( ( A e. CC /\ B e. CC ) -> ( A ^ 2 ) e. CC )
20 mulcl 
 |-  ( ( A e. CC /\ B e. CC ) -> ( A x. B ) e. CC )
21 sqcl 
 |-  ( B e. CC -> ( B ^ 2 ) e. CC )
22 21 adantl 
 |-  ( ( A e. CC /\ B e. CC ) -> ( B ^ 2 ) e. CC )
23 19 20 22 npncand 
 |-  ( ( A e. CC /\ B e. CC ) -> ( ( ( A ^ 2 ) - ( A x. B ) ) + ( ( A x. B ) - ( B ^ 2 ) ) ) = ( ( A ^ 2 ) - ( B ^ 2 ) ) )
24 4 17 23 3eqtrrd 
 |-  ( ( A e. CC /\ B e. CC ) -> ( ( A ^ 2 ) - ( B ^ 2 ) ) = ( ( A + B ) x. ( A - B ) ) )