Theorem renepnf 10769

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

Syntax hints:   → wi 4   = wceq 1542   ∈ wcel 2114   ≠ wne 2934  ℝcr 10616  +∞cpnf 10752

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1975  ax-7 2020  ax-8 2116  ax-9 2124  ax-ext 2710  ax-sep 5167  ax-nul 5174  ax-pr 5296  ax-un 7481  ax-resscn 10674

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 847  df-tru 1545  df-fal 1555  df-ex 1787  df-sb 2075  df-clab 2717  df-cleq 2730  df-clel 2811  df-ne 2935  df-nel 3039  df-rab 3062  df-v 3400  df-dif 3846  df-un 3848  df-in 3850  df-ss 3860  df-nul 4212  df-pw 4490  df-sn 4517  df-pr 4519  df-uni 4797  df-pnf 10757

This theorem is referenced by:  renepnfd  10772  renfdisj  10781  xrnepnf  12598  rexneg  12689  rexadd  12710  xaddnepnf  12715  xaddcom  12718  xaddid1  12719  xnn0xadd0  12725  xnegdi  12726  xpncan  12729  xleadd1a  12731  rexmul  12749  xmulpnf1  12752  xadddilem  12772  rpsup  13327  hashneq0  13819  hash1snb  13874  xrsnsgrp  20255  xaddeq0  30653  icorempo  35167  ovoliunnfl  35464  voliunnfl  35466  volsupnfl  35467  supxrgelem  42436  supxrge  42437  infleinflem1  42469  infleinflem2  42470  xrre4  42511  supminfxr2  42571  climxrre  42855  sge0repnf  43488  voliunsge0lem  43574