Theorem addcompi

Description: Addition of positive integers is commutative. (Contributed by NM, 27-Aug-1995) (New usage is discouraged.)

	Ref	Expression
Assertion	addcompi	⊢ ( 𝐴 +N 𝐵 ) = ( 𝐵 +N 𝐴 )

Proof

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