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

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

Proof of Theorem zre
StepHypRef Expression
1 elz 11571 . 2 (𝑁 ∈ ℤ ↔ (𝑁 ∈ ℝ ∧ (𝑁 = 0 ∨ 𝑁 ∈ ℕ ∨ -𝑁 ∈ ℕ)))
21simplbi 478 1 (𝑁 ∈ ℤ → 𝑁 ∈ ℝ)
Colors of variables: wff setvar class
Syntax hints:  wi 4  w3o 1071   = wceq 1632  wcel 2139  cr 10127  0cc0 10128  -cneg 10459  cn 11212  cz 11569
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1871  ax-4 1886  ax-5 1988  ax-6 2054  ax-7 2090  ax-9 2148  ax-10 2168  ax-11 2183  ax-12 2196  ax-13 2391  ax-ext 2740
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3or 1073  df-3an 1074  df-tru 1635  df-ex 1854  df-nf 1859  df-sb 2047  df-clab 2747  df-cleq 2753  df-clel 2756  df-nfc 2891  df-rex 3056  df-rab 3059  df-v 3342  df-dif 3718  df-un 3720  df-in 3722  df-ss 3729  df-nul 4059  df-if 4231  df-sn 4322  df-pr 4324  df-op 4328  df-uni 4589  df-br 4805  df-iota 6012  df-fv 6057  df-ov 6816  df-neg 10461  df-z 11570
This theorem is referenced by:  zcn  11574  zrei  11575  zssre  11576  elnn0z  11582  elnnz1  11595  znnnlt1  11596  zletr  11613  znnsub  11615  znn0sub  11616  nzadd  11617  zltp1le  11619  zleltp1  11620  nn0ge0div  11638  zextle  11642  btwnnz  11645  suprzcl  11649  msqznn  11651  peano2uz2  11657  uzind  11661  fzind  11667  fnn0ind  11668  eluzuzle  11888  uzid  11894  uzneg  11898  uztric  11901  uz11  11902  eluzp1m1  11903  eluzp1p1  11905  eluzaddi  11906  eluzsubi  11907  subeluzsub  11910  uzin  11913  uz3m2nn  11924  peano2uz  11934  nn0pzuz  11938  uzwo  11944  eluz2b2  11954  uz2mulcl  11959  uzinfi  11961  eqreznegel  11967  lbzbi  11969  uzsupss  11973  nn01to3  11974  zmin  11977  zmax  11978  zbtwnre  11979  rebtwnz  11980  qre  11986  rpnnen1lem2  12007  rpnnen1lem1  12008  rpnnen1lem3  12009  rpnnen1lem5  12011  rpnnen1lem1OLD  12014  rpnnen1lem3OLD  12015  rpnnen1lem5OLD  12017  z2ge  12222  qbtwnre  12223  zltaddlt1le  12517  elfz1eq  12545  fzn  12550  fzen  12551  uzsubsubfz  12556  fzaddel  12568  fzadd2  12569  ssfzunsnext  12579  ssfzunsn  12580  fzsuc2  12591  fzrev  12596  elfz1b  12602  fznuz  12615  uznfz  12616  fzp1nel  12617  elfz0fzfz0  12638  fz0fzelfz0  12639  fznn0sub2  12640  fz0fzdiffz0  12642  elfzmlbp  12644  difelfznle  12647  nelfzo  12669  elfzouz2  12678  fzo0n  12684  fzonlt0  12685  fzossrbm1  12691  fzospliti  12694  elfzo0z  12704  fzofzim  12709  fzo1fzo0n0  12713  eluzgtdifelfzo  12724  fzossfzop1  12740  ssfzoulel  12756  ssfzo12bi  12757  elfzonelfzo  12764  elfzomelpfzo  12766  elfznelfzob  12768  fzostep1  12778  fllt  12801  flid  12803  flbi2  12812  2tnp1ge0ge0  12824  flhalf  12825  fldiv4p1lem1div2  12830  fldiv4lem1div2uz2  12831  dfceil2  12834  ceile  12842  ceilid  12844  quoremz  12848  intfracq  12852  uzsup  12856  mulmod0  12870  zmod10  12880  zmodcl  12884  zmodfz  12886  zmodid2  12892  modcyc  12899  mulp1mod1  12905  modmuladd  12906  modmuladdim  12907  modmul1  12917  modaddmodup  12927  modaddmodlo  12928  modaddmulmod  12931  leexp2  13109  zsqcl2  13135  iexpcyc  13163  fi1uzind  13471  ccatsymb  13554  ccatval21sw  13557  lswccatn0lsw  13563  swrdnd  13632  swrd0  13634  swrdswrdlem  13659  swrdswrd  13660  swrdccatin2  13687  swrdccatin12lem2  13689  swrdccatin12lem3  13690  repswswrd  13731  cshwmodn  13741  cshwsublen  13742  cshwidxmod  13749  cshwidxmodr  13750  cshwidxm1  13753  repswcshw  13758  2cshw  13759  cshweqrep  13767  cshw1  13768  swrd2lsw  13896  nn0abscl  14251  rexuzre  14291  znnenlem  15139  dvdsval3  15186  p1modz1  15189  moddvds  15193  absdvdsb  15202  dvdsabsb  15203  dvdsle  15234  alzdvds  15244  mod2eq1n2dvds  15273  evennn02n  15276  evennn2n  15277  ltoddhalfle  15287  divalgmod  15331  divalgmodOLD  15332  fldivndvdslt  15340  flodddiv4t2lthalf  15342  bitsp1o  15357  gcdabs  15452  gcdabs1  15453  modgcd  15455  bezoutlem1  15458  dfgcd2  15465  algcvga  15494  lcmabs  15520  isprm3  15598  dvdsnprmd  15605  oddprmgt2  15613  sqnprm  15616  zgcdsq  15663  hashdvds  15682  vfermltlALT  15709  powm2modprm  15710  modprm0  15712  modprmn0modprm0  15714  fldivp1  15803  zgz  15839  4sqlem4  15858  prmgaplem5  15961  prmgaplem7  15963  cshwshashlem2  16005  setsstruct  16100  mulgmodid  17782  gexdvds  18199  zringunit  20038  prmirred  20045  znf1o  20102  chfacfscmul0  20865  chfacfscmulgsum  20867  chfacfpmmul0  20869  chfacfpmmulgsum  20871  dyadf  23559  dyadovol  23561  degltlem1  24031  coskpi  24471  cosne0  24475  relogexp  24541  cxpeq  24697  relogbzexp  24713  ppival2  25053  ppival2g  25054  ppiprm  25076  chtprm  25078  chtnprm  25079  ppip1le  25086  efexple  25205  zabsle1  25220  lgsdir2lem4  25252  lgsne0  25259  gausslemma2dlem1a  25289  gausslemma2dlem3  25292  gausslemma2dlem4  25293  lgsquadlem1  25304  lgsquadlem2  25305  2lgslem1a1  25313  2lgslem1a2  25314  2sqlem2  25342  rplogsumlem2  25373  pntrsumbnd  25454  axlowdim  26040  crctcshwlkn0lem3  26915  crctcshwlkn0lem5  26917  crctcshwlkn0  26924  crctcsh  26927  clwlkclwwlklem2fv2  27119  clwlkclwwlklem2a  27121  clwwisshclwwslemlem  27136  clwwlkinwwlk  27169  clwwlkext2edg  27186  wwlksubclwwlk  27189  clwlksfclwwlkOLD  27216  numclwwlk5  27556  topnfbey  27636  uzssico  29855  rezh  30324  zrhre  30372  hashf2  30455  ballotlemfc0  30863  ballotlemfcc  30864  chpvalz  31015  chtvalz  31016  elfzm12  31876  nn0prpwlem  32623  poimirlem24  33746  mblfinlem1  33759  mblfinlem2  33760  itg2addnclem2  33775  fzmul  33850  incsequz2  33858  ellz1  37832  lzunuz  37833  lzenom  37835  nerabdioph  37875  pell14qrgt0  37925  rmxycomplete  37984  monotuz  38008  monotoddzzfi  38009  oddcomabszz  38011  zindbi  38013  jm2.24  38032  congrep  38042  fzneg  38051  jm2.19  38062  oddfl  39988  fzdifsuc2  40023  climsuse  40343  stoweidlem26  40746  stoweidlem34  40754  fourierdlem20  40847  fourierdlem42  40869  fourierdlem51  40877  fourierdlem64  40890  fourierdlem76  40902  fourierdlem94  40920  fourierdlem97  40923  fourierdlem113  40939  zm1nn  41826  zgeltp1eq  41828  eluzge0nn0  41832  elfz2z  41835  2elfz2melfz  41838  elfzlble  41840  elfzelfzlble  41841  fzopredsuc  41843  smonoord  41851  fsummmodsndifre  41854  iccpartipre  41867  iccpartiltu  41868  iccpartigtl  41869  icceuelpartlem  41881  pfxccatin12lem2  41934  fmtno4prmfac  41994  lighneallem4b  42036  dfeven3  42080  dfodd4  42081  nn0o1gt2ALTV  42115  nnoALTV  42116  gbegt5  42159  gbowgt5  42160  sbgoldbwt  42175  nnsum3primesle9  42192  nnsum4primesodd  42194  nnsum4primesoddALTV  42195  evengpop3  42196  evengpoap3  42197  nnsum4primesevenALTV  42199  bgoldbtbndlem1  42203  bgoldbtbndlem2  42204  bgoldbtbndlem3  42205  bgoldbtbndlem4  42206  cznnring  42466  elfzolborelfzop1  42819  zgtp1leeq  42821  mod0mul  42824  modn0mul  42825  m1modmmod  42826  difmodm1lt  42827  rege1logbzge0  42863  fllog2  42872  dignn0ldlem  42906  dignn0flhalflem1  42919  dignn0flhalflem2  42920
  Copyright terms: Public domain W3C validator