Description: The addition operation of the extended real number structure. (Contributed by Mario Carneiro, 21-Aug-2015)
Ref | Expression | ||
---|---|---|---|
Assertion | xrsadd | โข +๐ = ( +g โ โ*๐ ) |
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 | โข โ*๐ = ( { โจ ( Base โ ndx ) , โ* โฉ , โจ ( +g โ ndx ) , +๐ โฉ , โจ ( .r โ ndx ) , ยทe โฉ } โช { โจ ( TopSet โ ndx ) , ( ordTop โ โค ) โฉ , โจ ( le โ ndx ) , โค โฉ , โจ ( dist โ ndx ) , ( ๐ฅ โ โ* , ๐ฆ โ โ* โฆ if ( ๐ฅ โค ๐ฆ , ( ๐ฆ +๐ -๐ ๐ฅ ) , ( ๐ฅ +๐ -๐ ๐ฆ ) ) ) โฉ } ) | |
7 | 6 | odrngplusg | โข ( +๐ โ V โ +๐ = ( +g โ โ*๐ ) ) |
8 | 5 7 | ax-mp | โข +๐ = ( +g โ โ*๐ ) |