![]() |
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 13042 | . 2 ⊢ -𝑒+∞ = if(+∞ = +∞, -∞, if(+∞ = -∞, +∞, -+∞)) | |
2 | eqid 2731 | . . 3 ⊢ +∞ = +∞ | |
3 | 2 | iftruei 4498 | . 2 ⊢ if(+∞ = +∞, -∞, if(+∞ = -∞, +∞, -+∞)) = -∞ |
4 | 1, 3 | eqtri 2759 | 1 ⊢ -𝑒+∞ = -∞ |
Colors of variables: wff setvar class |
Syntax hints: = wceq 1541 ifcif 4491 +∞cpnf 11195 -∞cmnf 11196 -cneg 11395 -𝑒cxne 13039 |
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 2702 |
This theorem depends on definitions: df-bi 206 df-an 397 df-or 846 df-ex 1782 df-sb 2068 df-clab 2709 df-cleq 2723 df-clel 2809 df-if 4492 df-xneg 13042 |
This theorem is referenced by: xnegcl 13142 xnegneg 13143 xltnegi 13145 xnegid 13167 xnegdi 13177 xaddass2 13179 xsubge0 13190 xlesubadd 13192 xmulneg1 13198 xmulmnf1 13205 xadddi2 13226 xrsdsreclblem 20880 xblss2ps 23791 xblss2 23792 xaddeq0 31726 supminfxr 43819 liminflbuz2 44176 |
Copyright terms: Public domain | W3C validator |