Theorem xnegmnf 13264

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 13165	. 2 ⊢ -𝑒-∞ = if(-∞ = +∞, -∞, if(-∞ = -∞, +∞, --∞))
2		mnfnepnf 11292	. . 3 ⊢ -∞ ≠ +∞
3		ifnefalse 4497	. . 3 ⊢ (-∞ ≠ +∞ → if(-∞ = +∞, -∞, if(-∞ = -∞, +∞, --∞)) = if(-∞ = -∞, +∞, --∞))
4	2, 3	ax-mp 5	. 2 ⊢ if(-∞ = +∞, -∞, if(-∞ = -∞, +∞, --∞)) = if(-∞ = -∞, +∞, --∞)
5		eqid 2762	. . 3 ⊢ -∞ = -∞
6	5	iftruei 4492	. 2 ⊢ if(-∞ = -∞, +∞, --∞) = +∞
7	1, 4, 6	3eqtri 2789	1 ⊢ -𝑒-∞ = +∞

This proof depends on syntax axioms:   = wceq 1570   ≠ wne 2957  ifcif 4485  +∞cpnf 11267  -∞cmnf 11268  -cneg 11469  -_𝑒cxne 13162

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2734  ax-sep 5255  ax-pow 5334  ax-un 7739  ax-cnex 11183

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2741  df-cleq 2754  df-clel 2837  df-ne 2958  df-rab 3415  df-v 3455  df-un 3907  df-in 3909  df-ss 3919  df-if 4486  df-pw 4562  df-sn 4588  df-pr 4590  df-uni 4871  df-pnf 11272  df-mnf 11273  df-xr 11274  df-xneg 13165

This theorem is used by:  xnegcl  13267  xnegneg  13268  xltnegi  13270  xnegid  13292  xnegdi  13302  xsubge0  13315  xmulneg1  13323  xmulpnf1n  13332  xadddi2  13351  xrsdsreclblem  21627  xaddeq0  33211  xrge0npcan  33447  carsgclctunlem2  34817  supminfxr  46279  supminfxr2  46284  liminf0  46608  liminflbuz2  46630  liminfpnfuz  46631