![]() |
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 13030 | . 2 ⊢ -𝑒+∞ = if(+∞ = +∞, -∞, if(+∞ = -∞, +∞, -+∞)) | |
2 | eqid 2736 | . . 3 ⊢ +∞ = +∞ | |
3 | 2 | iftruei 4492 | . 2 ⊢ if(+∞ = +∞, -∞, if(+∞ = -∞, +∞, -+∞)) = -∞ |
4 | 1, 3 | eqtri 2764 | 1 ⊢ -𝑒+∞ = -∞ |
Colors of variables: wff setvar class |
Syntax hints: = wceq 1541 ifcif 4485 +∞cpnf 11183 -∞cmnf 11184 -cneg 11383 -𝑒cxne 13027 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1797 ax-4 1811 ax-5 1913 ax-6 1971 ax-7 2011 ax-8 2108 ax-9 2116 ax-ext 2707 |
This theorem depends on definitions: df-bi 206 df-an 397 df-or 846 df-ex 1782 df-sb 2068 df-clab 2714 df-cleq 2728 df-clel 2814 df-if 4486 df-xneg 13030 |
This theorem is referenced by: xnegcl 13129 xnegneg 13130 xltnegi 13132 xnegid 13154 xnegdi 13164 xaddass2 13166 xsubge0 13177 xlesubadd 13179 xmulneg1 13185 xmulmnf1 13192 xadddi2 13213 xrsdsreclblem 20839 xblss2ps 23750 xblss2 23751 xaddeq0 31553 supminfxr 43673 liminflbuz2 44026 |
Copyright terms: Public domain | W3C validator |