Theorem xnegmnf 13340

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	⊢ -e-∞ = +∞

Proof of Theorem xnegmnf

Step	Hyp	Ref	Expression
1		df-xneg 13241	. 2 ⊢ -e-∞ = if(-∞ = +∞, -∞, if(-∞ = -∞, +∞, --∞))
2		mnfnepnf 11365	. . 3 ⊢ -∞ ≠ +∞
3		ifnefalse 4493	. . 3 ⊢ (-∞ ≠ +∞ → if(-∞ = +∞, -∞, if(-∞ = -∞, +∞, --∞)) = if(-∞ = -∞, +∞, --∞))
4	2, 3	ax-mp 5	. 2 ⊢ if(-∞ = +∞, -∞, if(-∞ = -∞, +∞, --∞)) = if(-∞ = -∞, +∞, --∞)
5		eqid 2760	. . 3 ⊢ -∞ = -∞
6	5	iftruei 4488	. 2 ⊢ if(-∞ = -∞, +∞, --∞) = +∞
7	1, 4, 6	3eqtri 2787	1 ⊢ -e-∞ = +∞

This proof depends on syntax axioms:   = wceq 1569   ≠ wne 2955  ifcif 4481  +∞cpnf 11340  -∞cmnf 11341   -cneg 11542   -_ecxne 13238

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-ext 2732  ax-sep 5248  ax-pow 5326  ax-un 7751  ax-cnex 11256

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1572  df-ex 1812  df-sb 2099  df-clab 2739  df-cleq 2752  df-clel 2835  df-ne 2956  df-rab 3413  df-v 3452  df-ss 3896  df-in 4091  df-un 4151  df-if 4482  df-pw 4558  df-sn 4584  df-pr 4586  df-uni 4867  df-pnf 11345  df-mnf 11346  df-xr 11347  df-xneg 13241

This theorem is used by:  xnegcl  13343  xnegneg  13344  xltnegi  13346  xnegid  13368  xnegdi  13378  xsubge0  13391  xmulneg1  13399  xmulpnf1n  13408  xadddi2  13427  xrsdsreclblem  21719  xaddeq0  33345  xrge0npcan  33581  carsgclctunlem2  34951  supminfxr  46474  supminfxr2  46479  liminf0  46803  liminflbuz2  46825  liminfpnfuz  46826