Theorem renepnf 11314

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 11307	. . . 4 ⊢ +∞ ∉ ℝ
2	1	neli 3063	. . 3 ⊢ ¬ +∞ ∈ ℝ
3		eleq1 2848	. . 3 ⊢ (𝐴 = +∞ → (𝐴 ∈ ℝ ↔ +∞ ∈ ℝ))
4	2, 3	mtbiri 330	. 2 ⊢ (𝐴 = +∞ → ¬ 𝐴 ∈ ℝ)
5	4	necon2ai 2984	1 ⊢ (𝐴 ∈ ℝ → 𝐴 ≠ +∞)

This proof depends on syntax axioms:   → wi 4   = wceq 1570   ∈ wcel 2145   ≠ wne 2955  ℝcr 11156  +∞cpnf 11297

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2732  ax-sep 5249  ax-resscn 11214

This proof depends on definitions:  df-bi 210  df-an 402  df-3an 1105  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2739  df-cleq 2752  df-clel 2835  df-ne 2956  df-nel 3062  df-rab 3413  df-v 3452  df-in 3906  df-ss 3916  df-pw 4559  df-uni 4868  df-pnf 11302

This theorem is used by:  renepnfd  11317  renfdisj  11326  xrnepnf  13202  rexneg  13296  rexadd  13317  xaddnepnf  13322  xaddcom  13325  xaddrid  13326  xnn0xadd0  13332  xnegdi  13333  xpncan  13336  xleadd1a  13338  rexmul  13356  xmulpnf1  13359  xadddilem  13379  rpsup  13960  hashneq0  14461  hash1snb  14517  xrsnsgrp  21661  xaddeq0  33264  icorempo  38188  ovoliunnfl  38494  voliunnfl  38496  volsupnfl  38497  supxrgelem  46265  supxrge  46266  infleinflem1  46297  infleinflem2  46298  xrre4  46337  supminfxr2  46395  climxrre  46676  sge0repnf  47312  voliunsge0lem  47398