| 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 13154 | . 2 ⊢ -𝑒-∞ = if(-∞ = +∞, -∞, if(-∞ = -∞, +∞, --∞)) | |
| 2 | mnfnepnf 11317 | . . 3 ⊢ -∞ ≠ +∞ | |
| 3 | ifnefalse 4537 | . . 3 ⊢ (-∞ ≠ +∞ → if(-∞ = +∞, -∞, if(-∞ = -∞, +∞, --∞)) = if(-∞ = -∞, +∞, --∞)) | |
| 4 | 2, 3 | ax-mp 5 | . 2 ⊢ if(-∞ = +∞, -∞, if(-∞ = -∞, +∞, --∞)) = if(-∞ = -∞, +∞, --∞) |
| 5 | eqid 2737 | . . 3 ⊢ -∞ = -∞ | |
| 6 | 5 | iftruei 4532 | . 2 ⊢ if(-∞ = -∞, +∞, --∞) = +∞ |
| 7 | 1, 4, 6 | 3eqtri 2769 | 1 ⊢ -𝑒-∞ = +∞ |
| Colors of variables: wff setvar class |
| Syntax hints: = wceq 1540 ≠ wne 2940 ifcif 4525 +∞cpnf 11292 -∞cmnf 11293 -cneg 11493 -𝑒cxne 13151 |
| This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1795 ax-4 1809 ax-5 1910 ax-6 1967 ax-7 2007 ax-8 2110 ax-9 2118 ax-ext 2708 ax-sep 5296 ax-pow 5365 ax-un 7755 ax-cnex 11211 |
| This theorem depends on definitions: df-bi 207 df-an 396 df-or 849 df-3an 1089 df-tru 1543 df-ex 1780 df-sb 2065 df-clab 2715 df-cleq 2729 df-clel 2816 df-ne 2941 df-rab 3437 df-v 3482 df-un 3956 df-in 3958 df-ss 3968 df-if 4526 df-pw 4602 df-sn 4627 df-pr 4629 df-uni 4908 df-pnf 11297 df-mnf 11298 df-xr 11299 df-xneg 13154 |
| This theorem is referenced by: xnegcl 13255 xnegneg 13256 xltnegi 13258 xnegid 13280 xnegdi 13290 xsubge0 13303 xmulneg1 13311 xmulpnf1n 13320 xadddi2 13339 xrsdsreclblem 21430 xaddeq0 32757 xrge0npcan 33025 carsgclctunlem2 34321 supminfxr 45475 supminfxr2 45480 liminf0 45808 liminflbuz2 45830 liminfpnfuz 45831 |
| Copyright terms: Public domain | W3C validator |