Theorem distrpi

Description: Multiplication of positive integers is distributive. (Contributed by NM, 21-Sep-1995) (New usage is discouraged.)

	Ref	Expression
Assertion	distrpi	|- ( A .N ( B +N C ) ) = ( ( A .N B ) +N ( A .N C ) )

Proof

Step	Hyp	Ref	Expression
1		pinn	|- ( A e. N. -> A e. _om )
2		pinn	|- ( B e. N. -> B e. _om )
3		pinn	|- ( C e. N. -> C e. _om )
4		nndi	|- ( ( A e. _om /\ B e. _om /\ C e. _om ) -> ( A .o ( B +o C ) ) = ( ( A .o B ) +o ( A .o C ) ) )
5	1 2 3 4	syl3an	|- ( ( A e. N. /\ B e. N. /\ C e. N. ) -> ( A .o ( B +o C ) ) = ( ( A .o B ) +o ( A .o C ) ) )
6		addclpi	|- ( ( B e. N. /\ C e. N. ) -> ( B +N C ) e. N. )
7		mulpiord	|- ( ( A e. N. /\ ( B +N C ) e. N. ) -> ( A .N ( B +N C ) ) = ( A .o ( B +N C ) ) )
8	6 7	sylan2	|- ( ( A e. N. /\ ( B e. N. /\ C e. N. ) ) -> ( A .N ( B +N C ) ) = ( A .o ( B +N C ) ) )
9		addpiord	|- ( ( B e. N. /\ C e. N. ) -> ( B +N C ) = ( B +o C ) )
10	9	oveq2d	|- ( ( B e. N. /\ C e. N. ) -> ( A .o ( B +N C ) ) = ( A .o ( B +o C ) ) )
11	10	adantl	|- ( ( A e. N. /\ ( B e. N. /\ C e. N. ) ) -> ( A .o ( B +N C ) ) = ( A .o ( B +o C ) ) )
12	8 11	eqtrd	|- ( ( A e. N. /\ ( B e. N. /\ C e. N. ) ) -> ( A .N ( B +N C ) ) = ( A .o ( B +o C ) ) )
13	12	3impb	|- ( ( A e. N. /\ B e. N. /\ C e. N. ) -> ( A .N ( B +N C ) ) = ( A .o ( B +o C ) ) )
14		mulclpi	|- ( ( A e. N. /\ B e. N. ) -> ( A .N B ) e. N. )
15		mulclpi	|- ( ( A e. N. /\ C e. N. ) -> ( A .N C ) e. N. )
16		addpiord	|- ( ( ( A .N B ) e. N. /\ ( A .N C ) e. N. ) -> ( ( A .N B ) +N ( A .N C ) ) = ( ( A .N B ) +o ( A .N C ) ) )
17	14 15 16	syl2an	|- ( ( ( A e. N. /\ B e. N. ) /\ ( A e. N. /\ C e. N. ) ) -> ( ( A .N B ) +N ( A .N C ) ) = ( ( A .N B ) +o ( A .N C ) ) )
18		mulpiord	|- ( ( A e. N. /\ B e. N. ) -> ( A .N B ) = ( A .o B ) )
19		mulpiord	|- ( ( A e. N. /\ C e. N. ) -> ( A .N C ) = ( A .o C ) )
20	18 19	oveqan12d	|- ( ( ( A e. N. /\ B e. N. ) /\ ( A e. N. /\ C e. N. ) ) -> ( ( A .N B ) +o ( A .N C ) ) = ( ( A .o B ) +o ( A .o C ) ) )
21	17 20	eqtrd	|- ( ( ( A e. N. /\ B e. N. ) /\ ( A e. N. /\ C e. N. ) ) -> ( ( A .N B ) +N ( A .N C ) ) = ( ( A .o B ) +o ( A .o C ) ) )
22	21	3impdi	|- ( ( A e. N. /\ B e. N. /\ C e. N. ) -> ( ( A .N B ) +N ( A .N C ) ) = ( ( A .o B ) +o ( A .o C ) ) )
23	5 13 22	3eqtr4d	|- ( ( A e. N. /\ B e. N. /\ C e. N. ) -> ( A .N ( B +N C ) ) = ( ( A .N B ) +N ( A .N C ) ) )
24		dmaddpi	|- dom +N = ( N. X. N. )
25		0npi	|- -. (/) e. N.
26		dmmulpi	|- dom .N = ( N. X. N. )
27	24 25 26	ndmovdistr	|- ( -. ( A e. N. /\ B e. N. /\ C e. N. ) -> ( A .N ( B +N C ) ) = ( ( A .N B ) +N ( A .N C ) ) )
28	23 27	pm2.61i	|- ( A .N ( B +N C ) ) = ( ( A .N B ) +N ( A .N C ) )