Theorem nnmcom

Description: Multiplication of natural numbers is commutative. Theorem 4K(5) of Enderton p. 81. (Contributed by NM, 21-Sep-1995) (Proof shortened by Andrew Salmon, 22-Oct-2011)

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

Proof

Step	Hyp	Ref	Expression
1		oveq1	$$⊢x=A\to x{\cdot }_{𝑜}B=A{\cdot }_{𝑜}B$$
2		oveq2	$$⊢x=A\to B{\cdot }_{𝑜}x=B{\cdot }_{𝑜}A$$
3	1 2	eqeq12d	$$⊢x=A\to \left(x{\cdot }_{𝑜}B=B{\cdot }_{𝑜}x\leftrightarrow A{\cdot }_{𝑜}B=B{\cdot }_{𝑜}A\right)$$
4	3	imbi2d	$$⊢x=A\to \left(\left(B\in \mathrm{\omega }\to x{\cdot }_{𝑜}B=B{\cdot }_{𝑜}x\right)\leftrightarrow \left(B\in \mathrm{\omega }\to A{\cdot }_{𝑜}B=B{\cdot }_{𝑜}A\right)\right)$$
5		oveq1	$$⊢x=\varnothing \to x{\cdot }_{𝑜}B=\varnothing {\cdot }_{𝑜}B$$
6		oveq2	$$⊢x=\varnothing \to B{\cdot }_{𝑜}x=B{\cdot }_{𝑜}\varnothing$$
7	5 6	eqeq12d	$$⊢x=\varnothing \to \left(x{\cdot }_{𝑜}B=B{\cdot }_{𝑜}x\leftrightarrow \varnothing {\cdot }_{𝑜}B=B{\cdot }_{𝑜}\varnothing \right)$$
8		oveq1	$$⊢x=y\to x{\cdot }_{𝑜}B=y{\cdot }_{𝑜}B$$
9		oveq2	$$⊢x=y\to B{\cdot }_{𝑜}x=B{\cdot }_{𝑜}y$$
10	8 9	eqeq12d	$$⊢x=y\to \left(x{\cdot }_{𝑜}B=B{\cdot }_{𝑜}x\leftrightarrow y{\cdot }_{𝑜}B=B{\cdot }_{𝑜}y\right)$$
11		oveq1	$$⊢x=\mathrm{suc}y\to x{\cdot }_{𝑜}B=\mathrm{suc}y{\cdot }_{𝑜}B$$
12		oveq2	$$⊢x=\mathrm{suc}y\to B{\cdot }_{𝑜}x=B{\cdot }_{𝑜}\mathrm{suc}y$$
13	11 12	eqeq12d	$$⊢x=\mathrm{suc}y\to \left(x{\cdot }_{𝑜}B=B{\cdot }_{𝑜}x\leftrightarrow \mathrm{suc}y{\cdot }_{𝑜}B=B{\cdot }_{𝑜}\mathrm{suc}y\right)$$
14		nnm0r	$$⊢B\in \mathrm{\omega }\to \varnothing {\cdot }_{𝑜}B=\varnothing$$
15		nnm0	$$⊢B\in \mathrm{\omega }\to B{\cdot }_{𝑜}\varnothing =\varnothing$$
16	14 15	eqtr4d	$$⊢B\in \mathrm{\omega }\to \varnothing {\cdot }_{𝑜}B=B{\cdot }_{𝑜}\varnothing$$
17		oveq1	$$⊢y{\cdot }_{𝑜}B=B{\cdot }_{𝑜}y\to \left(y{\cdot }_{𝑜}B\right){+}_{𝑜}B=\left(B{\cdot }_{𝑜}y\right){+}_{𝑜}B$$
18		nnmsucr	$$⊢\left(y\in \mathrm{\omega }\wedge B\in \mathrm{\omega }\right)\to \mathrm{suc}y{\cdot }_{𝑜}B=\left(y{\cdot }_{𝑜}B\right){+}_{𝑜}B$$
19		nnmsuc	$$⊢\left(B\in \mathrm{\omega }\wedge y\in \mathrm{\omega }\right)\to B{\cdot }_{𝑜}\mathrm{suc}y=\left(B{\cdot }_{𝑜}y\right){+}_{𝑜}B$$
20	19	ancoms	$$⊢\left(y\in \mathrm{\omega }\wedge B\in \mathrm{\omega }\right)\to B{\cdot }_{𝑜}\mathrm{suc}y=\left(B{\cdot }_{𝑜}y\right){+}_{𝑜}B$$
21	18 20	eqeq12d	$$⊢\left(y\in \mathrm{\omega }\wedge B\in \mathrm{\omega }\right)\to \left(\mathrm{suc}y{\cdot }_{𝑜}B=B{\cdot }_{𝑜}\mathrm{suc}y\leftrightarrow \left(y{\cdot }_{𝑜}B\right){+}_{𝑜}B=\left(B{\cdot }_{𝑜}y\right){+}_{𝑜}B\right)$$
22	17 21	imbitrrid	$$⊢\left(y\in \mathrm{\omega }\wedge B\in \mathrm{\omega }\right)\to \left(y{\cdot }_{𝑜}B=B{\cdot }_{𝑜}y\to \mathrm{suc}y{\cdot }_{𝑜}B=B{\cdot }_{𝑜}\mathrm{suc}y\right)$$
23	22	ex	$$⊢y\in \mathrm{\omega }\to \left(B\in \mathrm{\omega }\to \left(y{\cdot }_{𝑜}B=B{\cdot }_{𝑜}y\to \mathrm{suc}y{\cdot }_{𝑜}B=B{\cdot }_{𝑜}\mathrm{suc}y\right)\right)$$
24	7 10 13 16 23	finds2	$$⊢x\in \mathrm{\omega }\to \left(B\in \mathrm{\omega }\to x{\cdot }_{𝑜}B=B{\cdot }_{𝑜}x\right)$$
25	4 24	vtoclga	$$⊢A\in \mathrm{\omega }\to \left(B\in \mathrm{\omega }\to A{\cdot }_{𝑜}B=B{\cdot }_{𝑜}A\right)$$
26	25	imp	$$⊢\left(A\in \mathrm{\omega }\wedge B\in \mathrm{\omega }\right)\to A{\cdot }_{𝑜}B=B{\cdot }_{𝑜}A$$