Metamath Proof Explorer


Theorem nnmulcom

Description: Multiplication is commutative for natural numbers. (Contributed by SN, 5-Feb-2024)

Ref Expression
Assertion nnmulcom A B A B = B A

Proof

Step Hyp Ref Expression
1 oveq1 x = 1 x B = 1 B
2 oveq2 x = 1 B x = B 1
3 1 2 eqeq12d x = 1 x B = B x 1 B = B 1
4 3 imbi2d x = 1 B x B = B x B 1 B = B 1
5 oveq1 x = y x B = y B
6 oveq2 x = y B x = B y
7 5 6 eqeq12d x = y x B = B x y B = B y
8 7 imbi2d x = y B x B = B x B y B = B y
9 oveq1 x = y + 1 x B = y + 1 B
10 oveq2 x = y + 1 B x = B y + 1
11 9 10 eqeq12d x = y + 1 x B = B x y + 1 B = B y + 1
12 11 imbi2d x = y + 1 B x B = B x B y + 1 B = B y + 1
13 oveq1 x = A x B = A B
14 oveq2 x = A B x = B A
15 13 14 eqeq12d x = A x B = B x A B = B A
16 15 imbi2d x = A B x B = B x B A B = B A
17 nnmul1com B 1 B = B 1
18 simp3 y B y B = B y y B = B y
19 17 3ad2ant2 y B y B = B y 1 B = B 1
20 18 19 oveq12d y B y B = B y y B + 1 B = B y + B 1
21 simp1 y B y B = B y y
22 1nn 1
23 22 a1i y B y B = B y 1
24 simp2 y B y B = B y B
25 nnadddir y 1 B y + 1 B = y B + 1 B
26 21 23 24 25 syl3anc y B y B = B y y + 1 B = y B + 1 B
27 24 nncnd y B y B = B y B
28 21 nncnd y B y B = B y y
29 1cnd y B y B = B y 1
30 27 28 29 adddid y B y B = B y B y + 1 = B y + B 1
31 20 26 30 3eqtr4d y B y B = B y y + 1 B = B y + 1
32 31 3exp y B y B = B y y + 1 B = B y + 1
33 32 a2d y B y B = B y B y + 1 B = B y + 1
34 4 8 12 16 17 33 nnind A B A B = B A
35 34 imp A B A B = B A