Theorem nn0mulcom

Description: Multiplication is commutative for nonnegative integers. Proven without ax-mulcom . (Contributed by SN, 25-Jan-2025)

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

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		nnmulcom	$$⊢\left(A\in \mathbb{N}\wedge B\in \mathbb{N}\right)\to AB=BA$$
4		nnre	$$⊢B\in \mathbb{N}\to B\in ℝ$$
5		remul02	$$⊢B\in ℝ\to 0\cdot B=0$$
6		remul01	$$⊢B\in ℝ\to B\cdot 0=0$$
7	5 6	eqtr4d	$$⊢B\in ℝ\to 0\cdot B=B\cdot 0$$
8	4 7	syl	$$⊢B\in \mathbb{N}\to 0\cdot B=B\cdot 0$$
9		oveq1	$$⊢A=0\to AB=0\cdot B$$
10		oveq2	$$⊢A=0\to BA=B\cdot 0$$
11	9 10	eqeq12d	$$⊢A=0\to \left(AB=BA\leftrightarrow 0\cdot B=B\cdot 0\right)$$
12	8 11	syl5ibrcom	$$⊢B\in \mathbb{N}\to \left(A=0\to AB=BA\right)$$
13	12	impcom	$$⊢\left(A=0\wedge B\in \mathbb{N}\right)\to AB=BA$$
14	3 13	jaoian	$$⊢\left(\left(A\in \mathbb{N}\vee A=0\right)\wedge B\in \mathbb{N}\right)\to AB=BA$$
15	2 14	sylanb	$$⊢\left(A\in {\mathbb{N}}_0\wedge B\in \mathbb{N}\right)\to AB=BA$$
16		nn0re	$$⊢A\in {\mathbb{N}}_0\to A\in ℝ$$
17		remul01	$$⊢A\in ℝ\to A\cdot 0=0$$
18		remul02	$$⊢A\in ℝ\to 0\cdot A=0$$
19	17 18	eqtr4d	$$⊢A\in ℝ\to A\cdot 0=0\cdot A$$
20	16 19	syl	$$⊢A\in {\mathbb{N}}_0\to A\cdot 0=0\cdot A$$
21		oveq2	$$⊢B=0\to AB=A\cdot 0$$
22		oveq1	$$⊢B=0\to BA=0\cdot A$$
23	21 22	eqeq12d	$$⊢B=0\to \left(AB=BA\leftrightarrow A\cdot 0=0\cdot A\right)$$
24	20 23	syl5ibrcom	$$⊢A\in {\mathbb{N}}_0\to \left(B=0\to AB=BA\right)$$
25	24	imp	$$⊢\left(A\in {\mathbb{N}}_0\wedge B=0\right)\to AB=BA$$
26	15 25	jaodan	$$⊢\left(A\in {\mathbb{N}}_0\wedge \left(B\in \mathbb{N}\vee B=0\right)\right)\to AB=BA$$
27	1 26	sylan2b	$$⊢\left(A\in {\mathbb{N}}_0\wedge B\in {\mathbb{N}}_0\right)\to AB=BA$$