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

Metamath Proof Explorer

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