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 12495 | . 2 ⊢ -𝑒+∞ = if(+∞ = +∞, -∞, if(+∞ = -∞, +∞, -+∞)) | |
2 | eqid 2818 | . . 3 ⊢ +∞ = +∞ | |
3 | 2 | iftruei 4470 | . 2 ⊢ if(+∞ = +∞, -∞, if(+∞ = -∞, +∞, -+∞)) = -∞ |
4 | 1, 3 | eqtri 2841 | 1 ⊢ -𝑒+∞ = -∞ |
Colors of variables: wff setvar class |
Syntax hints: = wceq 1528 ifcif 4463 +∞cpnf 10660 -∞cmnf 10661 -cneg 10859 -𝑒cxne 12492 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1787 ax-4 1801 ax-5 1902 ax-6 1961 ax-7 2006 ax-8 2107 ax-9 2115 ax-ext 2790 |
This theorem depends on definitions: df-bi 208 df-an 397 df-or 842 df-ex 1772 df-sb 2061 df-clab 2797 df-cleq 2811 df-clel 2890 df-if 4464 df-xneg 12495 |
This theorem is referenced by: xnegcl 12594 xnegneg 12595 xltnegi 12597 xnegid 12619 xnegdi 12629 xaddass2 12631 xsubge0 12642 xlesubadd 12644 xmulneg1 12650 xmulmnf1 12657 xadddi2 12678 xrsdsreclblem 20519 xblss2ps 22938 xblss2 22939 xaddeq0 30403 supminfxr 41616 liminflbuz2 41972 |
Copyright terms: Public domain | W3C validator |