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 12590 | . 2 ⊢ -𝑒-∞ = if(-∞ = +∞, -∞, if(-∞ = -∞, +∞, --∞)) | |
2 | mnfnepnf 10775 | . . 3 ⊢ -∞ ≠ +∞ | |
3 | ifnefalse 4426 | . . 3 ⊢ (-∞ ≠ +∞ → if(-∞ = +∞, -∞, if(-∞ = -∞, +∞, --∞)) = if(-∞ = -∞, +∞, --∞)) | |
4 | 2, 3 | ax-mp 5 | . 2 ⊢ if(-∞ = +∞, -∞, if(-∞ = -∞, +∞, --∞)) = if(-∞ = -∞, +∞, --∞) |
5 | eqid 2738 | . . 3 ⊢ -∞ = -∞ | |
6 | 5 | iftruei 4421 | . 2 ⊢ if(-∞ = -∞, +∞, --∞) = +∞ |
7 | 1, 4, 6 | 3eqtri 2765 | 1 ⊢ -𝑒-∞ = +∞ |
Colors of variables: wff setvar class |
Syntax hints: = wceq 1542 ≠ wne 2934 ifcif 4414 +∞cpnf 10750 -∞cmnf 10751 -cneg 10949 -𝑒cxne 12587 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1802 ax-4 1816 ax-5 1917 ax-6 1975 ax-7 2020 ax-8 2116 ax-9 2124 ax-ext 2710 ax-sep 5167 ax-pow 5232 ax-un 7479 ax-cnex 10671 |
This theorem depends on definitions: df-bi 210 df-an 400 df-or 847 df-tru 1545 df-ex 1787 df-sb 2075 df-clab 2717 df-cleq 2730 df-clel 2811 df-ne 2935 df-rab 3062 df-v 3400 df-un 3848 df-in 3850 df-ss 3860 df-if 4415 df-pw 4490 df-sn 4517 df-pr 4519 df-uni 4797 df-pnf 10755 df-mnf 10756 df-xr 10757 df-xneg 12590 |
This theorem is referenced by: xnegcl 12689 xnegneg 12690 xltnegi 12692 xnegid 12714 xnegdi 12724 xsubge0 12737 xmulneg1 12745 xmulpnf1n 12754 xadddi2 12773 xrsdsreclblem 20263 xaddeq0 30651 xrge0npcan 30880 carsgclctunlem2 31856 supminfxr 42544 supminfxr2 42549 liminf0 42876 liminflbuz2 42898 liminfpnfuz 42899 |
Copyright terms: Public domain | W3C validator |