Theorem nnacom

Description: Addition of natural numbers is commutative. Theorem 4K(2) of Enderton p. 81. (Contributed by NM, 6-May-1995) (Revised by Mario Carneiro, 15-Nov-2014)

	Ref	Expression
Assertion	nnacom	$$⊢\left(A\in \mathrm{\omega }\wedge B\in \mathrm{\omega }\right)\to A{+}_{𝑜}B=B{+}_{𝑜}A$$

Proof

Step	Hyp	Ref	Expression
1		oveq1	$$⊢x=A\to x{+}_{𝑜}B=A{+}_{𝑜}B$$
2		oveq2	$$⊢x=A\to B{+}_{𝑜}x=B{+}_{𝑜}A$$
3	1 2	eqeq12d	$$⊢x=A\to \left(x{+}_{𝑜}B=B{+}_{𝑜}x\leftrightarrow A{+}_{𝑜}B=B{+}_{𝑜}A\right)$$
4	3	imbi2d	$$⊢x=A\to \left(\left(B\in \mathrm{\omega }\to x{+}_{𝑜}B=B{+}_{𝑜}x\right)\leftrightarrow \left(B\in \mathrm{\omega }\to A{+}_{𝑜}B=B{+}_{𝑜}A\right)\right)$$
5		oveq1	$$⊢x=\varnothing \to x{+}_{𝑜}B=\varnothing {+}_{𝑜}B$$
6		oveq2	$$⊢x=\varnothing \to B{+}_{𝑜}x=B{+}_{𝑜}\varnothing$$
7	5 6	eqeq12d	$$⊢x=\varnothing \to \left(x{+}_{𝑜}B=B{+}_{𝑜}x\leftrightarrow \varnothing {+}_{𝑜}B=B{+}_{𝑜}\varnothing \right)$$
8		oveq1	$$⊢x=y\to x{+}_{𝑜}B=y{+}_{𝑜}B$$
9		oveq2	$$⊢x=y\to B{+}_{𝑜}x=B{+}_{𝑜}y$$
10	8 9	eqeq12d	$$⊢x=y\to \left(x{+}_{𝑜}B=B{+}_{𝑜}x\leftrightarrow y{+}_{𝑜}B=B{+}_{𝑜}y\right)$$
11		oveq1	$$⊢x=\mathrm{suc}y\to x{+}_{𝑜}B=\mathrm{suc}y{+}_{𝑜}B$$
12		oveq2	$$⊢x=\mathrm{suc}y\to B{+}_{𝑜}x=B{+}_{𝑜}\mathrm{suc}y$$
13	11 12	eqeq12d	$$⊢x=\mathrm{suc}y\to \left(x{+}_{𝑜}B=B{+}_{𝑜}x\leftrightarrow \mathrm{suc}y{+}_{𝑜}B=B{+}_{𝑜}\mathrm{suc}y\right)$$
14		nna0r	$$⊢B\in \mathrm{\omega }\to \varnothing {+}_{𝑜}B=B$$
15		nna0	$$⊢B\in \mathrm{\omega }\to B{+}_{𝑜}\varnothing =B$$
16	14 15	eqtr4d	$$⊢B\in \mathrm{\omega }\to \varnothing {+}_{𝑜}B=B{+}_{𝑜}\varnothing$$
17		suceq	$$⊢y{+}_{𝑜}B=B{+}_{𝑜}y\to \mathrm{suc}\left(y{+}_{𝑜}B\right)=\mathrm{suc}\left(B{+}_{𝑜}y\right)$$
18		oveq2	$$⊢x=B\to \mathrm{suc}y{+}_{𝑜}x=\mathrm{suc}y{+}_{𝑜}B$$
19		oveq2	$$⊢x=B\to y{+}_{𝑜}x=y{+}_{𝑜}B$$
20		suceq	$$⊢y{+}_{𝑜}x=y{+}_{𝑜}B\to \mathrm{suc}\left(y{+}_{𝑜}x\right)=\mathrm{suc}\left(y{+}_{𝑜}B\right)$$
21	19 20	syl	$$⊢x=B\to \mathrm{suc}\left(y{+}_{𝑜}x\right)=\mathrm{suc}\left(y{+}_{𝑜}B\right)$$
22	18 21	eqeq12d	$$⊢x=B\to \left(\mathrm{suc}y{+}_{𝑜}x=\mathrm{suc}\left(y{+}_{𝑜}x\right)\leftrightarrow \mathrm{suc}y{+}_{𝑜}B=\mathrm{suc}\left(y{+}_{𝑜}B\right)\right)$$
23	22	imbi2d	$$⊢x=B\to \left(\left(y\in \mathrm{\omega }\to \mathrm{suc}y{+}_{𝑜}x=\mathrm{suc}\left(y{+}_{𝑜}x\right)\right)\leftrightarrow \left(y\in \mathrm{\omega }\to \mathrm{suc}y{+}_{𝑜}B=\mathrm{suc}\left(y{+}_{𝑜}B\right)\right)\right)$$
24		oveq2	$$⊢x=\varnothing \to \mathrm{suc}y{+}_{𝑜}x=\mathrm{suc}y{+}_{𝑜}\varnothing$$
25		oveq2	$$⊢x=\varnothing \to y{+}_{𝑜}x=y{+}_{𝑜}\varnothing$$
26		suceq	$$⊢y{+}_{𝑜}x=y{+}_{𝑜}\varnothing \to \mathrm{suc}\left(y{+}_{𝑜}x\right)=\mathrm{suc}\left(y{+}_{𝑜}\varnothing \right)$$
27	25 26	syl	$$⊢x=\varnothing \to \mathrm{suc}\left(y{+}_{𝑜}x\right)=\mathrm{suc}\left(y{+}_{𝑜}\varnothing \right)$$
28	24 27	eqeq12d	$$⊢x=\varnothing \to \left(\mathrm{suc}y{+}_{𝑜}x=\mathrm{suc}\left(y{+}_{𝑜}x\right)\leftrightarrow \mathrm{suc}y{+}_{𝑜}\varnothing =\mathrm{suc}\left(y{+}_{𝑜}\varnothing \right)\right)$$
29		oveq2	$$⊢x=z\to \mathrm{suc}y{+}_{𝑜}x=\mathrm{suc}y{+}_{𝑜}z$$
30		oveq2	$$⊢x=z\to y{+}_{𝑜}x=y{+}_{𝑜}z$$
31		suceq	$$⊢y{+}_{𝑜}x=y{+}_{𝑜}z\to \mathrm{suc}\left(y{+}_{𝑜}x\right)=\mathrm{suc}\left(y{+}_{𝑜}z\right)$$
32	30 31	syl	$$⊢x=z\to \mathrm{suc}\left(y{+}_{𝑜}x\right)=\mathrm{suc}\left(y{+}_{𝑜}z\right)$$
33	29 32	eqeq12d	$$⊢x=z\to \left(\mathrm{suc}y{+}_{𝑜}x=\mathrm{suc}\left(y{+}_{𝑜}x\right)\leftrightarrow \mathrm{suc}y{+}_{𝑜}z=\mathrm{suc}\left(y{+}_{𝑜}z\right)\right)$$
34		oveq2	$$⊢x=\mathrm{suc}z\to \mathrm{suc}y{+}_{𝑜}x=\mathrm{suc}y{+}_{𝑜}\mathrm{suc}z$$
35		oveq2	$$⊢x=\mathrm{suc}z\to y{+}_{𝑜}x=y{+}_{𝑜}\mathrm{suc}z$$
36		suceq	$$⊢y{+}_{𝑜}x=y{+}_{𝑜}\mathrm{suc}z\to \mathrm{suc}\left(y{+}_{𝑜}x\right)=\mathrm{suc}\left(y{+}_{𝑜}\mathrm{suc}z\right)$$
37	35 36	syl	$$⊢x=\mathrm{suc}z\to \mathrm{suc}\left(y{+}_{𝑜}x\right)=\mathrm{suc}\left(y{+}_{𝑜}\mathrm{suc}z\right)$$
38	34 37	eqeq12d	$$⊢x=\mathrm{suc}z\to \left(\mathrm{suc}y{+}_{𝑜}x=\mathrm{suc}\left(y{+}_{𝑜}x\right)\leftrightarrow \mathrm{suc}y{+}_{𝑜}\mathrm{suc}z=\mathrm{suc}\left(y{+}_{𝑜}\mathrm{suc}z\right)\right)$$
39		peano2	$$⊢y\in \mathrm{\omega }\to \mathrm{suc}y\in \mathrm{\omega }$$
40		nna0	$$⊢\mathrm{suc}y\in \mathrm{\omega }\to \mathrm{suc}y{+}_{𝑜}\varnothing =\mathrm{suc}y$$
41	39 40	syl	$$⊢y\in \mathrm{\omega }\to \mathrm{suc}y{+}_{𝑜}\varnothing =\mathrm{suc}y$$
42		nna0	$$⊢y\in \mathrm{\omega }\to y{+}_{𝑜}\varnothing =y$$
43		suceq	$$⊢y{+}_{𝑜}\varnothing =y\to \mathrm{suc}\left(y{+}_{𝑜}\varnothing \right)=\mathrm{suc}y$$
44	42 43	syl	$$⊢y\in \mathrm{\omega }\to \mathrm{suc}\left(y{+}_{𝑜}\varnothing \right)=\mathrm{suc}y$$
45	41 44	eqtr4d	$$⊢y\in \mathrm{\omega }\to \mathrm{suc}y{+}_{𝑜}\varnothing =\mathrm{suc}\left(y{+}_{𝑜}\varnothing \right)$$
46		suceq	$$⊢\mathrm{suc}y{+}_{𝑜}z=\mathrm{suc}\left(y{+}_{𝑜}z\right)\to \mathrm{suc}\left(\mathrm{suc}y{+}_{𝑜}z\right)=\mathrm{suc}\mathrm{suc}\left(y{+}_{𝑜}z\right)$$
47		nnasuc	$$⊢\left(\mathrm{suc}y\in \mathrm{\omega }\wedge z\in \mathrm{\omega }\right)\to \mathrm{suc}y{+}_{𝑜}\mathrm{suc}z=\mathrm{suc}\left(\mathrm{suc}y{+}_{𝑜}z\right)$$
48	39 47	sylan	$$⊢\left(y\in \mathrm{\omega }\wedge z\in \mathrm{\omega }\right)\to \mathrm{suc}y{+}_{𝑜}\mathrm{suc}z=\mathrm{suc}\left(\mathrm{suc}y{+}_{𝑜}z\right)$$
49		nnasuc	$$⊢\left(y\in \mathrm{\omega }\wedge z\in \mathrm{\omega }\right)\to y{+}_{𝑜}\mathrm{suc}z=\mathrm{suc}\left(y{+}_{𝑜}z\right)$$
50		suceq	$$⊢y{+}_{𝑜}\mathrm{suc}z=\mathrm{suc}\left(y{+}_{𝑜}z\right)\to \mathrm{suc}\left(y{+}_{𝑜}\mathrm{suc}z\right)=\mathrm{suc}\mathrm{suc}\left(y{+}_{𝑜}z\right)$$
51	49 50	syl	$$⊢\left(y\in \mathrm{\omega }\wedge z\in \mathrm{\omega }\right)\to \mathrm{suc}\left(y{+}_{𝑜}\mathrm{suc}z\right)=\mathrm{suc}\mathrm{suc}\left(y{+}_{𝑜}z\right)$$
52	48 51	eqeq12d	$$⊢\left(y\in \mathrm{\omega }\wedge z\in \mathrm{\omega }\right)\to \left(\mathrm{suc}y{+}_{𝑜}\mathrm{suc}z=\mathrm{suc}\left(y{+}_{𝑜}\mathrm{suc}z\right)\leftrightarrow \mathrm{suc}\left(\mathrm{suc}y{+}_{𝑜}z\right)=\mathrm{suc}\mathrm{suc}\left(y{+}_{𝑜}z\right)\right)$$
53	46 52	imbitrrid	$$⊢\left(y\in \mathrm{\omega }\wedge z\in \mathrm{\omega }\right)\to \left(\mathrm{suc}y{+}_{𝑜}z=\mathrm{suc}\left(y{+}_{𝑜}z\right)\to \mathrm{suc}y{+}_{𝑜}\mathrm{suc}z=\mathrm{suc}\left(y{+}_{𝑜}\mathrm{suc}z\right)\right)$$
54	53	expcom	$$⊢z\in \mathrm{\omega }\to \left(y\in \mathrm{\omega }\to \left(\mathrm{suc}y{+}_{𝑜}z=\mathrm{suc}\left(y{+}_{𝑜}z\right)\to \mathrm{suc}y{+}_{𝑜}\mathrm{suc}z=\mathrm{suc}\left(y{+}_{𝑜}\mathrm{suc}z\right)\right)\right)$$
55	28 33 38 45 54	finds2	$$⊢x\in \mathrm{\omega }\to \left(y\in \mathrm{\omega }\to \mathrm{suc}y{+}_{𝑜}x=\mathrm{suc}\left(y{+}_{𝑜}x\right)\right)$$
56	23 55	vtoclga	$$⊢B\in \mathrm{\omega }\to \left(y\in \mathrm{\omega }\to \mathrm{suc}y{+}_{𝑜}B=\mathrm{suc}\left(y{+}_{𝑜}B\right)\right)$$
57	56	imp	$$⊢\left(B\in \mathrm{\omega }\wedge y\in \mathrm{\omega }\right)\to \mathrm{suc}y{+}_{𝑜}B=\mathrm{suc}\left(y{+}_{𝑜}B\right)$$
58		nnasuc	$$⊢\left(B\in \mathrm{\omega }\wedge y\in \mathrm{\omega }\right)\to B{+}_{𝑜}\mathrm{suc}y=\mathrm{suc}\left(B{+}_{𝑜}y\right)$$
59	57 58	eqeq12d	$$⊢\left(B\in \mathrm{\omega }\wedge y\in \mathrm{\omega }\right)\to \left(\mathrm{suc}y{+}_{𝑜}B=B{+}_{𝑜}\mathrm{suc}y\leftrightarrow \mathrm{suc}\left(y{+}_{𝑜}B\right)=\mathrm{suc}\left(B{+}_{𝑜}y\right)\right)$$
60	17 59	imbitrrid	$$⊢\left(B\in \mathrm{\omega }\wedge y\in \mathrm{\omega }\right)\to \left(y{+}_{𝑜}B=B{+}_{𝑜}y\to \mathrm{suc}y{+}_{𝑜}B=B{+}_{𝑜}\mathrm{suc}y\right)$$
61	60	expcom	$$⊢y\in \mathrm{\omega }\to \left(B\in \mathrm{\omega }\to \left(y{+}_{𝑜}B=B{+}_{𝑜}y\to \mathrm{suc}y{+}_{𝑜}B=B{+}_{𝑜}\mathrm{suc}y\right)\right)$$
62	7 10 13 16 61	finds2	$$⊢x\in \mathrm{\omega }\to \left(B\in \mathrm{\omega }\to x{+}_{𝑜}B=B{+}_{𝑜}x\right)$$
63	4 62	vtoclga	$$⊢A\in \mathrm{\omega }\to \left(B\in \mathrm{\omega }\to A{+}_{𝑜}B=B{+}_{𝑜}A\right)$$
64	63	imp	$$⊢\left(A\in \mathrm{\omega }\wedge B\in \mathrm{\omega }\right)\to A{+}_{𝑜}B=B{+}_{𝑜}A$$