Theorem xnegmnf 13123

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 13024	. 2 ⊢ -𝑒-∞ = if(-∞ = +∞, -∞, if(-∞ = -∞, +∞, --∞))
2		mnfnepnf 11186	. . 3 ⊢ -∞ ≠ +∞
3		ifnefalse 4489	. . 3 ⊢ (-∞ ≠ +∞ → if(-∞ = +∞, -∞, if(-∞ = -∞, +∞, --∞)) = if(-∞ = -∞, +∞, --∞))
4	2, 3	ax-mp 5	. 2 ⊢ if(-∞ = +∞, -∞, if(-∞ = -∞, +∞, --∞)) = if(-∞ = -∞, +∞, --∞)
5		eqid 2734	. . 3 ⊢ -∞ = -∞
6	5	iftruei 4484	. 2 ⊢ if(-∞ = -∞, +∞, --∞) = +∞
7	1, 4, 6	3eqtri 2761	1 ⊢ -𝑒-∞ = +∞

Syntax hints:   = wceq 1541   ≠ wne 2930  ifcif 4477  +∞cpnf 11161  -∞cmnf 11162  -cneg 11363  -_𝑒cxne 13021

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2706  ax-sep 5239  ax-pow 5308  ax-un 7678  ax-cnex 11080

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1544  df-ex 1781  df-sb 2068  df-clab 2713  df-cleq 2726  df-clel 2809  df-ne 2931  df-rab 3398  df-v 3440  df-un 3904  df-in 3906  df-ss 3916  df-if 4478  df-pw 4554  df-sn 4579  df-pr 4581  df-uni 4862  df-pnf 11166  df-mnf 11167  df-xr 11168  df-xneg 13024

This theorem is referenced by:  xnegcl  13126  xnegneg  13127  xltnegi  13129  xnegid  13151  xnegdi  13161  xsubge0  13174  xmulneg1  13182  xmulpnf1n  13191  xadddi2  13210  xrsdsreclblem  21365  xaddeq0  32782  xrge0npcan  33051  carsgclctunlem2  34425  supminfxr  45650  supminfxr2  45655  liminf0  45979  liminflbuz2  46001  liminfpnfuz  46002