Theorem xnegmnf 13129

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 13030	. 2 ⊢ -𝑒-∞ = if(-∞ = +∞, -∞, if(-∞ = -∞, +∞, --∞))
2		mnfnepnf 11192	. . 3 ⊢ -∞ ≠ +∞
3		ifnefalse 4492	. . 3 ⊢ (-∞ ≠ +∞ → if(-∞ = +∞, -∞, if(-∞ = -∞, +∞, --∞)) = if(-∞ = -∞, +∞, --∞))
4	2, 3	ax-mp 5	. 2 ⊢ if(-∞ = +∞, -∞, if(-∞ = -∞, +∞, --∞)) = if(-∞ = -∞, +∞, --∞)
5		eqid 2737	. . 3 ⊢ -∞ = -∞
6	5	iftruei 4487	. 2 ⊢ if(-∞ = -∞, +∞, --∞) = +∞
7	1, 4, 6	3eqtri 2764	1 ⊢ -𝑒-∞ = +∞

Syntax hints:   = wceq 1542   ≠ wne 2933  ifcif 4480  +∞cpnf 11167  -∞cmnf 11168  -cneg 11369  -_𝑒cxne 13027

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709  ax-sep 5242  ax-pow 5311  ax-un 7682  ax-cnex 11086

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-ne 2934  df-rab 3401  df-v 3443  df-un 3907  df-in 3909  df-ss 3919  df-if 4481  df-pw 4557  df-sn 4582  df-pr 4584  df-uni 4865  df-pnf 11172  df-mnf 11173  df-xr 11174  df-xneg 13030

This theorem is referenced by:  xnegcl  13132  xnegneg  13133  xltnegi  13135  xnegid  13157  xnegdi  13167  xsubge0  13180  xmulneg1  13188  xmulpnf1n  13197  xadddi2  13216  xrsdsreclblem  21371  xaddeq0  32835  xrge0npcan  33104  carsgclctunlem2  34478  supminfxr  45775  supminfxr2  45780  liminf0  46104  liminflbuz2  46126  liminfpnfuz  46127