Theorem xnegmnf 12873

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 12777	. 2 ⊢ -𝑒-∞ = if(-∞ = +∞, -∞, if(-∞ = -∞, +∞, --∞))
2		mnfnepnf 10962	. . 3 ⊢ -∞ ≠ +∞
3		ifnefalse 4468	. . 3 ⊢ (-∞ ≠ +∞ → if(-∞ = +∞, -∞, if(-∞ = -∞, +∞, --∞)) = if(-∞ = -∞, +∞, --∞))
4	2, 3	ax-mp 5	. 2 ⊢ if(-∞ = +∞, -∞, if(-∞ = -∞, +∞, --∞)) = if(-∞ = -∞, +∞, --∞)
5		eqid 2738	. . 3 ⊢ -∞ = -∞
6	5	iftruei 4463	. 2 ⊢ if(-∞ = -∞, +∞, --∞) = +∞
7	1, 4, 6	3eqtri 2770	1 ⊢ -𝑒-∞ = +∞

Syntax hints:   = wceq 1539   ≠ wne 2942  ifcif 4456  +∞cpnf 10937  -∞cmnf 10938  -cneg 11136  -_𝑒cxne 12774

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-ext 2709  ax-sep 5218  ax-pow 5283  ax-un 7566  ax-cnex 10858

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 844  df-tru 1542  df-ex 1784  df-sb 2069  df-clab 2716  df-cleq 2730  df-clel 2817  df-ne 2943  df-rab 3072  df-v 3424  df-un 3888  df-in 3890  df-ss 3900  df-if 4457  df-pw 4532  df-sn 4559  df-pr 4561  df-uni 4837  df-pnf 10942  df-mnf 10943  df-xr 10944  df-xneg 12777

This theorem is referenced by:  xnegcl  12876  xnegneg  12877  xltnegi  12879  xnegid  12901  xnegdi  12911  xsubge0  12924  xmulneg1  12932  xmulpnf1n  12941  xadddi2  12960  xrsdsreclblem  20556  xaddeq0  30978  xrge0npcan  31205  carsgclctunlem2  32186  supminfxr  42894  supminfxr2  42899  liminf0  43224  liminflbuz2  43246  liminfpnfuz  43247