Metamath Proof Explorer


Theorem addresr

Description: Addition of real numbers in terms of intermediate signed reals. (Contributed by NM, 10-May-1996) (New usage is discouraged.)

Ref Expression
Assertion addresr A 𝑹 B 𝑹 A 0 𝑹 + B 0 𝑹 = A + 𝑹 B 0 𝑹

Proof

Step Hyp Ref Expression
1 0r 0 𝑹 𝑹
2 addcnsr A 𝑹 0 𝑹 𝑹 B 𝑹 0 𝑹 𝑹 A 0 𝑹 + B 0 𝑹 = A + 𝑹 B 0 𝑹 + 𝑹 0 𝑹
3 2 an4s A 𝑹 B 𝑹 0 𝑹 𝑹 0 𝑹 𝑹 A 0 𝑹 + B 0 𝑹 = A + 𝑹 B 0 𝑹 + 𝑹 0 𝑹
4 1 1 3 mpanr12 A 𝑹 B 𝑹 A 0 𝑹 + B 0 𝑹 = A + 𝑹 B 0 𝑹 + 𝑹 0 𝑹
5 0idsr 0 𝑹 𝑹 0 𝑹 + 𝑹 0 𝑹 = 0 𝑹
6 1 5 ax-mp 0 𝑹 + 𝑹 0 𝑹 = 0 𝑹
7 6 opeq2i A + 𝑹 B 0 𝑹 + 𝑹 0 𝑹 = A + 𝑹 B 0 𝑹
8 4 7 eqtrdi A 𝑹 B 𝑹 A 0 𝑹 + B 0 𝑹 = A + 𝑹 B 0 𝑹