MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  renepnf Structured version   Visualization version   GIF version

Theorem renepnf 11208
Description: No (finite) real equals plus infinity. (Contributed by NM, 14-Oct-2005.) (Proof shortened by Andrew Salmon, 19-Nov-2011.)
Assertion
Ref Expression
renepnf (𝐴 ∈ ℝ → 𝐴 ≠ +∞)

Proof of Theorem renepnf
StepHypRef Expression
1 pnfnre 11201 . . . 4 +∞ ∉ ℝ
21neli 3048 . . 3 ¬ +∞ ∈ ℝ
3 eleq1 2822 . . 3 (𝐴 = +∞ → (𝐴 ∈ ℝ ↔ +∞ ∈ ℝ))
42, 3mtbiri 327 . 2 (𝐴 = +∞ → ¬ 𝐴 ∈ ℝ)
54necon2ai 2970 1 (𝐴 ∈ ℝ → 𝐴 ≠ +∞)
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1542  wcel 2107  wne 2940  cr 11055  +∞cpnf 11191
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2704  ax-sep 5257  ax-pr 5385  ax-un 7673  ax-resscn 11113
This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-tru 1545  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-ne 2941  df-nel 3047  df-rab 3407  df-v 3446  df-un 3916  df-in 3918  df-ss 3928  df-pw 4563  df-sn 4588  df-pr 4590  df-uni 4867  df-pnf 11196
This theorem is referenced by:  renepnfd  11211  renfdisj  11220  xrnepnf  13044  rexneg  13136  rexadd  13157  xaddnepnf  13162  xaddcom  13165  xaddid1  13166  xnn0xadd0  13172  xnegdi  13173  xpncan  13176  xleadd1a  13178  rexmul  13196  xmulpnf1  13199  xadddilem  13219  rpsup  13777  hashneq0  14270  hash1snb  14325  xrsnsgrp  20849  xaddeq0  31705  icorempo  35868  ovoliunnfl  36166  voliunnfl  36168  volsupnfl  36169  supxrgelem  43658  supxrge  43659  infleinflem1  43691  infleinflem2  43692  xrre4  43732  supminfxr2  43790  climxrre  44077  sge0repnf  44713  voliunsge0lem  44799
  Copyright terms: Public domain W3C validator