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

Theorem renepnf 10681
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 10674 . . . 4 +∞ ∉ ℝ
21neli 3123 . . 3 ¬ +∞ ∈ ℝ
3 eleq1 2898 . . 3 (𝐴 = +∞ → (𝐴 ∈ ℝ ↔ +∞ ∈ ℝ))
42, 3mtbiri 329 . 2 (𝐴 = +∞ → ¬ 𝐴 ∈ ℝ)
54necon2ai 3043 1 (𝐴 ∈ ℝ → 𝐴 ≠ +∞)
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1530  wcel 2107  wne 3014  cr 10528  +∞cpnf 10664
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 1904  ax-6 1963  ax-7 2008  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2153  ax-12 2169  ax-ext 2791  ax-sep 5194  ax-nul 5201  ax-pr 5320  ax-un 7453  ax-resscn 10586
This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3an 1083  df-tru 1533  df-ex 1774  df-nf 1778  df-sb 2063  df-clab 2798  df-cleq 2812  df-clel 2891  df-nfc 2961  df-ne 3015  df-nel 3122  df-rex 3142  df-rab 3145  df-v 3495  df-dif 3937  df-un 3939  df-in 3941  df-ss 3950  df-nul 4290  df-pw 4539  df-sn 4560  df-pr 4562  df-uni 4831  df-pnf 10669
This theorem is referenced by:  renepnfd  10684  renfdisj  10693  xrnepnf  12505  rexneg  12596  rexadd  12617  xaddnepnf  12622  xaddcom  12625  xaddid1  12626  xnn0xadd0  12632  xnegdi  12633  xpncan  12636  xleadd1a  12638  rexmul  12656  xmulpnf1  12659  xadddilem  12679  rpsup  13226  hashneq0  13717  hash1snb  13772  xrsnsgrp  20573  xaddeq0  30469  icorempo  34614  ovoliunnfl  34916  voliunnfl  34918  volsupnfl  34919  supxrgelem  41584  supxrge  41585  infleinflem1  41617  infleinflem2  41618  xrre4  41664  supminfxr2  41724  climxrre  42010  sge0repnf  42648  voliunsge0lem  42734
  Copyright terms: Public domain W3C validator