Theorem xnegmnf 13109

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 13011	. 2 ⊢ -𝑒-∞ = if(-∞ = +∞, -∞, if(-∞ = -∞, +∞, --∞))
2		mnfnepnf 11168	. . 3 ⊢ -∞ ≠ +∞
3		ifnefalse 4484	. . 3 ⊢ (-∞ ≠ +∞ → if(-∞ = +∞, -∞, if(-∞ = -∞, +∞, --∞)) = if(-∞ = -∞, +∞, --∞))
4	2, 3	ax-mp 5	. 2 ⊢ if(-∞ = +∞, -∞, if(-∞ = -∞, +∞, --∞)) = if(-∞ = -∞, +∞, --∞)
5		eqid 2731	. . 3 ⊢ -∞ = -∞
6	5	iftruei 4479	. 2 ⊢ if(-∞ = -∞, +∞, --∞) = +∞
7	1, 4, 6	3eqtri 2758	1 ⊢ -𝑒-∞ = +∞

Syntax hints:   = wceq 1541   ≠ wne 2928  ifcif 4472  +∞cpnf 11143  -∞cmnf 11144  -cneg 11345  -_𝑒cxne 13008

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 2113  ax-9 2121  ax-ext 2703  ax-sep 5232  ax-pow 5301  ax-un 7668  ax-cnex 11062

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 2710  df-cleq 2723  df-clel 2806  df-ne 2929  df-rab 3396  df-v 3438  df-un 3902  df-in 3904  df-ss 3914  df-if 4473  df-pw 4549  df-sn 4574  df-pr 4576  df-uni 4857  df-pnf 11148  df-mnf 11149  df-xr 11150  df-xneg 13011

This theorem is referenced by:  xnegcl  13112  xnegneg  13113  xltnegi  13115  xnegid  13137  xnegdi  13147  xsubge0  13160  xmulneg1  13168  xmulpnf1n  13177  xadddi2  13196  xrsdsreclblem  21349  xaddeq0  32736  xrge0npcan  33001  carsgclctunlem2  34332  supminfxr  45572  supminfxr2  45577  liminf0  45901  liminflbuz2  45923  liminfpnfuz  45924