Theorem distrpi

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

	Ref	Expression
Assertion	distrpi	⊢ ( 𝐴 ·N ( 𝐵 +N 𝐶 ) ) = ( ( 𝐴 ·N 𝐵 ) +N ( 𝐴 ·N 𝐶 ) )

Proof

Step	Hyp	Ref	Expression
1		pinn	⊢ ( 𝐴 ∈ N → 𝐴 ∈ ω )
2		pinn	⊢ ( 𝐵 ∈ N → 𝐵 ∈ ω )
3		pinn	⊢ ( 𝐶 ∈ N → 𝐶 ∈ ω )
4		nndi	⊢ ( ( 𝐴 ∈ ω ∧ 𝐵 ∈ ω ∧ 𝐶 ∈ ω ) → ( 𝐴 ·o ( 𝐵 +o 𝐶 ) ) = ( ( 𝐴 ·o 𝐵 ) +o ( 𝐴 ·o 𝐶 ) ) )
5	1 2 3 4	syl3an	⊢ ( ( 𝐴 ∈ N ∧ 𝐵 ∈ N ∧ 𝐶 ∈ N ) → ( 𝐴 ·o ( 𝐵 +o 𝐶 ) ) = ( ( 𝐴 ·o 𝐵 ) +o ( 𝐴 ·o 𝐶 ) ) )
6		addclpi	⊢ ( ( 𝐵 ∈ N ∧ 𝐶 ∈ N ) → ( 𝐵 +N 𝐶 ) ∈ N )
7		mulpiord	⊢ ( ( 𝐴 ∈ N ∧ ( 𝐵 +N 𝐶 ) ∈ N ) → ( 𝐴 ·N ( 𝐵 +N 𝐶 ) ) = ( 𝐴 ·o ( 𝐵 +N 𝐶 ) ) )
8	6 7	sylan2	⊢ ( ( 𝐴 ∈ N ∧ ( 𝐵 ∈ N ∧ 𝐶 ∈ N ) ) → ( 𝐴 ·N ( 𝐵 +N 𝐶 ) ) = ( 𝐴 ·o ( 𝐵 +N 𝐶 ) ) )
9		addpiord	⊢ ( ( 𝐵 ∈ N ∧ 𝐶 ∈ N ) → ( 𝐵 +N 𝐶 ) = ( 𝐵 +o 𝐶 ) )
10	9	oveq2d	⊢ ( ( 𝐵 ∈ N ∧ 𝐶 ∈ N ) → ( 𝐴 ·o ( 𝐵 +N 𝐶 ) ) = ( 𝐴 ·o ( 𝐵 +o 𝐶 ) ) )
11	10	adantl	⊢ ( ( 𝐴 ∈ N ∧ ( 𝐵 ∈ N ∧ 𝐶 ∈ N ) ) → ( 𝐴 ·o ( 𝐵 +N 𝐶 ) ) = ( 𝐴 ·o ( 𝐵 +o 𝐶 ) ) )
12	8 11	eqtrd	⊢ ( ( 𝐴 ∈ N ∧ ( 𝐵 ∈ N ∧ 𝐶 ∈ N ) ) → ( 𝐴 ·N ( 𝐵 +N 𝐶 ) ) = ( 𝐴 ·o ( 𝐵 +o 𝐶 ) ) )
13	12	3impb	⊢ ( ( 𝐴 ∈ N ∧ 𝐵 ∈ N ∧ 𝐶 ∈ N ) → ( 𝐴 ·N ( 𝐵 +N 𝐶 ) ) = ( 𝐴 ·o ( 𝐵 +o 𝐶 ) ) )
14		mulclpi	⊢ ( ( 𝐴 ∈ N ∧ 𝐵 ∈ N ) → ( 𝐴 ·N 𝐵 ) ∈ N )
15		mulclpi	⊢ ( ( 𝐴 ∈ N ∧ 𝐶 ∈ N ) → ( 𝐴 ·N 𝐶 ) ∈ N )
16		addpiord	⊢ ( ( ( 𝐴 ·N 𝐵 ) ∈ N ∧ ( 𝐴 ·N 𝐶 ) ∈ N ) → ( ( 𝐴 ·N 𝐵 ) +N ( 𝐴 ·N 𝐶 ) ) = ( ( 𝐴 ·N 𝐵 ) +o ( 𝐴 ·N 𝐶 ) ) )
17	14 15 16	syl2an	⊢ ( ( ( 𝐴 ∈ N ∧ 𝐵 ∈ N ) ∧ ( 𝐴 ∈ N ∧ 𝐶 ∈ N ) ) → ( ( 𝐴 ·N 𝐵 ) +N ( 𝐴 ·N 𝐶 ) ) = ( ( 𝐴 ·N 𝐵 ) +o ( 𝐴 ·N 𝐶 ) ) )
18		mulpiord	⊢ ( ( 𝐴 ∈ N ∧ 𝐵 ∈ N ) → ( 𝐴 ·N 𝐵 ) = ( 𝐴 ·o 𝐵 ) )
19		mulpiord	⊢ ( ( 𝐴 ∈ N ∧ 𝐶 ∈ N ) → ( 𝐴 ·N 𝐶 ) = ( 𝐴 ·o 𝐶 ) )
20	18 19	oveqan12d	⊢ ( ( ( 𝐴 ∈ N ∧ 𝐵 ∈ N ) ∧ ( 𝐴 ∈ N ∧ 𝐶 ∈ N ) ) → ( ( 𝐴 ·N 𝐵 ) +o ( 𝐴 ·N 𝐶 ) ) = ( ( 𝐴 ·o 𝐵 ) +o ( 𝐴 ·o 𝐶 ) ) )
21	17 20	eqtrd	⊢ ( ( ( 𝐴 ∈ N ∧ 𝐵 ∈ N ) ∧ ( 𝐴 ∈ N ∧ 𝐶 ∈ N ) ) → ( ( 𝐴 ·N 𝐵 ) +N ( 𝐴 ·N 𝐶 ) ) = ( ( 𝐴 ·o 𝐵 ) +o ( 𝐴 ·o 𝐶 ) ) )
22	21	3impdi	⊢ ( ( 𝐴 ∈ N ∧ 𝐵 ∈ N ∧ 𝐶 ∈ N ) → ( ( 𝐴 ·N 𝐵 ) +N ( 𝐴 ·N 𝐶 ) ) = ( ( 𝐴 ·o 𝐵 ) +o ( 𝐴 ·o 𝐶 ) ) )
23	5 13 22	3eqtr4d	⊢ ( ( 𝐴 ∈ N ∧ 𝐵 ∈ N ∧ 𝐶 ∈ N ) → ( 𝐴 ·N ( 𝐵 +N 𝐶 ) ) = ( ( 𝐴 ·N 𝐵 ) +N ( 𝐴 ·N 𝐶 ) ) )
24		dmaddpi	⊢ dom +N = ( N × N )
25		0npi	⊢ ¬ ∅ ∈ N
26		dmmulpi	⊢ dom ·N = ( N × N )
27	24 25 26	ndmovdistr	⊢ ( ¬ ( 𝐴 ∈ N ∧ 𝐵 ∈ N ∧ 𝐶 ∈ N ) → ( 𝐴 ·N ( 𝐵 +N 𝐶 ) ) = ( ( 𝐴 ·N 𝐵 ) +N ( 𝐴 ·N 𝐶 ) ) )
28	23 27	pm2.61i	⊢ ( 𝐴 ·N ( 𝐵 +N 𝐶 ) ) = ( ( 𝐴 ·N 𝐵 ) +N ( 𝐴 ·N 𝐶 ) )