Theorem renepnf 11184

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 11177	. . . 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 11029  +∞cpnf 11167

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 5242  ax-pr 5378  ax-un 7682  ax-resscn 11087

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 3401  df-v 3443  df-un 3907  df-in 3909  df-ss 3919  df-pw 4557  df-sn 4582  df-pr 4584  df-uni 4865  df-pnf 11172

This theorem is referenced by:  renepnfd  11187  renfdisj  11196  xrnepnf  13036  rexneg  13130  rexadd  13151  xaddnepnf  13156  xaddcom  13159  xaddrid  13160  xnn0xadd0  13166  xnegdi  13167  xpncan  13170  xleadd1a  13172  rexmul  13190  xmulpnf1  13193  xadddilem  13213  rpsup  13790  hashneq0  14291  hash1snb  14346  xrsnsgrp  21366  xaddeq0  32835  icorempo  37558  ovoliunnfl  37865  voliunnfl  37867  volsupnfl  37868  supxrgelem  45649  supxrge  45650  infleinflem1  45681  infleinflem2  45682  xrre4  45722  supminfxr2  45780  climxrre  46061  sge0repnf  46697  voliunsge0lem  46783