Theorem zre 12704

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

This proof depends on syntax axioms:   → wi 4   ∨ w3o 1102   = wceq 1569   ∈ wcel 2144  ℝcr 11206  0cc0 11207   -cneg 11549  ℕcn 12342  ℤcz 12700

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3or 1104  df-3an 1105  df-tru 1572  df-fal 1582  df-ex 1812  df-sb 2099  df-clab 2739  df-cleq 2752  df-clel 2835  df-rab 3413  df-v 3452  df-ss 3897  df-dif 4046  df-un 4150  df-nul 4278  df-if 4482  df-sn 4585  df-pr 4587  df-op 4835  df-uni 4867  df-br 5103  df-iota 6497  df-fv 6551  df-ov 7427  df-neg 11551  df-z 12701

This theorem is used by:  zcn  12705  zrei  12706  zssre  12707  elnn0z  12713  elnnz1  12729  znnnlt1  12730  zletr  12747  znnsub  12749  znn0sub  12750  nzadd  12751  zltp1le  12753  zleltp1  12754  0nn0m1nnn0  12760  nn0ge0div  12775  zextle  12779  btwnnz  12782  suprzcl  12786  msqznn  12788  peano2uz2  12794  uzind  12798  fzind  12804  fnn0ind  12805  eluzuzle  12981  uzid  12987  uzneg  12992  uztric  12996  uz11  12997  eluzp1m1  12998  eluzp1p1  13000  eluzadd  13001  eluzsub  13002  subeluzsub  13005  uzin  13008  uz3m2nn  13028  peano2uz  13035  nn0pzuz  13039  uzwo  13045  eluz2b2  13055  uz2mulcl  13060  uzinfi  13062  eqreznegel  13068  lbzbi  13070  uzsupss  13074  nn01to3  13075  zmin  13078  zmax  13079  zbtwnre  13080  rebtwnz  13081  qre  13087  elpq  13110  rpnnen1lem2  13112  rpnnen1lem1  13113  rpnnen1lem3  13114  rpnnen1lem5  13116  z2ge  13335  qbtwnre  13336  zltaddlt1le  13643  elfz1eq  13675  fzn  13680  fzen  13681  uzsubsubfz  13687  fzaddel  13699  fzadd2  13700  ssfzunsnext  13710  ssfzunsn  13711  fzsuc2  13723  fzrev  13728  elfz1b  13734  fznuz  13750  uznfz  13751  fzp1nel  13752  elfz0fzfz0  13774  fz0fzelfz0  13775  fznn0sub2  13776  fz0fzdiffz0  13778  elfzmlbp  13780  difelfznle  13783  nelfzo  13806  elfzouz2  13816  fzo0n  13823  fzonlt0  13824  fzossrbm1  13830  fzospliti  13833  elfzo0z  13843  fzofzim  13851  fzo1fzo0n0  13857  eluzgtdifelfzo  13869  fzossfzop1  13885  ssfzoulel  13902  ssfzo12bi  13903  elfzonelfzo  13911  elfzomelpfzo  13914  elfznelfzob  13916  fzostep1  13928  fllt  13953  flid  13955  flbi2  13964  2tnp1ge0ge0  13976  flhalf  13977  fldiv4p1lem1div2  13982  fldiv4lem1div2uz2  13983  dfceil2  13986  ceile  13996  ceilid  13998  quoremz  14002  intfracq  14006  uzsup  14010  mulmod0  14024  zmod10  14034  zmodcl  14038  zmodfz  14040  zmodid2  14046  modcyc  14053  modaddid  14057  mulp1mod1  14061  muladdmod  14062  modmuladd  14063  modmuladdim  14064  modmul1  14074  modaddmodup  14084  modaddmodlo  14085  modaddmulmod  14088  zsqcl2  14288  leexp2  14321  iexpcyc  14358  fi1uzind  14659  ccatsymb  14735  ccatval21sw  14738  lswccatn0lsw  14745  swrdnd  14812  swrdnnn0nd  14814  swrd0  14816  swrdswrdlem  14861  swrdswrd  14862  swrdccatin2  14886  pfxccatin12lem2  14888  pfxccatin12lem3  14889  repswswrd  14943  cshwmodn  14954  cshwsublen  14955  cshwidxmod  14962  cshwidxmodr  14963  cshwidxm1  14966  repswcshw  14971  2cshw  14972  cshweqrep  14980  cshw1  14981  swrd2lsw  15114  nn0abscl  15488  rexuzre  15529  dvdsval3  16435  p1modz1  16438  moddvds  16442  absdvdsb  16453  dvdsabsb  16454  dvdsle  16489  alzdvds  16499  mod2eq1n2dvds  16526  evennn02n  16529  evennn2n  16530  ltoddhalfle  16540  divalgmod  16585  fldivndvdslt  16595  flodddiv4t2lthalf  16597  bitsp1o  16612  gcdabs1  16711  modgcd  16714  bezoutlem1  16721  dfgcd2  16728  algcvga  16763  lcmabs  16789  isprm3  16867  dvdsnprmd  16874  2mulprm  16877  oddprmgt2  16884  sqnprm  16887  zgcdsq  16938  hashdvds  16961  vfermltlALT  16989  powm2modprm  16990  modprm0  16992  modprmn0modprm0  16994  fldivp1  17084  zgz  17120  4sqlem4  17139  prmgaplem5  17242  prmgaplem7  17244  cshwshashlem2  17283  setsstruct  17363  mulgmodid  19332  gexdvds  19807  zringunit  21781  prmirred  21789  znf1o  21866  chfacfscmul0  23185  chfacfscmulgsum  23187  chfacfpmmul0  23189  chfacfpmmulgsum  23191  dyadf  25921  dyadovol  25923  degltlem1  26399  coskpi  26860  cosne0  26866  relogexp  26933  cxpeq  27094  relogbzexp  27113  ppival2  27464  ppival2g  27465  ppiprm  27487  chtprm  27489  chtnprm  27490  ppip1le  27497  efexple  27617  zabsle1  27632  lgsdir2lem4  27664  lgsne0  27671  gausslemma2dlem1a  27701  gausslemma2dlem3  27704  gausslemma2dlem4  27705  lgsquadlem1  27716  lgsquadlem2  27717  2lgslem1a1  27725  2lgslem1a2  27726  2sqlem2  27754  rplogsumlem2  27821  pntrsumbnd  27902  fltoprmgt3  28005  axlowdim  29548  crctcshwlkn0lem3  30410  crctcshwlkn0lem5  30412  crctcshwlkn0  30419  crctcsh  30422  clwlkclwwlklem2fv2  30596  clwlkclwwlklem2a  30598  clwwisshclwwslemlem  30613  clwwlkinwwlk  30640  clwwlkext2edg  30656  wwlksubclwwlk  30658  numclwwlk5  30998  topnfbey  31079  uzssico  33426  1fldgenq  33934  znfermltl  33972  ply1coedeg  34171  rezh  34651  zrhre  34701  hashf2  34766  ballotlemfc0  35175  ballotlemfcc  35176  chpvalz  35307  chtvalz  35308  zltp1ne  36008  elfzm12  36558  nn0prpwlem  37234  poimirlem24  38699  mblfinlem1  38712  mblfinlem2  38713  itg2addnclem2  38727  fzmul  38812  incsequz2  38820  fimgmcyc  43735  ellz1  43915  lzunuz  43916  lzenom  43918  nerabdioph  43953  pell14qrgt0  44003  rmxycomplete  44061  monotuz  44085  monotoddzzfi  44086  oddcomabszz  44088  zindbi  44090  jm2.24  44107  congrep  44117  fzneg  44126  jm2.19  44137  fzunt  44593  fzunt1d  44595  fzuntgd  44596  oddfl  46430  fzdifsuc2  46462  climsuse  46756  stoweidlem26  47172  stoweidlem34  47180  fourierdlem20  47273  fourierdlem42  47295  fourierdlem51  47303  fourierdlem64  47316  fourierdlem76  47328  fourierdlem94  47346  fourierdlem97  47349  fourierdlem113  47365  zm1nn  48508  zgeltp1eq  48515  eluzge0nn0  48518  elfz2z  48521  2elfz2melfz  48524  elfzlble  48526  elfzelfzlble  48527  fzopredsuc  48530  ceilbi  48543  mod0mul  48568  modn0mul  48569  m1modmmod  48570  difmodm1lt  48571  mod2addne  48576  modm2nep1  48578  modp2nep1  48579  modm1nep2  48580  modm1nem2  48581  modm1p1ne  48582  smonoord  48583  2timesltsqm1  48585  fsummmodsndifre  48588  muldvdsfacgt  48592  muldvdsfacm1  48593  iccpartipre  48639  iccpartiltu  48640  iccpartigtl  48641  icceuelpartlem  48653  fmtno4prmfac  48793  lighneallem4b  48830  nprmdvdsfacm1lem2  48842  nprmdvdsfacm1lem4  48844  dfeven3  48892  dfodd4  48893  nn0o1gt2ALTV  48928  nnoALTV  48929  fpprel2  48975  gbegt5  48995  gbowgt5  48996  sbgoldbwt  49011  nnsum3primesle9  49028  nnsum4primesodd  49030  nnsum4primesoddALTV  49031  evengpop3  49032  evengpoap3  49033  nnsum4primesevenALTV  49035  bgoldbtbndlem1  49039  bgoldbtbndlem2  49040  bgoldbtbndlem3  49041  bgoldbtbndlem4  49042  gpgprismgriedgdmss  49286  gpgusgralem  49290  gpgedgvtx1  49296  gpg5nbgrvtx03starlem2  49303  gpg5nbgrvtx13starlem2  49306  gpg3nbgrvtx0  49310  cznnring  49495  elfzolborelfzop1  49767  zgtp1leeq  49769  rege1logbzge0  49807  fllog2  49816  dignn0ldlem  49850  dignn0flhalflem1  49863  dignn0flhalflem2  49864