Theorem xnegmnf 13162

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 13063	. 2 ⊢ -𝑒-∞ = if(-∞ = +∞, -∞, if(-∞ = -∞, +∞, --∞))
2		mnfnepnf 11201	. . 3 ⊢ -∞ ≠ +∞
3		ifnefalse 4478	. . 3 ⊢ (-∞ ≠ +∞ → if(-∞ = +∞, -∞, if(-∞ = -∞, +∞, --∞)) = if(-∞ = -∞, +∞, --∞))
4	2, 3	ax-mp 5	. 2 ⊢ if(-∞ = +∞, -∞, if(-∞ = -∞, +∞, --∞)) = if(-∞ = -∞, +∞, --∞)
5		eqid 2736	. . 3 ⊢ -∞ = -∞
6	5	iftruei 4473	. 2 ⊢ if(-∞ = -∞, +∞, --∞) = +∞
7	1, 4, 6	3eqtri 2763	1 ⊢ -𝑒-∞ = +∞

Syntax hints:   = wceq 1542   ≠ wne 2932  ifcif 4466  +∞cpnf 11176  -∞cmnf 11177  -cneg 11378  -_𝑒cxne 13060

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2708  ax-sep 5231  ax-pow 5307  ax-un 7689  ax-cnex 11094

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2715  df-cleq 2728  df-clel 2811  df-ne 2933  df-rab 3390  df-v 3431  df-un 3894  df-in 3896  df-ss 3906  df-if 4467  df-pw 4543  df-sn 4568  df-pr 4570  df-uni 4851  df-pnf 11181  df-mnf 11182  df-xr 11183  df-xneg 13063

This theorem is referenced by:  xnegcl  13165  xnegneg  13166  xltnegi  13168  xnegid  13190  xnegdi  13200  xsubge0  13213  xmulneg1  13221  xmulpnf1n  13230  xadddi2  13249  xrsdsreclblem  21393  xaddeq0  32826  xrge0npcan  33080  carsgclctunlem2  34463  supminfxr  45892  supminfxr2  45897  liminf0  46221  liminflbuz2  46243  liminfpnfuz  46244