Theorem xnegmnf 12606

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 12510	. 2 ⊢ -𝑒-∞ = if(-∞ = +∞, -∞, if(-∞ = -∞, +∞, --∞))
2		mnfnepnf 10699	. . 3 ⊢ -∞ ≠ +∞
3		ifnefalse 4481	. . 3 ⊢ (-∞ ≠ +∞ → if(-∞ = +∞, -∞, if(-∞ = -∞, +∞, --∞)) = if(-∞ = -∞, +∞, --∞))
4	2, 3	ax-mp 5	. 2 ⊢ if(-∞ = +∞, -∞, if(-∞ = -∞, +∞, --∞)) = if(-∞ = -∞, +∞, --∞)
5		eqid 2823	. . 3 ⊢ -∞ = -∞
6	5	iftruei 4476	. 2 ⊢ if(-∞ = -∞, +∞, --∞) = +∞
7	1, 4, 6	3eqtri 2850	1 ⊢ -𝑒-∞ = +∞

Syntax hints:   = wceq 1537   ≠ wne 3018  ifcif 4469  +∞cpnf 10674  -∞cmnf 10675  -cneg 10873  -_𝑒cxne 12507

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2795  ax-sep 5205  ax-pow 5268  ax-un 7463  ax-cnex 10595

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-tru 1540  df-ex 1781  df-nf 1785  df-sb 2070  df-clab 2802  df-cleq 2816  df-clel 2895  df-nfc 2965  df-ne 3019  df-rab 3149  df-v 3498  df-un 3943  df-in 3945  df-ss 3954  df-if 4470  df-pw 4543  df-sn 4570  df-pr 4572  df-uni 4841  df-pnf 10679  df-mnf 10680  df-xr 10681  df-xneg 12510

This theorem is referenced by:  xnegcl  12609  xnegneg  12610  xltnegi  12612  xnegid  12634  xnegdi  12644  xsubge0  12657  xmulneg1  12665  xmulpnf1n  12674  xadddi2  12693  xrsdsreclblem  20593  xaddeq0  30479  xrge0npcan  30683  carsgclctunlem2  31579  supminfxr  41747  supminfxr2  41752  liminf0  42081  liminflbuz2  42103  liminfpnfuz  42104