Theorem renepnf 11198

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 11191	. . . 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 11043  +∞cpnf 11181

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 5246  ax-pr 5382  ax-un 7691  ax-resscn 11101

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 3403  df-v 3446  df-un 3916  df-in 3918  df-ss 3928  df-pw 4561  df-sn 4586  df-pr 4588  df-uni 4868  df-pnf 11186

This theorem is referenced by:  renepnfd  11201  renfdisj  11210  xrnepnf  13054  rexneg  13147  rexadd  13168  xaddnepnf  13173  xaddcom  13176  xaddrid  13177  xnn0xadd0  13183  xnegdi  13184  xpncan  13187  xleadd1a  13189  rexmul  13207  xmulpnf1  13210  xadddilem  13230  rpsup  13804  hashneq0  14305  hash1snb  14360  xrsnsgrp  21349  xaddeq0  32726  icorempo  37332  ovoliunnfl  37649  voliunnfl  37651  volsupnfl  37652  supxrgelem  45326  supxrge  45327  infleinflem1  45359  infleinflem2  45360  xrre4  45400  supminfxr2  45458  climxrre  45741  sge0repnf  46377  voliunsge0lem  46463