Theorem xnegmnf 12686

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 12590	. 2 ⊢ -𝑒-∞ = if(-∞ = +∞, -∞, if(-∞ = -∞, +∞, --∞))
2		mnfnepnf 10775	. . 3 ⊢ -∞ ≠ +∞
3		ifnefalse 4426	. . 3 ⊢ (-∞ ≠ +∞ → if(-∞ = +∞, -∞, if(-∞ = -∞, +∞, --∞)) = if(-∞ = -∞, +∞, --∞))
4	2, 3	ax-mp 5	. 2 ⊢ if(-∞ = +∞, -∞, if(-∞ = -∞, +∞, --∞)) = if(-∞ = -∞, +∞, --∞)
5		eqid 2738	. . 3 ⊢ -∞ = -∞
6	5	iftruei 4421	. 2 ⊢ if(-∞ = -∞, +∞, --∞) = +∞
7	1, 4, 6	3eqtri 2765	1 ⊢ -𝑒-∞ = +∞

Syntax hints:   = wceq 1542   ≠ wne 2934  ifcif 4414  +∞cpnf 10750  -∞cmnf 10751  -cneg 10949  -_𝑒cxne 12587

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1975  ax-7 2020  ax-8 2116  ax-9 2124  ax-ext 2710  ax-sep 5167  ax-pow 5232  ax-un 7479  ax-cnex 10671

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 847  df-tru 1545  df-ex 1787  df-sb 2075  df-clab 2717  df-cleq 2730  df-clel 2811  df-ne 2935  df-rab 3062  df-v 3400  df-un 3848  df-in 3850  df-ss 3860  df-if 4415  df-pw 4490  df-sn 4517  df-pr 4519  df-uni 4797  df-pnf 10755  df-mnf 10756  df-xr 10757  df-xneg 12590

This theorem is referenced by:  xnegcl  12689  xnegneg  12690  xltnegi  12692  xnegid  12714  xnegdi  12724  xsubge0  12737  xmulneg1  12745  xmulpnf1n  12754  xadddi2  12773  xrsdsreclblem  20263  xaddeq0  30651  xrge0npcan  30880  carsgclctunlem2  31856  supminfxr  42544  supminfxr2  42549  liminf0  42876  liminflbuz2  42898  liminfpnfuz  42899