Theorem zre 12519

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

Syntax hints:   → wi 4   ∨ w3o 1091   = wceq 1547   ∈ wcel 2119  ℝcr 11028  0cc0 11029  -cneg 11369  ℕcn 12165  ℤcz 12515

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-ext 2711

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 854  df-3or 1093  df-3an 1094  df-tru 1550  df-fal 1560  df-ex 1787  df-sb 2074  df-clab 2718  df-cleq 2731  df-clel 2814  df-rab 3392  df-v 3433  df-dif 3886  df-un 3888  df-ss 3900  df-nul 4262  df-if 4455  df-sn 4556  df-pr 4558  df-op 4562  df-uni 4839  df-br 5073  df-iota 6441  df-fv 6493  df-ov 7359  df-neg 11371  df-z 12516

This theorem is referenced by:  zcn  12520  zrei  12521  zssre  12522  elnn0z  12528  elnnz1  12544  znnnlt1  12545  zletr  12562  znnsub  12564  znn0sub  12565  nzadd  12566  zltp1le  12568  zleltp1  12569  nn0ge0div  12589  zextle  12593  btwnnz  12596  suprzcl  12600  msqznn  12602  peano2uz2  12608  uzind  12612  fzind  12618  fnn0ind  12619  eluzuzle  12788  uzid  12794  uzneg  12799  uztric  12803  uz11  12804  eluzp1m1  12805  eluzp1p1  12807  eluzadd  12808  eluzsub  12809  subeluzsub  12812  uzin  12815  uz3m2nn  12835  peano2uz  12842  nn0pzuz  12846  uzwo  12852  eluz2b2  12862  uz2mulcl  12867  uzinfi  12869  eqreznegel  12875  lbzbi  12877  uzsupss  12881  nn01to3  12882  zmin  12885  zmax  12886  zbtwnre  12887  rebtwnz  12888  qre  12894  elpq  12916  rpnnen1lem2  12918  rpnnen1lem1  12919  rpnnen1lem3  12920  rpnnen1lem5  12922  z2ge  13141  qbtwnre  13142  zltaddlt1le  13449  elfz1eq  13480  fzn  13485  fzen  13486  uzsubsubfz  13491  fzaddel  13503  fzadd2  13504  ssfzunsnext  13514  ssfzunsn  13515  fzsuc2  13527  fzrev  13532  elfz1b  13538  fznuz  13554  uznfz  13555  fzp1nel  13556  elfz0fzfz0  13578  fz0fzelfz0  13579  fznn0sub2  13580  fz0fzdiffz0  13582  elfzmlbp  13584  difelfznle  13587  nelfzo  13610  elfzouz2  13620  fzo0n  13627  fzonlt0  13628  fzossrbm1  13634  fzospliti  13637  elfzo0z  13647  fzofzim  13655  fzo1fzo0n0  13661  eluzgtdifelfzo  13673  fzossfzop1  13689  ssfzoulel  13706  ssfzo12bi  13707  elfzonelfzo  13715  elfzomelpfzo  13718  elfznelfzob  13720  fzostep1  13732  fllt  13756  flid  13758  flbi2  13767  2tnp1ge0ge0  13779  flhalf  13780  fldiv4p1lem1div2  13785  fldiv4lem1div2uz2  13786  dfceil2  13789  ceile  13799  ceilid  13801  quoremz  13805  intfracq  13809  uzsup  13813  mulmod0  13827  zmod10  13837  zmodcl  13841  zmodfz  13843  zmodid2  13849  modcyc  13856  modaddid  13860  mulp1mod1  13864  muladdmod  13865  modmuladd  13866  modmuladdim  13867  modmul1  13877  modaddmodup  13887  modaddmodlo  13888  modaddmulmod  13891  zsqcl2  14091  leexp2  14124  iexpcyc  14160  fi1uzind  14460  ccatsymb  14536  ccatval21sw  14539  lswccatn0lsw  14545  swrdnd  14608  swrdnnn0nd  14610  swrd0  14612  swrdswrdlem  14657  swrdswrd  14658  swrdccatin2  14682  pfxccatin12lem2  14684  pfxccatin12lem3  14685  repswswrd  14737  cshwmodn  14748  cshwsublen  14749  cshwidxmod  14756  cshwidxmodr  14757  cshwidxm1  14760  repswcshw  14765  2cshw  14766  cshweqrep  14774  cshw1  14775  swrd2lsw  14905  nn0abscl  15265  rexuzre  15306  dvdsval3  16216  p1modz1  16219  moddvds  16223  absdvdsb  16234  dvdsabsb  16235  dvdsle  16270  alzdvds  16280  mod2eq1n2dvds  16307  evennn02n  16310  evennn2n  16311  ltoddhalfle  16321  divalgmod  16366  fldivndvdslt  16376  flodddiv4t2lthalf  16378  bitsp1o  16393  gcdabs1  16489  modgcd  16492  bezoutlem1  16499  dfgcd2  16506  algcvga  16539  lcmabs  16565  isprm3  16643  dvdsnprmd  16650  2mulprm  16653  oddprmgt2  16660  sqnprm  16663  zgcdsq  16714  hashdvds  16736  vfermltlALT  16764  powm2modprm  16765  modprm0  16767  modprmn0modprm0  16769  fldivp1  16859  zgz  16895  4sqlem4  16914  prmgaplem5  17017  prmgaplem7  17019  cshwshashlem2  17058  setsstruct  17137  mulgmodid  19080  gexdvds  19550  zringunit  21441  prmirred  21449  znf1o  21526  chfacfscmul0  22841  chfacfscmulgsum  22843  chfacfpmmul0  22845  chfacfpmmulgsum  22847  dyadf  25576  dyadovol  25578  degltlem1  26055  coskpi  26505  cosne0  26511  relogexp  26578  cxpeq  26739  relogbzexp  26758  ppival2  27109  ppival2g  27110  ppiprm  27132  chtprm  27134  chtnprm  27135  ppip1le  27142  efexple  27262  zabsle1  27277  lgsdir2lem4  27309  lgsne0  27316  gausslemma2dlem1a  27346  gausslemma2dlem3  27349  gausslemma2dlem4  27350  lgsquadlem1  27361  lgsquadlem2  27362  2lgslem1a1  27370  2lgslem1a2  27371  2sqlem2  27399  rplogsumlem2  27466  pntrsumbnd  27547  axlowdim  29048  crctcshwlkn0lem3  29898  crctcshwlkn0lem5  29900  crctcshwlkn0  29907  crctcsh  29910  clwlkclwwlklem2fv2  30084  clwlkclwwlklem2a  30086  clwwisshclwwslemlem  30101  clwwlkinwwlk  30128  clwwlkext2edg  30144  wwlksubclwwlk  30146  numclwwlk5  30476  topnfbey  30557  uzssico  32876  1fldgenq  33406  znfermltl  33449  ply1coedeg  33672  rezh  34153  zrhre  34203  hashf2  34268  ballotlemfc0  34677  ballotlemfcc  34678  chpvalz  34812  chtvalz  34813  zltp1ne  35338  0nn0m1nnn0  35341  elfzm12  35903  nn0prpwlem  36550  poimirlem24  38011  mblfinlem1  38024  mblfinlem2  38025  itg2addnclem2  38039  fzmul  38108  incsequz2  38116  fimgmcyc  43020  ellz1  43216  lzunuz  43217  lzenom  43219  nerabdioph  43254  pell14qrgt0  43304  rmxycomplete  43362  monotuz  43386  monotoddzzfi  43387  oddcomabszz  43389  zindbi  43391  jm2.24  43408  congrep  43418  fzneg  43427  jm2.19  43438  fzunt  43899  fzunt1d  43901  fzuntgd  43902  oddfl  45726  fzdifsuc2  45758  climsuse  46053  stoweidlem26  46469  stoweidlem34  46477  fourierdlem20  46570  fourierdlem42  46592  fourierdlem51  46600  fourierdlem64  46613  fourierdlem76  46625  fourierdlem94  46643  fourierdlem97  46646  fourierdlem113  46662  natlocalincr  47321  natglobalincr  47322  zm1nn  47765  zgeltp1eq  47772  eluzge0nn0  47775  elfz2z  47778  2elfz2melfz  47781  elfzlble  47783  elfzelfzlble  47784  fzopredsuc  47787  ceilbi  47800  mod0mul  47825  modn0mul  47826  m1modmmod  47827  difmodm1lt  47828  mod2addne  47833  modm2nep1  47835  modp2nep1  47836  modm1nep2  47837  modm1nem2  47838  modm1p1ne  47839  smonoord  47840  2timesltsqm1  47842  fsummmodsndifre  47845  muldvdsfacgt  47849  muldvdsfacm1  47850  iccpartipre  47896  iccpartiltu  47897  iccpartigtl  47898  icceuelpartlem  47910  fmtno4prmfac  48050  lighneallem4b  48087  nprmdvdsfacm1lem2  48099  nprmdvdsfacm1lem4  48101  dfeven3  48149  dfodd4  48150  nn0o1gt2ALTV  48185  nnoALTV  48186  fpprel2  48232  gbegt5  48252  gbowgt5  48253  sbgoldbwt  48268  nnsum3primesle9  48285  nnsum4primesodd  48287  nnsum4primesoddALTV  48288  evengpop3  48289  evengpoap3  48290  nnsum4primesevenALTV  48292  bgoldbtbndlem1  48296  bgoldbtbndlem2  48297  bgoldbtbndlem3  48298  bgoldbtbndlem4  48299  gpgprismgriedgdmss  48543  gpgusgralem  48547  gpgedgvtx1  48553  gpg5nbgrvtx03starlem2  48560  gpg5nbgrvtx13starlem2  48563  gpg3nbgrvtx0  48567  cznnring  48753  elfzolborelfzop1  49010  zgtp1leeq  49012  rege1logbzge0  49050  fllog2  49059  dignn0ldlem  49093  dignn0flhalflem1  49106  dignn0flhalflem2  49107