Theorem nnaass

Description: Addition of natural numbers is associative. Theorem 4K(1) of Enderton p. 81. (Contributed by NM, 20-Sep-1995) (Revised by Mario Carneiro, 15-Nov-2014)

	Ref	Expression
Assertion	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)$$

Proof

Step	Hyp	Ref	Expression
1		oveq2	$$⊢x=C\to \left(A{+}_{𝑜}B\right){+}_{𝑜}x=\left(A{+}_{𝑜}B\right){+}_{𝑜}C$$
2		oveq2	$$⊢x=C\to B{+}_{𝑜}x=B{+}_{𝑜}C$$
3	2	oveq2d	$$⊢x=C\to A{+}_{𝑜}\left(B{+}_{𝑜}x\right)=A{+}_{𝑜}\left(B{+}_{𝑜}C\right)$$
4	1 3	eqeq12d	$$⊢x=C\to \left(\left(A{+}_{𝑜}B\right){+}_{𝑜}x=A{+}_{𝑜}\left(B{+}_{𝑜}x\right)\leftrightarrow \left(A{+}_{𝑜}B\right){+}_{𝑜}C=A{+}_{𝑜}\left(B{+}_{𝑜}C\right)\right)$$
5	4	imbi2d	$$⊢x=C\to \left(\left(\left(A\in \mathrm{\omega }\wedge B\in \mathrm{\omega }\right)\to \left(A{+}_{𝑜}B\right){+}_{𝑜}x=A{+}_{𝑜}\left(B{+}_{𝑜}x\right)\right)\leftrightarrow \left(\left(A\in \mathrm{\omega }\wedge B\in \mathrm{\omega }\right)\to \left(A{+}_{𝑜}B\right){+}_{𝑜}C=A{+}_{𝑜}\left(B{+}_{𝑜}C\right)\right)\right)$$
6		oveq2	$$⊢x=\varnothing \to \left(A{+}_{𝑜}B\right){+}_{𝑜}x=\left(A{+}_{𝑜}B\right){+}_{𝑜}\varnothing$$
7		oveq2	$$⊢x=\varnothing \to B{+}_{𝑜}x=B{+}_{𝑜}\varnothing$$
8	7	oveq2d	$$⊢x=\varnothing \to A{+}_{𝑜}\left(B{+}_{𝑜}x\right)=A{+}_{𝑜}\left(B{+}_{𝑜}\varnothing \right)$$
9	6 8	eqeq12d	$$⊢x=\varnothing \to \left(\left(A{+}_{𝑜}B\right){+}_{𝑜}x=A{+}_{𝑜}\left(B{+}_{𝑜}x\right)\leftrightarrow \left(A{+}_{𝑜}B\right){+}_{𝑜}\varnothing =A{+}_{𝑜}\left(B{+}_{𝑜}\varnothing \right)\right)$$
10		oveq2	$$⊢x=y\to \left(A{+}_{𝑜}B\right){+}_{𝑜}x=\left(A{+}_{𝑜}B\right){+}_{𝑜}y$$
11		oveq2	$$⊢x=y\to B{+}_{𝑜}x=B{+}_{𝑜}y$$
12	11	oveq2d	$$⊢x=y\to A{+}_{𝑜}\left(B{+}_{𝑜}x\right)=A{+}_{𝑜}\left(B{+}_{𝑜}y\right)$$
13	10 12	eqeq12d	$$⊢x=y\to \left(\left(A{+}_{𝑜}B\right){+}_{𝑜}x=A{+}_{𝑜}\left(B{+}_{𝑜}x\right)\leftrightarrow \left(A{+}_{𝑜}B\right){+}_{𝑜}y=A{+}_{𝑜}\left(B{+}_{𝑜}y\right)\right)$$
14		oveq2	$$⊢x=\mathrm{suc}y\to \left(A{+}_{𝑜}B\right){+}_{𝑜}x=\left(A{+}_{𝑜}B\right){+}_{𝑜}\mathrm{suc}y$$
15		oveq2	$$⊢x=\mathrm{suc}y\to B{+}_{𝑜}x=B{+}_{𝑜}\mathrm{suc}y$$
16	15	oveq2d	$$⊢x=\mathrm{suc}y\to A{+}_{𝑜}\left(B{+}_{𝑜}x\right)=A{+}_{𝑜}\left(B{+}_{𝑜}\mathrm{suc}y\right)$$
17	14 16	eqeq12d	$$⊢x=\mathrm{suc}y\to \left(\left(A{+}_{𝑜}B\right){+}_{𝑜}x=A{+}_{𝑜}\left(B{+}_{𝑜}x\right)\leftrightarrow \left(A{+}_{𝑜}B\right){+}_{𝑜}\mathrm{suc}y=A{+}_{𝑜}\left(B{+}_{𝑜}\mathrm{suc}y\right)\right)$$
18		nnacl	$$⊢\left(A\in \mathrm{\omega }\wedge B\in \mathrm{\omega }\right)\to A{+}_{𝑜}B\in \mathrm{\omega }$$
19		nna0	$$⊢A{+}_{𝑜}B\in \mathrm{\omega }\to \left(A{+}_{𝑜}B\right){+}_{𝑜}\varnothing =A{+}_{𝑜}B$$
20	18 19	syl	$$⊢\left(A\in \mathrm{\omega }\wedge B\in \mathrm{\omega }\right)\to \left(A{+}_{𝑜}B\right){+}_{𝑜}\varnothing =A{+}_{𝑜}B$$
21		nna0	$$⊢B\in \mathrm{\omega }\to B{+}_{𝑜}\varnothing =B$$
22	21	oveq2d	$$⊢B\in \mathrm{\omega }\to A{+}_{𝑜}\left(B{+}_{𝑜}\varnothing \right)=A{+}_{𝑜}B$$
23	22	adantl	$$⊢\left(A\in \mathrm{\omega }\wedge B\in \mathrm{\omega }\right)\to A{+}_{𝑜}\left(B{+}_{𝑜}\varnothing \right)=A{+}_{𝑜}B$$
24	20 23	eqtr4d	$$⊢\left(A\in \mathrm{\omega }\wedge B\in \mathrm{\omega }\right)\to \left(A{+}_{𝑜}B\right){+}_{𝑜}\varnothing =A{+}_{𝑜}\left(B{+}_{𝑜}\varnothing \right)$$
25		suceq	$$⊢\left(A{+}_{𝑜}B\right){+}_{𝑜}y=A{+}_{𝑜}\left(B{+}_{𝑜}y\right)\to \mathrm{suc}\left(\left(A{+}_{𝑜}B\right){+}_{𝑜}y\right)=\mathrm{suc}\left(A{+}_{𝑜}\left(B{+}_{𝑜}y\right)\right)$$
26		nnasuc	$$⊢\left(A{+}_{𝑜}B\in \mathrm{\omega }\wedge y\in \mathrm{\omega }\right)\to \left(A{+}_{𝑜}B\right){+}_{𝑜}\mathrm{suc}y=\mathrm{suc}\left(\left(A{+}_{𝑜}B\right){+}_{𝑜}y\right)$$
27	18 26	sylan	$$⊢\left(\left(A\in \mathrm{\omega }\wedge B\in \mathrm{\omega }\right)\wedge y\in \mathrm{\omega }\right)\to \left(A{+}_{𝑜}B\right){+}_{𝑜}\mathrm{suc}y=\mathrm{suc}\left(\left(A{+}_{𝑜}B\right){+}_{𝑜}y\right)$$
28		nnasuc	$$⊢\left(B\in \mathrm{\omega }\wedge y\in \mathrm{\omega }\right)\to B{+}_{𝑜}\mathrm{suc}y=\mathrm{suc}\left(B{+}_{𝑜}y\right)$$
29	28	oveq2d	$$⊢\left(B\in \mathrm{\omega }\wedge y\in \mathrm{\omega }\right)\to A{+}_{𝑜}\left(B{+}_{𝑜}\mathrm{suc}y\right)=A{+}_{𝑜}\mathrm{suc}\left(B{+}_{𝑜}y\right)$$
30	29	adantl	$$⊢\left(A\in \mathrm{\omega }\wedge \left(B\in \mathrm{\omega }\wedge y\in \mathrm{\omega }\right)\right)\to A{+}_{𝑜}\left(B{+}_{𝑜}\mathrm{suc}y\right)=A{+}_{𝑜}\mathrm{suc}\left(B{+}_{𝑜}y\right)$$
31		nnacl	$$⊢\left(B\in \mathrm{\omega }\wedge y\in \mathrm{\omega }\right)\to B{+}_{𝑜}y\in \mathrm{\omega }$$
32		nnasuc	$$⊢\left(A\in \mathrm{\omega }\wedge B{+}_{𝑜}y\in \mathrm{\omega }\right)\to A{+}_{𝑜}\mathrm{suc}\left(B{+}_{𝑜}y\right)=\mathrm{suc}\left(A{+}_{𝑜}\left(B{+}_{𝑜}y\right)\right)$$
33	31 32	sylan2	$$⊢\left(A\in \mathrm{\omega }\wedge \left(B\in \mathrm{\omega }\wedge y\in \mathrm{\omega }\right)\right)\to A{+}_{𝑜}\mathrm{suc}\left(B{+}_{𝑜}y\right)=\mathrm{suc}\left(A{+}_{𝑜}\left(B{+}_{𝑜}y\right)\right)$$
34	30 33	eqtrd	$$⊢\left(A\in \mathrm{\omega }\wedge \left(B\in \mathrm{\omega }\wedge y\in \mathrm{\omega }\right)\right)\to A{+}_{𝑜}\left(B{+}_{𝑜}\mathrm{suc}y\right)=\mathrm{suc}\left(A{+}_{𝑜}\left(B{+}_{𝑜}y\right)\right)$$
35	34	anassrs	$$⊢\left(\left(A\in \mathrm{\omega }\wedge B\in \mathrm{\omega }\right)\wedge y\in \mathrm{\omega }\right)\to A{+}_{𝑜}\left(B{+}_{𝑜}\mathrm{suc}y\right)=\mathrm{suc}\left(A{+}_{𝑜}\left(B{+}_{𝑜}y\right)\right)$$
36	27 35	eqeq12d	$$⊢\left(\left(A\in \mathrm{\omega }\wedge B\in \mathrm{\omega }\right)\wedge y\in \mathrm{\omega }\right)\to \left(\left(A{+}_{𝑜}B\right){+}_{𝑜}\mathrm{suc}y=A{+}_{𝑜}\left(B{+}_{𝑜}\mathrm{suc}y\right)\leftrightarrow \mathrm{suc}\left(\left(A{+}_{𝑜}B\right){+}_{𝑜}y\right)=\mathrm{suc}\left(A{+}_{𝑜}\left(B{+}_{𝑜}y\right)\right)\right)$$
37	25 36	imbitrrid	$$⊢\left(\left(A\in \mathrm{\omega }\wedge B\in \mathrm{\omega }\right)\wedge y\in \mathrm{\omega }\right)\to \left(\left(A{+}_{𝑜}B\right){+}_{𝑜}y=A{+}_{𝑜}\left(B{+}_{𝑜}y\right)\to \left(A{+}_{𝑜}B\right){+}_{𝑜}\mathrm{suc}y=A{+}_{𝑜}\left(B{+}_{𝑜}\mathrm{suc}y\right)\right)$$
38	37	expcom	$$⊢y\in \mathrm{\omega }\to \left(\left(A\in \mathrm{\omega }\wedge B\in \mathrm{\omega }\right)\to \left(\left(A{+}_{𝑜}B\right){+}_{𝑜}y=A{+}_{𝑜}\left(B{+}_{𝑜}y\right)\to \left(A{+}_{𝑜}B\right){+}_{𝑜}\mathrm{suc}y=A{+}_{𝑜}\left(B{+}_{𝑜}\mathrm{suc}y\right)\right)\right)$$
39	9 13 17 24 38	finds2	$$⊢x\in \mathrm{\omega }\to \left(\left(A\in \mathrm{\omega }\wedge B\in \mathrm{\omega }\right)\to \left(A{+}_{𝑜}B\right){+}_{𝑜}x=A{+}_{𝑜}\left(B{+}_{𝑜}x\right)\right)$$
40	5 39	vtoclga	$$⊢C\in \mathrm{\omega }\to \left(\left(A\in \mathrm{\omega }\wedge B\in \mathrm{\omega }\right)\to \left(A{+}_{𝑜}B\right){+}_{𝑜}C=A{+}_{𝑜}\left(B{+}_{𝑜}C\right)\right)$$
41	40	com12	$$⊢\left(A\in \mathrm{\omega }\wedge B\in \mathrm{\omega }\right)\to \left(C\in \mathrm{\omega }\to \left(A{+}_{𝑜}B\right){+}_{𝑜}C=A{+}_{𝑜}\left(B{+}_{𝑜}C\right)\right)$$
42	41	3impia	$$⊢\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)$$