Theorem addasspi

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

	Ref	Expression
Assertion	addasspi	$$⊢\left(A{+}_{𝑵}B\right){+}_{𝑵}C=A{+}_{𝑵}\left(B{+}_{𝑵}C\right)$$

Proof

Step	Hyp	Ref	Expression
1		pinn	$$⊢A\in 𝑵\to A\in \mathrm{\omega }$$
2		pinn	$$⊢B\in 𝑵\to B\in \mathrm{\omega }$$
3		pinn	$$⊢C\in 𝑵\to C\in \mathrm{\omega }$$
4		nnaass	$$⊢\left(A\in \mathrm{\omega }\wedge B\in \mathrm{\omega }\wedge C\in \mathrm{\omega }\right)\to \left(A{+}_{𝑜}B\right){+}_{𝑜}C=A{+}_{𝑜}\left(B{+}_{𝑜}C\right)$$
5	1 2 3 4	syl3an	$$⊢\left(A\in 𝑵\wedge B\in 𝑵\wedge C\in 𝑵\right)\to \left(A{+}_{𝑜}B\right){+}_{𝑜}C=A{+}_{𝑜}\left(B{+}_{𝑜}C\right)$$
6		addclpi	$$⊢\left(A\in 𝑵\wedge B\in 𝑵\right)\to A{+}_{𝑵}B\in 𝑵$$
7		addpiord	$$⊢\left(A{+}_{𝑵}B\in 𝑵\wedge C\in 𝑵\right)\to \left(A{+}_{𝑵}B\right){+}_{𝑵}C=\left(A{+}_{𝑵}B\right){+}_{𝑜}C$$
8	6 7	sylan	$$⊢\left(\left(A\in 𝑵\wedge B\in 𝑵\right)\wedge C\in 𝑵\right)\to \left(A{+}_{𝑵}B\right){+}_{𝑵}C=\left(A{+}_{𝑵}B\right){+}_{𝑜}C$$
9		addpiord	$$⊢\left(A\in 𝑵\wedge B\in 𝑵\right)\to A{+}_{𝑵}B=A{+}_{𝑜}B$$
10	9	oveq1d	$$⊢\left(A\in 𝑵\wedge B\in 𝑵\right)\to \left(A{+}_{𝑵}B\right){+}_{𝑜}C=\left(A{+}_{𝑜}B\right){+}_{𝑜}C$$
11	10	adantr	$$⊢\left(\left(A\in 𝑵\wedge B\in 𝑵\right)\wedge C\in 𝑵\right)\to \left(A{+}_{𝑵}B\right){+}_{𝑜}C=\left(A{+}_{𝑜}B\right){+}_{𝑜}C$$
12	8 11	eqtrd	$$⊢\left(\left(A\in 𝑵\wedge B\in 𝑵\right)\wedge C\in 𝑵\right)\to \left(A{+}_{𝑵}B\right){+}_{𝑵}C=\left(A{+}_{𝑜}B\right){+}_{𝑜}C$$
13	12	3impa	$$⊢\left(A\in 𝑵\wedge B\in 𝑵\wedge C\in 𝑵\right)\to \left(A{+}_{𝑵}B\right){+}_{𝑵}C=\left(A{+}_{𝑜}B\right){+}_{𝑜}C$$
14		addclpi	$$⊢\left(B\in 𝑵\wedge C\in 𝑵\right)\to B{+}_{𝑵}C\in 𝑵$$
15		addpiord	$$⊢\left(A\in 𝑵\wedge B{+}_{𝑵}C\in 𝑵\right)\to A{+}_{𝑵}\left(B{+}_{𝑵}C\right)=A{+}_{𝑜}\left(B{+}_{𝑵}C\right)$$
16	14 15	sylan2	$$⊢\left(A\in 𝑵\wedge \left(B\in 𝑵\wedge C\in 𝑵\right)\right)\to A{+}_{𝑵}\left(B{+}_{𝑵}C\right)=A{+}_{𝑜}\left(B{+}_{𝑵}C\right)$$
17		addpiord	$$⊢\left(B\in 𝑵\wedge C\in 𝑵\right)\to B{+}_{𝑵}C=B{+}_{𝑜}C$$
18	17	oveq2d	$$⊢\left(B\in 𝑵\wedge C\in 𝑵\right)\to A{+}_{𝑜}\left(B{+}_{𝑵}C\right)=A{+}_{𝑜}\left(B{+}_{𝑜}C\right)$$
19	18	adantl	$$⊢\left(A\in 𝑵\wedge \left(B\in 𝑵\wedge C\in 𝑵\right)\right)\to A{+}_{𝑜}\left(B{+}_{𝑵}C\right)=A{+}_{𝑜}\left(B{+}_{𝑜}C\right)$$
20	16 19	eqtrd	$$⊢\left(A\in 𝑵\wedge \left(B\in 𝑵\wedge C\in 𝑵\right)\right)\to A{+}_{𝑵}\left(B{+}_{𝑵}C\right)=A{+}_{𝑜}\left(B{+}_{𝑜}C\right)$$
21	20	3impb	$$⊢\left(A\in 𝑵\wedge B\in 𝑵\wedge C\in 𝑵\right)\to A{+}_{𝑵}\left(B{+}_{𝑵}C\right)=A{+}_{𝑜}\left(B{+}_{𝑜}C\right)$$
22	5 13 21	3eqtr4d	$$⊢\left(A\in 𝑵\wedge B\in 𝑵\wedge C\in 𝑵\right)\to \left(A{+}_{𝑵}B\right){+}_{𝑵}C=A{+}_{𝑵}\left(B{+}_{𝑵}C\right)$$
23		dmaddpi	$$⊢\mathrm{dom}{+}_{𝑵}=𝑵\times 𝑵$$
24		0npi	$$⊢\neg \varnothing \in 𝑵$$
25	23 24	ndmovass	$$⊢\neg \left(A\in 𝑵\wedge B\in 𝑵\wedge C\in 𝑵\right)\to \left(A{+}_{𝑵}B\right){+}_{𝑵}C=A{+}_{𝑵}\left(B{+}_{𝑵}C\right)$$
26	22 25	pm2.61i	$$⊢\left(A{+}_{𝑵}B\right){+}_{𝑵}C=A{+}_{𝑵}\left(B{+}_{𝑵}C\right)$$