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

Theorem renepnf 9944
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 9938 . . . 4 +∞ ∉ ℝ
21neli 2885 . . 3 ¬ +∞ ∈ ℝ
3 eleq1 2676 . . 3 (𝐴 = +∞ → (𝐴 ∈ ℝ ↔ +∞ ∈ ℝ))
42, 3mtbiri 316 . 2 (𝐴 = +∞ → ¬ 𝐴 ∈ ℝ)
54necon2ai 2811 1 (𝐴 ∈ ℝ → 𝐴 ≠ +∞)
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1475  wcel 1977  wne 2780  cr 9792  +∞cpnf 9928
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-8 1979  ax-9 1986  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590  ax-sep 4704  ax-nul 4712  ax-pow 4764  ax-pr 4828  ax-un 6825  ax-resscn 9850
This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-3an 1033  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-ne 2782  df-nel 2783  df-rex 2902  df-rab 2905  df-v 3175  df-dif 3543  df-un 3545  df-in 3547  df-ss 3554  df-nul 3875  df-pw 4110  df-sn 4126  df-pr 4128  df-uni 4368  df-pnf 9933
This theorem is referenced by:  renepnfd  9947  renfdisj  9950  xrnepnf  11792  rexneg  11878  rexadd  11899  xaddnepnf  11903  xaddcom  11906  xaddid1  11907  xnegdi  11910  xpncan  11913  xleadd1a  11915  rexmul  11933  xmulpnf1  11936  xadddilem  11956  rpsup  12485  hashneq0  12971  hash1snb  13023  xrsnsgrp  19550  xaddeq0  28701  icorempt2  32169  ovoliunnfl  32415  voliunnfl  32417  volsupnfl  32418  supxrgelem  38288  supxrge  38289  infleinflem1  38321  infleinflem2  38322  sge0repnf  39073  voliunsge0lem  39159  xnn0xadd0  40207
  Copyright terms: Public domain W3C validator