Metamath Proof Explorer

Theorem addasspi

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

Ref Expression
Assertion addasspi ( ( 𝐴 +N 𝐵 ) +N 𝐶 ) = ( 𝐴 +N ( 𝐵 +N 𝐶 ) )

Proof

Step Hyp Ref Expression
1 pinn ⊢ ( 𝐴 ∈ N → 𝐴 ∈ ω )
2 pinn ⊢ ( 𝐵 ∈ N → 𝐵 ∈ ω )
3 pinn ⊢ ( 𝐶 ∈ N → 𝐶 ∈ ω )
4 nnaass ⊢ ( ( 𝐴 ∈ ω ∧ 𝐵 ∈ ω ∧ 𝐶 ∈ ω ) → ( ( 𝐴 +o 𝐵 ) +o 𝐶 ) = ( 𝐴 +o ( 𝐵 +o 𝐶 ) ) )
5 1 2 3 4 syl3an ⊢ ( ( 𝐴 ∈ N ∧ 𝐵 ∈ N ∧ 𝐶 ∈ N ) → ( ( 𝐴 +o 𝐵 ) +o 𝐶 ) = ( 𝐴 +o ( 𝐵 +o 𝐶 ) ) )
6 addclpi ⊢ ( ( 𝐴 ∈ N ∧ 𝐵 ∈ N ) → ( 𝐴 +N 𝐵 ) ∈ N )
7 addpiord ⊢ ( ( ( 𝐴 +N 𝐵 ) ∈ N ∧ 𝐶 ∈ N ) → ( ( 𝐴 +N 𝐵 ) +N 𝐶 ) = ( ( 𝐴 +N 𝐵 ) +o 𝐶 ) )
8 6 7 sylan ⊢ ( ( ( 𝐴 ∈ N ∧ 𝐵 ∈ N ) ∧ 𝐶 ∈ N ) → ( ( 𝐴 +N 𝐵 ) +N 𝐶 ) = ( ( 𝐴 +N 𝐵 ) +o 𝐶 ) )
9 addpiord ⊢ ( ( 𝐴 ∈ N ∧ 𝐵 ∈ N ) → ( 𝐴 +N 𝐵 ) = ( 𝐴 +o 𝐵 ) )
10 9 oveq1d ⊢ ( ( 𝐴 ∈ N ∧ 𝐵 ∈ N ) → ( ( 𝐴 +N 𝐵 ) +o 𝐶 ) = ( ( 𝐴 +o 𝐵 ) +o 𝐶 ) )
11 10 adantr ⊢ ( ( ( 𝐴 ∈ N ∧ 𝐵 ∈ N ) ∧ 𝐶 ∈ N ) → ( ( 𝐴 +N 𝐵 ) +o 𝐶 ) = ( ( 𝐴 +o 𝐵 ) +o 𝐶 ) )
12 8 11 eqtrd ⊢ ( ( ( 𝐴 ∈ N ∧ 𝐵 ∈ N ) ∧ 𝐶 ∈ N ) → ( ( 𝐴 +N 𝐵 ) +N 𝐶 ) = ( ( 𝐴 +o 𝐵 ) +o 𝐶 ) )
13 12 3impa ⊢ ( ( 𝐴 ∈ N ∧ 𝐵 ∈ N ∧ 𝐶 ∈ N ) → ( ( 𝐴 +N 𝐵 ) +N 𝐶 ) = ( ( 𝐴 +o 𝐵 ) +o 𝐶 ) )
14 addclpi ⊢ ( ( 𝐵 ∈ N ∧ 𝐶 ∈ N ) → ( 𝐵 +N 𝐶 ) ∈ N )
15 addpiord ⊢ ( ( 𝐴 ∈ N ∧ ( 𝐵 +N 𝐶 ) ∈ N ) → ( 𝐴 +N ( 𝐵 +N 𝐶 ) ) = ( 𝐴 +o ( 𝐵 +N 𝐶 ) ) )
16 14 15 sylan2 ⊢ ( ( 𝐴 ∈ N ∧ ( 𝐵 ∈ N ∧ 𝐶 ∈ N ) ) → ( 𝐴 +N ( 𝐵 +N 𝐶 ) ) = ( 𝐴 +o ( 𝐵 +N 𝐶 ) ) )
17 addpiord ⊢ ( ( 𝐵 ∈ N ∧ 𝐶 ∈ N ) → ( 𝐵 +N 𝐶 ) = ( 𝐵 +o 𝐶 ) )
18 17 oveq2d ⊢ ( ( 𝐵 ∈ N ∧ 𝐶 ∈ N ) → ( 𝐴 +o ( 𝐵 +N 𝐶 ) ) = ( 𝐴 +o ( 𝐵 +o 𝐶 ) ) )
19 18 adantl ⊢ ( ( 𝐴 ∈ N ∧ ( 𝐵 ∈ N ∧ 𝐶 ∈ N ) ) → ( 𝐴 +o ( 𝐵 +N 𝐶 ) ) = ( 𝐴 +o ( 𝐵 +o 𝐶 ) ) )
20 16 19 eqtrd ⊢ ( ( 𝐴 ∈ N ∧ ( 𝐵 ∈ N ∧ 𝐶 ∈ N ) ) → ( 𝐴 +N ( 𝐵 +N 𝐶 ) ) = ( 𝐴 +o ( 𝐵 +o 𝐶 ) ) )
21 20 3impb ⊢ ( ( 𝐴 ∈ N ∧ 𝐵 ∈ N ∧ 𝐶 ∈ N ) → ( 𝐴 +N ( 𝐵 +N 𝐶 ) ) = ( 𝐴 +o ( 𝐵 +o 𝐶 ) ) )
22 5 13 21 3eqtr4d ⊢ ( ( 𝐴 ∈ N ∧ 𝐵 ∈ N ∧ 𝐶 ∈ N ) → ( ( 𝐴 +N 𝐵 ) +N 𝐶 ) = ( 𝐴 +N ( 𝐵 +N 𝐶 ) ) )
23 dmaddpi ⊢ dom +N = ( N × N )
24 0npi ⊢ ¬ ∅ ∈ N
25 23 24 ndmovass ⊢ ( ¬ ( 𝐴 ∈ N ∧ 𝐵 ∈ N ∧ 𝐶 ∈ N ) → ( ( 𝐴 +N 𝐵 ) +N 𝐶 ) = ( 𝐴 +N ( 𝐵 +N 𝐶 ) ) )
26 22 25 pm2.61i ⊢ ( ( 𝐴 +N 𝐵 ) +N 𝐶 ) = ( 𝐴 +N ( 𝐵 +N 𝐶 ) )