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