Theorem renepnf 11023

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

Step	Hyp	Ref	Expression
1		pnfnre 11016	. . . 4 ⊢ +∞ ∉ ℝ
2	1	neli 3051	. . 3 ⊢ ¬ +∞ ∈ ℝ
3		eleq1 2826	. . 3 ⊢ (𝐴 = +∞ → (𝐴 ∈ ℝ ↔ +∞ ∈ ℝ))
4	2, 3	mtbiri 327	. 2 ⊢ (𝐴 = +∞ → ¬ 𝐴 ∈ ℝ)
5	4	necon2ai 2973	1 ⊢ (𝐴 ∈ ℝ → 𝐴 ≠ +∞)

Syntax hints:   → wi 4   = wceq 1539   ∈ wcel 2106   ≠ wne 2943  ℝcr 10870  +∞cpnf 11006

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 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2709  ax-sep 5223  ax-nul 5230  ax-pr 5352  ax-un 7588  ax-resscn 10928

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-tru 1542  df-fal 1552  df-ex 1783  df-sb 2068  df-clab 2716  df-cleq 2730  df-clel 2816  df-ne 2944  df-nel 3050  df-rab 3073  df-v 3434  df-dif 3890  df-un 3892  df-in 3894  df-ss 3904  df-nul 4257  df-pw 4535  df-sn 4562  df-pr 4564  df-uni 4840  df-pnf 11011

This theorem is referenced by:  renepnfd  11026  renfdisj  11035  xrnepnf  12854  rexneg  12945  rexadd  12966  xaddnepnf  12971  xaddcom  12974  xaddid1  12975  xnn0xadd0  12981  xnegdi  12982  xpncan  12985  xleadd1a  12987  rexmul  13005  xmulpnf1  13008  xadddilem  13028  rpsup  13586  hashneq0  14079  hash1snb  14134  xrsnsgrp  20634  xaddeq0  31076  icorempo  35522  ovoliunnfl  35819  voliunnfl  35821  volsupnfl  35822  supxrgelem  42876  supxrge  42877  infleinflem1  42909  infleinflem2  42910  xrre4  42951  supminfxr2  43009  climxrre  43291  sge0repnf  43924  voliunsge0lem  44010