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

Theorem zre 11419
Description: An integer is a real. (Contributed by NM, 8-Jan-2002.)
Assertion
Ref Expression
zre (𝑁 ∈ ℤ → 𝑁 ∈ ℝ)

Proof of Theorem zre
StepHypRef Expression
1 elz 11417 . 2 (𝑁 ∈ ℤ ↔ (𝑁 ∈ ℝ ∧ (𝑁 = 0 ∨ 𝑁 ∈ ℕ ∨ -𝑁 ∈ ℕ)))
21simplbi 475 1 (𝑁 ∈ ℤ → 𝑁 ∈ ℝ)
Colors of variables: wff setvar class
Syntax hints:  wi 4  w3o 1053   = wceq 1523  wcel 2030  cr 9973  0cc0 9974  -cneg 10305  cn 11058  cz 11415
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-9 2039  ax-10 2059  ax-11 2074  ax-12 2087  ax-13 2282  ax-ext 2631
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3or 1055  df-3an 1056  df-tru 1526  df-ex 1745  df-nf 1750  df-sb 1938  df-clab 2638  df-cleq 2644  df-clel 2647  df-nfc 2782  df-rex 2947  df-rab 2950  df-v 3233  df-dif 3610  df-un 3612  df-in 3614  df-ss 3621  df-nul 3949  df-if 4120  df-sn 4211  df-pr 4213  df-op 4217  df-uni 4469  df-br 4686  df-iota 5889  df-fv 5934  df-ov 6693  df-neg 10307  df-z 11416
This theorem is referenced by:  zcn  11420  zrei  11421  zssre  11422  elnn0z  11428  elnnz1  11441  znnnlt1  11442  zletr  11459  znnsub  11461  znn0sub  11462  nzadd  11463  zltp1le  11465  zleltp1  11466  nn0ge0div  11484  zextle  11488  btwnnz  11491  suprzcl  11495  msqznn  11497  peano2uz2  11503  uzind  11507  fzind  11513  fnn0ind  11514  eluzuzle  11734  uzid  11740  uzneg  11744  uztric  11747  uz11  11748  eluzp1m1  11749  eluzp1p1  11751  eluzaddi  11752  eluzsubi  11753  uzin  11758  uz3m2nn  11769  peano2uz  11779  nn0pzuz  11783  uzwo  11789  eluz2b2  11799  uz2mulcl  11804  uzinfi  11806  eqreznegel  11812  lbzbi  11814  uzsupss  11818  nn01to3  11819  zmin  11822  zmax  11823  zbtwnre  11824  rebtwnz  11825  qre  11831  rpnnen1lem2  11852  rpnnen1lem1  11853  rpnnen1lem3  11854  rpnnen1lem5  11856  rpnnen1lem1OLD  11859  rpnnen1lem3OLD  11860  rpnnen1lem5OLD  11862  z2ge  12067  qbtwnre  12068  zltaddlt1le  12362  elfz1eq  12390  fzn  12395  fzen  12396  uzsubsubfz  12401  fzaddel  12413  fzadd2  12414  ssfzunsnext  12424  ssfzunsn  12425  fzsuc2  12436  fzrev  12441  elfz1b  12447  fznuz  12460  uznfz  12461  fzp1nel  12462  elfz0fzfz0  12483  fz0fzelfz0  12484  fznn0sub2  12485  fz0fzdiffz0  12487  elfzmlbp  12489  difelfznle  12492  nelfzo  12514  elfzouz2  12523  fzo0n  12529  fzonlt0  12530  fzossrbm1  12536  fzospliti  12539  elfzo0z  12549  fzofzim  12554  fzo1fzo0n0  12558  eluzgtdifelfzo  12569  fzossfzop1  12585  ssfzoulel  12602  ssfzo12bi  12603  elfzonelfzo  12610  elfzomelpfzo  12612  elfznelfzob  12614  fzostep1  12624  fllt  12647  flid  12649  flbi2  12658  2tnp1ge0ge0  12670  flhalf  12671  fldiv4p1lem1div2  12676  fldiv4lem1div2uz2  12677  dfceil2  12680  ceile  12688  ceilid  12690  quoremz  12694  intfracq  12698  uzsup  12702  mulmod0  12716  zmod10  12726  zmodcl  12730  zmodfz  12732  zmodid2  12738  modcyc  12745  mulp1mod1  12751  modmuladd  12752  modmuladdim  12753  modmul1  12763  modaddmodup  12773  modaddmodlo  12774  modaddmulmod  12777  leexp2  12955  zsqcl2  12981  iexpcyc  13009  fi1uzind  13317  ccatsymb  13400  ccatval21sw  13403  lswccatn0lsw  13409  swrdnd  13478  swrd0  13480  swrdswrdlem  13505  swrdswrd  13506  swrdccatin2  13533  swrdccatin12lem2  13535  swrdccatin12lem3  13536  repswswrd  13577  cshwmodn  13587  cshwsublen  13588  cshwidxmod  13595  cshwidxmodr  13596  cshwidxm1  13599  repswcshw  13604  2cshw  13605  cshweqrep  13613  cshw1  13614  swrd2lsw  13741  nn0abscl  14096  rexuzre  14136  znnenlem  14984  dvdsval3  15031  p1modz1  15034  moddvds  15038  absdvdsb  15047  dvdsabsb  15048  dvdsle  15079  alzdvds  15089  mod2eq1n2dvds  15118  evennn02n  15121  evennn2n  15122  ltoddhalfle  15132  divalgmod  15176  divalgmodOLD  15177  fldivndvdslt  15185  flodddiv4t2lthalf  15187  bitsp1o  15202  gcdabs  15297  gcdabs1  15298  modgcd  15300  bezoutlem1  15303  dfgcd2  15310  algcvga  15339  lcmabs  15365  isprm3  15443  dvdsnprmd  15450  oddprmgt2  15458  sqnprm  15461  zgcdsq  15508  hashdvds  15527  vfermltlALT  15554  powm2modprm  15555  modprm0  15557  modprmn0modprm0  15559  fldivp1  15648  zgz  15684  4sqlem4  15703  prmgaplem5  15806  prmgaplem7  15808  cshwshashlem2  15850  setsstruct  15945  mulgmodid  17628  gexdvds  18045  zringunit  19884  prmirred  19891  znf1o  19948  chfacfscmul0  20711  chfacfscmulgsum  20713  chfacfpmmul0  20715  chfacfpmmulgsum  20717  dyadf  23405  dyadovol  23407  degltlem1  23877  coskpi  24317  cosne0  24321  relogexp  24387  cxpeq  24543  relogbzexp  24559  ppival2  24899  ppival2g  24900  ppiprm  24922  chtprm  24924  chtnprm  24925  ppip1le  24932  efexple  25051  zabsle1  25066  lgsdir2lem4  25098  lgsne0  25105  gausslemma2dlem1a  25135  gausslemma2dlem3  25138  gausslemma2dlem4  25139  lgsquadlem1  25150  lgsquadlem2  25151  2lgslem1a1  25159  2lgslem1a2  25160  2sqlem2  25188  rplogsumlem2  25219  pntrsumbnd  25300  axlowdim  25886  crctcshwlkn0lem3  26760  crctcshwlkn0lem5  26762  crctcshwlkn0  26769  crctcsh  26772  clwlkclwwlklem2fv2  26962  clwlkclwwlklem2a  26964  clwwisshclwwslemlem  26970  clwwlkinwwlk  27003  clwwlkext2edg  27020  wwlksubclwwlk  27023  clwlksfclwwlk  27049  numclwwlk5  27375  topnfbey  27455  uzssico  29674  rezh  30143  zrhre  30191  hashf2  30274  ballotlemfc0  30682  ballotlemfcc  30683  chpvalz  30834  chtvalz  30835  elfzm12  31695  nn0prpwlem  32442  poimirlem24  33563  mblfinlem1  33576  mblfinlem2  33577  itg2addnclem2  33592  fzmul  33667  incsequz2  33675  ellz1  37647  lzunuz  37648  lzenom  37650  nerabdioph  37690  pell14qrgt0  37740  rmxycomplete  37799  monotuz  37823  monotoddzzfi  37824  oddcomabszz  37826  zindbi  37828  jm2.24  37847  congrep  37857  fzneg  37866  jm2.19  37877  oddfl  39803  fzdifsuc2  39838  climsuse  40158  stoweidlem26  40561  stoweidlem34  40569  fourierdlem20  40662  fourierdlem42  40684  fourierdlem51  40692  fourierdlem64  40705  fourierdlem76  40717  fourierdlem94  40735  fourierdlem97  40738  fourierdlem113  40754  zm1nn  41641  zgeltp1eq  41643  eluzge0nn0  41647  elfz2z  41650  2elfz2melfz  41653  elfzlble  41655  elfzelfzlble  41656  fzopredsuc  41658  smonoord  41666  fsummmodsndifre  41669  iccpartipre  41682  iccpartiltu  41683  iccpartigtl  41684  icceuelpartlem  41696  pfxccatin12lem2  41749  fmtno4prmfac  41809  lighneallem4b  41851  dfeven3  41895  dfodd4  41896  nn0o1gt2ALTV  41930  nnoALTV  41931  gbegt5  41974  gbowgt5  41975  sbgoldbwt  41990  nnsum3primesle9  42007  nnsum4primesodd  42009  nnsum4primesoddALTV  42010  evengpop3  42011  evengpoap3  42012  nnsum4primesevenALTV  42014  bgoldbtbndlem1  42018  bgoldbtbndlem2  42019  bgoldbtbndlem3  42020  bgoldbtbndlem4  42021  cznnring  42281  elfzolborelfzop1  42634  zgtp1leeq  42636  mod0mul  42639  modn0mul  42640  m1modmmod  42641  difmodm1lt  42642  rege1logbzge0  42678  fllog2  42687  dignn0ldlem  42721  dignn0flhalflem1  42734  dignn0flhalflem2  42735
  Copyright terms: Public domain W3C validator