Theorem renepnf 11216

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

Syntax hints:   → wi 4   = wceq 1550   ∈ wcel 2132   ≠ wne 2947  ℝcr 11058  +∞cpnf 11199

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1805  ax-4 1819  ax-5 1920  ax-6 1977  ax-7 2018  ax-8 2134  ax-9 2142  ax-ext 2724  ax-sep 5236  ax-resscn 11116

This theorem depends on definitions:  df-bi 209  df-an 399  df-3an 1097  df-tru 1553  df-ex 1790  df-sb 2081  df-clab 2731  df-cleq 2744  df-clel 2827  df-ne 2948  df-nel 3052  df-rab 3405  df-v 3446  df-in 3902  df-ss 3912  df-pw 4547  df-uni 4856  df-pnf 11204

This theorem is referenced by:  renepnfd  11219  renfdisj  11228  xrnepnf  13106  rexneg  13200  rexadd  13221  xaddnepnf  13226  xaddcom  13229  xaddrid  13230  xnn0xadd0  13236  xnegdi  13237  xpncan  13240  xleadd1a  13242  rexmul  13260  xmulpnf1  13263  xadddilem  13283  rpsup  13862  hashneq0  14363  hash1snb  14418  xrsnsgrp  21429  xaddeq0  32894  icorempo  37783  ovoliunnfl  38099  voliunnfl  38101  volsupnfl  38102  supxrgelem  45851  supxrge  45852  infleinflem1  45883  infleinflem2  45884  xrre4  45923  supminfxr2  45981  climxrre  46262  sge0repnf  46898  voliunsge0lem  46984