Theorem xnegmnf 13170

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

Syntax hints:   = wceq 1540   ≠ wne 2925  ifcif 4488  +∞cpnf 11205  -∞cmnf 11206  -cneg 11406  -_𝑒cxne 13069

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 5251  ax-pow 5320  ax-un 7711  ax-cnex 11124

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 3406  df-v 3449  df-un 3919  df-in 3921  df-ss 3931  df-if 4489  df-pw 4565  df-sn 4590  df-pr 4592  df-uni 4872  df-pnf 11210  df-mnf 11211  df-xr 11212  df-xneg 13072

This theorem is referenced by:  xnegcl  13173  xnegneg  13174  xltnegi  13176  xnegid  13198  xnegdi  13208  xsubge0  13221  xmulneg1  13229  xmulpnf1n  13238  xadddi2  13257  xrsdsreclblem  21329  xaddeq0  32676  xrge0npcan  32961  carsgclctunlem2  34310  supminfxr  45460  supminfxr2  45465  liminf0  45791  liminflbuz2  45813  liminfpnfuz  45814