Theorem renepnf 11260

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 11253	. . . 4 ⊢ +∞ ∉ ℝ
2	1	neli 3073	. . 3 ⊢ ¬ +∞ ∈ ℝ
3		eleq1 2858	. . 3 ⊢ (𝐴 = +∞ → (𝐴 ∈ ℝ ↔ +∞ ∈ ℝ))
4	2, 3	mtbiri 330	. 2 ⊢ (𝐴 = +∞ → ¬ 𝐴 ∈ ℝ)
5	4	necon2ai 2994	1 ⊢ (𝐴 ∈ ℝ → 𝐴 ≠ +∞)

Syntax hints:   → wi 4   = wceq 1568   ∈ wcel 2150   ≠ wne 2965  ℝcr 11102  +∞cpnf 11243

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1823  ax-4 1837  ax-5 1938  ax-6 1995  ax-7 2036  ax-8 2152  ax-9 2160  ax-ext 2742  ax-sep 5262  ax-resscn 11160

This theorem depends on definitions:  df-bi 210  df-an 401  df-3an 1103  df-tru 1571  df-ex 1808  df-sb 2099  df-clab 2749  df-cleq 2762  df-clel 2845  df-ne 2966  df-nel 3072  df-rab 3424  df-v 3464  df-in 3920  df-ss 3930  df-pw 4569  df-uni 4878  df-pnf 11248

This theorem is referenced by:  renepnfd  11263  renfdisj  11272  xrnepnf  13146  rexneg  13240  rexadd  13261  xaddnepnf  13266  xaddcom  13269  xaddrid  13270  xnn0xadd0  13276  xnegdi  13277  xpncan  13280  xleadd1a  13282  rexmul  13300  xmulpnf1  13303  xadddilem  13323  rpsup  13902  hashneq0  14403  hash1snb  14459  xrsnsgrp  21541  xaddeq0  33068  icorempo  37945  ovoliunnfl  38261  voliunnfl  38263  volsupnfl  38264  supxrgelem  46005  supxrge  46006  infleinflem1  46037  infleinflem2  46038  xrre4  46077  supminfxr2  46135  climxrre  46416  sge0repnf  47052  voliunsge0lem  47138