Metamath Proof Explorer


Theorem pn0sr

Description: A signed real plus its negative is zero. (Contributed by NM, 14-May-1996) (New usage is discouraged.)

Ref Expression
Assertion pn0sr A 𝑹 A + 𝑹 A 𝑹 -1 𝑹 = 0 𝑹

Proof

Step Hyp Ref Expression
1 1idsr A 𝑹 A 𝑹 1 𝑹 = A
2 1 oveq1d A 𝑹 A 𝑹 1 𝑹 + 𝑹 A 𝑹 -1 𝑹 = A + 𝑹 A 𝑹 -1 𝑹
3 distrsr A 𝑹 -1 𝑹 + 𝑹 1 𝑹 = A 𝑹 -1 𝑹 + 𝑹 A 𝑹 1 𝑹
4 m1p1sr -1 𝑹 + 𝑹 1 𝑹 = 0 𝑹
5 4 oveq2i A 𝑹 -1 𝑹 + 𝑹 1 𝑹 = A 𝑹 0 𝑹
6 addcomsr A 𝑹 -1 𝑹 + 𝑹 A 𝑹 1 𝑹 = A 𝑹 1 𝑹 + 𝑹 A 𝑹 -1 𝑹
7 3 5 6 3eqtr3i A 𝑹 0 𝑹 = A 𝑹 1 𝑹 + 𝑹 A 𝑹 -1 𝑹
8 00sr A 𝑹 A 𝑹 0 𝑹 = 0 𝑹
9 7 8 eqtr3id A 𝑹 A 𝑹 1 𝑹 + 𝑹 A 𝑹 -1 𝑹 = 0 𝑹
10 2 9 eqtr3d A 𝑹 A + 𝑹 A 𝑹 -1 𝑹 = 0 𝑹