Theorem zre 12620

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 12618	. 2 ⊢ (𝑁 ∈ ℤ ↔ (𝑁 ∈ ℝ ∧ (𝑁 = 0 ∨ 𝑁 ∈ ℕ ∨ -𝑁 ∈ ℕ)))
2	1	simplbi 502	1 ⊢ (𝑁 ∈ ℤ → 𝑁 ∈ ℝ)

This proof depends on syntax axioms:   → wi 4   ∨ w3o 1102   = wceq 1570   ∈ wcel 2145  ℝcr 11124  0cc0 11125  -cneg 11467  ℕcn 12258  ℤcz 12616

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3or 1104  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-sb 2100  df-clab 2739  df-cleq 2752  df-clel 2835  df-rab 3413  df-v 3452  df-dif 3902  df-un 3904  df-ss 3916  df-nul 4280  df-if 4483  df-sn 4585  df-pr 4587  df-op 4591  df-uni 4868  df-br 5104  df-iota 6489  df-fv 6541  df-ov 7417  df-neg 11469  df-z 12617

This theorem is used by:  zcn  12621  zrei  12622  zssre  12623  elnn0z  12629  elnnz1  12645  znnnlt1  12646  zletr  12663  znnsub  12665  znn0sub  12666  nzadd  12667  zltp1le  12669  zleltp1  12670  0nn0m1nnn0  12676  nn0ge0div  12691  zextle  12695  btwnnz  12698  suprzcl  12702  msqznn  12704  peano2uz2  12710  uzind  12714  fzind  12720  fnn0ind  12721  eluzuzle  12897  uzid  12903  uzneg  12908  uztric  12912  uz11  12913  eluzp1m1  12914  eluzp1p1  12916  eluzadd  12917  eluzsub  12918  subeluzsub  12921  uzin  12924  uz3m2nn  12944  peano2uz  12951  nn0pzuz  12955  uzwo  12961  eluz2b2  12971  uz2mulcl  12976  uzinfi  12978  eqreznegel  12984  lbzbi  12986  uzsupss  12990  nn01to3  12991  zmin  12994  zmax  12995  zbtwnre  12996  rebtwnz  12997  qre  13003  elpq  13026  rpnnen1lem2  13028  rpnnen1lem1  13029  rpnnen1lem3  13030  rpnnen1lem5  13032  z2ge  13251  qbtwnre  13252  zltaddlt1le  13559  elfz1eq  13590  fzn  13595  fzen  13596  uzsubsubfz  13602  fzaddel  13614  fzadd2  13615  ssfzunsnext  13625  ssfzunsn  13626  fzsuc2  13638  fzrev  13643  elfz1b  13649  fznuz  13665  uznfz  13666  fzp1nel  13667  elfz0fzfz0  13689  fz0fzelfz0  13690  fznn0sub2  13691  fz0fzdiffz0  13693  elfzmlbp  13695  difelfznle  13698  nelfzo  13721  elfzouz2  13731  fzo0n  13738  fzonlt0  13739  fzossrbm1  13745  fzospliti  13748  elfzo0z  13758  fzofzim  13766  fzo1fzo0n0  13772  eluzgtdifelfzo  13784  fzossfzop1  13800  ssfzoulel  13817  ssfzo12bi  13818  elfzonelfzo  13826  elfzomelpfzo  13829  elfznelfzob  13831  fzostep1  13843  fllt  13868  flid  13870  flbi2  13879  2tnp1ge0ge0  13891  flhalf  13892  fldiv4p1lem1div2  13897  fldiv4lem1div2uz2  13898  dfceil2  13901  ceile  13911  ceilid  13913  quoremz  13917  intfracq  13921  uzsup  13925  mulmod0  13939  zmod10  13949  zmodcl  13953  zmodfz  13955  zmodid2  13961  modcyc  13968  modaddid  13972  mulp1mod1  13976  muladdmod  13977  modmuladd  13978  modmuladdim  13979  modmul1  13989  modaddmodup  13999  modaddmodlo  14000  modaddmulmod  14003  zsqcl2  14203  leexp2  14236  iexpcyc  14272  fi1uzind  14573  ccatsymb  14649  ccatval21sw  14652  lswccatn0lsw  14659  swrdnd  14725  swrdnnn0nd  14727  swrd0  14729  swrdswrdlem  14774  swrdswrd  14775  swrdccatin2  14799  pfxccatin12lem2  14801  pfxccatin12lem3  14802  repswswrd  14856  cshwmodn  14867  cshwsublen  14868  cshwidxmod  14875  cshwidxmodr  14876  cshwidxm1  14879  repswcshw  14884  2cshw  14885  cshweqrep  14893  cshw1  14894  swrd2lsw  15026  nn0abscl  15400  rexuzre  15441  dvdsval3  16347  p1modz1  16350  moddvds  16354  absdvdsb  16365  dvdsabsb  16366  dvdsle  16401  alzdvds  16411  mod2eq1n2dvds  16438  evennn02n  16441  evennn2n  16442  ltoddhalfle  16452  divalgmod  16497  fldivndvdslt  16507  flodddiv4t2lthalf  16509  bitsp1o  16524  gcdabs1  16620  modgcd  16623  bezoutlem1  16630  dfgcd2  16637  algcvga  16670  lcmabs  16696  isprm3  16774  dvdsnprmd  16781  2mulprm  16784  oddprmgt2  16791  sqnprm  16794  zgcdsq  16845  hashdvds  16867  vfermltlALT  16895  powm2modprm  16896  modprm0  16898  modprmn0modprm0  16900  fldivp1  16990  zgz  17026  4sqlem4  17045  prmgaplem5  17148  prmgaplem7  17150  cshwshashlem2  17189  setsstruct  17269  mulgmodid  19237  gexdvds  19712  zringunit  21680  prmirred  21688  znf1o  21765  chfacfscmul0  23084  chfacfscmulgsum  23086  chfacfpmmul0  23088  chfacfpmmulgsum  23090  dyadf  25820  dyadovol  25822  degltlem1  26298  coskpi  26761  cosne0  26767  relogexp  26834  cxpeq  26995  relogbzexp  27014  ppival2  27365  ppival2g  27366  ppiprm  27388  chtprm  27390  chtnprm  27391  ppip1le  27398  efexple  27518  zabsle1  27533  lgsdir2lem4  27565  lgsne0  27572  gausslemma2dlem1a  27602  gausslemma2dlem3  27605  gausslemma2dlem4  27606  lgsquadlem1  27617  lgsquadlem2  27618  2lgslem1a1  27626  2lgslem1a2  27627  2sqlem2  27655  rplogsumlem2  27722  pntrsumbnd  27803  axlowdim  29419  crctcshwlkn0lem3  30281  crctcshwlkn0lem5  30283  crctcshwlkn0  30290  crctcsh  30293  clwlkclwwlklem2fv2  30467  clwlkclwwlklem2a  30469  clwwisshclwwslemlem  30484  clwwlkinwwlk  30511  clwwlkext2edg  30527  wwlksubclwwlk  30529  numclwwlk5  30869  topnfbey  30950  uzssico  33256  1fldgenq  33764  znfermltl  33802  ply1coedeg  34000  rezh  34480  zrhre  34530  hashf2  34595  ballotlemfc0  35005  ballotlemfcc  35006  chpvalz  35137  chtvalz  35138  zltp1ne  35715  elfzm12  36255  nn0prpwlem  36942  poimirlem24  38394  mblfinlem1  38407  mblfinlem2  38408  itg2addnclem2  38422  fzmul  38492  incsequz2  38500  fimgmcyc  43417  ellz1  43613  lzunuz  43614  lzenom  43616  nerabdioph  43651  pell14qrgt0  43701  rmxycomplete  43759  monotuz  43783  monotoddzzfi  43784  oddcomabszz  43786  zindbi  43788  jm2.24  43805  congrep  43815  fzneg  43824  jm2.19  43835  fzunt  44296  fzunt1d  44298  fzuntgd  44299  oddfl  46112  fzdifsuc2  46144  climsuse  46439  stoweidlem26  46855  stoweidlem34  46863  fourierdlem20  46956  fourierdlem42  46978  fourierdlem51  46986  fourierdlem64  46999  fourierdlem76  47011  fourierdlem94  47029  fourierdlem97  47032  fourierdlem113  47048  zm1nn  48191  zgeltp1eq  48198  eluzge0nn0  48201  elfz2z  48204  2elfz2melfz  48207  elfzlble  48209  elfzelfzlble  48210  fzopredsuc  48213  ceilbi  48226  mod0mul  48251  modn0mul  48252  m1modmmod  48253  difmodm1lt  48254  mod2addne  48259  modm2nep1  48261  modp2nep1  48262  modm1nep2  48263  modm1nem2  48264  modm1p1ne  48265  smonoord  48266  2timesltsqm1  48268  fsummmodsndifre  48271  muldvdsfacgt  48275  muldvdsfacm1  48276  iccpartipre  48322  iccpartiltu  48323  iccpartigtl  48324  icceuelpartlem  48336  fmtno4prmfac  48476  lighneallem4b  48513  nprmdvdsfacm1lem2  48525  nprmdvdsfacm1lem4  48527  dfeven3  48575  dfodd4  48576  nn0o1gt2ALTV  48611  nnoALTV  48612  fpprel2  48658  gbegt5  48678  gbowgt5  48679  sbgoldbwt  48694  nnsum3primesle9  48711  nnsum4primesodd  48713  nnsum4primesoddALTV  48714  evengpop3  48715  evengpoap3  48716  nnsum4primesevenALTV  48718  bgoldbtbndlem1  48722  bgoldbtbndlem2  48723  bgoldbtbndlem3  48724  bgoldbtbndlem4  48725  gpgprismgriedgdmss  48969  gpgusgralem  48973  gpgedgvtx1  48979  gpg5nbgrvtx03starlem2  48986  gpg5nbgrvtx13starlem2  48989  gpg3nbgrvtx0  48993  cznnring  49178  elfzolborelfzop1  49450  zgtp1leeq  49452  rege1logbzge0  49490  fllog2  49499  dignn0ldlem  49533  dignn0flhalflem1  49546  dignn0flhalflem2  49547