Theorem xnegmnf 12944

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

Syntax hints:   = wceq 1539   ≠ wne 2943  ifcif 4459  +∞cpnf 11006  -∞cmnf 11007  -cneg 11206  -_𝑒cxne 12845

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2709  ax-sep 5223  ax-pow 5288  ax-un 7588  ax-cnex 10927

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-tru 1542  df-ex 1783  df-sb 2068  df-clab 2716  df-cleq 2730  df-clel 2816  df-ne 2944  df-rab 3073  df-v 3434  df-un 3892  df-in 3894  df-ss 3904  df-if 4460  df-pw 4535  df-sn 4562  df-pr 4564  df-uni 4840  df-pnf 11011  df-mnf 11012  df-xr 11013  df-xneg 12848

This theorem is referenced by:  xnegcl  12947  xnegneg  12948  xltnegi  12950  xnegid  12972  xnegdi  12982  xsubge0  12995  xmulneg1  13003  xmulpnf1n  13012  xadddi2  13031  xrsdsreclblem  20644  xaddeq0  31076  xrge0npcan  31303  carsgclctunlem2  32286  supminfxr  43004  supminfxr2  43009  liminf0  43334  liminflbuz2  43356  liminfpnfuz  43357