Metamath Proof Explorer


Theorem renegid2

Description: Commuted version of renegid . (Contributed by SN, 4-May-2024)

Ref Expression
Assertion renegid2 A 0 - A + A = 0

Proof

Step Hyp Ref Expression
1 renegid A A + 0 - A = 0
2 1 oveq2d A 0 - A + A + 0 - A = 0 - A + 0
3 rernegcl A 0 - A
4 readdid1 0 - A 0 - A + 0 = 0 - A
5 3 4 syl A 0 - A + 0 = 0 - A
6 2 5 eqtrd A 0 - A + A + 0 - A = 0 - A
7 3 recnd A 0 - A
8 recn A A
9 7 8 7 addassd A 0 - A + A + 0 - A = 0 - A + A + 0 - A
10 readdid2 0 - A 0 + 0 - A = 0 - A
11 3 10 syl A 0 + 0 - A = 0 - A
12 6 9 11 3eqtr4d A 0 - A + A + 0 - A = 0 + 0 - A
13 id A A
14 3 13 readdcld A 0 - A + A
15 elre0re A 0
16 readdcan2 0 - A + A 0 0 - A 0 - A + A + 0 - A = 0 + 0 - A 0 - A + A = 0
17 14 15 3 16 syl3anc A 0 - A + A + 0 - A = 0 + 0 - A 0 - A + A = 0
18 12 17 mpbid A 0 - A + A = 0