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 12848 | . 2 ⊢ -𝑒-∞ = if(-∞ = +∞, -∞, if(-∞ = -∞, +∞, --∞)) | |
2 | mnfnepnf 11031 | . . 3 ⊢ -∞ ≠ +∞ | |
3 | ifnefalse 4471 | . . 3 ⊢ (-∞ ≠ +∞ → if(-∞ = +∞, -∞, if(-∞ = -∞, +∞, --∞)) = if(-∞ = -∞, +∞, --∞)) | |
4 | 2, 3 | ax-mp 5 | . 2 ⊢ if(-∞ = +∞, -∞, if(-∞ = -∞, +∞, --∞)) = if(-∞ = -∞, +∞, --∞) |
5 | eqid 2738 | . . 3 ⊢ -∞ = -∞ | |
6 | 5 | iftruei 4466 | . 2 ⊢ if(-∞ = -∞, +∞, --∞) = +∞ |
7 | 1, 4, 6 | 3eqtri 2770 | 1 ⊢ -𝑒-∞ = +∞ |
Colors of variables: wff setvar class |
Syntax hints: = wceq 1539 ≠ wne 2943 ifcif 4459 +∞cpnf 11006 -∞cmnf 11007 -cneg 11206 -𝑒cxne 12845 |
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 1913 ax-6 1971 ax-7 2011 ax-8 2108 ax-9 2116 ax-ext 2709 ax-sep 5223 ax-pow 5288 ax-un 7588 ax-cnex 10927 |
This theorem depends on definitions: df-bi 206 df-an 397 df-or 845 df-tru 1542 df-ex 1783 df-sb 2068 df-clab 2716 df-cleq 2730 df-clel 2816 df-ne 2944 df-rab 3073 df-v 3434 df-un 3892 df-in 3894 df-ss 3904 df-if 4460 df-pw 4535 df-sn 4562 df-pr 4564 df-uni 4840 df-pnf 11011 df-mnf 11012 df-xr 11013 df-xneg 12848 |
This theorem is referenced by: xnegcl 12947 xnegneg 12948 xltnegi 12950 xnegid 12972 xnegdi 12982 xsubge0 12995 xmulneg1 13003 xmulpnf1n 13012 xadddi2 13031 xrsdsreclblem 20644 xaddeq0 31076 xrge0npcan 31303 carsgclctunlem2 32286 supminfxr 43004 supminfxr2 43009 liminf0 43334 liminflbuz2 43356 liminfpnfuz 43357 |
Copyright terms: Public domain | W3C validator |