Theorem renepnf 11306

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

Syntax hints:   → wi 4   = wceq 1536   ∈ wcel 2105   ≠ wne 2937  ℝcr 11151  +∞cpnf 11289

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-8 2107  ax-9 2115  ax-ext 2705  ax-sep 5301  ax-pr 5437  ax-un 7753  ax-resscn 11209

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1539  df-ex 1776  df-sb 2062  df-clab 2712  df-cleq 2726  df-clel 2813  df-ne 2938  df-nel 3044  df-rab 3433  df-v 3479  df-un 3967  df-in 3969  df-ss 3979  df-pw 4606  df-sn 4631  df-pr 4633  df-uni 4912  df-pnf 11294

This theorem is referenced by:  renepnfd  11309  renfdisj  11318  xrnepnf  13157  rexneg  13249  rexadd  13270  xaddnepnf  13275  xaddcom  13278  xaddrid  13279  xnn0xadd0  13285  xnegdi  13286  xpncan  13289  xleadd1a  13291  rexmul  13309  xmulpnf1  13312  xadddilem  13332  rpsup  13902  hashneq0  14399  hash1snb  14454  xrsnsgrp  21437  xaddeq0  32763  icorempo  37333  ovoliunnfl  37648  voliunnfl  37650  volsupnfl  37651  supxrgelem  45286  supxrge  45287  infleinflem1  45319  infleinflem2  45320  xrre4  45360  supminfxr2  45418  climxrre  45705  sge0repnf  46341  voliunsge0lem  46427