Theorem xnegmnf 13193

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 13096	. 2 ⊢ -𝑒-∞ = if(-∞ = +∞, -∞, if(-∞ = -∞, +∞, --∞))
2		mnfnepnf 11274	. . 3 ⊢ -∞ ≠ +∞
3		ifnefalse 4539	. . 3 ⊢ (-∞ ≠ +∞ → if(-∞ = +∞, -∞, if(-∞ = -∞, +∞, --∞)) = if(-∞ = -∞, +∞, --∞))
4	2, 3	ax-mp 5	. 2 ⊢ if(-∞ = +∞, -∞, if(-∞ = -∞, +∞, --∞)) = if(-∞ = -∞, +∞, --∞)
5		eqid 2730	. . 3 ⊢ -∞ = -∞
6	5	iftruei 4534	. 2 ⊢ if(-∞ = -∞, +∞, --∞) = +∞
7	1, 4, 6	3eqtri 2762	1 ⊢ -𝑒-∞ = +∞

Syntax hints:   = wceq 1539   ≠ wne 2938  ifcif 4527  +∞cpnf 11249  -∞cmnf 11250  -cneg 11449  -_𝑒cxne 13093

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 1911  ax-6 1969  ax-7 2009  ax-8 2106  ax-9 2114  ax-ext 2701  ax-sep 5298  ax-pow 5362  ax-un 7727  ax-cnex 11168

This theorem depends on definitions:  df-bi 206  df-an 395  df-or 844  df-tru 1542  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2722  df-clel 2808  df-ne 2939  df-rab 3431  df-v 3474  df-un 3952  df-in 3954  df-ss 3964  df-if 4528  df-pw 4603  df-sn 4628  df-pr 4630  df-uni 4908  df-pnf 11254  df-mnf 11255  df-xr 11256  df-xneg 13096

This theorem is referenced by:  xnegcl  13196  xnegneg  13197  xltnegi  13199  xnegid  13221  xnegdi  13231  xsubge0  13244  xmulneg1  13252  xmulpnf1n  13261  xadddi2  13280  xrsdsreclblem  21191  xaddeq0  32233  xrge0npcan  32462  carsgclctunlem2  33616  supminfxr  44472  supminfxr2  44477  liminf0  44807  liminflbuz2  44829  liminfpnfuz  44830