Theorem xnegpnf 13363

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 13265	. 2 ⊢ -e+∞ = if(+∞ = +∞, -∞, if(+∞ = -∞, +∞, -+∞))
2		eqid 2763	. . 3 ⊢ +∞ = +∞
3	2	iftruei 4492	. 2 ⊢ if(+∞ = +∞, -∞, if(+∞ = -∞, +∞, -+∞)) = -∞
4	1, 3	eqtri 2786	1 ⊢ -e+∞ = -∞

This proof depends on syntax axioms:   = wceq 1570  ifcif 4485  +∞cpnf 11364  -∞cmnf 11365   -cneg 11566   -_ecxne 13262

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-ext 2735

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-ex 1813  df-sb 2102  df-clab 2742  df-cleq 2755  df-clel 2839  df-if 4486  df-xneg 13265

This theorem is used by:  xnegcl  13367  xnegneg  13368  xltnegi  13370  xnegid  13392  xnegdi  13402  xaddass2  13404  xsubge0  13415  xlesubadd  13417  xmulneg1  13423  xmulmnf1  13430  xadddi2  13451  xrsdsreclblem  21746  xblss2ps  24747  xblss2  24748  xaddeq0  33412  supminfxr  46677  liminflbuz2  47028