Theorem xnegmnf 13185

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 13088	. 2 ⊢ -𝑒-∞ = if(-∞ = +∞, -∞, if(-∞ = -∞, +∞, --∞))
2		mnfnepnf 11266	. . 3 ⊢ -∞ ≠ +∞
3		ifnefalse 4532	. . 3 ⊢ (-∞ ≠ +∞ → if(-∞ = +∞, -∞, if(-∞ = -∞, +∞, --∞)) = if(-∞ = -∞, +∞, --∞))
4	2, 3	ax-mp 5	. 2 ⊢ if(-∞ = +∞, -∞, if(-∞ = -∞, +∞, --∞)) = if(-∞ = -∞, +∞, --∞)
5		eqid 2724	. . 3 ⊢ -∞ = -∞
6	5	iftruei 4527	. 2 ⊢ if(-∞ = -∞, +∞, --∞) = +∞
7	1, 4, 6	3eqtri 2756	1 ⊢ -𝑒-∞ = +∞

Syntax hints:   = wceq 1533   ≠ wne 2932  ifcif 4520  +∞cpnf 11241  -∞cmnf 11242  -cneg 11441  -_𝑒cxne 13085

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-ext 2695  ax-sep 5289  ax-pow 5353  ax-un 7718  ax-cnex 11161

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 845  df-tru 1536  df-ex 1774  df-sb 2060  df-clab 2702  df-cleq 2716  df-clel 2802  df-ne 2933  df-rab 3425  df-v 3468  df-un 3945  df-in 3947  df-ss 3957  df-if 4521  df-pw 4596  df-sn 4621  df-pr 4623  df-uni 4900  df-pnf 11246  df-mnf 11247  df-xr 11248  df-xneg 13088

This theorem is referenced by:  xnegcl  13188  xnegneg  13189  xltnegi  13191  xnegid  13213  xnegdi  13223  xsubge0  13236  xmulneg1  13244  xmulpnf1n  13253  xadddi2  13272  xrsdsreclblem  21274  xaddeq0  32401  xrge0npcan  32626  carsgclctunlem2  33773  supminfxr  44625  supminfxr2  44630  liminf0  44960  liminflbuz2  44982  liminfpnfuz  44983