Theorem renepnf 11229

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

Syntax hints:   → wi 4   = wceq 1540   ∈ wcel 2109   ≠ wne 2926  ℝcr 11074  +∞cpnf 11212

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2702  ax-sep 5254  ax-pr 5390  ax-un 7714  ax-resscn 11132

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2709  df-cleq 2722  df-clel 2804  df-ne 2927  df-nel 3031  df-rab 3409  df-v 3452  df-un 3922  df-in 3924  df-ss 3934  df-pw 4568  df-sn 4593  df-pr 4595  df-uni 4875  df-pnf 11217

This theorem is referenced by:  renepnfd  11232  renfdisj  11241  xrnepnf  13085  rexneg  13178  rexadd  13199  xaddnepnf  13204  xaddcom  13207  xaddrid  13208  xnn0xadd0  13214  xnegdi  13215  xpncan  13218  xleadd1a  13220  rexmul  13238  xmulpnf1  13241  xadddilem  13261  rpsup  13835  hashneq0  14336  hash1snb  14391  xrsnsgrp  21326  xaddeq0  32683  icorempo  37346  ovoliunnfl  37663  voliunnfl  37665  volsupnfl  37666  supxrgelem  45340  supxrge  45341  infleinflem1  45373  infleinflem2  45374  xrre4  45414  supminfxr2  45472  climxrre  45755  sge0repnf  46391  voliunsge0lem  46477