Theorem mulcompi

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

	Ref	Expression
Assertion	mulcompi	⊢ ( 𝐴 ·N 𝐵 ) = ( 𝐵 ·N 𝐴 )

Proof

Step	Hyp	Ref	Expression
1		pinn	⊢ ( 𝐴 ∈ N → 𝐴 ∈ ω )
2		pinn	⊢ ( 𝐵 ∈ N → 𝐵 ∈ ω )
3		nnmcom	⊢ ( ( 𝐴 ∈ ω ∧ 𝐵 ∈ ω ) → ( 𝐴 ·o 𝐵 ) = ( 𝐵 ·o 𝐴 ) )
4	1 2 3	syl2an	⊢ ( ( 𝐴 ∈ N ∧ 𝐵 ∈ N ) → ( 𝐴 ·o 𝐵 ) = ( 𝐵 ·o 𝐴 ) )
5		mulpiord	⊢ ( ( 𝐴 ∈ N ∧ 𝐵 ∈ N ) → ( 𝐴 ·N 𝐵 ) = ( 𝐴 ·o 𝐵 ) )
6		mulpiord	⊢ ( ( 𝐵 ∈ N ∧ 𝐴 ∈ N ) → ( 𝐵 ·N 𝐴 ) = ( 𝐵 ·o 𝐴 ) )
7	6	ancoms	⊢ ( ( 𝐴 ∈ N ∧ 𝐵 ∈ N ) → ( 𝐵 ·N 𝐴 ) = ( 𝐵 ·o 𝐴 ) )
8	4 5 7	3eqtr4d	⊢ ( ( 𝐴 ∈ N ∧ 𝐵 ∈ N ) → ( 𝐴 ·N 𝐵 ) = ( 𝐵 ·N 𝐴 ) )
9		dmmulpi	⊢ dom ·N = ( N × N )
10	9	ndmovcom	⊢ ( ¬ ( 𝐴 ∈ N ∧ 𝐵 ∈ N ) → ( 𝐴 ·N 𝐵 ) = ( 𝐵 ·N 𝐴 ) )
11	8 10	pm2.61i	⊢ ( 𝐴 ·N 𝐵 ) = ( 𝐵 ·N 𝐴 )