Theorem xnegmnf 13112

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 13014	. 2 ⊢ -𝑒-∞ = if(-∞ = +∞, -∞, if(-∞ = -∞, +∞, --∞))
2		mnfnepnf 11171	. . 3 ⊢ -∞ ≠ +∞
3		ifnefalse 4488	. . 3 ⊢ (-∞ ≠ +∞ → if(-∞ = +∞, -∞, if(-∞ = -∞, +∞, --∞)) = if(-∞ = -∞, +∞, --∞))
4	2, 3	ax-mp 5	. 2 ⊢ if(-∞ = +∞, -∞, if(-∞ = -∞, +∞, --∞)) = if(-∞ = -∞, +∞, --∞)
5		eqid 2729	. . 3 ⊢ -∞ = -∞
6	5	iftruei 4483	. 2 ⊢ if(-∞ = -∞, +∞, --∞) = +∞
7	1, 4, 6	3eqtri 2756	1 ⊢ -𝑒-∞ = +∞

Syntax hints:   = wceq 1540   ≠ wne 2925  ifcif 4476  +∞cpnf 11146  -∞cmnf 11147  -cneg 11348  -_𝑒cxne 13011

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701  ax-sep 5235  ax-pow 5304  ax-un 7671  ax-cnex 11065

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-ne 2926  df-rab 3395  df-v 3438  df-un 3908  df-in 3910  df-ss 3920  df-if 4477  df-pw 4553  df-sn 4578  df-pr 4580  df-uni 4859  df-pnf 11151  df-mnf 11152  df-xr 11153  df-xneg 13014

This theorem is referenced by:  xnegcl  13115  xnegneg  13116  xltnegi  13118  xnegid  13140  xnegdi  13150  xsubge0  13163  xmulneg1  13171  xmulpnf1n  13180  xadddi2  13199  xrsdsreclblem  21319  xaddeq0  32697  xrge0npcan  32975  carsgclctunlem2  34293  supminfxr  45453  supminfxr2  45458  liminf0  45784  liminflbuz2  45806  liminfpnfuz  45807