Metamath Proof Explorer


Theorem zaddcomlem

Description: Lemma for zaddcom . (Contributed by SN, 1-Feb-2025)

Ref Expression
Assertion zaddcomlem A 0 - A B 0 A + B = B + A

Proof

Step Hyp Ref Expression
1 simpr A 0 - A B 0 B 0
2 1 nn0cnd A 0 - A B 0 B
3 rernegcl A 0 - A
4 3 ad2antrr A 0 - A B 0 0 - A
5 4 recnd A 0 - A B 0 0 - A
6 simpll A 0 - A B 0 A
7 6 recnd A 0 - A B 0 A
8 2 5 7 addassd A 0 - A B 0 B + 0 - A + A = B + 0 - A + A
9 renegid2 A 0 - A + A = 0
10 9 ad2antrr A 0 - A B 0 0 - A + A = 0
11 10 oveq2d A 0 - A B 0 B + 0 - A + A = B + 0
12 nn0re B 0 B
13 readdrid B B + 0 = B
14 12 13 syl B 0 B + 0 = B
15 14 adantl A 0 - A B 0 B + 0 = B
16 8 11 15 3eqtrrd A 0 - A B 0 B = B + 0 - A + A
17 9 oveq1d A 0 - A + A + B = 0 + B
18 17 adantr A 0 - A 0 - A + A + B = 0 + B
19 readdlid B 0 + B = B
20 12 19 syl B 0 0 + B = B
21 18 20 sylan9eq A 0 - A B 0 0 - A + A + B = B
22 nnnn0 0 - A 0 - A 0
23 nn0addcom 0 - A 0 B 0 0 - A + B = B + 0 - A
24 22 23 sylan 0 - A B 0 0 - A + B = B + 0 - A
25 24 adantll A 0 - A B 0 0 - A + B = B + 0 - A
26 25 oveq1d A 0 - A B 0 0 - A + B + A = B + 0 - A + A
27 16 21 26 3eqtr4d A 0 - A B 0 0 - A + A + B = 0 - A + B + A
28 5 7 2 addassd A 0 - A B 0 0 - A + A + B = 0 - A + A + B
29 5 2 7 addassd A 0 - A B 0 0 - A + B + A = 0 - A + B + A
30 27 28 29 3eqtr3d A 0 - A B 0 0 - A + A + B = 0 - A + B + A
31 7 2 addcld A 0 - A B 0 A + B
32 2 7 addcld A 0 - A B 0 B + A
33 5 31 32 sn-addcand A 0 - A B 0 0 - A + A + B = 0 - A + B + A A + B = B + A
34 30 33 mpbid A 0 - A B 0 A + B = B + A