![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > xnegpnf | Structured version Visualization version GIF version |
Description: Minus +∞. Remark of [BourbakiTop1] p. IV.15. (Contributed by FL, 26-Dec-2011.) |
Ref | Expression |
---|---|
xnegpnf | ⊢ -𝑒+∞ = -∞ |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | df-xneg 13137 | . 2 ⊢ -𝑒+∞ = if(+∞ = +∞, -∞, if(+∞ = -∞, +∞, -+∞)) | |
2 | eqid 2726 | . . 3 ⊢ +∞ = +∞ | |
3 | 2 | iftruei 4530 | . 2 ⊢ if(+∞ = +∞, -∞, if(+∞ = -∞, +∞, -+∞)) = -∞ |
4 | 1, 3 | eqtri 2754 | 1 ⊢ -𝑒+∞ = -∞ |
Colors of variables: wff setvar class |
Syntax hints: = wceq 1534 ifcif 4523 +∞cpnf 11283 -∞cmnf 11284 -cneg 11483 -𝑒cxne 13134 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1790 ax-4 1804 ax-5 1906 ax-6 1964 ax-7 2004 ax-8 2101 ax-9 2109 ax-ext 2697 |
This theorem depends on definitions: df-bi 206 df-an 395 df-or 846 df-ex 1775 df-sb 2061 df-clab 2704 df-cleq 2718 df-clel 2803 df-if 4524 df-xneg 13137 |
This theorem is referenced by: xnegcl 13237 xnegneg 13238 xltnegi 13240 xnegid 13262 xnegdi 13272 xaddass2 13274 xsubge0 13285 xlesubadd 13287 xmulneg1 13293 xmulmnf1 13300 xadddi2 13321 xrsdsreclblem 21402 xblss2ps 24392 xblss2 24393 xaddeq0 32657 supminfxr 45112 liminflbuz2 45469 |
Copyright terms: Public domain | W3C validator |