Theorem xnegmnf 13272

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 13175	. 2 ⊢ -𝑒-∞ = if(-∞ = +∞, -∞, if(-∞ = -∞, +∞, --∞))
2		mnfnepnf 11346	. . 3 ⊢ -∞ ≠ +∞
3		ifnefalse 4560	. . 3 ⊢ (-∞ ≠ +∞ → if(-∞ = +∞, -∞, if(-∞ = -∞, +∞, --∞)) = if(-∞ = -∞, +∞, --∞))
4	2, 3	ax-mp 5	. 2 ⊢ if(-∞ = +∞, -∞, if(-∞ = -∞, +∞, --∞)) = if(-∞ = -∞, +∞, --∞)
5		eqid 2740	. . 3 ⊢ -∞ = -∞
6	5	iftruei 4555	. 2 ⊢ if(-∞ = -∞, +∞, --∞) = +∞
7	1, 4, 6	3eqtri 2772	1 ⊢ -𝑒-∞ = +∞

Syntax hints:   = wceq 1537   ≠ wne 2946  ifcif 4548  +∞cpnf 11321  -∞cmnf 11322  -cneg 11521  -_𝑒cxne 13172

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2711  ax-sep 5317  ax-pow 5383  ax-un 7770  ax-cnex 11240

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 847  df-3an 1089  df-tru 1540  df-ex 1778  df-sb 2065  df-clab 2718  df-cleq 2732  df-clel 2819  df-ne 2947  df-rab 3444  df-v 3490  df-un 3981  df-in 3983  df-ss 3993  df-if 4549  df-pw 4624  df-sn 4649  df-pr 4651  df-uni 4932  df-pnf 11326  df-mnf 11327  df-xr 11328  df-xneg 13175

This theorem is referenced by:  xnegcl  13275  xnegneg  13276  xltnegi  13278  xnegid  13300  xnegdi  13310  xsubge0  13323  xmulneg1  13331  xmulpnf1n  13340  xadddi2  13359  xrsdsreclblem  21453  xaddeq0  32760  xrge0npcan  33006  carsgclctunlem2  34284  supminfxr  45379  supminfxr2  45384  liminf0  45714  liminflbuz2  45736  liminfpnfuz  45737