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

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

Proof of Theorem zre
StepHypRef Expression
1 elz 11971 . 2 (𝑁 ∈ ℤ ↔ (𝑁 ∈ ℝ ∧ (𝑁 = 0 ∨ 𝑁 ∈ ℕ ∨ -𝑁 ∈ ℕ)))
21simplbi 498 1 (𝑁 ∈ ℤ → 𝑁 ∈ ℝ)
Colors of variables: wff setvar class
Syntax hints:  wi 4  w3o 1078   = wceq 1528  wcel 2105  cr 10524  0cc0 10525  -cneg 10859  cn 11626  cz 11969
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1787  ax-4 1801  ax-5 1902  ax-6 1961  ax-7 2006  ax-8 2107  ax-9 2115  ax-10 2136  ax-11 2151  ax-12 2167  ax-ext 2790
This theorem depends on definitions:  df-bi 208  df-an 397  df-or 842  df-3or 1080  df-3an 1081  df-tru 1531  df-ex 1772  df-nf 1776  df-sb 2061  df-clab 2797  df-cleq 2811  df-clel 2890  df-nfc 2960  df-rex 3141  df-rab 3144  df-v 3494  df-dif 3936  df-un 3938  df-in 3940  df-ss 3949  df-nul 4289  df-if 4464  df-sn 4558  df-pr 4560  df-op 4564  df-uni 4831  df-br 5058  df-iota 6307  df-fv 6356  df-ov 7148  df-neg 10861  df-z 11970
This theorem is referenced by:  zcn  11974  zrei  11975  zssre  11976  elnn0z  11982  elnnz1  11996  znnnlt1  11997  zletr  12014  znnsub  12016  znn0sub  12017  nzadd  12018  zltp1le  12020  zleltp1  12021  nn0ge0div  12039  zextle  12043  btwnnz  12046  suprzcl  12050  msqznn  12052  peano2uz2  12058  uzind  12062  fzind  12068  fnn0ind  12069  eluzuzle  12240  uzid  12246  uzneg  12251  uztric  12254  uz11  12255  eluzp1m1  12256  eluzp1p1  12258  eluzaddi  12259  eluzsubi  12260  subeluzsub  12263  uzin  12266  uz3m2nn  12279  peano2uz  12289  nn0pzuz  12293  uzwo  12299  eluz2b2  12309  uz2mulcl  12314  uzinfi  12316  eqreznegel  12322  lbzbi  12324  uzsupss  12328  nn01to3  12329  zmin  12332  zmax  12333  zbtwnre  12334  rebtwnz  12335  qre  12341  elpq  12362  rpnnen1lem2  12364  rpnnen1lem1  12365  rpnnen1lem3  12366  rpnnen1lem5  12368  z2ge  12579  qbtwnre  12580  zltaddlt1le  12878  elfz1eq  12906  fzn  12911  fzen  12912  uzsubsubfz  12917  fzaddel  12929  fzadd2  12930  ssfzunsnext  12940  ssfzunsn  12941  fzsuc2  12953  fzrev  12958  elfz1b  12964  fznuz  12977  uznfz  12978  fzp1nel  12979  elfz0fzfz0  13000  fz0fzelfz0  13001  fznn0sub2  13002  fz0fzdiffz0  13004  elfzmlbp  13006  difelfznle  13009  nelfzo  13031  elfzouz2  13040  fzo0n  13047  fzonlt0  13048  fzossrbm1  13054  fzospliti  13057  elfzo0z  13067  fzofzim  13072  fzo1fzo0n0  13076  eluzgtdifelfzo  13087  fzossfzop1  13103  ssfzoulel  13119  ssfzo12bi  13120  elfzonelfzo  13127  elfzomelpfzo  13129  elfznelfzob  13131  fzostep1  13141  fllt  13164  flid  13166  flbi2  13175  2tnp1ge0ge0  13187  flhalf  13188  fldiv4p1lem1div2  13193  fldiv4lem1div2uz2  13194  dfceil2  13197  ceile  13205  ceilid  13207  quoremz  13211  intfracq  13215  uzsup  13219  mulmod0  13233  zmod10  13243  zmodcl  13247  zmodfz  13249  zmodid2  13255  modcyc  13262  mulp1mod1  13268  modmuladd  13269  modmuladdim  13270  modmul1  13280  modaddmodup  13290  modaddmodlo  13291  modaddmulmod  13294  zsqcl2  13490  leexp2  13523  iexpcyc  13557  fi1uzind  13843  ccatsymb  13924  ccatval21sw  13927  lswccatn0lsw  13933  swrdnd  14004  swrdnnn0nd  14006  swrd0  14008  swrdswrdlem  14054  swrdswrd  14055  swrdccatin2  14079  pfxccatin12lem2  14081  pfxccatin12lem3  14082  repswswrd  14134  cshwmodn  14145  cshwsublen  14146  cshwidxmod  14153  cshwidxmodr  14154  cshwidxm1  14157  repswcshw  14162  2cshw  14163  cshweqrep  14171  cshw1  14172  swrd2lsw  14302  nn0abscl  14660  rexuzre  14700  dvdsval3  15599  p1modz1  15602  moddvds  15606  absdvdsb  15616  dvdsabsb  15617  dvdsle  15648  alzdvds  15658  mod2eq1n2dvds  15684  evennn02n  15687  evennn2n  15688  ltoddhalfle  15698  divalgmod  15745  fldivndvdslt  15753  flodddiv4t2lthalf  15755  bitsp1o  15770  gcdabs  15865  gcdabs1  15866  modgcd  15868  bezoutlem1  15875  dfgcd2  15882  algcvga  15911  lcmabs  15937  isprm3  16015  dvdsnprmd  16022  2mulprm  16025  oddprmgt2  16031  sqnprm  16034  zgcdsq  16081  hashdvds  16100  vfermltlALT  16127  powm2modprm  16128  modprm0  16130  modprmn0modprm0  16132  fldivp1  16221  zgz  16257  4sqlem4  16276  prmgaplem5  16379  prmgaplem7  16381  cshwshashlem2  16418  setsstruct  16511  mulgmodid  18204  gexdvds  18638  zringunit  20563  prmirred  20570  znf1o  20626  chfacfscmul0  21394  chfacfscmulgsum  21396  chfacfpmmul0  21398  chfacfpmmulgsum  21400  dyadf  24119  dyadovol  24121  degltlem1  24593  coskpi  25035  cosne0  25041  relogexp  25106  cxpeq  25265  relogbzexp  25281  ppival2  25632  ppival2g  25633  ppiprm  25655  chtprm  25657  chtnprm  25658  ppip1le  25665  efexple  25784  zabsle1  25799  lgsdir2lem4  25831  lgsne0  25838  gausslemma2dlem1a  25868  gausslemma2dlem3  25871  gausslemma2dlem4  25872  lgsquadlem1  25883  lgsquadlem2  25884  2lgslem1a1  25892  2lgslem1a2  25893  2sqlem2  25921  rplogsumlem2  25988  pntrsumbnd  26069  axlowdim  26674  crctcshwlkn0lem3  27517  crctcshwlkn0lem5  27519  crctcshwlkn0  27526  crctcsh  27529  clwlkclwwlklem2fv2  27701  clwlkclwwlklem2a  27703  clwwisshclwwslemlem  27718  clwwlkinwwlk  27745  clwwlkext2edg  27762  wwlksubclwwlk  27764  numclwwlk5  28094  topnfbey  28175  uzssico  30433  rezh  31111  zrhre  31159  hashf2  31242  ballotlemfc0  31649  ballotlemfcc  31650  chpvalz  31798  chtvalz  31799  zltp1ne  32245  0nn0m1nnn0  32248  elfzm12  32815  nn0prpwlem  33567  poimirlem24  34797  mblfinlem1  34810  mblfinlem2  34811  itg2addnclem2  34825  fzmul  34897  incsequz2  34905  ellz1  39242  lzunuz  39243  lzenom  39245  nerabdioph  39284  pell14qrgt0  39334  rmxycomplete  39392  monotuz  39416  monotoddzzfi  39417  oddcomabszz  39419  zindbi  39421  jm2.24  39438  congrep  39448  fzneg  39457  jm2.19  39468  oddfl  41419  fzdifsuc2  41453  climsuse  41765  stoweidlem26  42188  stoweidlem34  42196  fourierdlem20  42289  fourierdlem42  42311  fourierdlem51  42319  fourierdlem64  42332  fourierdlem76  42344  fourierdlem94  42362  fourierdlem97  42365  fourierdlem113  42381  zm1nn  43379  zgeltp1eq  43386  eluzge0nn0  43389  elfz2z  43392  2elfz2melfz  43395  elfzlble  43397  elfzelfzlble  43398  fzopredsuc  43400  smonoord  43408  fsummmodsndifre  43411  iccpartipre  43458  iccpartiltu  43459  iccpartigtl  43460  icceuelpartlem  43472  fmtno4prmfac  43611  lighneallem4b  43651  dfeven3  43700  dfodd4  43701  nn0o1gt2ALTV  43736  nnoALTV  43737  fpprel2  43783  gbegt5  43803  gbowgt5  43804  sbgoldbwt  43819  nnsum3primesle9  43836  nnsum4primesodd  43838  nnsum4primesoddALTV  43839  evengpop3  43840  evengpoap3  43841  nnsum4primesevenALTV  43843  bgoldbtbndlem1  43847  bgoldbtbndlem2  43848  bgoldbtbndlem3  43849  bgoldbtbndlem4  43850  cznnring  44155  elfzolborelfzop1  44502  zgtp1leeq  44504  mod0mul  44507  modn0mul  44508  m1modmmod  44509  difmodm1lt  44510  rege1logbzge0  44547  fllog2  44556  dignn0ldlem  44590  dignn0flhalflem1  44603  dignn0flhalflem2  44604
  Copyright terms: Public domain W3C validator