Theorem renepnf 11222

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 11215	. . . 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 11067  +∞cpnf 11205

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 5251  ax-pr 5387  ax-un 7711  ax-resscn 11125

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 3406  df-v 3449  df-un 3919  df-in 3921  df-ss 3931  df-pw 4565  df-sn 4590  df-pr 4592  df-uni 4872  df-pnf 11210

This theorem is referenced by:  renepnfd  11225  renfdisj  11234  xrnepnf  13078  rexneg  13171  rexadd  13192  xaddnepnf  13197  xaddcom  13200  xaddrid  13201  xnn0xadd0  13207  xnegdi  13208  xpncan  13211  xleadd1a  13213  rexmul  13231  xmulpnf1  13234  xadddilem  13254  rpsup  13828  hashneq0  14329  hash1snb  14384  xrsnsgrp  21319  xaddeq0  32676  icorempo  37339  ovoliunnfl  37656  voliunnfl  37658  volsupnfl  37659  supxrgelem  45333  supxrge  45334  infleinflem1  45366  infleinflem2  45367  xrre4  45407  supminfxr2  45465  climxrre  45748  sge0repnf  46384  voliunsge0lem  46470