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

Metamath Proof Explorer

Theorem mulcompi

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

Ref Expression
Assertion mulcompi 
|- ( A .N B ) = ( B .N A )

Proof

Step Hyp Ref Expression
1 pinn 
 |-  ( A e. N. -> A e. _om )
2 pinn 
 |-  ( B e. N. -> B e. _om )
3 nnmcom 
 |-  ( ( A e. _om /\ B e. _om ) -> ( A .o B ) = ( B .o A ) )
4 1 2 3 syl2an 
 |-  ( ( A e. N. /\ B e. N. ) -> ( A .o B ) = ( B .o A ) )
5 mulpiord 
 |-  ( ( A e. N. /\ B e. N. ) -> ( A .N B ) = ( A .o B ) )
6 mulpiord 
 |-  ( ( B e. N. /\ A e. N. ) -> ( B .N A ) = ( B .o A ) )
7 6 ancoms 
 |-  ( ( A e. N. /\ B e. N. ) -> ( B .N A ) = ( B .o A ) )
8 4 5 7 3eqtr4d 
 |-  ( ( A e. N. /\ B e. N. ) -> ( A .N B ) = ( B .N A ) )
9 dmmulpi 
 |-  dom .N = ( N. X. N. )
10 9 ndmovcom 
 |-  ( -. ( A e. N. /\ B e. N. ) -> ( A .N B ) = ( B .N A ) )
11 8 10 pm2.61i 
 |-  ( A .N B ) = ( B .N A )