MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  zre Structured version   Visualization version   Unicode version

Theorem zre 10975
Description: An integer is a real. (Contributed by NM, 8-Jan-2002.)
Assertion
Ref Expression
zre  |-  ( N  e.  ZZ  ->  N  e.  RR )

Proof of Theorem zre
StepHypRef Expression
1 elz 10973 . 2  |-  ( N  e.  ZZ  <->  ( N  e.  RR  /\  ( N  =  0  \/  N  e.  NN  \/  -u N  e.  NN ) ) )
21simplbi 466 1  |-  ( N  e.  ZZ  ->  N  e.  RR )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    \/ w3o 990    = wceq 1455    e. wcel 1898   RRcr 9569   0cc0 9570   -ucneg 9892   NNcn 10642   ZZcz 10971
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1680  ax-4 1693  ax-5 1769  ax-6 1816  ax-7 1862  ax-10 1926  ax-11 1931  ax-12 1944  ax-13 2102  ax-ext 2442
This theorem depends on definitions:  df-bi 190  df-or 376  df-an 377  df-3or 992  df-3an 993  df-tru 1458  df-ex 1675  df-nf 1679  df-sb 1809  df-clab 2449  df-cleq 2455  df-clel 2458  df-nfc 2592  df-rex 2755  df-rab 2758  df-v 3059  df-dif 3419  df-un 3421  df-in 3423  df-ss 3430  df-nul 3744  df-if 3894  df-sn 3981  df-pr 3983  df-op 3987  df-uni 4213  df-br 4419  df-iota 5569  df-fv 5613  df-ov 6323  df-neg 9894  df-z 10972
This theorem is referenced by:  zcn  10976  zrei  10977  zssre  10978  elnn0z  10984  elnnz1  10997  znnnlt1  10998  zletr  11015  znnsub  11017  znn0sub  11018  zltp1le  11020  zleltp1  11021  nn0ge0div  11039  zextle  11043  btwnnz  11046  suprzcl  11049  msqznn  11051  peano2uz2  11057  uzind  11061  fzind  11067  fnn0ind  11068  eluzuzle  11201  uzid  11207  uzneg  11211  uztric  11214  uz11  11215  eluzp1m1  11216  eluzp1p1  11218  eluzaddi  11219  eluzsubi  11220  uzin  11225  uz3m2nn  11235  peano2uz  11246  nn0pzuz  11250  uzwo  11256  eluz2b2  11265  uz2mulcl  11270  uzinfi  11272  eqreznegel  11283  lbzbi  11286  uzsupss  11290  nn01to3  11291  zmin  11294  zmax  11295  zbtwnre  11296  rebtwnz  11297  qre  11303  rpnnen1lem1  11324  rpnnen1lem2  11325  rpnnen1lem3  11326  rpnnen1lem5  11328  z2ge  11525  qbtwnre  11526  elfz1eq  11845  fzn  11850  fzen  11851  uzsubsubfz  11856  fzaddel  11868  fzsuc2  11888  fzrev  11893  elfz1b  11899  fznuz  11911  uznfz  11912  fzp1nel  11913  elfz0fzfz0  11931  fz0fzelfz0  11932  fznn0sub2  11933  fz0fzdiffz0  11935  elfzmlbmOLD  11937  elfzmlbp  11938  difelfznle  11941  nelfzo  11962  elfzouz2  11971  fzo0n  11977  fzonlt0  11978  fzossrbm1  11984  fzospliti  11987  fzo1fzo0n0  11994  elfzo0z  11995  fzofzim  11999  eluzgtdifelfzo  12013  fzossfzop1  12028  ssfzoulel  12042  ssfzo12bi  12043  elfzonelfzo  12048  elfzomelpfzo  12050  elfznelfzob  12052  fzosplitprm1  12055  fzostep1  12058  fllt  12080  flid  12082  flbi2  12090  flhalf  12100  dfceil2  12106  ceile  12114  ceilid  12116  quoremz  12120  intfracq  12124  uzsup  12128  mulmod0  12142  zmod10  12151  zmodcl  12154  zmodfz  12156  modidmul0OLD  12161  zmodid2  12163  modcyc  12170  modmul1  12181  modaddmodup  12191  modaddmodlo  12192  modaddmulmod  12194  leexp2  12365  zsqcl2  12390  iexpcyc  12417  fi1uzind  12689  ccatsymb  12769  lswccatn0lsw  12776  swrdnd  12831  swrd0  12833  swrdswrdlem  12858  swrdswrd  12859  swrdccatin2  12886  swrdccatin12lem2  12888  swrdccatin12lem3  12889  repswswrd  12930  cshwmodn  12940  cshwsublen  12941  cshwidxmod  12948  cshwidxm1  12951  repswcshw  12954  2cshw  12955  cshweqrep  12963  cshw1  12964  swrd2lsw  13082  nn0abscl  13430  rexuzre  13470  znnenlem  14319  dvdsval3  14364  moddvds  14367  absdvdsb  14376  dvdsabsb  14377  dvdsle  14405  alzdvds  14410  mulmoddvds  14418  divalgmod  14442  bitsp1o  14461  gcdabs  14552  gcdabs1  14553  modgcd  14555  bezoutlem1  14558  algcvga  14593  lcmabs  14625  isprm3  14688  prmn2uzge3  14699  sqnprm  14701  zgcdsq  14757  hashdvds  14778  vfermltlALT  14808  powm2modprm  14809  modprm0  14811  modprmn0modprm0  14813  fldivp1  14897  zgz  14932  4sqlem4  14951  prmgaplem5  15080  prmgaplem7  15082  cshwshashlem2  15122  gexdvds  17290  zringunit  19117  prmirred  19121  znf1o  19177  chfacfscmul0  19937  chfacfscmulgsum  19939  chfacfpmmul0  19941  chfacfpmmulgsum  19943  dyadf  22605  dyadovol  22607  degltlem1  23077  coskpi  23531  cosne0  23535  relogexp  23601  cxpeq  23753  relogbzexp  23769  ppival2  24111  ppival2g  24112  ppiprm  24134  chtprm  24136  chtnprm  24137  ppip1le  24144  efexple  24265  lgsdir2lem4  24310  lgsne0  24317  lgsquadlem1  24338  lgsquadlem2  24339  2sqlem2  24348  rplogsumlem2  24379  pntrsumbnd  24460  axlowdim  25047  clwlkisclwwlklem2fv2  25567  clwlkisclwwlklem2a  25569  clwwlkext2edg  25586  wwlksubclwwlk  25588  clwwisshclwwlem1  25589  usg2cwwkdifex  25605  clwlkfclwwlk  25628  extwwlkfablem2  25862  numclwwlkovf2ex  25870  numclwlk1lem2f1  25878  frgrareg  25901  frgraregord013  25902  topnfbey  25962  gxnval  26044  gxmodid  26063  rezh  28826  zrhre  28874  hashf2  28956  ballotlemfc0  29375  ballotlemfcc  29376  elfzm12  30369  nn0prpwlem  31028  poimirlem24  32010  mblfinlem1  32023  mblfinlem2  32024  dvtanlemOLD  32037  itg2addnclem2  32040  fzmul  32115  fzadd2  32116  incsequz2  32124  ellz1  35655  lzunuz  35656  lzenom  35658  nerabdioph  35698  pell14qrgt0  35751  rmxycomplete  35811  monotuz  35835  monotoddzzfi  35836  oddcomabszz  35838  zindbi  35840  jm2.24  35859  congrep  35869  fzneg  35878  jm2.19  35894  oddfl  37562  fzdifsuc2  37605  climsuse  37773  stoweidlem26  37987  stoweidlem34  37996  fourierdlem20  38090  fourierdlem42  38113  fourierdlem42OLD  38114  fourierdlem51  38122  fourierdlem64  38135  fourierdlem76  38147  fourierdlem94  38165  fourierdlem97  38168  fourierdlem113  38184  zgeltp1eq  38852  smonoord  38853  fzopredsuc  38855  mod2eq1n2dvds  38860  elmod2OLD  38861  iccpartipre  38870  iccpartiltu  38871  iccpartigtl  38872  icceuelpartlem  38884  dfeven3  38922  dfodd4  38923  nn0o1gt2ALTV  38958  nnoALTV  38959  gbegt5  38997  gbogt5  38998  bgoldbwt  39013  nnsum3primesle9  39024  nnsum4primesodd  39026  nnsum4primesoddALTV  39027  evengpop3  39028  evengpoap3  39029  nnsum4primesevenALTV  39031  bgoldbtbndlem1  39035  bgoldbtbndlem2  39036  bgoldbtbndlem3  39037  bgoldbtbndlem4  39038  pfxccatin12lem2  39102  zm1nn  39187  eluzge0nn0  39191  elfz2z  39193  2elfz2melfz  39196  elfzlble  39198  elfzelfzlble  39199  fsummmodsndifre  39235  cznnring  40327  elfzolborelfzop1  40685  zgtp1leeq  40688  mod0mul  40691  modn0mul  40692  m1modmmod  40693  difmodm1lt  40694  rege1logbzge0  40739  fllog2  40748  dignn0ldlem  40782  dignn0flhalflem1  40795  dignn0flhalflem2  40796
  Copyright terms: Public domain W3C validator