Theorem renepnf 10691

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 10684	. . . 4 ⊢ +∞ ∉ ℝ
2	1	neli 3127	. . 3 ⊢ ¬ +∞ ∈ ℝ
3		eleq1 2902	. . 3 ⊢ (𝐴 = +∞ → (𝐴 ∈ ℝ ↔ +∞ ∈ ℝ))
4	2, 3	mtbiri 329	. 2 ⊢ (𝐴 = +∞ → ¬ 𝐴 ∈ ℝ)
5	4	necon2ai 3047	1 ⊢ (𝐴 ∈ ℝ → 𝐴 ≠ +∞)

Syntax hints:   → wi 4   = wceq 1537   ∈ wcel 2114   ≠ wne 3018  ℝcr 10538  +∞cpnf 10674

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2795  ax-sep 5205  ax-nul 5212  ax-pr 5332  ax-un 7463  ax-resscn 10596

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3an 1085  df-tru 1540  df-ex 1781  df-nf 1785  df-sb 2070  df-clab 2802  df-cleq 2816  df-clel 2895  df-nfc 2965  df-ne 3019  df-nel 3126  df-rab 3149  df-v 3498  df-dif 3941  df-un 3943  df-in 3945  df-ss 3954  df-nul 4294  df-pw 4543  df-sn 4570  df-pr 4572  df-uni 4841  df-pnf 10679

This theorem is referenced by:  renepnfd  10694  renfdisj  10703  xrnepnf  12516  rexneg  12607  rexadd  12628  xaddnepnf  12633  xaddcom  12636  xaddid1  12637  xnn0xadd0  12643  xnegdi  12644  xpncan  12647  xleadd1a  12649  rexmul  12667  xmulpnf1  12670  xadddilem  12690  rpsup  13237  hashneq0  13728  hash1snb  13783  xrsnsgrp  20583  xaddeq0  30479  icorempo  34634  ovoliunnfl  34936  voliunnfl  34938  volsupnfl  34939  supxrgelem  41612  supxrge  41613  infleinflem1  41645  infleinflem2  41646  xrre4  41692  supminfxr2  41752  climxrre  42038  sge0repnf  42675  voliunsge0lem  42761