Metamath Proof Explorer


Theorem xrsadd

Description: The addition operation of the extended real number structure. (Contributed by Mario Carneiro, 21-Aug-2015)

Ref Expression
Assertion xrsadd +𝑒=+𝑠*

Proof

Step Hyp Ref Expression
1 xaddf +𝑒:*×**
2 xrex *V
3 2 2 xpex *×*V
4 fex2 +𝑒:*×***×*V*V+𝑒V
5 1 3 2 4 mp3an +𝑒V
6 df-xrs 𝑠*=Basendx*+ndx+𝑒ndx𝑒TopSetndxordTopndxdistndxx*,y*ifxyy+𝑒xx+𝑒y
7 6 odrngplusg +𝑒V+𝑒=+𝑠*
8 5 7 ax-mp +𝑒=+𝑠*