Theorem renepnf 11281

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

Syntax hints:   → wi 4   = wceq 1540   ∈ wcel 2108   ≠ wne 2932  ℝcr 11126  +∞cpnf 11264

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2707  ax-sep 5266  ax-pr 5402  ax-un 7727  ax-resscn 11184

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-ex 1780  df-sb 2065  df-clab 2714  df-cleq 2727  df-clel 2809  df-ne 2933  df-nel 3037  df-rab 3416  df-v 3461  df-un 3931  df-in 3933  df-ss 3943  df-pw 4577  df-sn 4602  df-pr 4604  df-uni 4884  df-pnf 11269

This theorem is referenced by:  renepnfd  11284  renfdisj  11293  xrnepnf  13132  rexneg  13225  rexadd  13246  xaddnepnf  13251  xaddcom  13254  xaddrid  13255  xnn0xadd0  13261  xnegdi  13262  xpncan  13265  xleadd1a  13267  rexmul  13285  xmulpnf1  13288  xadddilem  13308  rpsup  13881  hashneq0  14380  hash1snb  14435  xrsnsgrp  21368  xaddeq0  32676  icorempo  37315  ovoliunnfl  37632  voliunnfl  37634  volsupnfl  37635  supxrgelem  45312  supxrge  45313  infleinflem1  45345  infleinflem2  45346  xrre4  45386  supminfxr2  45444  climxrre  45727  sge0repnf  46363  voliunsge0lem  46449