Metamath Proof Explorer


Theorem nn0addcom

Description: Addition is commutative for nonnegative integers. Proven without ax-mulcom . (Contributed by SN, 1-Feb-2025)

Ref Expression
Assertion nn0addcom 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 nnaddcom A B A + B = B + A
4 nnre B B
5 readdlid B 0 + B = B
6 readdrid B B + 0 = B
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 readdrid A A + 0 = A
18 readdlid A 0 + A = A
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