Metamath Proof Explorer


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 AωBωA𝑜B=B𝑜A

Proof

Step Hyp Ref Expression
1 oveq1 x=Ax𝑜B=A𝑜B
2 oveq2 x=AB𝑜x=B𝑜A
3 1 2 eqeq12d x=Ax𝑜B=B𝑜xA𝑜B=B𝑜A
4 3 imbi2d x=ABωx𝑜B=B𝑜xBωA𝑜B=B𝑜A
5 oveq1 x=x𝑜B=𝑜B
6 oveq2 x=B𝑜x=B𝑜
7 5 6 eqeq12d x=x𝑜B=B𝑜x𝑜B=B𝑜
8 oveq1 x=yx𝑜B=y𝑜B
9 oveq2 x=yB𝑜x=B𝑜y
10 8 9 eqeq12d x=yx𝑜B=B𝑜xy𝑜B=B𝑜y
11 oveq1 x=sucyx𝑜B=sucy𝑜B
12 oveq2 x=sucyB𝑜x=B𝑜sucy
13 11 12 eqeq12d x=sucyx𝑜B=B𝑜xsucy𝑜B=B𝑜sucy
14 nnm0r Bω𝑜B=
15 nnm0 BωB𝑜=
16 14 15 eqtr4d Bω𝑜B=B𝑜
17 oveq1 y𝑜B=B𝑜yy𝑜B+𝑜B=B𝑜y+𝑜B
18 nnmsucr yωBωsucy𝑜B=y𝑜B+𝑜B
19 nnmsuc BωyωB𝑜sucy=B𝑜y+𝑜B
20 19 ancoms yωBωB𝑜sucy=B𝑜y+𝑜B
21 18 20 eqeq12d yωBωsucy𝑜B=B𝑜sucyy𝑜B+𝑜B=B𝑜y+𝑜B
22 17 21 syl5ibr yωBωy𝑜B=B𝑜ysucy𝑜B=B𝑜sucy
23 22 ex yωBωy𝑜B=B𝑜ysucy𝑜B=B𝑜sucy
24 7 10 13 16 23 finds2 xωBωx𝑜B=B𝑜x
25 4 24 vtoclga AωBωA𝑜B=B𝑜A
26 25 imp AωBωA𝑜B=B𝑜A