Theorem xnegmnf 13157

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 13058	. 2 ⊢ -𝑒-∞ = if(-∞ = +∞, -∞, if(-∞ = -∞, +∞, --∞))
2		mnfnepnf 11196	. . 3 ⊢ -∞ ≠ +∞
3		ifnefalse 4469	. . 3 ⊢ (-∞ ≠ +∞ → if(-∞ = +∞, -∞, if(-∞ = -∞, +∞, --∞)) = if(-∞ = -∞, +∞, --∞))
4	2, 3	ax-mp 5	. 2 ⊢ if(-∞ = +∞, -∞, if(-∞ = -∞, +∞, --∞)) = if(-∞ = -∞, +∞, --∞)
5		eqid 2741	. . 3 ⊢ -∞ = -∞
6	5	iftruei 4464	. 2 ⊢ if(-∞ = -∞, +∞, --∞) = +∞
7	1, 4, 6	3eqtri 2768	1 ⊢ -𝑒-∞ = +∞

Syntax hints:   = wceq 1548   ≠ wne 2936  ifcif 4457  +∞cpnf 11171  -∞cmnf 11172  -cneg 11373  -_𝑒cxne 13055

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1975  ax-7 2016  ax-8 2123  ax-9 2131  ax-ext 2713  ax-sep 5221  ax-pow 5297  ax-un 7682  ax-cnex 11089

This theorem depends on definitions:  df-bi 209  df-an 398  df-or 855  df-3an 1095  df-tru 1551  df-ex 1788  df-sb 2075  df-clab 2720  df-cleq 2733  df-clel 2816  df-ne 2937  df-rab 3394  df-v 3435  df-un 3890  df-in 3892  df-ss 3902  df-if 4458  df-pw 4534  df-sn 4559  df-pr 4561  df-uni 4842  df-pnf 11176  df-mnf 11177  df-xr 11178  df-xneg 13058

This theorem is referenced by:  xnegcl  13160  xnegneg  13161  xltnegi  13163  xnegid  13185  xnegdi  13195  xsubge0  13208  xmulneg1  13216  xmulpnf1n  13225  xadddi2  13244  xrsdsreclblem  21392  xaddeq0  32849  xrge0npcan  33103  carsgclctunlem2  34515  supminfxr  45921  supminfxr2  45926  liminf0  46250  liminflbuz2  46272  liminfpnfuz  46273