Theorem renepnf 11262

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 11255	. . . 4 ⊢ +∞ ∉ ℝ
2	1	neli 3049	. . 3 ⊢ ¬ +∞ ∈ ℝ
3		eleq1 2822	. . 3 ⊢ (𝐴 = +∞ → (𝐴 ∈ ℝ ↔ +∞ ∈ ℝ))
4	2, 3	mtbiri 327	. 2 ⊢ (𝐴 = +∞ → ¬ 𝐴 ∈ ℝ)
5	4	necon2ai 2971	1 ⊢ (𝐴 ∈ ℝ → 𝐴 ≠ +∞)

Syntax hints:   → wi 4   = wceq 1542   ∈ wcel 2107   ≠ wne 2941  ℝcr 11109  +∞cpnf 11245

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 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2704  ax-sep 5300  ax-pr 5428  ax-un 7725  ax-resscn 11167

This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-tru 1545  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-ne 2942  df-nel 3048  df-rab 3434  df-v 3477  df-un 3954  df-in 3956  df-ss 3966  df-pw 4605  df-sn 4630  df-pr 4632  df-uni 4910  df-pnf 11250

This theorem is referenced by:  renepnfd  11265  renfdisj  11274  xrnepnf  13098  rexneg  13190  rexadd  13211  xaddnepnf  13216  xaddcom  13219  xaddrid  13220  xnn0xadd0  13226  xnegdi  13227  xpncan  13230  xleadd1a  13232  rexmul  13250  xmulpnf1  13253  xadddilem  13273  rpsup  13831  hashneq0  14324  hash1snb  14379  xrsnsgrp  20981  xaddeq0  31966  icorempo  36232  ovoliunnfl  36530  voliunnfl  36532  volsupnfl  36533  supxrgelem  44047  supxrge  44048  infleinflem1  44080  infleinflem2  44081  xrre4  44121  supminfxr2  44179  climxrre  44466  sge0repnf  45102  voliunsge0lem  45188