Theorem zre 12572

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

Syntax hints:   → wi 4   ∨ w3o 1097   = wceq 1560   ∈ wcel 2142  ℝcr 11072  0cc0 11073  -cneg 11415  ℕcn 12210  ℤcz 12568

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1815  ax-4 1829  ax-5 1930  ax-6 1987  ax-7 2028  ax-8 2144  ax-9 2152  ax-ext 2734

This theorem depends on definitions:  df-bi 209  df-an 400  df-or 859  df-3or 1099  df-3an 1100  df-tru 1563  df-fal 1573  df-ex 1800  df-sb 2091  df-clab 2741  df-cleq 2754  df-clel 2837  df-rab 3415  df-v 3456  df-dif 3907  df-un 3909  df-ss 3921  df-nul 4286  df-if 4481  df-sn 4583  df-pr 4585  df-op 4589  df-uni 4866  df-br 5101  df-iota 6477  df-fv 6529  df-ov 7399  df-neg 11417  df-z 12569

This theorem is referenced by:  zcn  12573  zrei  12574  zssre  12575  elnn0z  12581  elnnz1  12597  znnnlt1  12598  zletr  12615  znnsub  12617  znn0sub  12618  nzadd  12619  zltp1le  12621  zleltp1  12622  nn0ge0div  12642  zextle  12646  btwnnz  12649  suprzcl  12653  msqznn  12655  peano2uz2  12661  uzind  12665  fzind  12671  fnn0ind  12672  eluzuzle  12848  uzid  12854  uzneg  12859  uztric  12863  uz11  12864  eluzp1m1  12865  eluzp1p1  12867  eluzadd  12868  eluzsub  12869  subeluzsub  12872  uzin  12875  uz3m2nn  12895  peano2uz  12902  nn0pzuz  12906  uzwo  12912  eluz2b2  12922  uz2mulcl  12927  uzinfi  12929  eqreznegel  12935  lbzbi  12937  uzsupss  12941  nn01to3  12942  zmin  12945  zmax  12946  zbtwnre  12947  rebtwnz  12948  qre  12954  elpq  12976  rpnnen1lem2  12978  rpnnen1lem1  12979  rpnnen1lem3  12980  rpnnen1lem5  12982  z2ge  13201  qbtwnre  13202  zltaddlt1le  13509  elfz1eq  13540  fzn  13545  fzen  13546  uzsubsubfz  13551  fzaddel  13563  fzadd2  13564  ssfzunsnext  13574  ssfzunsn  13575  fzsuc2  13587  fzrev  13592  elfz1b  13598  fznuz  13614  uznfz  13615  fzp1nel  13616  elfz0fzfz0  13638  fz0fzelfz0  13639  fznn0sub2  13640  fz0fzdiffz0  13642  elfzmlbp  13644  difelfznle  13647  nelfzo  13670  elfzouz2  13680  fzo0n  13687  fzonlt0  13688  fzossrbm1  13694  fzospliti  13697  elfzo0z  13707  fzofzim  13715  fzo1fzo0n0  13721  eluzgtdifelfzo  13733  fzossfzop1  13749  ssfzoulel  13766  ssfzo12bi  13767  elfzonelfzo  13775  elfzomelpfzo  13778  elfznelfzob  13780  fzostep1  13792  fllt  13816  flid  13818  flbi2  13827  2tnp1ge0ge0  13839  flhalf  13840  fldiv4p1lem1div2  13845  fldiv4lem1div2uz2  13846  dfceil2  13849  ceile  13859  ceilid  13861  quoremz  13865  intfracq  13869  uzsup  13873  mulmod0  13887  zmod10  13897  zmodcl  13901  zmodfz  13903  zmodid2  13909  modcyc  13916  modaddid  13920  mulp1mod1  13924  muladdmod  13925  modmuladd  13926  modmuladdim  13927  modmul1  13937  modaddmodup  13947  modaddmodlo  13948  modaddmulmod  13951  zsqcl2  14151  leexp2  14184  iexpcyc  14220  fi1uzind  14520  ccatsymb  14596  ccatval21sw  14599  lswccatn0lsw  14605  swrdnd  14668  swrdnnn0nd  14670  swrd0  14672  swrdswrdlem  14717  swrdswrd  14718  swrdccatin2  14742  pfxccatin12lem2  14744  pfxccatin12lem3  14745  repswswrd  14797  cshwmodn  14808  cshwsublen  14809  cshwidxmod  14816  cshwidxmodr  14817  cshwidxm1  14820  repswcshw  14825  2cshw  14826  cshweqrep  14834  cshw1  14835  swrd2lsw  14965  nn0abscl  15339  rexuzre  15380  dvdsval3  16290  p1modz1  16293  moddvds  16297  absdvdsb  16308  dvdsabsb  16309  dvdsle  16344  alzdvds  16354  mod2eq1n2dvds  16381  evennn02n  16384  evennn2n  16385  ltoddhalfle  16395  divalgmod  16440  fldivndvdslt  16450  flodddiv4t2lthalf  16452  bitsp1o  16467  gcdabs1  16563  modgcd  16566  bezoutlem1  16573  dfgcd2  16580  algcvga  16613  lcmabs  16639  isprm3  16717  dvdsnprmd  16724  2mulprm  16727  oddprmgt2  16734  sqnprm  16737  zgcdsq  16788  hashdvds  16810  vfermltlALT  16838  powm2modprm  16839  modprm0  16841  modprmn0modprm0  16843  fldivp1  16933  zgz  16969  4sqlem4  16988  prmgaplem5  17091  prmgaplem7  17093  cshwshashlem2  17132  setsstruct  17212  mulgmodid  19155  gexdvds  19624  zringunit  21518  prmirred  21526  znf1o  21603  chfacfscmul0  22918  chfacfscmulgsum  22920  chfacfpmmul0  22922  chfacfpmmulgsum  22924  dyadf  25653  dyadovol  25655  degltlem1  26132  coskpi  26588  cosne0  26594  relogexp  26661  cxpeq  26822  relogbzexp  26841  ppival2  27192  ppival2g  27193  ppiprm  27215  chtprm  27217  chtnprm  27218  ppip1le  27225  efexple  27345  zabsle1  27360  lgsdir2lem4  27392  lgsne0  27399  gausslemma2dlem1a  27429  gausslemma2dlem3  27432  gausslemma2dlem4  27433  lgsquadlem1  27444  lgsquadlem2  27445  2lgslem1a1  27453  2lgslem1a2  27454  2sqlem2  27482  rplogsumlem2  27549  pntrsumbnd  27630  axlowdim  29162  crctcshwlkn0lem3  30012  crctcshwlkn0lem5  30014  crctcshwlkn0  30021  crctcsh  30024  clwlkclwwlklem2fv2  30198  clwlkclwwlklem2a  30200  clwwisshclwwslemlem  30215  clwwlkinwwlk  30242  clwwlkext2edg  30258  wwlksubclwwlk  30260  numclwwlk5  30590  topnfbey  30671  uzssico  32986  1fldgenq  33509  znfermltl  33552  ply1coedeg  33785  rezh  34266  zrhre  34316  hashf2  34381  ballotlemfc0  34790  ballotlemfcc  34791  chpvalz  34922  chtvalz  34923  zltp1ne  35460  0nn0m1nnn0  35463  elfzm12  36025  nn0prpwlem  36682  poimirlem24  38143  mblfinlem1  38156  mblfinlem2  38157  itg2addnclem2  38171  fzmul  38240  incsequz2  38248  fimgmcyc  43152  ellz1  43348  lzunuz  43349  lzenom  43351  nerabdioph  43386  pell14qrgt0  43436  rmxycomplete  43494  monotuz  43518  monotoddzzfi  43519  oddcomabszz  43521  zindbi  43523  jm2.24  43540  congrep  43550  fzneg  43559  jm2.19  43570  fzunt  44031  fzunt1d  44033  fzuntgd  44034  oddfl  45857  fzdifsuc2  45889  climsuse  46184  stoweidlem26  46600  stoweidlem34  46608  fourierdlem20  46701  fourierdlem42  46723  fourierdlem51  46731  fourierdlem64  46744  fourierdlem76  46756  fourierdlem94  46774  fourierdlem97  46777  fourierdlem113  46793  natlocalincr  47452  natglobalincr  47453  zm1nn  47896  zgeltp1eq  47903  eluzge0nn0  47906  elfz2z  47909  2elfz2melfz  47912  elfzlble  47914  elfzelfzlble  47915  fzopredsuc  47918  ceilbi  47931  mod0mul  47956  modn0mul  47957  m1modmmod  47958  difmodm1lt  47959  mod2addne  47964  modm2nep1  47966  modp2nep1  47967  modm1nep2  47968  modm1nem2  47969  modm1p1ne  47970  smonoord  47971  2timesltsqm1  47973  fsummmodsndifre  47976  muldvdsfacgt  47980  muldvdsfacm1  47981  iccpartipre  48027  iccpartiltu  48028  iccpartigtl  48029  icceuelpartlem  48041  fmtno4prmfac  48181  lighneallem4b  48218  nprmdvdsfacm1lem2  48230  nprmdvdsfacm1lem4  48232  dfeven3  48280  dfodd4  48281  nn0o1gt2ALTV  48316  nnoALTV  48317  fpprel2  48363  gbegt5  48383  gbowgt5  48384  sbgoldbwt  48399  nnsum3primesle9  48416  nnsum4primesodd  48418  nnsum4primesoddALTV  48419  evengpop3  48420  evengpoap3  48421  nnsum4primesevenALTV  48423  bgoldbtbndlem1  48427  bgoldbtbndlem2  48428  bgoldbtbndlem3  48429  bgoldbtbndlem4  48430  gpgprismgriedgdmss  48674  gpgusgralem  48678  gpgedgvtx1  48684  gpg5nbgrvtx03starlem2  48691  gpg5nbgrvtx13starlem2  48694  gpg3nbgrvtx0  48698  cznnring  48884  elfzolborelfzop1  49141  zgtp1leeq  49143  rege1logbzge0  49181  fllog2  49190  dignn0ldlem  49224  dignn0flhalflem1  49237  dignn0flhalflem2  49238