Theorem renepnf 10678

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

Syntax hints:   → wi 4   = wceq 1538   ∈ wcel 2111   ≠ wne 2987  ℝcr 10525  +∞cpnf 10661

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-10 2142  ax-11 2158  ax-12 2175  ax-ext 2770  ax-sep 5167  ax-nul 5174  ax-pr 5295  ax-un 7441  ax-resscn 10583

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3an 1086  df-tru 1541  df-ex 1782  df-nf 1786  df-sb 2070  df-clab 2777  df-cleq 2791  df-clel 2870  df-nfc 2938  df-ne 2988  df-nel 3092  df-rab 3115  df-v 3443  df-dif 3884  df-un 3886  df-in 3888  df-ss 3898  df-nul 4244  df-pw 4499  df-sn 4526  df-pr 4528  df-uni 4801  df-pnf 10666

This theorem is referenced by:  renepnfd  10681  renfdisj  10690  xrnepnf  12501  rexneg  12592  rexadd  12613  xaddnepnf  12618  xaddcom  12621  xaddid1  12622  xnn0xadd0  12628  xnegdi  12629  xpncan  12632  xleadd1a  12634  rexmul  12652  xmulpnf1  12655  xadddilem  12675  rpsup  13229  hashneq0  13721  hash1snb  13776  xrsnsgrp  20127  xaddeq0  30503  icorempo  34768  ovoliunnfl  35099  voliunnfl  35101  volsupnfl  35102  supxrgelem  41969  supxrge  41970  infleinflem1  42002  infleinflem2  42003  xrre4  42048  supminfxr2  42108  climxrre  42392  sge0repnf  43025  voliunsge0lem  43111