Theorem nn0addcom

Description: Addition is commutative for nonnegative integers. Proven without ax-mulcom . (Contributed by SN, 1-Feb-2025)

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

Proof

Step	Hyp	Ref	Expression
1		elnn0	$$⊢B\in {\mathbb{N}}_0\leftrightarrow \left(B\in \mathbb{N}\vee B=0\right)$$
2		elnn0	$$⊢A\in {\mathbb{N}}_0\leftrightarrow \left(A\in \mathbb{N}\vee A=0\right)$$
3		nnaddcom	$$⊢\left(A\in \mathbb{N}\wedge B\in \mathbb{N}\right)\to A+B=B+A$$
4		nnre	$$⊢B\in \mathbb{N}\to B\in ℝ$$
5		readdlid	$$⊢B\in ℝ\to 0+B=B$$
6		readdrid	$$⊢B\in ℝ\to B+0=B$$
7	5 6	eqtr4d	$$⊢B\in ℝ\to 0+B=B+0$$
8	4 7	syl	$$⊢B\in \mathbb{N}\to 0+B=B+0$$
9		oveq1	$$⊢A=0\to A+B=0+B$$
10		oveq2	$$⊢A=0\to B+A=B+0$$
11	9 10	eqeq12d	$$⊢A=0\to \left(A+B=B+A\leftrightarrow 0+B=B+0\right)$$
12	8 11	syl5ibrcom	$$⊢B\in \mathbb{N}\to \left(A=0\to A+B=B+A\right)$$
13	12	impcom	$$⊢\left(A=0\wedge B\in \mathbb{N}\right)\to A+B=B+A$$
14	3 13	jaoian	$$⊢\left(\left(A\in \mathbb{N}\vee A=0\right)\wedge B\in \mathbb{N}\right)\to A+B=B+A$$
15	2 14	sylanb	$$⊢\left(A\in {\mathbb{N}}_0\wedge B\in \mathbb{N}\right)\to A+B=B+A$$
16		nn0re	$$⊢A\in {\mathbb{N}}_0\to A\in ℝ$$
17		readdrid	$$⊢A\in ℝ\to A+0=A$$
18		readdlid	$$⊢A\in ℝ\to 0+A=A$$
19	17 18	eqtr4d	$$⊢A\in ℝ\to A+0=0+A$$
20	16 19	syl	$$⊢A\in {\mathbb{N}}_0\to A+0=0+A$$
21		oveq2	$$⊢B=0\to A+B=A+0$$
22		oveq1	$$⊢B=0\to B+A=0+A$$
23	21 22	eqeq12d	$$⊢B=0\to \left(A+B=B+A\leftrightarrow A+0=0+A\right)$$
24	20 23	syl5ibrcom	$$⊢A\in {\mathbb{N}}_0\to \left(B=0\to A+B=B+A\right)$$
25	24	imp	$$⊢\left(A\in {\mathbb{N}}_0\wedge B=0\right)\to A+B=B+A$$
26	15 25	jaodan	$$⊢\left(A\in {\mathbb{N}}_0\wedge \left(B\in \mathbb{N}\vee B=0\right)\right)\to A+B=B+A$$
27	1 26	sylan2b	$$⊢\left(A\in {\mathbb{N}}_0\wedge B\in {\mathbb{N}}_0\right)\to A+B=B+A$$