![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > xnegmnf | Structured version Visualization version GIF version |
Description: Minus -∞. Remark of [BourbakiTop1] p. IV.15. (Contributed by FL, 26-Dec-2011.) (Revised by Mario Carneiro, 20-Aug-2015.) |
Ref | Expression |
---|---|
xnegmnf | ⊢ -𝑒-∞ = +∞ |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | df-xneg 13092 | . 2 ⊢ -𝑒-∞ = if(-∞ = +∞, -∞, if(-∞ = -∞, +∞, --∞)) | |
2 | mnfnepnf 11270 | . . 3 ⊢ -∞ ≠ +∞ | |
3 | ifnefalse 4541 | . . 3 ⊢ (-∞ ≠ +∞ → if(-∞ = +∞, -∞, if(-∞ = -∞, +∞, --∞)) = if(-∞ = -∞, +∞, --∞)) | |
4 | 2, 3 | ax-mp 5 | . 2 ⊢ if(-∞ = +∞, -∞, if(-∞ = -∞, +∞, --∞)) = if(-∞ = -∞, +∞, --∞) |
5 | eqid 2733 | . . 3 ⊢ -∞ = -∞ | |
6 | 5 | iftruei 4536 | . 2 ⊢ if(-∞ = -∞, +∞, --∞) = +∞ |
7 | 1, 4, 6 | 3eqtri 2765 | 1 ⊢ -𝑒-∞ = +∞ |
Colors of variables: wff setvar class |
Syntax hints: = wceq 1542 ≠ wne 2941 ifcif 4529 +∞cpnf 11245 -∞cmnf 11246 -cneg 11445 -𝑒cxne 13089 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1798 ax-4 1812 ax-5 1914 ax-6 1972 ax-7 2012 ax-8 2109 ax-9 2117 ax-ext 2704 ax-sep 5300 ax-pow 5364 ax-un 7725 ax-cnex 11166 |
This theorem depends on definitions: df-bi 206 df-an 398 df-or 847 df-tru 1545 df-ex 1783 df-sb 2069 df-clab 2711 df-cleq 2725 df-clel 2811 df-ne 2942 df-rab 3434 df-v 3477 df-un 3954 df-in 3956 df-ss 3966 df-if 4530 df-pw 4605 df-sn 4630 df-pr 4632 df-uni 4910 df-pnf 11250 df-mnf 11251 df-xr 11252 df-xneg 13092 |
This theorem is referenced by: xnegcl 13192 xnegneg 13193 xltnegi 13195 xnegid 13217 xnegdi 13227 xsubge0 13240 xmulneg1 13248 xmulpnf1n 13257 xadddi2 13276 xrsdsreclblem 20991 xaddeq0 31966 xrge0npcan 32195 carsgclctunlem2 33318 supminfxr 44174 supminfxr2 44179 liminf0 44509 liminflbuz2 44531 liminfpnfuz 44532 |
Copyright terms: Public domain | W3C validator |