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 | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | oveq1 | |
|
2 | oveq2 | |
|
3 | 1 2 | eqeq12d | |
4 | 3 | imbi2d | |
5 | oveq1 | |
|
6 | oveq2 | |
|
7 | 5 6 | eqeq12d | |
8 | oveq1 | |
|
9 | oveq2 | |
|
10 | 8 9 | eqeq12d | |
11 | oveq1 | |
|
12 | oveq2 | |
|
13 | 11 12 | eqeq12d | |
14 | nnm0r | |
|
15 | nnm0 | |
|
16 | 14 15 | eqtr4d | |
17 | oveq1 | |
|
18 | nnmsucr | |
|
19 | nnmsuc | |
|
20 | 19 | ancoms | |
21 | 18 20 | eqeq12d | |
22 | 17 21 | syl5ibr | |
23 | 22 | ex | |
24 | 7 10 13 16 23 | finds2 | |
25 | 4 24 | vtoclga | |
26 | 25 | imp | |