Theorem xnegmnf 13364

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	⊢ -e-∞ = +∞

Proof of Theorem xnegmnf

Step	Hyp	Ref	Expression
1		df-xneg 13265	. 2 ⊢ -e-∞ = if(-∞ = +∞, -∞, if(-∞ = -∞, +∞, --∞))
2		mnfnepnf 11389	. . 3 ⊢ -∞ ≠ +∞
3		ifnefalse 4497	. . 3 ⊢ (-∞ ≠ +∞ → if(-∞ = +∞, -∞, if(-∞ = -∞, +∞, --∞)) = if(-∞ = -∞, +∞, --∞))
4	2, 3	ax-mp 5	. 2 ⊢ if(-∞ = +∞, -∞, if(-∞ = -∞, +∞, --∞)) = if(-∞ = -∞, +∞, --∞)
5		eqid 2763	. . 3 ⊢ -∞ = -∞
6	5	iftruei 4492	. 2 ⊢ if(-∞ = -∞, +∞, --∞) = +∞
7	1, 4, 6	3eqtri 2790	1 ⊢ -e-∞ = +∞

This proof depends on syntax axioms:   = wceq 1570   ≠ wne 2959  ifcif 4485  +∞cpnf 11364  -∞cmnf 11365   -cneg 11566   -_ecxne 13262

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-ext 2735  ax-sep 5252  ax-pow 5331  ax-un 7772  ax-cnex 11280

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-ex 1813  df-sb 2102  df-clab 2742  df-cleq 2755  df-clel 2839  df-ne 2960  df-rab 3417  df-v 3456  df-ss 3901  df-in 4094  df-un 4154  df-if 4486  df-pw 4562  df-sn 4589  df-pr 4591  df-uni 4871  df-pnf 11369  df-mnf 11370  df-xr 11371  df-xneg 13265

This theorem is used by:  xnegcl  13367  xnegneg  13368  xltnegi  13370  xnegid  13392  xnegdi  13402  xsubge0  13415  xmulneg1  13423  xmulpnf1n  13432  xadddi2  13451  xrsdsreclblem  21746  xaddeq0  33412  xrge0npcan  33648  carsgclctunlem2  35018  supminfxr  46677  supminfxr2  46682  liminf0  47006  liminflbuz2  47028  liminfpnfuz  47029