Theorem zre 12528

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

Syntax hints:   → wi 4   ∨ w3o 1086   = wceq 1542   ∈ wcel 2114  ℝcr 11037  0cc0 11038  -cneg 11378  ℕcn 12174  ℤcz 12524

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3or 1088  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-sb 2069  df-clab 2715  df-cleq 2728  df-clel 2811  df-rab 3390  df-v 3431  df-dif 3892  df-un 3894  df-ss 3906  df-nul 4274  df-if 4467  df-sn 4568  df-pr 4570  df-op 4574  df-uni 4851  df-br 5086  df-iota 6454  df-fv 6506  df-ov 7370  df-neg 11380  df-z 12525

This theorem is referenced by:  zcn  12529  zrei  12530  zssre  12531  elnn0z  12537  elnnz1  12553  znnnlt1  12554  zletr  12571  znnsub  12573  znn0sub  12574  nzadd  12575  zltp1le  12577  zleltp1  12578  nn0ge0div  12598  zextle  12602  btwnnz  12605  suprzcl  12609  msqznn  12611  peano2uz2  12617  uzind  12621  fzind  12627  fnn0ind  12628  eluzuzle  12797  uzid  12803  uzneg  12808  uztric  12812  uz11  12813  eluzp1m1  12814  eluzp1p1  12816  eluzadd  12817  eluzsub  12818  subeluzsub  12821  uzin  12824  uz3m2nn  12844  peano2uz  12851  nn0pzuz  12855  uzwo  12861  eluz2b2  12871  uz2mulcl  12876  uzinfi  12878  eqreznegel  12884  lbzbi  12886  uzsupss  12890  nn01to3  12891  zmin  12894  zmax  12895  zbtwnre  12896  rebtwnz  12897  qre  12903  elpq  12925  rpnnen1lem2  12927  rpnnen1lem1  12928  rpnnen1lem3  12929  rpnnen1lem5  12931  z2ge  13150  qbtwnre  13151  zltaddlt1le  13458  elfz1eq  13489  fzn  13494  fzen  13495  uzsubsubfz  13500  fzaddel  13512  fzadd2  13513  ssfzunsnext  13523  ssfzunsn  13524  fzsuc2  13536  fzrev  13541  elfz1b  13547  fznuz  13563  uznfz  13564  fzp1nel  13565  elfz0fzfz0  13587  fz0fzelfz0  13588  fznn0sub2  13589  fz0fzdiffz0  13591  elfzmlbp  13593  difelfznle  13596  nelfzo  13619  elfzouz2  13629  fzo0n  13636  fzonlt0  13637  fzossrbm1  13643  fzospliti  13646  elfzo0z  13656  fzofzim  13664  fzo1fzo0n0  13670  eluzgtdifelfzo  13682  fzossfzop1  13698  ssfzoulel  13715  ssfzo12bi  13716  elfzonelfzo  13724  elfzomelpfzo  13727  elfznelfzob  13729  fzostep1  13741  fllt  13765  flid  13767  flbi2  13776  2tnp1ge0ge0  13788  flhalf  13789  fldiv4p1lem1div2  13794  fldiv4lem1div2uz2  13795  dfceil2  13798  ceile  13808  ceilid  13810  quoremz  13814  intfracq  13818  uzsup  13822  mulmod0  13836  zmod10  13846  zmodcl  13850  zmodfz  13852  zmodid2  13858  modcyc  13865  modaddid  13869  mulp1mod1  13873  muladdmod  13874  modmuladd  13875  modmuladdim  13876  modmul1  13886  modaddmodup  13896  modaddmodlo  13897  modaddmulmod  13900  zsqcl2  14100  leexp2  14133  iexpcyc  14169  fi1uzind  14469  ccatsymb  14545  ccatval21sw  14548  lswccatn0lsw  14554  swrdnd  14617  swrdnnn0nd  14619  swrd0  14621  swrdswrdlem  14666  swrdswrd  14667  swrdccatin2  14691  pfxccatin12lem2  14693  pfxccatin12lem3  14694  repswswrd  14746  cshwmodn  14757  cshwsublen  14758  cshwidxmod  14765  cshwidxmodr  14766  cshwidxm1  14769  repswcshw  14774  2cshw  14775  cshweqrep  14783  cshw1  14784  swrd2lsw  14914  nn0abscl  15274  rexuzre  15315  dvdsval3  16225  p1modz1  16228  moddvds  16232  absdvdsb  16243  dvdsabsb  16244  dvdsle  16279  alzdvds  16289  mod2eq1n2dvds  16316  evennn02n  16319  evennn2n  16320  ltoddhalfle  16330  divalgmod  16375  fldivndvdslt  16385  flodddiv4t2lthalf  16387  bitsp1o  16402  gcdabs1  16498  modgcd  16501  bezoutlem1  16508  dfgcd2  16515  algcvga  16548  lcmabs  16574  isprm3  16652  dvdsnprmd  16659  2mulprm  16662  oddprmgt2  16669  sqnprm  16672  zgcdsq  16723  hashdvds  16745  vfermltlALT  16773  powm2modprm  16774  modprm0  16776  modprmn0modprm0  16778  fldivp1  16868  zgz  16904  4sqlem4  16923  prmgaplem5  17026  prmgaplem7  17028  cshwshashlem2  17067  setsstruct  17146  mulgmodid  19089  gexdvds  19559  zringunit  21446  prmirred  21454  znf1o  21531  chfacfscmul0  22823  chfacfscmulgsum  22825  chfacfpmmul0  22827  chfacfpmmulgsum  22829  dyadf  25558  dyadovol  25560  degltlem1  26037  coskpi  26487  cosne0  26493  relogexp  26560  cxpeq  26721  relogbzexp  26740  ppival2  27091  ppival2g  27092  ppiprm  27114  chtprm  27116  chtnprm  27117  ppip1le  27124  efexple  27244  zabsle1  27259  lgsdir2lem4  27291  lgsne0  27298  gausslemma2dlem1a  27328  gausslemma2dlem3  27331  gausslemma2dlem4  27332  lgsquadlem1  27343  lgsquadlem2  27344  2lgslem1a1  27352  2lgslem1a2  27353  2sqlem2  27381  rplogsumlem2  27448  pntrsumbnd  27529  axlowdim  29030  crctcshwlkn0lem3  29880  crctcshwlkn0lem5  29882  crctcshwlkn0  29889  crctcsh  29892  clwlkclwwlklem2fv2  30066  clwlkclwwlklem2a  30068  clwwisshclwwslemlem  30083  clwwlkinwwlk  30110  clwwlkext2edg  30126  wwlksubclwwlk  30128  numclwwlk5  30458  topnfbey  30539  uzssico  32857  1fldgenq  33383  znfermltl  33426  ply1coedeg  33649  rezh  34113  zrhre  34163  hashf2  34228  ballotlemfc0  34637  ballotlemfcc  34638  chpvalz  34772  chtvalz  34773  zltp1ne  35292  0nn0m1nnn0  35295  elfzm12  35857  nn0prpwlem  36504  poimirlem24  37965  mblfinlem1  37978  mblfinlem2  37979  itg2addnclem2  37993  fzmul  38062  incsequz2  38070  fimgmcyc  42979  ellz1  43199  lzunuz  43200  lzenom  43202  nerabdioph  43237  pell14qrgt0  43287  rmxycomplete  43345  monotuz  43369  monotoddzzfi  43370  oddcomabszz  43372  zindbi  43374  jm2.24  43391  congrep  43401  fzneg  43410  jm2.19  43421  fzunt  43882  fzunt1d  43884  fzuntgd  43885  oddfl  45711  fzdifsuc2  45743  climsuse  46038  stoweidlem26  46454  stoweidlem34  46462  fourierdlem20  46555  fourierdlem42  46577  fourierdlem51  46585  fourierdlem64  46598  fourierdlem76  46610  fourierdlem94  46628  fourierdlem97  46631  fourierdlem113  46647  natlocalincr  47306  natglobalincr  47307  zm1nn  47750  zgeltp1eq  47757  eluzge0nn0  47760  elfz2z  47763  2elfz2melfz  47766  elfzlble  47768  elfzelfzlble  47769  fzopredsuc  47772  ceilbi  47785  mod0mul  47810  modn0mul  47811  m1modmmod  47812  difmodm1lt  47813  mod2addne  47818  modm2nep1  47820  modp2nep1  47821  modm1nep2  47822  modm1nem2  47823  modm1p1ne  47824  smonoord  47825  2timesltsqm1  47827  fsummmodsndifre  47830  muldvdsfacgt  47834  muldvdsfacm1  47835  iccpartipre  47881  iccpartiltu  47882  iccpartigtl  47883  icceuelpartlem  47895  fmtno4prmfac  48035  lighneallem4b  48072  nprmdvdsfacm1lem2  48084  nprmdvdsfacm1lem4  48086  dfeven3  48134  dfodd4  48135  nn0o1gt2ALTV  48170  nnoALTV  48171  fpprel2  48217  gbegt5  48237  gbowgt5  48238  sbgoldbwt  48253  nnsum3primesle9  48270  nnsum4primesodd  48272  nnsum4primesoddALTV  48273  evengpop3  48274  evengpoap3  48275  nnsum4primesevenALTV  48277  bgoldbtbndlem1  48281  bgoldbtbndlem2  48282  bgoldbtbndlem3  48283  bgoldbtbndlem4  48284  gpgprismgriedgdmss  48528  gpgusgralem  48532  gpgedgvtx1  48538  gpg5nbgrvtx03starlem2  48545  gpg5nbgrvtx13starlem2  48548  gpg3nbgrvtx0  48552  cznnring  48738  elfzolborelfzop1  48995  zgtp1leeq  48997  rege1logbzge0  49035  fllog2  49044  dignn0ldlem  49078  dignn0flhalflem1  49091  dignn0flhalflem2  49092