Theorem nnaddcom

Description: Addition is commutative for natural numbers. Uses fewer axioms than addcom . (Contributed by Steven Nguyen, 9-Dec-2022)

	Ref	Expression
Assertion	nnaddcom	$$⊢\left(A\in \mathbb{N}\wedge B\in \mathbb{N}\right)\to A+B=B+A$$

Proof

Step	Hyp	Ref	Expression
1		oveq1	$$⊢x=1\to x+B=1+B$$
2		oveq2	$$⊢x=1\to B+x=B+1$$
3	1 2	eqeq12d	$$⊢x=1\to \left(x+B=B+x\leftrightarrow 1+B=B+1\right)$$
4	3	imbi2d	$$⊢x=1\to \left(\left(B\in \mathbb{N}\to x+B=B+x\right)\leftrightarrow \left(B\in \mathbb{N}\to 1+B=B+1\right)\right)$$
5		oveq1	$$⊢x=y\to x+B=y+B$$
6		oveq2	$$⊢x=y\to B+x=B+y$$
7	5 6	eqeq12d	$$⊢x=y\to \left(x+B=B+x\leftrightarrow y+B=B+y\right)$$
8	7	imbi2d	$$⊢x=y\to \left(\left(B\in \mathbb{N}\to x+B=B+x\right)\leftrightarrow \left(B\in \mathbb{N}\to y+B=B+y\right)\right)$$
9		oveq1	$$⊢x=y+1\to x+B=y+1+B$$
10		oveq2	$$⊢x=y+1\to B+x=B+y+1$$
11	9 10	eqeq12d	$$⊢x=y+1\to \left(x+B=B+x\leftrightarrow y+1+B=B+y+1\right)$$
12	11	imbi2d	$$⊢x=y+1\to \left(\left(B\in \mathbb{N}\to x+B=B+x\right)\leftrightarrow \left(B\in \mathbb{N}\to y+1+B=B+y+1\right)\right)$$
13		oveq1	$$⊢x=A\to x+B=A+B$$
14		oveq2	$$⊢x=A\to B+x=B+A$$
15	13 14	eqeq12d	$$⊢x=A\to \left(x+B=B+x\leftrightarrow A+B=B+A\right)$$
16	15	imbi2d	$$⊢x=A\to \left(\left(B\in \mathbb{N}\to x+B=B+x\right)\leftrightarrow \left(B\in \mathbb{N}\to A+B=B+A\right)\right)$$
17		nnadd1com	$$⊢B\in \mathbb{N}\to B+1=1+B$$
18	17	eqcomd	$$⊢B\in \mathbb{N}\to 1+B=B+1$$
19		oveq1	$$⊢y+B=B+y\to y+B+1=B+y+1$$
20	17	oveq2d	$$⊢B\in \mathbb{N}\to y+B+1=y+1+B$$
21	20	adantl	$$⊢\left(y\in \mathbb{N}\wedge B\in \mathbb{N}\right)\to y+B+1=y+1+B$$
22		nncn	$$⊢y\in \mathbb{N}\to y\in ℂ$$
23	22	adantr	$$⊢\left(y\in \mathbb{N}\wedge B\in \mathbb{N}\right)\to y\in ℂ$$
24		nncn	$$⊢B\in \mathbb{N}\to B\in ℂ$$
25	24	adantl	$$⊢\left(y\in \mathbb{N}\wedge B\in \mathbb{N}\right)\to B\in ℂ$$
26		1cnd	$$⊢\left(y\in \mathbb{N}\wedge B\in \mathbb{N}\right)\to 1\in ℂ$$
27	23 25 26	addassd	$$⊢\left(y\in \mathbb{N}\wedge B\in \mathbb{N}\right)\to y+B+1=y+B+1$$
28	23 26 25	addassd	$$⊢\left(y\in \mathbb{N}\wedge B\in \mathbb{N}\right)\to y+1+B=y+1+B$$
29	21 27 28	3eqtr4d	$$⊢\left(y\in \mathbb{N}\wedge B\in \mathbb{N}\right)\to y+B+1=y+1+B$$
30	25 23 26	addassd	$$⊢\left(y\in \mathbb{N}\wedge B\in \mathbb{N}\right)\to B+y+1=B+y+1$$
31	29 30	eqeq12d	$$⊢\left(y\in \mathbb{N}\wedge B\in \mathbb{N}\right)\to \left(y+B+1=B+y+1\leftrightarrow y+1+B=B+y+1\right)$$
32	19 31	imbitrid	$$⊢\left(y\in \mathbb{N}\wedge B\in \mathbb{N}\right)\to \left(y+B=B+y\to y+1+B=B+y+1\right)$$
33	32	ex	$$⊢y\in \mathbb{N}\to \left(B\in \mathbb{N}\to \left(y+B=B+y\to y+1+B=B+y+1\right)\right)$$
34	33	a2d	$$⊢y\in \mathbb{N}\to \left(\left(B\in \mathbb{N}\to y+B=B+y\right)\to \left(B\in \mathbb{N}\to y+1+B=B+y+1\right)\right)$$
35	4 8 12 16 18 34	nnind	$$⊢A\in \mathbb{N}\to \left(B\in \mathbb{N}\to A+B=B+A\right)$$
36	35	imp	$$⊢\left(A\in \mathbb{N}\wedge B\in \mathbb{N}\right)\to A+B=B+A$$