Theorem renepnf 11338

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

Syntax hints:   → wi 4   = wceq 1537   ∈ wcel 2108   ≠ wne 2946  ℝcr 11183  +∞cpnf 11321

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2711  ax-sep 5317  ax-pr 5447  ax-un 7770  ax-resscn 11241

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 847  df-3an 1089  df-tru 1540  df-ex 1778  df-sb 2065  df-clab 2718  df-cleq 2732  df-clel 2819  df-ne 2947  df-nel 3053  df-rab 3444  df-v 3490  df-un 3981  df-in 3983  df-ss 3993  df-pw 4624  df-sn 4649  df-pr 4651  df-uni 4932  df-pnf 11326

This theorem is referenced by:  renepnfd  11341  renfdisj  11350  xrnepnf  13181  rexneg  13273  rexadd  13294  xaddnepnf  13299  xaddcom  13302  xaddrid  13303  xnn0xadd0  13309  xnegdi  13310  xpncan  13313  xleadd1a  13315  rexmul  13333  xmulpnf1  13336  xadddilem  13356  rpsup  13917  hashneq0  14413  hash1snb  14468  xrsnsgrp  21443  xaddeq0  32760  icorempo  37317  ovoliunnfl  37622  voliunnfl  37624  volsupnfl  37625  supxrgelem  45252  supxrge  45253  infleinflem1  45285  infleinflem2  45286  xrre4  45326  supminfxr2  45384  climxrre  45671  sge0repnf  46307  voliunsge0lem  46393