Theorem renepnf 9662

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 9656	. . . 4
2	1	neli 2792	. . 3
3		eleq1 2529	. . 3
4	2, 3	mtbiri 303	. 2
5	4	necon2ai 2692	1

Syntax hints:  ->wi 4  =wceq 1395  e.wcel 1818  =/=wne 2652  cr 9512  cpnf 9646

This theorem is referenced by:  renepnfd  9665  renfdisj  9668  xrnepnf  11358  rexneg  11439  rexadd  11460  xaddnepnf  11463  xaddcom  11466  xaddid1  11467  xnegdi  11469  xpncan  11472  xleadd1a  11474  rexmul  11492  xmulpnf1  11495  xadddilem  11515  rpsup  11993  hashneq0  12434  hash1snb  12479  xrsnsgrp  18454  xaddeq0  27573  ovoliunnfl  30056  voliunnfl  30058  volsupnfl  30059

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1618  ax-4 1631  ax-5 1704  ax-6 1747  ax-7 1790  ax-8 1820  ax-9 1822  ax-10 1837  ax-11 1842  ax-12 1854  ax-13 1999  ax-ext 2435  ax-sep 4573  ax-nul 4581  ax-pow 4630  ax-pr 4691  ax-un 6592  ax-resscn 9570

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 975  df-tru 1398  df-ex 1613  df-nf 1617  df-sb 1740  df-clab 2443  df-cleq 2449  df-clel 2452  df-nfc 2607  df-ne 2654  df-nel 2655  df-rex 2813  df-rab 2816  df-v 3111  df-dif 3478  df-un 3480  df-in 3482  df-ss 3489  df-nul 3785  df-pw 4014  df-sn 4030  df-pr 4032  df-uni 4250  df-pnf 9651