Theorem renepnf 11160

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

Syntax hints:   → wi 4   = wceq 1541   ∈ wcel 2111   ≠ wne 2928  ℝcr 11005  +∞cpnf 11143

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2113  ax-9 2121  ax-ext 2703  ax-sep 5232  ax-pr 5368  ax-un 7668  ax-resscn 11063

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1544  df-ex 1781  df-sb 2068  df-clab 2710  df-cleq 2723  df-clel 2806  df-ne 2929  df-nel 3033  df-rab 3396  df-v 3438  df-un 3902  df-in 3904  df-ss 3914  df-pw 4549  df-sn 4574  df-pr 4576  df-uni 4857  df-pnf 11148

This theorem is referenced by:  renepnfd  11163  renfdisj  11172  xrnepnf  13017  rexneg  13110  rexadd  13131  xaddnepnf  13136  xaddcom  13139  xaddrid  13140  xnn0xadd0  13146  xnegdi  13147  xpncan  13150  xleadd1a  13152  rexmul  13170  xmulpnf1  13173  xadddilem  13193  rpsup  13770  hashneq0  14271  hash1snb  14326  xrsnsgrp  21344  xaddeq0  32736  icorempo  37395  ovoliunnfl  37701  voliunnfl  37703  volsupnfl  37704  supxrgelem  45435  supxrge  45436  infleinflem1  45467  infleinflem2  45468  xrre4  45508  supminfxr2  45566  climxrre  45847  sge0repnf  46483  voliunsge0lem  46569