Theorem xnegpnf 13339

Description: Minus +∞. Remark of [BourbakiTop1] p. IV.15. (Contributed by FL, 26-Dec-2011.)

Assertion

Ref	Expression
xnegpnf	⊢ -e+∞ = -∞

Proof of Theorem xnegpnf

Step	Hyp	Ref	Expression
1		df-xneg 13241	. 2 ⊢ -e+∞ = if(+∞ = +∞, -∞, if(+∞ = -∞, +∞, -+∞))
2		eqid 2760	. . 3 ⊢ +∞ = +∞
3	2	iftruei 4488	. 2 ⊢ if(+∞ = +∞, -∞, if(+∞ = -∞, +∞, -+∞)) = -∞
4	1, 3	eqtri 2783	1 ⊢ -e+∞ = -∞

This proof depends on syntax axioms:   = wceq 1569  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

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-ex 1812  df-sb 2099  df-clab 2739  df-cleq 2752  df-clel 2835  df-if 4482  df-xneg 13241

This theorem is used by:  xnegcl  13343  xnegneg  13344  xltnegi  13346  xnegid  13368  xnegdi  13378  xaddass2  13380  xsubge0  13391  xlesubadd  13393  xmulneg1  13399  xmulmnf1  13406  xadddi2  13427  xrsdsreclblem  21719  xblss2ps  24720  xblss2  24721  xaddeq0  33345  supminfxr  46474  liminflbuz2  46825