Theorem renepnf 11232

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 11225	. . . 4 ⊢ +∞ ∉ ℝ
2	1	neli 3065	. . 3 ⊢ ¬ +∞ ∈ ℝ
3		eleq1 2852	. . 3 ⊢ (𝐴 = +∞ → (𝐴 ∈ ℝ ↔ +∞ ∈ ℝ))
4	2, 3	mtbiri 329	. 2 ⊢ (𝐴 = +∞ → ¬ 𝐴 ∈ ℝ)
5	4	necon2ai 2988	1 ⊢ (𝐴 ∈ ℝ → 𝐴 ≠ +∞)

Syntax hints:   → wi 4   = wceq 1562   ∈ wcel 2144   ≠ wne 2959  ℝcr 11074  +∞cpnf 11215

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1817  ax-4 1831  ax-5 1932  ax-6 1989  ax-7 2030  ax-8 2146  ax-9 2154  ax-ext 2736  ax-sep 5248  ax-resscn 11132

This theorem depends on definitions:  df-bi 209  df-an 400  df-3an 1101  df-tru 1565  df-ex 1802  df-sb 2093  df-clab 2743  df-cleq 2756  df-clel 2839  df-ne 2960  df-nel 3064  df-rab 3417  df-v 3458  df-in 3913  df-ss 3923  df-pw 4559  df-uni 4868  df-pnf 11220

This theorem is referenced by:  renepnfd  11235  renfdisj  11244  xrnepnf  13122  rexneg  13216  rexadd  13237  xaddnepnf  13242  xaddcom  13245  xaddrid  13246  xnn0xadd0  13252  xnegdi  13253  xpncan  13256  xleadd1a  13258  rexmul  13276  xmulpnf1  13279  xadddilem  13299  rpsup  13878  hashneq0  14379  hash1snb  14434  xrsnsgrp  21462  xaddeq0  32957  icorempo  37850  ovoliunnfl  38166  voliunnfl  38168  volsupnfl  38169  supxrgelem  45918  supxrge  45919  infleinflem1  45950  infleinflem2  45951  xrre4  45990  supminfxr2  46048  climxrre  46329  sge0repnf  46965  voliunsge0lem  47051