Metamath Proof Explorer


Theorem renegneg

Description: A real number is equal to the negative of its negative. Compare negneg . (Contributed by SN, 13-Feb-2024)

Ref Expression
Assertion renegneg A 0 - 0 - A = A

Proof

Step Hyp Ref Expression
1 rernegcl A 0 - A
2 rernegcl 0 - A 0 - 0 - A
3 1 2 syl A 0 - 0 - A
4 id A A
5 renegid A A + 0 - A = 0
6 elre0re A 0
7 5 6 eqeltrd A A + 0 - A
8 readdid1 A A + 0 = A
9 repncan3 0 - A 0 0 - A + 0 - 0 - A = 0
10 1 6 9 syl2anc A 0 - A + 0 - 0 - A = 0
11 10 oveq2d A A + 0 - A + 0 - 0 - A = A + 0
12 readdid2 A 0 + A = A
13 8 11 12 3eqtr4d A A + 0 - A + 0 - 0 - A = 0 + A
14 recn A A
15 1 recnd A 0 - A
16 3 recnd A 0 - 0 - A
17 14 15 16 addassd A A + 0 - A + 0 - 0 - A = A + 0 - A + 0 - 0 - A
18 5 oveq1d A A + 0 - A + A = 0 + A
19 13 17 18 3eqtr4d A A + 0 - A + 0 - 0 - A = A + 0 - A + A
20 readdcan 0 - 0 - A A A + 0 - A A + 0 - A + 0 - 0 - A = A + 0 - A + A 0 - 0 - A = A
21 20 biimpa 0 - 0 - A A A + 0 - A A + 0 - A + 0 - 0 - A = A + 0 - A + A 0 - 0 - A = A
22 3 4 7 19 21 syl31anc A 0 - 0 - A = A