Theorem zre 12559

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

Syntax hints:   → wi 4   ∨ w3o 1087   = wceq 1542   ∈ wcel 2107  ℝcr 11106  0cc0 11107  -cneg 11442  ℕcn 12209  ℤcz 12555

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2704

This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3or 1089  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-rab 3434  df-v 3477  df-dif 3951  df-un 3953  df-in 3955  df-ss 3965  df-nul 4323  df-if 4529  df-sn 4629  df-pr 4631  df-op 4635  df-uni 4909  df-br 5149  df-iota 6493  df-fv 6549  df-ov 7409  df-neg 11444  df-z 12556

This theorem is referenced by:  zcn  12560  zrei  12561  zssre  12562  elnn0z  12568  elnnz1  12585  znnnlt1  12586  zletr  12603  znnsub  12605  znn0sub  12606  nzadd  12607  zltp1le  12609  zleltp1  12610  nn0ge0div  12628  zextle  12632  btwnnz  12635  suprzcl  12639  msqznn  12641  peano2uz2  12647  uzind  12651  fzind  12657  fnn0ind  12658  eluzuzle  12828  uzid  12834  uzneg  12839  uztric  12843  uz11  12844  eluzp1m1  12845  eluzp1p1  12847  eluzadd  12848  eluzsub  12849  eluzaddiOLD  12851  eluzsubiOLD  12853  subeluzsub  12856  uzin  12859  uz3m2nn  12872  peano2uz  12882  nn0pzuz  12886  uzwo  12892  eluz2b2  12902  uz2mulcl  12907  uzinfi  12909  eqreznegel  12915  lbzbi  12917  uzsupss  12921  nn01to3  12922  zmin  12925  zmax  12926  zbtwnre  12927  rebtwnz  12928  qre  12934  elpq  12956  rpnnen1lem2  12958  rpnnen1lem1  12959  rpnnen1lem3  12960  rpnnen1lem5  12962  z2ge  13174  qbtwnre  13175  zltaddlt1le  13479  elfz1eq  13509  fzn  13514  fzen  13515  uzsubsubfz  13520  fzaddel  13532  fzadd2  13533  ssfzunsnext  13543  ssfzunsn  13544  fzsuc2  13556  fzrev  13561  elfz1b  13567  fznuz  13580  uznfz  13581  fzp1nel  13582  elfz0fzfz0  13603  fz0fzelfz0  13604  fznn0sub2  13605  fz0fzdiffz0  13607  elfzmlbp  13609  difelfznle  13612  nelfzo  13634  elfzouz2  13644  fzo0n  13651  fzonlt0  13652  fzossrbm1  13658  fzospliti  13661  elfzo0z  13671  fzofzim  13676  fzo1fzo0n0  13680  eluzgtdifelfzo  13691  fzossfzop1  13707  ssfzoulel  13723  ssfzo12bi  13724  elfzonelfzo  13731  elfzomelpfzo  13733  elfznelfzob  13735  fzostep1  13745  fllt  13768  flid  13770  flbi2  13779  2tnp1ge0ge0  13791  flhalf  13792  fldiv4p1lem1div2  13797  fldiv4lem1div2uz2  13798  dfceil2  13801  ceile  13811  ceilid  13813  quoremz  13817  intfracq  13821  uzsup  13825  mulmod0  13839  zmod10  13849  zmodcl  13853  zmodfz  13855  zmodid2  13861  modcyc  13868  mulp1mod1  13874  modmuladd  13875  modmuladdim  13876  modmul1  13886  modaddmodup  13896  modaddmodlo  13897  modaddmulmod  13900  zsqcl2  14100  leexp2  14133  iexpcyc  14168  fi1uzind  14455  ccatsymb  14529  ccatval21sw  14532  lswccatn0lsw  14538  swrdnd  14601  swrdnnn0nd  14603  swrd0  14605  swrdswrdlem  14651  swrdswrd  14652  swrdccatin2  14676  pfxccatin12lem2  14678  pfxccatin12lem3  14679  repswswrd  14731  cshwmodn  14742  cshwsublen  14743  cshwidxmod  14750  cshwidxmodr  14751  cshwidxm1  14754  repswcshw  14759  2cshw  14760  cshweqrep  14768  cshw1  14769  swrd2lsw  14900  nn0abscl  15256  rexuzre  15296  dvdsval3  16198  p1modz1  16201  moddvds  16205  absdvdsb  16215  dvdsabsb  16216  dvdsle  16250  alzdvds  16260  mod2eq1n2dvds  16287  evennn02n  16290  evennn2n  16291  ltoddhalfle  16301  divalgmod  16346  fldivndvdslt  16354  flodddiv4t2lthalf  16356  bitsp1o  16371  gcdabs1  16467  gcdabsOLD  16470  modgcd  16471  bezoutlem1  16478  dfgcd2  16485  algcvga  16513  lcmabs  16539  isprm3  16617  dvdsnprmd  16624  2mulprm  16627  oddprmgt2  16633  sqnprm  16636  zgcdsq  16686  hashdvds  16705  vfermltlALT  16732  powm2modprm  16733  modprm0  16735  modprmn0modprm0  16737  fldivp1  16827  zgz  16863  4sqlem4  16882  prmgaplem5  16985  prmgaplem7  16987  cshwshashlem2  17027  setsstruct  17106  mulgmodid  18988  gexdvds  19447  zringunit  21028  prmirred  21036  znf1o  21099  chfacfscmul0  22352  chfacfscmulgsum  22354  chfacfpmmul0  22356  chfacfpmmulgsum  22358  dyadf  25100  dyadovol  25102  degltlem1  25582  coskpi  26024  cosne0  26030  relogexp  26096  cxpeq  26255  relogbzexp  26271  ppival2  26622  ppival2g  26623  ppiprm  26645  chtprm  26647  chtnprm  26648  ppip1le  26655  efexple  26774  zabsle1  26789  lgsdir2lem4  26821  lgsne0  26828  gausslemma2dlem1a  26858  gausslemma2dlem3  26861  gausslemma2dlem4  26862  lgsquadlem1  26873  lgsquadlem2  26874  2lgslem1a1  26882  2lgslem1a2  26883  2sqlem2  26911  rplogsumlem2  26978  pntrsumbnd  27059  axlowdim  28209  crctcshwlkn0lem3  29056  crctcshwlkn0lem5  29058  crctcshwlkn0  29065  crctcsh  29068  clwlkclwwlklem2fv2  29239  clwlkclwwlklem2a  29241  clwwisshclwwslemlem  29256  clwwlkinwwlk  29283  clwwlkext2edg  29299  wwlksubclwwlk  29301  numclwwlk5  29631  topnfbey  29712  uzssico  31983  1fldgenq  32401  znfermltl  32468  rezh  32940  zrhre  32988  hashf2  33071  ballotlemfc0  33480  ballotlemfcc  33481  chpvalz  33629  chtvalz  33630  zltp1ne  34088  0nn0m1nnn0  34091  elfzm12  34649  nn0prpwlem  35196  poimirlem24  36501  mblfinlem1  36514  mblfinlem2  36515  itg2addnclem2  36529  fzmul  36598  incsequz2  36606  ellz1  41491  lzunuz  41492  lzenom  41494  nerabdioph  41533  pell14qrgt0  41583  rmxycomplete  41642  monotuz  41666  monotoddzzfi  41667  oddcomabszz  41669  zindbi  41671  jm2.24  41688  congrep  41698  fzneg  41707  jm2.19  41718  fzunt  42192  fzunt1d  42194  fzuntgd  42195  oddfl  43974  fzdifsuc2  44007  climsuse  44311  stoweidlem26  44729  stoweidlem34  44737  fourierdlem20  44830  fourierdlem42  44852  fourierdlem51  44860  fourierdlem64  44873  fourierdlem76  44885  fourierdlem94  44903  fourierdlem97  44906  fourierdlem113  44922  natlocalincr  45577  natglobalincr  45578  zm1nn  45997  zgeltp1eq  46004  eluzge0nn0  46007  elfz2z  46010  2elfz2melfz  46013  elfzlble  46015  elfzelfzlble  46016  fzopredsuc  46018  smonoord  46026  fsummmodsndifre  46029  iccpartipre  46076  iccpartiltu  46077  iccpartigtl  46078  icceuelpartlem  46090  fmtno4prmfac  46227  lighneallem4b  46264  dfeven3  46313  dfodd4  46314  nn0o1gt2ALTV  46349  nnoALTV  46350  fpprel2  46396  gbegt5  46416  gbowgt5  46417  sbgoldbwt  46432  nnsum3primesle9  46449  nnsum4primesodd  46451  nnsum4primesoddALTV  46452  evengpop3  46453  evengpoap3  46454  nnsum4primesevenALTV  46456  bgoldbtbndlem1  46460  bgoldbtbndlem2  46461  bgoldbtbndlem3  46462  bgoldbtbndlem4  46463  cznnring  46808  elfzolborelfzop1  47154  zgtp1leeq  47156  mod0mul  47159  modn0mul  47160  m1modmmod  47161  difmodm1lt  47162  rege1logbzge0  47199  fllog2  47208  dignn0ldlem  47242  dignn0flhalflem1  47255  dignn0flhalflem2  47256