Theorem renepnf 11163

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

Syntax hints:   → wi 4   = wceq 1540   ∈ wcel 2109   ≠ wne 2925  ℝcr 11008  +∞cpnf 11146

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 2701  ax-sep 5235  ax-pr 5371  ax-un 7671  ax-resscn 11066

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 2708  df-cleq 2721  df-clel 2803  df-ne 2926  df-nel 3030  df-rab 3395  df-v 3438  df-un 3908  df-in 3910  df-ss 3920  df-pw 4553  df-sn 4578  df-pr 4580  df-uni 4859  df-pnf 11151

This theorem is referenced by:  renepnfd  11166  renfdisj  11175  xrnepnf  13020  rexneg  13113  rexadd  13134  xaddnepnf  13139  xaddcom  13142  xaddrid  13143  xnn0xadd0  13149  xnegdi  13150  xpncan  13153  xleadd1a  13155  rexmul  13173  xmulpnf1  13176  xadddilem  13196  rpsup  13770  hashneq0  14271  hash1snb  14326  xrsnsgrp  21314  xaddeq0  32697  icorempo  37335  ovoliunnfl  37652  voliunnfl  37654  volsupnfl  37655  supxrgelem  45327  supxrge  45328  infleinflem1  45359  infleinflem2  45360  xrre4  45400  supminfxr2  45458  climxrre  45741  sge0repnf  46377  voliunsge0lem  46463