Theorem zre 12614

Description: An integer is a real. (Contributed by NM, 8-Jan-2002.)

Assertion

Ref	Expression
zre	⊢ (𝑁 ∈ ℤ → 𝑁 ∈ ℝ)

Proof of Theorem zre

Step	Hyp	Ref	Expression
1		elz 12612	. 2 ⊢ (𝑁 ∈ ℤ ↔ (𝑁 ∈ ℝ ∧ (𝑁 = 0 ∨ 𝑁 ∈ ℕ ∨ -𝑁 ∈ ℕ)))
2	1	simplbi 497	1 ⊢ (𝑁 ∈ ℤ → 𝑁 ∈ ℝ)

Syntax hints:   → wi 4   ∨ w3o 1085   = wceq 1536   ∈ wcel 2105  ℝcr 11151  0cc0 11152  -cneg 11490  ℕcn 12263  ℤcz 12610

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-8 2107  ax-9 2115  ax-ext 2705

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1539  df-fal 1549  df-ex 1776  df-sb 2062  df-clab 2712  df-cleq 2726  df-clel 2813  df-rab 3433  df-v 3479  df-dif 3965  df-un 3967  df-ss 3979  df-nul 4339  df-if 4531  df-sn 4631  df-pr 4633  df-op 4637  df-uni 4912  df-br 5148  df-iota 6515  df-fv 6570  df-ov 7433  df-neg 11492  df-z 12611

