Theorem renepnf 11294

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 11287	. . . 4 ⊢ +∞ ∉ ℝ
2	1	neli 3037	. . 3 ⊢ ¬ +∞ ∈ ℝ
3		eleq1 2813	. . 3 ⊢ (𝐴 = +∞ → (𝐴 ∈ ℝ ↔ +∞ ∈ ℝ))
4	2, 3	mtbiri 326	. 2 ⊢ (𝐴 = +∞ → ¬ 𝐴 ∈ ℝ)
5	4	necon2ai 2959	1 ⊢ (𝐴 ∈ ℝ → 𝐴 ≠ +∞)

Syntax hints:   → wi 4   = wceq 1533   ∈ wcel 2098   ≠ wne 2929  ℝcr 11139  +∞cpnf 11277

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-ext 2696  ax-sep 5300  ax-pr 5429  ax-un 7741  ax-resscn 11197

This theorem depends on definitions:  df-bi 206  df-an 395  df-or 846  df-3an 1086  df-tru 1536  df-ex 1774  df-sb 2060  df-clab 2703  df-cleq 2717  df-clel 2802  df-ne 2930  df-nel 3036  df-rab 3419  df-v 3463  df-un 3949  df-in 3951  df-ss 3961  df-pw 4606  df-sn 4631  df-pr 4633  df-uni 4910  df-pnf 11282

This theorem is referenced by:  renepnfd  11297  renfdisj  11306  xrnepnf  13133  rexneg  13225  rexadd  13246  xaddnepnf  13251  xaddcom  13254  xaddrid  13255  xnn0xadd0  13261  xnegdi  13262  xpncan  13265  xleadd1a  13267  rexmul  13285  xmulpnf1  13288  xadddilem  13308  rpsup  13867  hashneq0  14359  hash1snb  14414  xrsnsgrp  21352  xaddeq0  32605  icorempo  36961  ovoliunnfl  37266  voliunnfl  37268  volsupnfl  37269  supxrgelem  44857  supxrge  44858  infleinflem1  44890  infleinflem2  44891  xrre4  44931  supminfxr2  44989  climxrre  45276  sge0repnf  45912  voliunsge0lem  45998