Theorem renepnf 11178

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

Syntax hints:   → wi 4   = wceq 1541   ∈ wcel 2113   ≠ wne 2930  ℝcr 11023  +∞cpnf 11161

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2706  ax-sep 5239  ax-pr 5375  ax-un 7678  ax-resscn 11081

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1544  df-ex 1781  df-sb 2068  df-clab 2713  df-cleq 2726  df-clel 2809  df-ne 2931  df-nel 3035  df-rab 3398  df-v 3440  df-un 3904  df-in 3906  df-ss 3916  df-pw 4554  df-sn 4579  df-pr 4581  df-uni 4862  df-pnf 11166

This theorem is referenced by:  renepnfd  11181  renfdisj  11190  xrnepnf  13030  rexneg  13124  rexadd  13145  xaddnepnf  13150  xaddcom  13153  xaddrid  13154  xnn0xadd0  13160  xnegdi  13161  xpncan  13164  xleadd1a  13166  rexmul  13184  xmulpnf1  13187  xadddilem  13207  rpsup  13784  hashneq0  14285  hash1snb  14340  xrsnsgrp  21360  xaddeq0  32782  icorempo  37495  ovoliunnfl  37802  voliunnfl  37804  volsupnfl  37805  supxrgelem  45524  supxrge  45525  infleinflem1  45556  infleinflem2  45557  xrre4  45597  supminfxr2  45655  climxrre  45936  sge0repnf  46572  voliunsge0lem  46658