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

Metamath Proof Explorer

Theorem mulasspi

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

Ref Expression
Assertion mulasspi 
|- ( ( A .N B ) .N C ) = ( A .N ( B .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 nnmass 
 |-  ( ( A e. _om /\ B e. _om /\ C e. _om ) -> ( ( A .o B ) .o C ) = ( A .o ( B .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 C ) ) )
6 mulclpi 
 |-  ( ( A e. N. /\ B e. N. ) -> ( A .N B ) e. N. )
7 mulpiord 
 |-  ( ( ( A .N B ) e. N. /\ C e. N. ) -> ( ( A .N B ) .N C ) = ( ( A .N B ) .o C ) )
8 6 7 sylan 
 |-  ( ( ( A e. N. /\ B e. N. ) /\ C e. N. ) -> ( ( A .N B ) .N C ) = ( ( A .N B ) .o C ) )
9 mulpiord 
 |-  ( ( A e. N. /\ B e. N. ) -> ( A .N B ) = ( A .o B ) )
10 9 oveq1d 
 |-  ( ( A e. N. /\ B e. N. ) -> ( ( A .N B ) .o C ) = ( ( A .o B ) .o C ) )
11 10 adantr 
 |-  ( ( ( A e. N. /\ B e. N. ) /\ C e. N. ) -> ( ( A .N B ) .o 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 3impa 
 |-  ( ( A e. N. /\ B e. N. /\ C e. N. ) -> ( ( A .N B ) .N C ) = ( ( A .o B ) .o C ) )
14 mulclpi 
 |-  ( ( B e. N. /\ C e. N. ) -> ( B .N C ) e. N. )
15 mulpiord 
 |-  ( ( A e. N. /\ ( B .N C ) e. N. ) -> ( A .N ( B .N C ) ) = ( A .o ( B .N C ) ) )
16 14 15 sylan2 
 |-  ( ( A e. N. /\ ( B e. N. /\ C e. N. ) ) -> ( A .N ( B .N C ) ) = ( A .o ( B .N C ) ) )
17 mulpiord 
 |-  ( ( B e. N. /\ C e. N. ) -> ( B .N C ) = ( B .o C ) )
18 17 oveq2d 
 |-  ( ( B e. N. /\ C e. N. ) -> ( A .o ( B .N C ) ) = ( A .o ( B .o C ) ) )
19 18 adantl 
 |-  ( ( A e. N. /\ ( B e. N. /\ C e. N. ) ) -> ( A .o ( B .N C ) ) = ( A .o ( B .o C ) ) )
20 16 19 eqtrd 
 |-  ( ( A e. N. /\ ( B e. N. /\ C e. N. ) ) -> ( A .N ( B .N C ) ) = ( A .o ( B .o C ) ) )
21 20 3impb 
 |-  ( ( A e. N. /\ B e. N. /\ C e. N. ) -> ( A .N ( B .N C ) ) = ( A .o ( B .o C ) ) )
22 5 13 21 3eqtr4d 
 |-  ( ( A e. N. /\ B e. N. /\ C e. N. ) -> ( ( A .N B ) .N C ) = ( A .N ( B .N C ) ) )
23 dmmulpi 
 |-  dom .N = ( N. X. N. )
24 0npi 
 |-  -. (/) e. N.
25 23 24 ndmovass 
 |-  ( -. ( A e. N. /\ B e. N. /\ C e. N. ) -> ( ( A .N B ) .N C ) = ( A .N ( B .N C ) ) )
26 22 25 pm2.61i 
 |-  ( ( A .N B ) .N C ) = ( A .N ( B .N C ) )