![]() |
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 12192 | . 2 ⊢ -𝑒+∞ = if(+∞ = +∞, -∞, if(+∞ = -∞, +∞, -+∞)) | |
2 | eqid 2800 | . . 3 ⊢ +∞ = +∞ | |
3 | 2 | iftruei 4285 | . 2 ⊢ if(+∞ = +∞, -∞, if(+∞ = -∞, +∞, -+∞)) = -∞ |
4 | 1, 3 | eqtri 2822 | 1 ⊢ -𝑒+∞ = -∞ |
Colors of variables: wff setvar class |
Syntax hints: = wceq 1653 ifcif 4278 +∞cpnf 10361 -∞cmnf 10362 -cneg 10558 -𝑒cxne 12189 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1891 ax-4 1905 ax-5 2006 ax-6 2072 ax-7 2107 ax-9 2166 ax-10 2185 ax-11 2200 ax-12 2213 ax-ext 2778 |
This theorem depends on definitions: df-bi 199 df-an 386 df-or 875 df-tru 1657 df-ex 1876 df-nf 1880 df-sb 2065 df-clab 2787 df-cleq 2793 df-clel 2796 df-if 4279 df-xneg 12192 |
This theorem is referenced by: xnegcl 12292 xnegneg 12293 xltnegi 12295 xnegid 12317 xnegdi 12326 xaddass2 12328 xsubge0 12339 xlesubadd 12341 xmulneg1 12347 xmulmnf1 12354 xadddi2 12375 xrsdsreclblem 20113 xblss2ps 22533 xblss2 22534 xaddeq0 30035 supminfxr 40432 |
Copyright terms: Public domain | W3C validator |