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 ) ) )