Metamath Proof Explorer


Theorem zaddcom

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

Ref Expression
Assertion zaddcom A B A + B = B + A

Proof

Step Hyp Ref Expression
1 reelznn0nn A A 0 A 0 - A
2 reelznn0nn B B 0 B 0 - B
3 nn0addcom A 0 B 0 A + B = B + A
4 zaddcomlem A 0 - A B 0 A + B = B + A
5 zaddcomlem B 0 - B A 0 B + A = A + B
6 5 eqcomd B 0 - B A 0 A + B = B + A
7 6 ancoms A 0 B 0 - B A + B = B + A
8 renegid2 B 0 - B + B = 0
9 8 ad2antrl A 0 - A B 0 - B 0 - B + B = 0
10 renegid2 A 0 - A + A = 0
11 10 ad2antrr A 0 - A B 0 - B 0 - A + A = 0
12 11 oveq1d A 0 - A B 0 - B 0 - A + A + B = 0 + B
13 simplr A 0 - A B 0 - B 0 - A
14 13 nncnd A 0 - A B 0 - B 0 - A
15 simpll A 0 - A B 0 - B A
16 15 recnd A 0 - A B 0 - B A
17 simprl A 0 - A B 0 - B B
18 17 recnd A 0 - A B 0 - B B
19 14 16 18 addassd A 0 - A B 0 - B 0 - A + A + B = 0 - A + A + B
20 readdlid B 0 + B = B
21 20 ad2antrl A 0 - A B 0 - B 0 + B = B
22 12 19 21 3eqtr3d A 0 - A B 0 - B 0 - A + A + B = B
23 22 oveq2d A 0 - A B 0 - B 0 - B + 0 - A + A + B = 0 - B + B
24 9 23 11 3eqtr4d A 0 - A B 0 - B 0 - B + 0 - A + A + B = 0 - A + A
25 simprr A 0 - A B 0 - B 0 - B
26 25 nncnd A 0 - A B 0 - B 0 - B
27 16 18 addcld A 0 - A B 0 - B A + B
28 26 14 27 addassd A 0 - A B 0 - B 0 - B + 0 - A + A + B = 0 - B + 0 - A + A + B
29 9 oveq1d A 0 - A B 0 - B 0 - B + B + A = 0 + A
30 26 18 16 addassd A 0 - A B 0 - B 0 - B + B + A = 0 - B + B + A
31 readdlid A 0 + A = A
32 31 ad2antrr A 0 - A B 0 - B 0 + A = A
33 29 30 32 3eqtr3d A 0 - A B 0 - B 0 - B + B + A = A
34 33 oveq2d A 0 - A B 0 - B 0 - A + 0 - B + B + A = 0 - A + A
35 24 28 34 3eqtr4d A 0 - A B 0 - B 0 - B + 0 - A + A + B = 0 - A + 0 - B + B + A
36 nnaddcom 0 - A 0 - B 0 - A + 0 - B = 0 - B + 0 - A
37 36 ad2ant2l A 0 - A B 0 - B 0 - A + 0 - B = 0 - B + 0 - A
38 37 oveq1d A 0 - A B 0 - B 0 - A + 0 - B + A + B = 0 - B + 0 - A + A + B
39 18 16 addcld A 0 - A B 0 - B B + A
40 14 26 39 addassd A 0 - A B 0 - B 0 - A + 0 - B + B + A = 0 - A + 0 - B + B + A
41 35 38 40 3eqtr4d A 0 - A B 0 - B 0 - A + 0 - B + A + B = 0 - A + 0 - B + B + A
42 13 25 nnaddcld A 0 - A B 0 - B 0 - A + 0 - B
43 42 nncnd A 0 - A B 0 - B 0 - A + 0 - B
44 43 27 39 sn-addcand A 0 - A B 0 - B 0 - A + 0 - B + A + B = 0 - A + 0 - B + B + A A + B = B + A
45 41 44 mpbid A 0 - A B 0 - B A + B = B + A
46 3 4 7 45 ccase A 0 A 0 - A B 0 B 0 - B A + B = B + A
47 1 2 46 syl2anb A B A + B = B + A