Theorem xnegmnf 13177

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 13079	. 2 ⊢ -𝑒-∞ = if(-∞ = +∞, -∞, if(-∞ = -∞, +∞, --∞))
2		mnfnepnf 11237	. . 3 ⊢ -∞ ≠ +∞
3		ifnefalse 4503	. . 3 ⊢ (-∞ ≠ +∞ → if(-∞ = +∞, -∞, if(-∞ = -∞, +∞, --∞)) = if(-∞ = -∞, +∞, --∞))
4	2, 3	ax-mp 5	. 2 ⊢ if(-∞ = +∞, -∞, if(-∞ = -∞, +∞, --∞)) = if(-∞ = -∞, +∞, --∞)
5		eqid 2730	. . 3 ⊢ -∞ = -∞
6	5	iftruei 4498	. 2 ⊢ if(-∞ = -∞, +∞, --∞) = +∞
7	1, 4, 6	3eqtri 2757	1 ⊢ -𝑒-∞ = +∞

Syntax hints:   = wceq 1540   ≠ wne 2926  ifcif 4491  +∞cpnf 11212  -∞cmnf 11213  -cneg 11413  -_𝑒cxne 13076

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 2702  ax-sep 5254  ax-pow 5323  ax-un 7714  ax-cnex 11131

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 2709  df-cleq 2722  df-clel 2804  df-ne 2927  df-rab 3409  df-v 3452  df-un 3922  df-in 3924  df-ss 3934  df-if 4492  df-pw 4568  df-sn 4593  df-pr 4595  df-uni 4875  df-pnf 11217  df-mnf 11218  df-xr 11219  df-xneg 13079

This theorem is referenced by:  xnegcl  13180  xnegneg  13181  xltnegi  13183  xnegid  13205  xnegdi  13215  xsubge0  13228  xmulneg1  13236  xmulpnf1n  13245  xadddi2  13264  xrsdsreclblem  21336  xaddeq0  32683  xrge0npcan  32968  carsgclctunlem2  34317  supminfxr  45467  supminfxr2  45472  liminf0  45798  liminflbuz2  45820  liminfpnfuz  45821