Theorem renepnf 11357

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

This proof depends on syntax axioms:   → wi 4   = wceq 1569   ∈ wcel 2144   ≠ wne 2955  ℝcr 11199  +∞cpnf 11340

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-ext 2732  ax-sep 5248  ax-resscn 11257

This proof depends on definitions:  df-bi 210  df-an 402  df-3an 1105  df-tru 1572  df-ex 1812  df-sb 2099  df-clab 2739  df-cleq 2752  df-clel 2835  df-ne 2956  df-nel 3062  df-rab 3413  df-v 3452  df-ss 3896  df-in 4091  df-pw 4558  df-uni 4867  df-pnf 11345

This theorem is used by:  renepnfd  11360  renfdisj  11369  xrnepnf  13247  rexneg  13341  rexadd  13362  xaddnepnf  13367  xaddcom  13370  xaddrid  13371  xnn0xadd0  13377  xnegdi  13378  xpncan  13381  xleadd1a  13383  rexmul  13401  xmulpnf1  13404  xadddilem  13424  rpsup  14006  hashneq0  14508  hash1snb  14564  xrsnsgrp  21714  xaddeq0  33345  icorempo  38275  ovoliunnfl  38581  voliunnfl  38583  volsupnfl  38584  supxrgelem  46349  supxrge  46350  infleinflem1  46381  infleinflem2  46382  xrre4  46421  supminfxr2  46479  climxrre  46760  sge0repnf  47396  voliunsge0lem  47482