Theorem xnegmnf 13226

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 13128	. 2 ⊢ -𝑒-∞ = if(-∞ = +∞, -∞, if(-∞ = -∞, +∞, --∞))
2		mnfnepnf 11291	. . 3 ⊢ -∞ ≠ +∞
3		ifnefalse 4512	. . 3 ⊢ (-∞ ≠ +∞ → if(-∞ = +∞, -∞, if(-∞ = -∞, +∞, --∞)) = if(-∞ = -∞, +∞, --∞))
4	2, 3	ax-mp 5	. 2 ⊢ if(-∞ = +∞, -∞, if(-∞ = -∞, +∞, --∞)) = if(-∞ = -∞, +∞, --∞)
5		eqid 2735	. . 3 ⊢ -∞ = -∞
6	5	iftruei 4507	. 2 ⊢ if(-∞ = -∞, +∞, --∞) = +∞
7	1, 4, 6	3eqtri 2762	1 ⊢ -𝑒-∞ = +∞

Syntax hints:   = wceq 1540   ≠ wne 2932  ifcif 4500  +∞cpnf 11266  -∞cmnf 11267  -cneg 11467  -_𝑒cxne 13125

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2707  ax-sep 5266  ax-pow 5335  ax-un 7729  ax-cnex 11185

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-ex 1780  df-sb 2065  df-clab 2714  df-cleq 2727  df-clel 2809  df-ne 2933  df-rab 3416  df-v 3461  df-un 3931  df-in 3933  df-ss 3943  df-if 4501  df-pw 4577  df-sn 4602  df-pr 4604  df-uni 4884  df-pnf 11271  df-mnf 11272  df-xr 11273  df-xneg 13128

This theorem is referenced by:  xnegcl  13229  xnegneg  13230  xltnegi  13232  xnegid  13254  xnegdi  13264  xsubge0  13277  xmulneg1  13285  xmulpnf1n  13294  xadddi2  13313  xrsdsreclblem  21380  xaddeq0  32730  xrge0npcan  33015  carsgclctunlem2  34351  supminfxr  45491  supminfxr2  45496  liminf0  45822  liminflbuz2  45844  liminfpnfuz  45845