Theorem renepnf 11188

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 11181	. . . 4 ⊢ +∞ ∉ ℝ
2	1	neli 3042	. . 3 ⊢ ¬ +∞ ∈ ℝ
3		eleq1 2829	. . 3 ⊢ (𝐴 = +∞ → (𝐴 ∈ ℝ ↔ +∞ ∈ ℝ))
4	2, 3	mtbiri 329	. 2 ⊢ (𝐴 = +∞ → ¬ 𝐴 ∈ ℝ)
5	4	necon2ai 2965	1 ⊢ (𝐴 ∈ ℝ → 𝐴 ≠ +∞)

Syntax hints:   → wi 4   = wceq 1548   ∈ wcel 2121   ≠ wne 2936  ℝcr 11032  +∞cpnf 11171

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1975  ax-7 2016  ax-8 2123  ax-9 2131  ax-ext 2713  ax-sep 5221  ax-pr 5365  ax-un 7682  ax-resscn 11090

This theorem depends on definitions:  df-bi 209  df-an 398  df-or 855  df-3an 1095  df-tru 1551  df-ex 1788  df-sb 2075  df-clab 2720  df-cleq 2733  df-clel 2816  df-ne 2937  df-nel 3041  df-rab 3394  df-v 3435  df-un 3890  df-in 3892  df-ss 3902  df-pw 4534  df-sn 4559  df-pr 4561  df-uni 4842  df-pnf 11176

This theorem is referenced by:  renepnfd  11191  renfdisj  11200  xrnepnf  13064  rexneg  13158  rexadd  13179  xaddnepnf  13184  xaddcom  13187  xaddrid  13188  xnn0xadd0  13194  xnegdi  13195  xpncan  13198  xleadd1a  13200  rexmul  13218  xmulpnf1  13221  xadddilem  13241  rpsup  13820  hashneq0  14321  hash1snb  14376  xrsnsgrp  21387  xaddeq0  32849  icorempo  37728  ovoliunnfl  38044  voliunnfl  38046  volsupnfl  38047  supxrgelem  45796  supxrge  45797  infleinflem1  45828  infleinflem2  45829  xrre4  45868  supminfxr2  45926  climxrre  46207  sge0repnf  46843  voliunsge0lem  46929