Theorem zre 12590

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

Syntax hints:   → wi 4   ∨ w3o 1102   = wceq 1570   ∈ wcel 2143  ℝcr 11094  0cc0 11095  -cneg 11437  ℕcn 12228  ℤcz 12586

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-ext 2735

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3or 1104  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1810  df-sb 2097  df-clab 2742  df-cleq 2755  df-clel 2838  df-rab 3417  df-v 3457  df-dif 3908  df-un 3910  df-ss 3922  df-nul 4287  df-if 4488  df-sn 4590  df-pr 4592  df-op 4596  df-uni 4873  df-br 5110  df-iota 6492  df-fv 6544  df-ov 7413  df-neg 11439  df-z 12587

This theorem is referenced by:  zcn  12591  zrei  12592  zssre  12593  elnn0z  12599  elnnz1  12615  znnnlt1  12616  zletr  12633  znnsub  12635  znn0sub  12636  nzadd  12637  zltp1le  12639  zleltp1  12640  nn0ge0div  12660  zextle  12664  btwnnz  12667  suprzcl  12671  msqznn  12673  peano2uz2  12679  uzind  12683  fzind  12689  fnn0ind  12690  eluzuzle  12866  uzid  12872  uzneg  12877  uztric  12881  uz11  12882  eluzp1m1  12883  eluzp1p1  12885  eluzadd  12886  eluzsub  12887  subeluzsub  12890  uzin  12893  uz3m2nn  12913  peano2uz  12920  nn0pzuz  12924  uzwo  12930  eluz2b2  12940  uz2mulcl  12945  uzinfi  12947  eqreznegel  12953  lbzbi  12955  uzsupss  12959  nn01to3  12960  zmin  12963  zmax  12964  zbtwnre  12965  rebtwnz  12966  qre  12972  elpq  12994  rpnnen1lem2  12996  rpnnen1lem1  12997  rpnnen1lem3  12998  rpnnen1lem5  13000  z2ge  13219  qbtwnre  13220  zltaddlt1le  13527  elfz1eq  13558  fzn  13563  fzen  13564  uzsubsubfz  13570  fzaddel  13582  fzadd2  13583  ssfzunsnext  13593  ssfzunsn  13594  fzsuc2  13606  fzrev  13611  elfz1b  13617  fznuz  13633  uznfz  13634  fzp1nel  13635  elfz0fzfz0  13657  fz0fzelfz0  13658  fznn0sub2  13659  fz0fzdiffz0  13661  elfzmlbp  13663  difelfznle  13666  nelfzo  13689  elfzouz2  13699  fzo0n  13706  fzonlt0  13707  fzossrbm1  13713  fzospliti  13716  elfzo0z  13726  fzofzim  13734  fzo1fzo0n0  13740  eluzgtdifelfzo  13752  fzossfzop1  13768  ssfzoulel  13785  ssfzo12bi  13786  elfzonelfzo  13794  elfzomelpfzo  13797  elfznelfzob  13799  fzostep1  13811  fllt  13835  flid  13837  flbi2  13846  2tnp1ge0ge0  13858  flhalf  13859  fldiv4p1lem1div2  13864  fldiv4lem1div2uz2  13865  dfceil2  13868  ceile  13878  ceilid  13880  quoremz  13884  intfracq  13888  uzsup  13892  mulmod0  13906  zmod10  13916  zmodcl  13920  zmodfz  13922  zmodid2  13928  modcyc  13935  modaddid  13939  mulp1mod1  13943  muladdmod  13944  modmuladd  13945  modmuladdim  13946  modmul1  13956  modaddmodup  13966  modaddmodlo  13967  modaddmulmod  13970  zsqcl2  14170  leexp2  14203  iexpcyc  14239  fi1uzind  14540  ccatsymb  14616  ccatval21sw  14619  lswccatn0lsw  14625  swrdnd  14688  swrdnnn0nd  14690  swrd0  14692  swrdswrdlem  14737  swrdswrd  14738  swrdccatin2  14762  pfxccatin12lem2  14764  pfxccatin12lem3  14765  repswswrd  14817  cshwmodn  14828  cshwsublen  14829  cshwidxmod  14836  cshwidxmodr  14837  cshwidxm1  14840  repswcshw  14845  2cshw  14846  cshweqrep  14854  cshw1  14855  swrd2lsw  14985  nn0abscl  15359  rexuzre  15400  dvdsval3  16309  p1modz1  16312  moddvds  16316  absdvdsb  16327  dvdsabsb  16328  dvdsle  16363  alzdvds  16373  mod2eq1n2dvds  16400  evennn02n  16403  evennn2n  16404  ltoddhalfle  16414  divalgmod  16459  fldivndvdslt  16469  flodddiv4t2lthalf  16471  bitsp1o  16486  gcdabs1  16582  modgcd  16585  bezoutlem1  16592  dfgcd2  16599  algcvga  16632  lcmabs  16658  isprm3  16736  dvdsnprmd  16743  2mulprm  16746  oddprmgt2  16753  sqnprm  16756  zgcdsq  16807  hashdvds  16829  vfermltlALT  16857  powm2modprm  16858  modprm0  16860  modprmn0modprm0  16862  fldivp1  16952  zgz  16988  4sqlem4  17007  prmgaplem5  17110  prmgaplem7  17112  cshwshashlem2  17151  setsstruct  17231  mulgmodid  19174  gexdvds  19649  zringunit  21616  prmirred  21624  znf1o  21701  chfacfscmul0  23015  chfacfscmulgsum  23017  chfacfpmmul0  23019  chfacfpmmulgsum  23021  dyadf  25750  dyadovol  25752  degltlem1  26229  coskpi  26688  cosne0  26694  relogexp  26761  cxpeq  26922  relogbzexp  26941  ppival2  27292  ppival2g  27293  ppiprm  27315  chtprm  27317  chtnprm  27318  ppip1le  27325  efexple  27445  zabsle1  27460  lgsdir2lem4  27492  lgsne0  27499  gausslemma2dlem1a  27529  gausslemma2dlem3  27532  gausslemma2dlem4  27533  lgsquadlem1  27544  lgsquadlem2  27545  2lgslem1a1  27553  2lgslem1a2  27554  2sqlem2  27582  rplogsumlem2  27649  pntrsumbnd  27730  axlowdim  29311  crctcshwlkn0lem3  30161  crctcshwlkn0lem5  30163  crctcshwlkn0  30170  crctcsh  30173  clwlkclwwlklem2fv2  30347  clwlkclwwlklem2a  30349  clwwisshclwwslemlem  30364  clwwlkinwwlk  30391  clwwlkext2edg  30407  wwlksubclwwlk  30409  numclwwlk5  30739  topnfbey  30820  uzssico  33129  1fldgenq  33643  znfermltl  33681  ply1coedeg  33879  rezh  34359  zrhre  34409  hashf2  34474  ballotlemfc0  34883  ballotlemfcc  34884  chpvalz  35015  chtvalz  35016  zltp1ne  35601  0nn0m1nnn0  35604  elfzm12  36167  nn0prpwlem  36833  poimirlem24  38295  mblfinlem1  38308  mblfinlem2  38309  itg2addnclem2  38323  fzmul  38392  incsequz2  38400  fimgmcyc  43302  ellz1  43498  lzunuz  43499  lzenom  43501  nerabdioph  43536  pell14qrgt0  43586  rmxycomplete  43644  monotuz  43668  monotoddzzfi  43669  oddcomabszz  43671  zindbi  43673  jm2.24  43690  congrep  43700  fzneg  43709  jm2.19  43720  fzunt  44181  fzunt1d  44183  fzuntgd  44184  oddfl  45997  fzdifsuc2  46029  climsuse  46324  stoweidlem26  46740  stoweidlem34  46748  fourierdlem20  46841  fourierdlem42  46863  fourierdlem51  46871  fourierdlem64  46884  fourierdlem76  46896  fourierdlem94  46914  fourierdlem97  46917  fourierdlem113  46933  natlocalincr  47592  natglobalincr  47593  zm1nn  48039  zgeltp1eq  48046  eluzge0nn0  48049  elfz2z  48052  2elfz2melfz  48055  elfzlble  48057  elfzelfzlble  48058  fzopredsuc  48061  ceilbi  48074  mod0mul  48099  modn0mul  48100  m1modmmod  48101  difmodm1lt  48102  mod2addne  48107  modm2nep1  48109  modp2nep1  48110  modm1nep2  48111  modm1nem2  48112  modm1p1ne  48113  smonoord  48114  2timesltsqm1  48116  fsummmodsndifre  48119  muldvdsfacgt  48123  muldvdsfacm1  48124  iccpartipre  48170  iccpartiltu  48171  iccpartigtl  48172  icceuelpartlem  48184  fmtno4prmfac  48324  lighneallem4b  48361  nprmdvdsfacm1lem2  48373  nprmdvdsfacm1lem4  48375  dfeven3  48423  dfodd4  48424  nn0o1gt2ALTV  48459  nnoALTV  48460  fpprel2  48506  gbegt5  48526  gbowgt5  48527  sbgoldbwt  48542  nnsum3primesle9  48559  nnsum4primesodd  48561  nnsum4primesoddALTV  48562  evengpop3  48563  evengpoap3  48564  nnsum4primesevenALTV  48566  bgoldbtbndlem1  48570  bgoldbtbndlem2  48571  bgoldbtbndlem3  48572  bgoldbtbndlem4  48573  gpgprismgriedgdmss  48817  gpgusgralem  48821  gpgedgvtx1  48827  gpg5nbgrvtx03starlem2  48834  gpg5nbgrvtx13starlem2  48837  gpg3nbgrvtx0  48841  cznnring  49027  elfzolborelfzop1  49299  zgtp1leeq  49301  rege1logbzge0  49339  fllog2  49348  dignn0ldlem  49382  dignn0flhalflem1  49395  dignn0flhalflem2  49396