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 )