Theorem xnegmnf 13309

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 13210	. 2 ⊢ -𝑒-∞ = if(-∞ = +∞, -∞, if(-∞ = -∞, +∞, --∞))
2		mnfnepnf 11336	. . 3 ⊢ -∞ ≠ +∞
3		ifnefalse 4493	. . 3 ⊢ (-∞ ≠ +∞ → if(-∞ = +∞, -∞, if(-∞ = -∞, +∞, --∞)) = if(-∞ = -∞, +∞, --∞))
4	2, 3	ax-mp 5	. 2 ⊢ if(-∞ = +∞, -∞, if(-∞ = -∞, +∞, --∞)) = if(-∞ = -∞, +∞, --∞)
5		eqid 2760	. . 3 ⊢ -∞ = -∞
6	5	iftruei 4488	. 2 ⊢ if(-∞ = -∞, +∞, --∞) = +∞
7	1, 4, 6	3eqtri 2787	1 ⊢ -𝑒-∞ = +∞

This proof depends on syntax axioms:   = wceq 1570   ≠ wne 2955  ifcif 4481  +∞cpnf 11311  -∞cmnf 11312  -cneg 11513  -_𝑒cxne 13207

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 2732  ax-sep 5248  ax-pow 5326  ax-un 7734  ax-cnex 11227

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 2739  df-cleq 2752  df-clel 2835  df-ne 2956  df-rab 3413  df-v 3452  df-un 3903  df-in 3905  df-ss 3915  df-if 4482  df-pw 4558  df-sn 4584  df-pr 4586  df-uni 4867  df-pnf 11316  df-mnf 11317  df-xr 11318  df-xneg 13210

This theorem is used by:  xnegcl  13312  xnegneg  13313  xltnegi  13315  xnegid  13337  xnegdi  13347  xsubge0  13360  xmulneg1  13368  xmulpnf1n  13377  xadddi2  13396  xrsdsreclblem  21680  xaddeq0  33278  xrge0npcan  33514  carsgclctunlem2  34885  supminfxr  46396  supminfxr2  46401  liminf0  46725  liminflbuz2  46747  liminfpnfuz  46748