Theorem zre 12475

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

Syntax hints:   → wi 4   ∨ w3o 1085   = wceq 1540   ∈ wcel 2109  ℝcr 11008  0cc0 11009  -cneg 11348  ℕcn 12128  ℤcz 12471

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-rab 3395  df-v 3438  df-dif 3906  df-un 3908  df-ss 3920  df-nul 4285  df-if 4477  df-sn 4578  df-pr 4580  df-op 4584  df-uni 4859  df-br 5093  df-iota 6438  df-fv 6490  df-ov 7352  df-neg 11350  df-z 12472

This theorem is referenced by:  zcn  12476  zrei  12477  zssre  12478  elnn0z  12484  elnnz1  12501  znnnlt1  12502  zletr  12519  znnsub  12521  znn0sub  12522  nzadd  12523  zltp1le  12525  zleltp1  12526  nn0ge0div  12545  zextle  12549  btwnnz  12552  suprzcl  12556  msqznn  12558  peano2uz2  12564  uzind  12568  fzind  12574  fnn0ind  12575  eluzuzle  12744  uzid  12750  uzneg  12755  uztric  12759  uz11  12760  eluzp1m1  12761  eluzp1p1  12763  eluzadd  12764  eluzsub  12765  eluzaddiOLD  12767  eluzsubiOLD  12769  subeluzsub  12772  uzin  12775  uz3m2nn  12795  peano2uz  12802  nn0pzuz  12806  uzwo  12812  eluz2b2  12822  uz2mulcl  12827  uzinfi  12829  eqreznegel  12835  lbzbi  12837  uzsupss  12841  nn01to3  12842  zmin  12845  zmax  12846  zbtwnre  12847  rebtwnz  12848  qre  12854  elpq  12876  rpnnen1lem2  12878  rpnnen1lem1  12879  rpnnen1lem3  12880  rpnnen1lem5  12882  z2ge  13100  qbtwnre  13101  zltaddlt1le  13408  elfz1eq  13438  fzn  13443  fzen  13444  uzsubsubfz  13449  fzaddel  13461  fzadd2  13462  ssfzunsnext  13472  ssfzunsn  13473  fzsuc2  13485  fzrev  13490  elfz1b  13496  fznuz  13512  uznfz  13513  fzp1nel  13514  elfz0fzfz0  13536  fz0fzelfz0  13537  fznn0sub2  13538  fz0fzdiffz0  13540  elfzmlbp  13542  difelfznle  13545  nelfzo  13567  elfzouz2  13577  fzo0n  13584  fzonlt0  13585  fzossrbm1  13591  fzospliti  13594  elfzo0z  13604  fzofzim  13612  fzo1fzo0n0  13618  eluzgtdifelfzo  13630  fzossfzop1  13646  ssfzoulel  13663  ssfzo12bi  13664  elfzonelfzo  13672  elfzomelpfzo  13674  elfznelfzob  13676  fzostep1  13686  fllt  13710  flid  13712  flbi2  13721  2tnp1ge0ge0  13733  flhalf  13734  fldiv4p1lem1div2  13739  fldiv4lem1div2uz2  13740  dfceil2  13743  ceile  13753  ceilid  13755  quoremz  13759  intfracq  13763  uzsup  13767  mulmod0  13781  zmod10  13791  zmodcl  13795  zmodfz  13797  zmodid2  13803  modcyc  13810  modaddid  13814  mulp1mod1  13818  muladdmod  13819  modmuladd  13820  modmuladdim  13821  modmul1  13831  modaddmodup  13841  modaddmodlo  13842  modaddmulmod  13845  zsqcl2  14045  leexp2  14078  iexpcyc  14114  fi1uzind  14414  ccatsymb  14489  ccatval21sw  14492  lswccatn0lsw  14498  swrdnd  14561  swrdnnn0nd  14563  swrd0  14565  swrdswrdlem  14610  swrdswrd  14611  swrdccatin2  14635  pfxccatin12lem2  14637  pfxccatin12lem3  14638  repswswrd  14690  cshwmodn  14701  cshwsublen  14702  cshwidxmod  14709  cshwidxmodr  14710  cshwidxm1  14713  repswcshw  14718  2cshw  14719  cshweqrep  14727  cshw1  14728  swrd2lsw  14859  nn0abscl  15219  rexuzre  15260  dvdsval3  16167  p1modz1  16170  moddvds  16174  absdvdsb  16185  dvdsabsb  16186  dvdsle  16221  alzdvds  16231  mod2eq1n2dvds  16258  evennn02n  16261  evennn2n  16262  ltoddhalfle  16272  divalgmod  16317  fldivndvdslt  16327  flodddiv4t2lthalf  16329  bitsp1o  16344  gcdabs1  16440  modgcd  16443  bezoutlem1  16450  dfgcd2  16457  algcvga  16490  lcmabs  16516  isprm3  16594  dvdsnprmd  16601  2mulprm  16604  oddprmgt2  16610  sqnprm  16613  zgcdsq  16664  hashdvds  16686  vfermltlALT  16714  powm2modprm  16715  modprm0  16717  modprmn0modprm0  16719  fldivp1  16809  zgz  16845  4sqlem4  16864  prmgaplem5  16967  prmgaplem7  16969  cshwshashlem2  17008  setsstruct  17087  mulgmodid  18992  gexdvds  19463  zringunit  21373  prmirred  21381  znf1o  21458  chfacfscmul0  22743  chfacfscmulgsum  22745  chfacfpmmul0  22747  chfacfpmmulgsum  22749  dyadf  25490  dyadovol  25492  degltlem1  25975  coskpi  26430  cosne0  26436  relogexp  26503  cxpeq  26665  relogbzexp  26684  ppival2  27036  ppival2g  27037  ppiprm  27059  chtprm  27061  chtnprm  27062  ppip1le  27069  efexple  27190  zabsle1  27205  lgsdir2lem4  27237  lgsne0  27244  gausslemma2dlem1a  27274  gausslemma2dlem3  27277  gausslemma2dlem4  27278  lgsquadlem1  27289  lgsquadlem2  27290  2lgslem1a1  27298  2lgslem1a2  27299  2sqlem2  27327  rplogsumlem2  27394  pntrsumbnd  27475  axlowdim  28906  crctcshwlkn0lem3  29757  crctcshwlkn0lem5  29759  crctcshwlkn0  29766  crctcsh  29769  clwlkclwwlklem2fv2  29940  clwlkclwwlklem2a  29942  clwwisshclwwslemlem  29957  clwwlkinwwlk  29984  clwwlkext2edg  30000  wwlksubclwwlk  30002  numclwwlk5  30332  topnfbey  30413  uzssico  32727  1fldgenq  33261  znfermltl  33303  rezh  33936  zrhre  33986  hashf2  34051  ballotlemfc0  34461  ballotlemfcc  34462  chpvalz  34596  chtvalz  34597  zltp1ne  35087  0nn0m1nnn0  35090  elfzm12  35652  nn0prpwlem  36300  poimirlem24  37628  mblfinlem1  37641  mblfinlem2  37642  itg2addnclem2  37656  fzmul  37725  incsequz2  37733  fimgmcyc  42511  ellz1  42744  lzunuz  42745  lzenom  42747  nerabdioph  42786  pell14qrgt0  42836  rmxycomplete  42894  monotuz  42918  monotoddzzfi  42919  oddcomabszz  42921  zindbi  42923  jm2.24  42940  congrep  42950  fzneg  42959  jm2.19  42970  fzunt  43432  fzunt1d  43434  fzuntgd  43435  oddfl  45264  fzdifsuc2  45296  climsuse  45593  stoweidlem26  46011  stoweidlem34  46019  fourierdlem20  46112  fourierdlem42  46134  fourierdlem51  46142  fourierdlem64  46155  fourierdlem76  46167  fourierdlem94  46185  fourierdlem97  46188  fourierdlem113  46204  natlocalincr  46861  natglobalincr  46862  zm1nn  47290  zgeltp1eq  47297  eluzge0nn0  47300  elfz2z  47303  2elfz2melfz  47306  elfzlble  47308  elfzelfzlble  47309  fzopredsuc  47311  ceilbi  47321  mod0mul  47344  modn0mul  47345  m1modmmod  47346  difmodm1lt  47347  mod2addne  47352  modm2nep1  47354  modp2nep1  47355  modm1nep2  47356  modm1nem2  47357  modm1p1ne  47358  smonoord  47359  fsummmodsndifre  47362  iccpartipre  47409  iccpartiltu  47410  iccpartigtl  47411  icceuelpartlem  47423  fmtno4prmfac  47560  lighneallem4b  47597  dfeven3  47646  dfodd4  47647  nn0o1gt2ALTV  47682  nnoALTV  47683  fpprel2  47729  gbegt5  47749  gbowgt5  47750  sbgoldbwt  47765  nnsum3primesle9  47782  nnsum4primesodd  47784  nnsum4primesoddALTV  47785  evengpop3  47786  evengpoap3  47787  nnsum4primesevenALTV  47789  bgoldbtbndlem1  47793  bgoldbtbndlem2  47794  bgoldbtbndlem3  47795  bgoldbtbndlem4  47796  gpgprismgriedgdmss  48040  gpgusgralem  48044  gpgedgvtx1  48050  gpg5nbgrvtx03starlem2  48057  gpg5nbgrvtx13starlem2  48060  gpg3nbgrvtx0  48064  cznnring  48250  elfzolborelfzop1  48508  zgtp1leeq  48510  rege1logbzge0  48548  fllog2  48557  dignn0ldlem  48591  dignn0flhalflem1  48604  dignn0flhalflem2  48605