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

Metamath Proof Explorer

Theorem subdi

Description: Distribution of multiplication over subtraction. Theorem I.5 of Apostol p. 18. (Contributed by NM, 18-Nov-2004)

Ref Expression
Assertion subdi 
|- ( ( A e. CC /\ B e. CC /\ C e. CC ) -> ( A x. ( B - C ) ) = ( ( A x. B ) - ( A x. C ) ) )

Proof

Step Hyp Ref Expression
1 simp1 
 |-  ( ( A e. CC /\ B e. CC /\ C e. CC ) -> A e. CC )
2 simp3 
 |-  ( ( A e. CC /\ B e. CC /\ C e. CC ) -> C e. CC )
3 subcl 
 |-  ( ( B e. CC /\ C e. CC ) -> ( B - C ) e. CC )
4 3 3adant1 
 |-  ( ( A e. CC /\ B e. CC /\ C e. CC ) -> ( B - C ) e. CC )
5 1 2 4 adddid 
 |-  ( ( A e. CC /\ B e. CC /\ C e. CC ) -> ( A x. ( C + ( B - C ) ) ) = ( ( A x. C ) + ( A x. ( B - C ) ) ) )
6 pncan3 
 |-  ( ( C e. CC /\ B e. CC ) -> ( C + ( B - C ) ) = B )
7 6 ancoms 
 |-  ( ( B e. CC /\ C e. CC ) -> ( C + ( B - C ) ) = B )
8 7 3adant1 
 |-  ( ( A e. CC /\ B e. CC /\ C e. CC ) -> ( C + ( B - C ) ) = B )
9 8 oveq2d 
 |-  ( ( A e. CC /\ B e. CC /\ C e. CC ) -> ( A x. ( C + ( B - C ) ) ) = ( A x. B ) )
10 5 9 eqtr3d 
 |-  ( ( A e. CC /\ B e. CC /\ C e. CC ) -> ( ( A x. C ) + ( A x. ( B - C ) ) ) = ( A x. B ) )
11 mulcl 
 |-  ( ( A e. CC /\ B e. CC ) -> ( A x. B ) e. CC )
12 11 3adant3 
 |-  ( ( A e. CC /\ B e. CC /\ C e. CC ) -> ( A x. B ) e. CC )
13 mulcl 
 |-  ( ( A e. CC /\ C e. CC ) -> ( A x. C ) e. CC )
14 13 3adant2 
 |-  ( ( A e. CC /\ B e. CC /\ C e. CC ) -> ( A x. C ) e. CC )
15 mulcl 
 |-  ( ( A e. CC /\ ( B - C ) e. CC ) -> ( A x. ( B - C ) ) e. CC )
16 3 15 sylan2 
 |-  ( ( A e. CC /\ ( B e. CC /\ C e. CC ) ) -> ( A x. ( B - C ) ) e. CC )
17 16 3impb 
 |-  ( ( A e. CC /\ B e. CC /\ C e. CC ) -> ( A x. ( B - C ) ) e. CC )
18 12 14 17 subaddd 
 |-  ( ( A e. CC /\ B e. CC /\ C e. CC ) -> ( ( ( A x. B ) - ( A x. C ) ) = ( A x. ( B - C ) ) <-> ( ( A x. C ) + ( A x. ( B - C ) ) ) = ( A x. B ) ) )
19 10 18 mpbird 
 |-  ( ( A e. CC /\ B e. CC /\ C e. CC ) -> ( ( A x. B ) - ( A x. C ) ) = ( A x. ( B - C ) ) )
20 19 eqcomd 
 |-  ( ( A e. CC /\ B e. CC /\ C e. CC ) -> ( A x. ( B - C ) ) = ( ( A x. B ) - ( A x. C ) ) )