Theorem nnadd1com

Description: Addition with 1 is commutative for natural numbers. (Contributed by Steven Nguyen, 9-Dec-2022)

	Ref	Expression
Assertion	nnadd1com	$$⊢A\in \mathbb{N}\to A+1=1+A$$

Proof

Step	Hyp	Ref	Expression
1		oveq1	$$⊢x=1\to x+1=1+1$$
2		oveq2	$$⊢x=1\to 1+x=1+1$$
3	1 2	eqeq12d	$$⊢x=1\to \left(x+1=1+x\leftrightarrow 1+1=1+1\right)$$
4		oveq1	$$⊢x=y\to x+1=y+1$$
5		oveq2	$$⊢x=y\to 1+x=1+y$$
6	4 5	eqeq12d	$$⊢x=y\to \left(x+1=1+x\leftrightarrow y+1=1+y\right)$$
7		oveq1	$$⊢x=y+1\to x+1=y+1+1$$
8		oveq2	$$⊢x=y+1\to 1+x=1+y+1$$
9	7 8	eqeq12d	$$⊢x=y+1\to \left(x+1=1+x\leftrightarrow y+1+1=1+y+1\right)$$
10		oveq1	$$⊢x=A\to x+1=A+1$$
11		oveq2	$$⊢x=A\to 1+x=1+A$$
12	10 11	eqeq12d	$$⊢x=A\to \left(x+1=1+x\leftrightarrow A+1=1+A\right)$$
13		eqid	$$⊢1+1=1+1$$
14		oveq1	$$⊢y+1=1+y\to y+1+1=1+y+1$$
15		1cnd	$$⊢y\in \mathbb{N}\to 1\in ℂ$$
16		nncn	$$⊢y\in \mathbb{N}\to y\in ℂ$$
17	15 16 15	addassd	$$⊢y\in \mathbb{N}\to 1+y+1=1+y+1$$
18	14 17	sylan9eqr	$$⊢\left(y\in \mathbb{N}\wedge y+1=1+y\right)\to y+1+1=1+y+1$$
19	18	ex	$$⊢y\in \mathbb{N}\to \left(y+1=1+y\to y+1+1=1+y+1\right)$$
20	3 6 9 12 13 19	nnind	$$⊢A\in \mathbb{N}\to A+1=1+A$$