Theorem renepnf 11284

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

This proof depends on syntax axioms:   → wi 4   = wceq 1570   ∈ wcel 2145   ≠ wne 2957  ℝcr 11126  +∞cpnf 11267

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2734  ax-sep 5255  ax-resscn 11184

This proof depends on definitions:  df-bi 210  df-an 402  df-3an 1105  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2741  df-cleq 2754  df-clel 2837  df-ne 2958  df-nel 3064  df-rab 3415  df-v 3455  df-in 3909  df-ss 3919  df-pw 4562  df-uni 4871  df-pnf 11272

This theorem is used by:  renepnfd  11287  renfdisj  11296  xrnepnf  13171  rexneg  13265  rexadd  13286  xaddnepnf  13291  xaddcom  13294  xaddrid  13295  xnn0xadd0  13301  xnegdi  13302  xpncan  13305  xleadd1a  13307  rexmul  13325  xmulpnf1  13328  xadddilem  13348  rpsup  13929  hashneq0  14430  hash1snb  14486  xrsnsgrp  21622  xaddeq0  33211  icorempo  38092  ovoliunnfl  38398  voliunnfl  38400  volsupnfl  38401  supxrgelem  46154  supxrge  46155  infleinflem1  46186  infleinflem2  46187  xrre4  46226  supminfxr2  46284  climxrre  46565  sge0repnf  47201  voliunsge0lem  47287