Theorem xnegmnf 12591

Description: Minus -∞. Remark of [BourbakiTop1] p. IV.15. (Contributed by FL, 26-Dec-2011.) (Revised by Mario Carneiro, 20-Aug-2015.)

Assertion

Ref	Expression
xnegmnf	⊢ -𝑒-∞ = +∞

Proof of Theorem xnegmnf

Step	Hyp	Ref	Expression
1		df-xneg 12495	. 2 ⊢ -𝑒-∞ = if(-∞ = +∞, -∞, if(-∞ = -∞, +∞, --∞))
2		mnfnepnf 10686	. . 3 ⊢ -∞ ≠ +∞
3		ifnefalse 4437	. . 3 ⊢ (-∞ ≠ +∞ → if(-∞ = +∞, -∞, if(-∞ = -∞, +∞, --∞)) = if(-∞ = -∞, +∞, --∞))
4	2, 3	ax-mp 5	. 2 ⊢ if(-∞ = +∞, -∞, if(-∞ = -∞, +∞, --∞)) = if(-∞ = -∞, +∞, --∞)
5		eqid 2798	. . 3 ⊢ -∞ = -∞
6	5	iftruei 4432	. 2 ⊢ if(-∞ = -∞, +∞, --∞) = +∞
7	1, 4, 6	3eqtri 2825	1 ⊢ -𝑒-∞ = +∞

Syntax hints:   = wceq 1538   ≠ wne 2987  ifcif 4425  +∞cpnf 10661  -∞cmnf 10662  -cneg 10860  -_𝑒cxne 12492

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 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-10 2142  ax-11 2158  ax-12 2175  ax-ext 2770  ax-sep 5167  ax-pow 5231  ax-un 7441  ax-cnex 10582

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-tru 1541  df-ex 1782  df-nf 1786  df-sb 2070  df-clab 2777  df-cleq 2791  df-clel 2870  df-nfc 2938  df-ne 2988  df-rab 3115  df-v 3443  df-un 3886  df-in 3888  df-ss 3898  df-if 4426  df-pw 4499  df-sn 4526  df-pr 4528  df-uni 4801  df-pnf 10666  df-mnf 10667  df-xr 10668  df-xneg 12495

This theorem is referenced by:  xnegcl  12594  xnegneg  12595  xltnegi  12597  xnegid  12619  xnegdi  12629  xsubge0  12642  xmulneg1  12650  xmulpnf1n  12659  xadddi2  12678  xrsdsreclblem  20137  xaddeq0  30503  xrge0npcan  30728  carsgclctunlem2  31687  supminfxr  42103  supminfxr2  42108  liminf0  42435  liminflbuz2  42457  liminfpnfuz  42458