Theorem renemnf 11320

Description: No real equals minus infinity. (Contributed by NM, 14-Oct-2005.) (Proof shortened by Andrew Salmon, 19-Nov-2011.)

Assertion

Ref	Expression
renemnf	⊢ (𝐴 ∈ ℝ → 𝐴 ≠ -∞)

Proof of Theorem renemnf

Step	Hyp	Ref	Expression
1		mnfnre 11314	. . . 4 ⊢ -∞ ∉ ℝ
2	1	neli 3041	. . 3 ⊢ ¬ -∞ ∈ ℝ
3		eleq1 2817	. . 3 ⊢ (𝐴 = -∞ → (𝐴 ∈ ℝ ↔ -∞ ∈ ℝ))
4	2, 3	mtbiri 326	. 2 ⊢ (𝐴 = -∞ → ¬ 𝐴 ∈ ℝ)
5	4	necon2ai 2963	1 ⊢ (𝐴 ∈ ℝ → 𝐴 ≠ -∞)

Syntax hints:   → wi 4   = wceq 1534   ∈ wcel 2100   ≠ wne 2933  ℝcr 11164  -∞cmnf 11303

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906  ax-6 1964  ax-7 2004  ax-8 2102  ax-9 2110  ax-10 2133  ax-11 2150  ax-12 2170  ax-ext 2700  ax-sep 5307  ax-nul 5314  ax-pow 5373  ax-pr 5437  ax-un 7751  ax-resscn 11222

This theorem depends on definitions:  df-bi 206  df-an 395  df-or 846  df-3an 1086  df-tru 1537  df-fal 1547  df-ex 1775  df-nf 1779  df-sb 2062  df-mo 2532  df-eu 2561  df-clab 2707  df-cleq 2721  df-clel 2806  df-nfc 2881  df-ne 2934  df-nel 3040  df-ral 3055  df-rex 3064  df-rab 3429  df-v 3474  df-sbc 3789  df-csb 3905  df-dif 3962  df-un 3964  df-in 3966  df-ss 3976  df-nul 4336  df-if 4537  df-pw 4612  df-sn 4637  df-pr 4639  df-op 4643  df-uni 4919  df-br 5157  df-opab 5219  df-mpt 5240  df-id 5584  df-xp 5692  df-rel 5693  df-cnv 5694  df-co 5695  df-dm 5696  df-rn 5697  df-res 5698  df-ima 5699  df-iota 6510  df-fun 6560  df-fn 6561  df-f 6562  df-f1 6563  df-fo 6564  df-f1o 6565  df-fv 6566  df-er 8742  df-en 8983  df-dom 8984  df-sdom 8985  df-pnf 11307  df-mnf 11308

This theorem is referenced by:  renemnfd  11323  renfdisj  11331  xrnemnf  13161  rexneg  13254  rexadd  13275  xaddnemnf  13279  xaddcom  13283  xaddrid  13284  xnegdi  13291  xpncan  13294  xleadd1a  13296  rexmul  13314  xadddilem  13337  xrs1mnd  21423  xrs10  21424  isxmet2d  24347  imasdsf1olem  24393  xaddeq0  32685  icorempo  37105  infrpge  45036  infleinflem1  45055  xrre4  45096  climxrre  45441