Theorem xnegmnf 13146

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 13048	. 2 ⊢ -𝑒-∞ = if(-∞ = +∞, -∞, if(-∞ = -∞, +∞, --∞))
2		mnfnepnf 11206	. . 3 ⊢ -∞ ≠ +∞
3		ifnefalse 4496	. . 3 ⊢ (-∞ ≠ +∞ → if(-∞ = +∞, -∞, if(-∞ = -∞, +∞, --∞)) = if(-∞ = -∞, +∞, --∞))
4	2, 3	ax-mp 5	. 2 ⊢ if(-∞ = +∞, -∞, if(-∞ = -∞, +∞, --∞)) = if(-∞ = -∞, +∞, --∞)
5		eqid 2729	. . 3 ⊢ -∞ = -∞
6	5	iftruei 4491	. 2 ⊢ if(-∞ = -∞, +∞, --∞) = +∞
7	1, 4, 6	3eqtri 2756	1 ⊢ -𝑒-∞ = +∞

Syntax hints:   = wceq 1540   ≠ wne 2925  ifcif 4484  +∞cpnf 11181  -∞cmnf 11182  -cneg 11382  -_𝑒cxne 13045

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 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701  ax-sep 5246  ax-pow 5315  ax-un 7691  ax-cnex 11100

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-ne 2926  df-rab 3403  df-v 3446  df-un 3916  df-in 3918  df-ss 3928  df-if 4485  df-pw 4561  df-sn 4586  df-pr 4588  df-uni 4868  df-pnf 11186  df-mnf 11187  df-xr 11188  df-xneg 13048

This theorem is referenced by:  xnegcl  13149  xnegneg  13150  xltnegi  13152  xnegid  13174  xnegdi  13184  xsubge0  13197  xmulneg1  13205  xmulpnf1n  13214  xadddi2  13233  xrsdsreclblem  21354  xaddeq0  32726  xrge0npcan  33004  carsgclctunlem2  34303  supminfxr  45453  supminfxr2  45458  liminf0  45784  liminflbuz2  45806  liminfpnfuz  45807