Theorem renepnf 11194

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

Syntax hints:   → wi 4   = wceq 1542   ∈ wcel 2114   ≠ wne 2933  ℝcr 11039  +∞cpnf 11177

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709  ax-sep 5245  ax-pr 5381  ax-un 7692  ax-resscn 11097

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-ne 2934  df-nel 3038  df-rab 3402  df-v 3444  df-un 3908  df-in 3910  df-ss 3920  df-pw 4558  df-sn 4583  df-pr 4585  df-uni 4866  df-pnf 11182

This theorem is referenced by:  renepnfd  11197  renfdisj  11206  xrnepnf  13046  rexneg  13140  rexadd  13161  xaddnepnf  13166  xaddcom  13169  xaddrid  13170  xnn0xadd0  13176  xnegdi  13177  xpncan  13180  xleadd1a  13182  rexmul  13200  xmulpnf1  13203  xadddilem  13223  rpsup  13800  hashneq0  14301  hash1snb  14356  xrsnsgrp  21379  xaddeq0  32850  icorempo  37633  ovoliunnfl  37942  voliunnfl  37944  volsupnfl  37945  supxrgelem  45725  supxrge  45726  infleinflem1  45757  infleinflem2  45758  xrre4  45798  supminfxr2  45856  climxrre  46137  sge0repnf  46773  voliunsge0lem  46859