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 A + 𝑵 B + 𝑵 C = A + 𝑵 B + 𝑵 C

Proof

Step Hyp Ref Expression
1 pinn A 𝑵 A ω
2 pinn B 𝑵 B ω
3 pinn C 𝑵 C ω
4 nnaass A ω B ω C ω A + 𝑜 B + 𝑜 C = A + 𝑜 B + 𝑜 C
5 1 2 3 4 syl3an A 𝑵 B 𝑵 C 𝑵 A + 𝑜 B + 𝑜 C = A + 𝑜 B + 𝑜 C
6 addclpi A 𝑵 B 𝑵 A + 𝑵 B 𝑵
7 addpiord A + 𝑵 B 𝑵 C 𝑵 A + 𝑵 B + 𝑵 C = A + 𝑵 B + 𝑜 C
8 6 7 sylan A 𝑵 B 𝑵 C 𝑵 A + 𝑵 B + 𝑵 C = A + 𝑵 B + 𝑜 C
9 addpiord A 𝑵 B 𝑵 A + 𝑵 B = A + 𝑜 B
10 9 oveq1d A 𝑵 B 𝑵 A + 𝑵 B + 𝑜 C = A + 𝑜 B + 𝑜 C
11 10 adantr A 𝑵 B 𝑵 C 𝑵 A + 𝑵 B + 𝑜 C = A + 𝑜 B + 𝑜 C
12 8 11 eqtrd A 𝑵 B 𝑵 C 𝑵 A + 𝑵 B + 𝑵 C = A + 𝑜 B + 𝑜 C
13 12 3impa A 𝑵 B 𝑵 C 𝑵 A + 𝑵 B + 𝑵 C = A + 𝑜 B + 𝑜 C
14 addclpi B 𝑵 C 𝑵 B + 𝑵 C 𝑵
15 addpiord A 𝑵 B + 𝑵 C 𝑵 A + 𝑵 B + 𝑵 C = A + 𝑜 B + 𝑵 C
16 14 15 sylan2 A 𝑵 B 𝑵 C 𝑵 A + 𝑵 B + 𝑵 C = A + 𝑜 B + 𝑵 C
17 addpiord B 𝑵 C 𝑵 B + 𝑵 C = B + 𝑜 C
18 17 oveq2d B 𝑵 C 𝑵 A + 𝑜 B + 𝑵 C = A + 𝑜 B + 𝑜 C
19 18 adantl A 𝑵 B 𝑵 C 𝑵 A + 𝑜 B + 𝑵 C = A + 𝑜 B + 𝑜 C
20 16 19 eqtrd A 𝑵 B 𝑵 C 𝑵 A + 𝑵 B + 𝑵 C = A + 𝑜 B + 𝑜 C
21 20 3impb A 𝑵 B 𝑵 C 𝑵 A + 𝑵 B + 𝑵 C = A + 𝑜 B + 𝑜 C
22 5 13 21 3eqtr4d A 𝑵 B 𝑵 C 𝑵 A + 𝑵 B + 𝑵 C = A + 𝑵 B + 𝑵 C
23 dmaddpi dom + 𝑵 = 𝑵 × 𝑵
24 0npi ¬ 𝑵
25 23 24 ndmovass ¬ A 𝑵 B 𝑵 C 𝑵 A + 𝑵 B + 𝑵 C = A + 𝑵 B + 𝑵 C
26 22 25 pm2.61i A + 𝑵 B + 𝑵 C = A + 𝑵 B + 𝑵 C