Theorem xnegmnf 13236

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 13137	. 2 ⊢ -𝑒-∞ = if(-∞ = +∞, -∞, if(-∞ = -∞, +∞, --∞))
2		mnfnepnf 11265	. . 3 ⊢ -∞ ≠ +∞
3		ifnefalse 4502	. . 3 ⊢ (-∞ ≠ +∞ → if(-∞ = +∞, -∞, if(-∞ = -∞, +∞, --∞)) = if(-∞ = -∞, +∞, --∞))
4	2, 3	ax-mp 5	. 2 ⊢ if(-∞ = +∞, -∞, if(-∞ = -∞, +∞, --∞)) = if(-∞ = -∞, +∞, --∞)
5		eqid 2769	. . 3 ⊢ -∞ = -∞
6	5	iftruei 4497	. 2 ⊢ if(-∞ = -∞, +∞, --∞) = +∞
7	1, 4, 6	3eqtri 2796	1 ⊢ -𝑒-∞ = +∞

Syntax hints:   = wceq 1567   ≠ wne 2964  ifcif 4490  +∞cpnf 11240  -∞cmnf 11241  -cneg 11442  -_𝑒cxne 13134

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-8 2151  ax-9 2159  ax-ext 2741  ax-sep 5259  ax-pow 5337  ax-un 7733  ax-cnex 11156

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1103  df-tru 1570  df-ex 1807  df-sb 2098  df-clab 2748  df-cleq 2761  df-clel 2844  df-ne 2965  df-rab 3423  df-v 3463  df-un 3916  df-in 3918  df-ss 3928  df-if 4491  df-pw 4567  df-sn 4593  df-pr 4595  df-uni 4875  df-pnf 11245  df-mnf 11246  df-xr 11247  df-xneg 13137

This theorem is referenced by:  xnegcl  13239  xnegneg  13240  xltnegi  13242  xnegid  13264  xnegdi  13274  xsubge0  13287  xmulneg1  13295  xmulpnf1n  13304  xadddi2  13323  xrsdsreclblem  21532  xaddeq0  33039  xrge0npcan  33281  carsgclctunlem2  34654  supminfxr  46105  supminfxr2  46110  liminf0  46434  liminflbuz2  46456  liminfpnfuz  46457