This theorem is referenced by:  zcn  12615  zrei  12616  zssre  12617  elnn0z  12623  elnnz1  12640  znnnlt1  12641  zletr  12658  znnsub  12660  znn0sub  12661  nzadd  12662  zltp1le  12664  zleltp1  12665  nn0ge0div  12684  zextle  12688  btwnnz  12691  suprzcl  12695  msqznn  12697  peano2uz2  12703  uzind  12707  fzind  12713  fnn0ind  12714  eluzuzle  12884  uzid  12890  uzneg  12895  uztric  12899  uz11  12900  eluzp1m1  12901  eluzp1p1  12903  eluzadd  12904  eluzsub  12905  eluzaddiOLD  12907  eluzsubiOLD  12909  subeluzsub  12912  uzin  12915  uz3m2nn  12930  peano2uz  12940  nn0pzuz  12944  uzwo  12950  eluz2b2  12960  uz2mulcl  12965  uzinfi  12967  eqreznegel  12973  lbzbi  12975  uzsupss  12979  nn01to3  12980  zmin  12983  zmax  12984  zbtwnre  12985  rebtwnz  12986  qre  12992  elpq  13014  rpnnen1lem2  13016  rpnnen1lem1  13017  rpnnen1lem3  13018  rpnnen1lem5  13020  z2ge  13236  qbtwnre  13237  zltaddlt1le  13541  elfz1eq  13571  fzn  13576  fzen  13577  uzsubsubfz  13582  fzaddel  13594  fzadd2  13595  ssfzunsnext  13605  ssfzunsn  13606  fzsuc2  13618  fzrev  13623  elfz1b  13629  fznuz  13645  uznfz  13646  fzp1nel  13647  elfz0fzfz0  13669  fz0fzelfz0  13670  fznn0sub2  13671  fz0fzdiffz0  13673  elfzmlbp  13675  difelfznle  13678  nelfzo  13700  elfzouz2  13710  fzo0n  13717  fzonlt0  13718  fzossrbm1  13724  fzospliti  13727  elfzo0z  13737  fzofzim  13745  fzo1fzo0n0  13750  eluzgtdifelfzo  13762  fzossfzop1  13778  ssfzoulel  13795  ssfzo12bi  13796  elfzonelfzo  13804  elfzomelpfzo  13806  elfznelfzob  13808  fzostep1  13818  fllt  13842  flid  13844  flbi2  13853  2tnp1ge0ge0  13865  flhalf  13866  fldiv4p1lem1div2  13871  fldiv4lem1div2uz2  13872  dfceil2  13875  ceile  13885  ceilid  13887  quoremz  13891  intfracq  13895  uzsup  13899  mulmod0  13913  zmod10  13923  zmodcl  13927  zmodfz  13929  zmodid2  13935  modcyc  13942  mulp1mod1  13948  muladdmod  13949  modmuladd  13950  modmuladdim  13951  modmul1  13961  modaddmodup  13971  modaddmodlo  13972  modaddmulmod  13975  zsqcl2  14174  leexp2  14207  iexpcyc  14242  fi1uzind  14542  ccatsymb  14616  ccatval21sw  14619  lswccatn0lsw  14625  swrdnd  14688  swrdnnn0nd  14690  swrd0  14692  swrdswrdlem  14738  swrdswrd  14739  swrdccatin2  14763  pfxccatin12lem2  14765  pfxccatin12lem3  14766  repswswrd  14818  cshwmodn  14829  cshwsublen  14830  cshwidxmod  14837  cshwidxmodr  14838  cshwidxm1  14841  repswcshw  14846  2cshw  14847  cshweqrep  14855  cshw1  14856  swrd2lsw  14987  nn0abscl  15347  rexuzre  15387  dvdsval3  16290  p1modz1  16293  moddvds  16297  absdvdsb  16308  dvdsabsb  16309  dvdsle  16343  alzdvds  16353  mod2eq1n2dvds  16380  evennn02n  16383  evennn2n  16384  ltoddhalfle  16394  divalgmod  16439  fldivndvdslt  16449  flodddiv4t2lthalf  16451  bitsp1o  16466  gcdabs1  16562  modgcd  16565  bezoutlem1  16572  dfgcd2  16579  algcvga  16612  lcmabs  16638  isprm3  16716  dvdsnprmd  16723  2mulprm  16726  oddprmgt2  16732  sqnprm  16735  zgcdsq  16786  hashdvds  16808  vfermltlALT  16835  powm2modprm  16836  modprm0  16838  modprmn0modprm0  16840  fldivp1  16930  zgz  16966  4sqlem4  16985  prmgaplem5  17088  prmgaplem7  17090  cshwshashlem2  17130  setsstruct  17209  mulgmodid  19143  gexdvds  19616  zringunit  21494  prmirred  21502  znf1o  21587  chfacfscmul0  22879  chfacfscmulgsum  22881  chfacfpmmul0  22883  chfacfpmmulgsum  22885  dyadf  25639  dyadovol  25641  degltlem1  26125  coskpi  26579  cosne0  26585  relogexp  26652  cxpeq  26814  relogbzexp  26833  ppival2  27185  ppival2g  27186  ppiprm  27208  chtprm  27210  chtnprm  27211  ppip1le  27218  efexple  27339  zabsle1  27354  lgsdir2lem4  27386  lgsne0  27393  gausslemma2dlem1a  27423  gausslemma2dlem3  27426  gausslemma2dlem4  27427  lgsquadlem1  27438  lgsquadlem2  27439  2lgslem1a1  27447  2lgslem1a2  27448  2sqlem2  27476  rplogsumlem2  27543  pntrsumbnd  27624  axlowdim  28990  crctcshwlkn0lem3  29841  crctcshwlkn0lem5  29843  crctcshwlkn0  29850  crctcsh  29853  clwlkclwwlklem2fv2  30024  clwlkclwwlklem2a  30026  clwwisshclwwslemlem  30041  clwwlkinwwlk  30068  clwwlkext2edg  30084  wwlksubclwwlk  30086  numclwwlk5  30416  topnfbey  30497  uzssico  32792  1fldgenq  33303  znfermltl  33373  rezh  33931  zrhre  33981  hashf2  34064  ballotlemfc0  34473  ballotlemfcc  34474  chpvalz  34621  chtvalz  34622  zltp1ne  35093  0nn0m1nnn0  35096  elfzm12  35659  nn0prpwlem  36304  poimirlem24  37630  mblfinlem1  37643  mblfinlem2  37644  itg2addnclem2  37658  fzmul  37727  incsequz2  37735  fimgmcyc  42520  ellz1  42754  lzunuz  42755  lzenom  42757  nerabdioph  42796  pell14qrgt0  42846  rmxycomplete  42905  monotuz  42929  monotoddzzfi  42930  oddcomabszz  42932  zindbi  42934  jm2.24  42951  congrep  42961  fzneg  42970  jm2.19  42981  fzunt  43444  fzunt1d  43446  fzuntgd  43447  oddfl  45227  fzdifsuc2  45260  climsuse  45563  stoweidlem26  45981  stoweidlem34  45989  fourierdlem20  46082  fourierdlem42  46104  fourierdlem51  46112  fourierdlem64  46125  fourierdlem76  46137  fourierdlem94  46155  fourierdlem97  46158  fourierdlem113  46174  natlocalincr  46829  natglobalincr  46830  zm1nn  47251  zgeltp1eq  47258  eluzge0nn0  47261  elfz2z  47264  2elfz2melfz  47267  elfzlble  47269  elfzelfzlble  47270  fzopredsuc  47272  smonoord  47295  fsummmodsndifre  47298  iccpartipre  47345  iccpartiltu  47346  iccpartigtl  47347  icceuelpartlem  47359  fmtno4prmfac  47496  lighneallem4b  47533  dfeven3  47582  dfodd4  47583  nn0o1gt2ALTV  47618  nnoALTV  47619  fpprel2  47665  gbegt5  47685  gbowgt5  47686  sbgoldbwt  47701  nnsum3primesle9  47718  nnsum4primesodd  47720  nnsum4primesoddALTV  47721  evengpop3  47722  evengpoap3  47723  nnsum4primesevenALTV  47725  bgoldbtbndlem1  47729  bgoldbtbndlem2  47730  bgoldbtbndlem3  47731  bgoldbtbndlem4  47732  gpgusgralem  47945  gpgedgvtx1  47954  gpg5nbgrvtx03starlem2  47959  gpg5nbgrvtx13starlem2  47962  gpg3nbgrvtx0  47966  cznnring  48105  elfzolborelfzop1  48364  zgtp1leeq  48366  mod0mul  48368  modn0mul  48369  m1modmmod  48370  difmodm1lt  48371  rege1logbzge0  48408  fllog2  48417  dignn0ldlem  48451  dignn0flhalflem1  48464  dignn0flhalflem2  48465