Theorem renepnf 10954

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 10947	. . . 4 ⊢ +∞ ∉ ℝ
2	1	neli 3050	. . 3 ⊢ ¬ +∞ ∈ ℝ
3		eleq1 2826	. . 3 ⊢ (𝐴 = +∞ → (𝐴 ∈ ℝ ↔ +∞ ∈ ℝ))
4	2, 3	mtbiri 326	. 2 ⊢ (𝐴 = +∞ → ¬ 𝐴 ∈ ℝ)
5	4	necon2ai 2972	1 ⊢ (𝐴 ∈ ℝ → 𝐴 ≠ +∞)

Syntax hints:   → wi 4   = wceq 1539   ∈ wcel 2108   ≠ wne 2942  ℝcr 10801  +∞cpnf 10937

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-ext 2709  ax-sep 5218  ax-nul 5225  ax-pr 5347  ax-un 7566  ax-resscn 10859

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 844  df-tru 1542  df-fal 1552  df-ex 1784  df-sb 2069  df-clab 2716  df-cleq 2730  df-clel 2817  df-ne 2943  df-nel 3049  df-rab 3072  df-v 3424  df-dif 3886  df-un 3888  df-in 3890  df-ss 3900  df-nul 4254  df-pw 4532  df-sn 4559  df-pr 4561  df-uni 4837  df-pnf 10942

This theorem is referenced by:  renepnfd  10957  renfdisj  10966  xrnepnf  12783  rexneg  12874  rexadd  12895  xaddnepnf  12900  xaddcom  12903  xaddid1  12904  xnn0xadd0  12910  xnegdi  12911  xpncan  12914  xleadd1a  12916  rexmul  12934  xmulpnf1  12937  xadddilem  12957  rpsup  13514  hashneq0  14007  hash1snb  14062  xrsnsgrp  20546  xaddeq0  30978  icorempo  35449  ovoliunnfl  35746  voliunnfl  35748  volsupnfl  35749  supxrgelem  42766  supxrge  42767  infleinflem1  42799  infleinflem2  42800  xrre4  42841  supminfxr2  42899  climxrre  43181  sge0repnf  43814  voliunsge0lem  43900