Metamath Proof Explorer


Theorem nn0mulcom

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

Ref Expression
Assertion nn0mulcom A 0 B 0 A B = B A

Proof

Step Hyp Ref Expression
1 elnn0 B 0 B B = 0
2 elnn0 A 0 A A = 0
3 nnmulcom A B A B = B A
4 nnre B B
5 remul02 B 0 B = 0
6 remul01 B B 0 = 0
7 5 6 eqtr4d B 0 B = B 0
8 4 7 syl B 0 B = B 0
9 oveq1 A = 0 A B = 0 B
10 oveq2 A = 0 B A = B 0
11 9 10 eqeq12d A = 0 A B = B A 0 B = B 0
12 8 11 syl5ibrcom B A = 0 A B = B A
13 12 impcom A = 0 B A B = B A
14 3 13 jaoian A A = 0 B A B = B A
15 2 14 sylanb A 0 B A B = B A
16 nn0re A 0 A
17 remul01 A A 0 = 0
18 remul02 A 0 A = 0
19 17 18 eqtr4d A A 0 = 0 A
20 16 19 syl A 0 A 0 = 0 A
21 oveq2 B = 0 A B = A 0
22 oveq1 B = 0 B A = 0 A
23 21 22 eqeq12d B = 0 A B = B A A 0 = 0 A
24 20 23 syl5ibrcom A 0 B = 0 A B = B A
25 24 imp A 0 B = 0 A B = B A
26 15 25 jaodan A 0 B B = 0 A B = B A
27 1 26 sylan2b A 0 B 0 A B = B A