Theorem renepnf 11266

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

Syntax hints:   → wi 4   = wceq 1539   ∈ wcel 2104   ≠ wne 2938  ℝcr 11111  +∞cpnf 11249

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 1911  ax-6 1969  ax-7 2009  ax-8 2106  ax-9 2114  ax-ext 2701  ax-sep 5298  ax-pr 5426  ax-un 7727  ax-resscn 11169

This theorem depends on definitions:  df-bi 206  df-an 395  df-or 844  df-tru 1542  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2722  df-clel 2808  df-ne 2939  df-nel 3045  df-rab 3431  df-v 3474  df-un 3952  df-in 3954  df-ss 3964  df-pw 4603  df-sn 4628  df-pr 4630  df-uni 4908  df-pnf 11254

This theorem is referenced by:  renepnfd  11269  renfdisj  11278  xrnepnf  13102  rexneg  13194  rexadd  13215  xaddnepnf  13220  xaddcom  13223  xaddrid  13224  xnn0xadd0  13230  xnegdi  13231  xpncan  13234  xleadd1a  13236  rexmul  13254  xmulpnf1  13257  xadddilem  13277  rpsup  13835  hashneq0  14328  hash1snb  14383  xrsnsgrp  21181  xaddeq0  32233  icorempo  36535  ovoliunnfl  36833  voliunnfl  36835  volsupnfl  36836  supxrgelem  44345  supxrge  44346  infleinflem1  44378  infleinflem2  44379  xrre4  44419  supminfxr2  44477  climxrre  44764  sge0repnf  45400  voliunsge0lem  45486