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

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

Proof of Theorem zre
StepHypRef Expression
1 elz 11212 . 2 (𝑁 ∈ ℤ ↔ (𝑁 ∈ ℝ ∧ (𝑁 = 0 ∨ 𝑁 ∈ ℕ ∨ -𝑁 ∈ ℕ)))
21simplbi 474 1 (𝑁 ∈ ℤ → 𝑁 ∈ ℝ)
Colors of variables: wff setvar class
Syntax hints:  wi 4  w3o 1029   = wceq 1474  wcel 1976  cr 9791  0cc0 9792  -cneg 10118  cn 10867  cz 11210
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1712  ax-4 1727  ax-5 1826  ax-6 1874  ax-7 1921  ax-10 2005  ax-11 2020  ax-12 2033  ax-13 2233  ax-ext 2589
This theorem depends on definitions:  df-bi 195  df-or 383  df-an 384  df-3or 1031  df-3an 1032  df-tru 1477  df-ex 1695  df-nf 1700  df-sb 1867  df-clab 2596  df-cleq 2602  df-clel 2605  df-nfc 2739  df-rex 2901  df-rab 2904  df-v 3174  df-dif 3542  df-un 3544  df-in 3546  df-ss 3553  df-nul 3874  df-if 4036  df-sn 4125  df-pr 4127  df-op 4131  df-uni 4367  df-br 4578  df-iota 5754  df-fv 5798  df-ov 6530  df-neg 10120  df-z 11211
This theorem is referenced by:  zcn  11215  zrei  11216  zssre  11217  elnn0z  11223  elnnz1  11236  znnnlt1  11237  zletr  11254  znnsub  11256  znn0sub  11257  nzadd  11258  zltp1le  11260  zleltp1  11261  nn0ge0div  11278  zextle  11282  btwnnz  11285  suprzcl  11289  msqznn  11291  peano2uz2  11297  uzind  11301  fzind  11307  fnn0ind  11308  eluzuzle  11528  uzid  11534  uzneg  11538  uztric  11541  uz11  11542  eluzp1m1  11543  eluzp1p1  11545  eluzaddi  11546  eluzsubi  11547  uzin  11552  uz3m2nn  11563  peano2uz  11573  nn0pzuz  11577  uzwo  11583  eluz2b2  11593  uz2mulcl  11598  uzinfi  11600  eqreznegel  11606  lbzbi  11608  uzsupss  11612  nn01to3  11613  zmin  11616  zmax  11617  zbtwnre  11618  rebtwnz  11619  qre  11625  rpnnen1lem2  11646  rpnnen1lem1  11647  rpnnen1lem3  11648  rpnnen1lem5  11650  rpnnen1lem1OLD  11653  rpnnen1lem3OLD  11654  rpnnen1lem5OLD  11656  z2ge  11862  qbtwnre  11863  zltaddlt1le  12151  elfz1eq  12178  fzn  12183  fzen  12184  uzsubsubfz  12189  fzaddel  12201  fzadd2  12202  ssfzunsn  12212  fzsuc2  12223  fzrev  12228  elfz1b  12234  fznuz  12246  uznfz  12247  fzp1nel  12248  elfz0fzfz0  12268  fz0fzelfz0  12269  fznn0sub2  12270  fz0fzdiffz0  12272  elfzmlbp  12274  difelfznle  12277  nelfzo  12299  elfzouz2  12308  fzo0n  12314  fzonlt0  12315  fzossrbm1  12321  fzospliti  12324  elfzo0z  12332  fzofzim  12337  fzo1fzo0n0  12341  eluzgtdifelfzo  12352  fzossfzop1  12367  ssfzoulel  12383  ssfzo12bi  12384  elfzonelfzo  12391  elfzomelpfzo  12393  elfznelfzob  12395  fzosplitprm1  12398  fzostep1  12401  fllt  12424  flid  12426  flbi2  12435  2tnp1ge0ge0  12447  flhalf  12448  fldiv4p1lem1div2  12453  fldiv4lem1div2uz2  12454  dfceil2  12457  ceile  12465  ceilid  12467  quoremz  12471  intfracq  12475  uzsup  12479  mulmod0  12493  zmod10  12503  zmodcl  12507  zmodfz  12509  zmodid2  12515  modcyc  12522  mulp1mod1  12528  modmuladd  12529  modmuladdim  12530  modmul1  12540  modaddmodup  12550  modaddmodlo  12551  modaddmulmod  12554  leexp2  12732  zsqcl2  12758  iexpcyc  12786  fi1uzind  13080  fi1uzindOLD  13086  ccatsymb  13165  lswccatn0lsw  13172  swrdnd  13230  swrd0  13232  swrdswrdlem  13257  swrdswrd  13258  swrdccatin2  13284  swrdccatin12lem2  13286  swrdccatin12lem3  13287  repswswrd  13328  cshwmodn  13338  cshwsublen  13339  cshwidxmod  13346  cshwidxmodr  13347  cshwidxm1  13350  repswcshw  13355  2cshw  13356  cshweqrep  13364  cshw1  13365  swrd2lsw  13489  nn0abscl  13846  rexuzre  13886  znnenlem  14725  dvdsval3  14771  moddvds  14775  absdvdsb  14784  dvdsabsb  14785  dvdsle  14816  alzdvds  14826  mulmoddvds  14835  mod2eq1n2dvds  14855  evennn02n  14858  evennn2n  14859  ltoddhalfle  14869  divalgmod  14913  divalgmodOLD  14914  fldivndvdslt  14922  flodddiv4t2lthalf  14924  bitsp1o  14939  gcdabs  15034  gcdabs1  15035  modgcd  15037  bezoutlem1  15040  dfgcd2  15047  algcvga  15076  lcmabs  15102  isprm3  15180  dvdsnprmd  15187  oddprmgt2  15195  sqnprm  15198  zgcdsq  15245  hashdvds  15264  vfermltlALT  15291  powm2modprm  15292  modprm0  15294  modprmn0modprm0  15296  fldivp1  15385  zgz  15421  4sqlem4  15440  prmgaplem5  15543  prmgaplem7  15545  cshwshashlem2  15587  mulgmodid  17350  gexdvds  17768  zringunit  19603  prmirred  19607  znf1o  19664  chfacfscmul0  20424  chfacfscmulgsum  20426  chfacfpmmul0  20428  chfacfpmmulgsum  20430  dyadf  23082  dyadovol  23084  degltlem1  23553  coskpi  23993  cosne0  23997  relogexp  24063  cxpeq  24215  relogbzexp  24231  ppival2  24571  ppival2g  24572  ppiprm  24594  chtprm  24596  chtnprm  24597  ppip1le  24604  efexple  24723  zabsle1  24738  lgsdir2lem4  24770  lgsne0  24777  gausslemma2dlem1a  24807  gausslemma2dlem3  24810  gausslemma2dlem4  24811  lgsquadlem1  24822  lgsquadlem2  24823  2lgslem1a1  24831  2lgslem1a2  24832  2sqlem2  24860  rplogsumlem2  24891  pntrsumbnd  24972  axlowdim  25559  clwlkisclwwlklem2fv2  26077  clwlkisclwwlklem2a  26079  clwwlkext2edg  26096  wwlksubclwwlk  26098  clwwisshclwwlem1  26099  usg2cwwkdifex  26115  clwlkfclwwlk  26137  extwwlkfablem2  26371  numclwwlkovf2ex  26379  numclwlk1lem2f1  26387  frgrareg  26410  frgraregord013  26411  topnfbey  26483  rezh  29149  zrhre  29197  hashf2  29279  ballotlemfc0  29687  ballotlemfcc  29688  elfzm12  30629  nn0prpwlem  31293  poimirlem24  32399  mblfinlem1  32412  mblfinlem2  32413  itg2addnclem2  32428  fzmul  32503  incsequz2  32511  ellz1  36144  lzunuz  36145  lzenom  36147  nerabdioph  36187  pell14qrgt0  36237  rmxycomplete  36296  monotuz  36320  monotoddzzfi  36321  oddcomabszz  36323  zindbi  36325  jm2.24  36344  congrep  36354  fzneg  36363  jm2.19  36374  oddfl  38226  fzdifsuc2  38263  climsuse  38472  stoweidlem26  38716  stoweidlem34  38724  fourierdlem20  38817  fourierdlem42  38839  fourierdlem51  38847  fourierdlem64  38860  fourierdlem76  38872  fourierdlem94  38890  fourierdlem97  38893  fourierdlem113  38909  zgeltp1eq  39741  smonoord  39742  fzopredsuc  39744  iccpartipre  39757  iccpartiltu  39758  iccpartigtl  39759  icceuelpartlem  39771  fmtno4prmfac  39820  lighneallem4b  39862  dfeven3  39906  dfodd4  39907  nn0o1gt2ALTV  39941  nnoALTV  39942  gbegt5  39981  gbogt5  39982  bgoldbwt  39997  nnsum3primesle9  40008  nnsum4primesodd  40010  nnsum4primesoddALTV  40011  evengpop3  40012  evengpoap3  40013  nnsum4primesevenALTV  40015  bgoldbtbndlem1  40019  bgoldbtbndlem2  40020  bgoldbtbndlem3  40021  bgoldbtbndlem4  40022  pfxccatin12lem2  40085  zm1nn  40168  eluzge0nn0  40170  elfz2z  40172  2elfz2melfz  40175  elfzlble  40177  elfzelfzlble  40178  fsummmodsndifre  40216  crctcsh1wlkn0lem3  41010  crctcsh1wlkn0lem5  41012  crctcsh1wlkn0  41019  crctcsh  41022  clwlkclwwlklem2fv2  41200  clwlkclwwlklem2a  41202  clwwlksext2edg  41225  wwlksubclwwlks  41227  clwwisshclwwslemlem  41228  clwlksfclwwlk  41264  av-numclwwlkovf2ex  41512  av-numclwlk1lem2f1  41519  av-numclwwlk5  41537  cznnring  41743  elfzolborelfzop1  42098  zgtp1leeq  42100  mod0mul  42103  modn0mul  42104  m1modmmod  42105  difmodm1lt  42106  rege1logbzge0  42146  fllog2  42155  dignn0ldlem  42189  dignn0flhalflem1  42202  dignn0flhalflem2  42203
  Copyright terms: Public domain W3C validator