Theorem xnegmnf 13215

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 13116	. 2 ⊢ -𝑒-∞ = if(-∞ = +∞, -∞, if(-∞ = -∞, +∞, --∞))
2		mnfnepnf 11240	. . 3 ⊢ -∞ ≠ +∞
3		ifnefalse 4494	. . 3 ⊢ (-∞ ≠ +∞ → if(-∞ = +∞, -∞, if(-∞ = -∞, +∞, --∞)) = if(-∞ = -∞, +∞, --∞))
4	2, 3	ax-mp 5	. 2 ⊢ if(-∞ = +∞, -∞, if(-∞ = -∞, +∞, --∞)) = if(-∞ = -∞, +∞, --∞)
5		eqid 2764	. . 3 ⊢ -∞ = -∞
6	5	iftruei 4489	. 2 ⊢ if(-∞ = -∞, +∞, --∞) = +∞
7	1, 4, 6	3eqtri 2791	1 ⊢ -𝑒-∞ = +∞

Syntax hints:   = wceq 1562   ≠ wne 2959  ifcif 4482  +∞cpnf 11215  -∞cmnf 11216  -cneg 11417  -_𝑒cxne 13113

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1817  ax-4 1831  ax-5 1932  ax-6 1989  ax-7 2030  ax-8 2146  ax-9 2154  ax-ext 2736  ax-sep 5248  ax-pow 5324  ax-un 7720  ax-cnex 11131

This theorem depends on definitions:  df-bi 209  df-an 400  df-or 859  df-3an 1101  df-tru 1565  df-ex 1802  df-sb 2093  df-clab 2743  df-cleq 2756  df-clel 2839  df-ne 2960  df-rab 3417  df-v 3458  df-un 3911  df-in 3913  df-ss 3923  df-if 4483  df-pw 4559  df-sn 4585  df-pr 4587  df-uni 4868  df-pnf 11220  df-mnf 11221  df-xr 11222  df-xneg 13116

This theorem is referenced by:  xnegcl  13218  xnegneg  13219  xltnegi  13221  xnegid  13243  xnegdi  13253  xsubge0  13266  xmulneg1  13274  xmulpnf1n  13283  xadddi2  13302  xrsdsreclblem  21467  xaddeq0  32957  xrge0npcan  33200  carsgclctunlem2  34618  supminfxr  46043  supminfxr2  46048  liminf0  46372  liminflbuz2  46394  liminfpnfuz  46395