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

Theorem renepnf 11294
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 11287 . . . 4 +∞ ∉ ℝ
21neli 3037 . . 3 ¬ +∞ ∈ ℝ
3 eleq1 2813 . . 3 (𝐴 = +∞ → (𝐴 ∈ ℝ ↔ +∞ ∈ ℝ))
42, 3mtbiri 326 . 2 (𝐴 = +∞ → ¬ 𝐴 ∈ ℝ)
54necon2ai 2959 1 (𝐴 ∈ ℝ → 𝐴 ≠ +∞)
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1533  wcel 2098  wne 2929  cr 11139  +∞cpnf 11277
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-ext 2696  ax-sep 5300  ax-pr 5429  ax-un 7741  ax-resscn 11197
This theorem depends on definitions:  df-bi 206  df-an 395  df-or 846  df-3an 1086  df-tru 1536  df-ex 1774  df-sb 2060  df-clab 2703  df-cleq 2717  df-clel 2802  df-ne 2930  df-nel 3036  df-rab 3419  df-v 3463  df-un 3949  df-in 3951  df-ss 3961  df-pw 4606  df-sn 4631  df-pr 4633  df-uni 4910  df-pnf 11282
This theorem is referenced by:  renepnfd  11297  renfdisj  11306  xrnepnf  13133  rexneg  13225  rexadd  13246  xaddnepnf  13251  xaddcom  13254  xaddrid  13255  xnn0xadd0  13261  xnegdi  13262  xpncan  13265  xleadd1a  13267  rexmul  13285  xmulpnf1  13288  xadddilem  13308  rpsup  13867  hashneq0  14359  hash1snb  14414  xrsnsgrp  21352  xaddeq0  32605  icorempo  36961  ovoliunnfl  37266  voliunnfl  37268  volsupnfl  37269  supxrgelem  44857  supxrge  44858  infleinflem1  44890  infleinflem2  44891  xrre4  44931  supminfxr2  44989  climxrre  45276  sge0repnf  45912  voliunsge0lem  45998
  Copyright terms: Public domain W3C validator