Theorem renepnf 9966

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 9960	. . . 4 ⊢ +∞ ∉ ℝ
2	1	neli 2885	. . 3 ⊢ ¬ +∞ ∈ ℝ
3		eleq1 2676	. . 3 ⊢ (𝐴 = +∞ → (𝐴 ∈ ℝ ↔ +∞ ∈ ℝ))
4	2, 3	mtbiri 316	. 2 ⊢ (𝐴 = +∞ → ¬ 𝐴 ∈ ℝ)
5	4	necon2ai 2811	1 ⊢ (𝐴 ∈ ℝ → 𝐴 ≠ +∞)

Syntax hints:   → wi 4   = wceq 1475   ∈ wcel 1977   ≠ wne 2780  ℝcr 9814  +∞cpnf 9950

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-8 1979  ax-9 1986  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590  ax-sep 4709  ax-nul 4717  ax-pow 4769  ax-pr 4833  ax-un 6847  ax-resscn 9872

This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-3an 1033  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-ne 2782  df-nel 2783  df-rex 2902  df-rab 2905  df-v 3175  df-dif 3543  df-un 3545  df-in 3547  df-ss 3554  df-nul 3875  df-pw 4110  df-sn 4126  df-pr 4128  df-uni 4373  df-pnf 9955

This theorem is referenced by:  renepnfd  9969  renfdisj  9977  xrnepnf  11828  rexneg  11916  rexadd  11937  xaddnepnf  11942  xaddcom  11945  xaddid1  11946  xnn0xadd0  11949  xnegdi  11950  xpncan  11953  xleadd1a  11955  rexmul  11973  xmulpnf1  11976  xadddilem  11996  rpsup  12527  hashneq0  13016  hash1snb  13068  xrsnsgrp  19601  xaddeq0  28907  icorempt2  32375  ovoliunnfl  32621  voliunnfl  32623  volsupnfl  32624  supxrgelem  38494  supxrge  38495  infleinflem1  38527  infleinflem2  38528  sge0repnf  39279  voliunsge0lem  39365