Theorem renepnf 11193

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

Syntax hints:   → wi 4   = wceq 1542   ∈ wcel 2114   ≠ wne 2932  ℝcr 11037  +∞cpnf 11176

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 2708  ax-sep 5231  ax-pr 5375  ax-un 7689  ax-resscn 11095

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 2715  df-cleq 2728  df-clel 2811  df-ne 2933  df-nel 3037  df-rab 3390  df-v 3431  df-un 3894  df-in 3896  df-ss 3906  df-pw 4543  df-sn 4568  df-pr 4570  df-uni 4851  df-pnf 11181

This theorem is referenced by:  renepnfd  11196  renfdisj  11205  xrnepnf  13069  rexneg  13163  rexadd  13184  xaddnepnf  13189  xaddcom  13192  xaddrid  13193  xnn0xadd0  13199  xnegdi  13200  xpncan  13203  xleadd1a  13205  rexmul  13223  xmulpnf1  13226  xadddilem  13246  rpsup  13825  hashneq0  14326  hash1snb  14381  xrsnsgrp  21388  xaddeq0  32826  icorempo  37667  ovoliunnfl  37983  voliunnfl  37985  volsupnfl  37986  supxrgelem  45767  supxrge  45768  infleinflem1  45799  infleinflem2  45800  xrre4  45839  supminfxr2  45897  climxrre  46178  sge0repnf  46814  voliunsge0lem  46900