Theorem zre 12610

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

This proof depends on syntax axioms:   → wi 4   ∨ w3o 1102   = wceq 1570   ∈ wcel 2146  ℝcr 11114  0cc0 11115  -cneg 11457  ℕcn 12248  ℤcz 12606

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2148  ax-9 2156  ax-ext 2737

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3or 1104  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-sb 2100  df-clab 2744  df-cleq 2757  df-clel 2840  df-rab 3419  df-v 3459  df-dif 3909  df-un 3911  df-ss 3923  df-nul 4287  df-if 4490  df-sn 4592  df-pr 4594  df-op 4598  df-uni 4875  df-br 5112  df-iota 6496  df-fv 6548  df-ov 7422  df-neg 11459  df-z 12607

This theorem is used by:  zcn  12611  zrei  12612  zssre  12613  elnn0z  12619  elnnz1  12635  znnnlt1  12636  zletr  12653  znnsub  12655  znn0sub  12656  nzadd  12657  zltp1le  12659  zleltp1  12660  0nn0m1nnn0  12666  nn0ge0div  12681  zextle  12685  btwnnz  12688  suprzcl  12692  msqznn  12694  peano2uz2  12700  uzind  12704  fzind  12710  fnn0ind  12711  eluzuzle  12887  uzid  12893  uzneg  12898  uztric  12902  uz11  12903  eluzp1m1  12904  eluzp1p1  12906  eluzadd  12907  eluzsub  12908  subeluzsub  12911  uzin  12914  uz3m2nn  12934  peano2uz  12941  nn0pzuz  12945  uzwo  12951  eluz2b2  12961  uz2mulcl  12966  uzinfi  12968  eqreznegel  12974  lbzbi  12976  uzsupss  12980  nn01to3  12981  zmin  12984  zmax  12985  zbtwnre  12986  rebtwnz  12987  qre  12993  elpq  13015  rpnnen1lem2  13017  rpnnen1lem1  13018  rpnnen1lem3  13019  rpnnen1lem5  13021  z2ge  13240  qbtwnre  13241  zltaddlt1le  13548  elfz1eq  13579  fzn  13584  fzen  13585  uzsubsubfz  13591  fzaddel  13603  fzadd2  13604  ssfzunsnext  13614  ssfzunsn  13615  fzsuc2  13627  fzrev  13632  elfz1b  13638  fznuz  13654  uznfz  13655  fzp1nel  13656  elfz0fzfz0  13678  fz0fzelfz0  13679  fznn0sub2  13680  fz0fzdiffz0  13682  elfzmlbp  13684  difelfznle  13687  nelfzo  13710  elfzouz2  13720  fzo0n  13727  fzonlt0  13728  fzossrbm1  13734  fzospliti  13737  elfzo0z  13747  fzofzim  13755  fzo1fzo0n0  13761  eluzgtdifelfzo  13773  fzossfzop1  13789  ssfzoulel  13806  ssfzo12bi  13807  elfzonelfzo  13815  elfzomelpfzo  13818  elfznelfzob  13820  fzostep1  13832  fllt  13857  flid  13859  flbi2  13868  2tnp1ge0ge0  13880  flhalf  13881  fldiv4p1lem1div2  13886  fldiv4lem1div2uz2  13887  dfceil2  13890  ceile  13900  ceilid  13902  quoremz  13906  intfracq  13910  uzsup  13914  mulmod0  13928  zmod10  13938  zmodcl  13942  zmodfz  13944  zmodid2  13950  modcyc  13957  modaddid  13961  mulp1mod1  13965  muladdmod  13966  modmuladd  13967  modmuladdim  13968  modmul1  13978  modaddmodup  13988  modaddmodlo  13989  modaddmulmod  13992  zsqcl2  14192  leexp2  14225  iexpcyc  14261  fi1uzind  14562  ccatsymb  14638  ccatval21sw  14641  lswccatn0lsw  14648  swrdnd  14714  swrdnnn0nd  14716  swrd0  14718  swrdswrdlem  14763  swrdswrd  14764  swrdccatin2  14788  pfxccatin12lem2  14790  pfxccatin12lem3  14791  repswswrd  14845  cshwmodn  14856  cshwsublen  14857  cshwidxmod  14864  cshwidxmodr  14865  cshwidxm1  14868  repswcshw  14873  2cshw  14874  cshweqrep  14882  cshw1  14883  swrd2lsw  15013  nn0abscl  15387  rexuzre  15428  dvdsval3  16336  p1modz1  16339  moddvds  16343  absdvdsb  16354  dvdsabsb  16355  dvdsle  16390  alzdvds  16400  mod2eq1n2dvds  16427  evennn02n  16430  evennn2n  16431  ltoddhalfle  16441  divalgmod  16486  fldivndvdslt  16496  flodddiv4t2lthalf  16498  bitsp1o  16513  gcdabs1  16609  modgcd  16612  bezoutlem1  16619  dfgcd2  16626  algcvga  16659  lcmabs  16685  isprm3  16763  dvdsnprmd  16770  2mulprm  16773  oddprmgt2  16780  sqnprm  16783  zgcdsq  16834  hashdvds  16856  vfermltlALT  16884  powm2modprm  16885  modprm0  16887  modprmn0modprm0  16889  fldivp1  16979  zgz  17015  4sqlem4  17034  prmgaplem5  17137  prmgaplem7  17139  cshwshashlem2  17178  setsstruct  17258  mulgmodid  19223  gexdvds  19698  zringunit  21666  prmirred  21674  znf1o  21751  chfacfscmul0  23065  chfacfscmulgsum  23067  chfacfpmmul0  23069  chfacfpmmulgsum  23071  dyadf  25801  dyadovol  25803  degltlem1  26280  coskpi  26739  cosne0  26745  relogexp  26812  cxpeq  26973  relogbzexp  26992  ppival2  27343  ppival2g  27344  ppiprm  27366  chtprm  27368  chtnprm  27369  ppip1le  27376  efexple  27496  zabsle1  27511  lgsdir2lem4  27543  lgsne0  27550  gausslemma2dlem1a  27580  gausslemma2dlem3  27583  gausslemma2dlem4  27584  lgsquadlem1  27595  lgsquadlem2  27596  2lgslem1a1  27604  2lgslem1a2  27605  2sqlem2  27633  rplogsumlem2  27700  pntrsumbnd  27781  axlowdim  29366  crctcshwlkn0lem3  30228  crctcshwlkn0lem5  30230  crctcshwlkn0  30237  crctcsh  30240  clwlkclwwlklem2fv2  30414  clwlkclwwlklem2a  30416  clwwisshclwwslemlem  30431  clwwlkinwwlk  30458  clwwlkext2edg  30474  wwlksubclwwlk  30476  numclwwlk5  30810  topnfbey  30891  uzssico  33199  1fldgenq  33707  znfermltl  33745  ply1coedeg  33943  rezh  34423  zrhre  34473  hashf2  34538  ballotlemfc0  34948  ballotlemfcc  34949  chpvalz  35080  chtvalz  35081  zltp1ne  35658  elfzm12  36204  nn0prpwlem  36890  poimirlem24  38352  mblfinlem1  38365  mblfinlem2  38366  itg2addnclem2  38380  fzmul  38450  incsequz2  38458  fimgmcyc  43360  ellz1  43556  lzunuz  43557  lzenom  43559  nerabdioph  43594  pell14qrgt0  43644  rmxycomplete  43702  monotuz  43726  monotoddzzfi  43727  oddcomabszz  43729  zindbi  43731  jm2.24  43748  congrep  43758  fzneg  43767  jm2.19  43778  fzunt  44239  fzunt1d  44241  fzuntgd  44242  oddfl  46055  fzdifsuc2  46087  climsuse  46382  stoweidlem26  46798  stoweidlem34  46806  fourierdlem20  46899  fourierdlem42  46921  fourierdlem51  46929  fourierdlem64  46942  fourierdlem76  46954  fourierdlem94  46972  fourierdlem97  46975  fourierdlem113  46991  natlocalincr  47650  natglobalincr  47651  zm1nn  48097  zgeltp1eq  48104  eluzge0nn0  48107  elfz2z  48110  2elfz2melfz  48113  elfzlble  48115  elfzelfzlble  48116  fzopredsuc  48119  ceilbi  48132  mod0mul  48157  modn0mul  48158  m1modmmod  48159  difmodm1lt  48160  mod2addne  48165  modm2nep1  48167  modp2nep1  48168  modm1nep2  48169  modm1nem2  48170  modm1p1ne  48171  smonoord  48172  2timesltsqm1  48174  fsummmodsndifre  48177  muldvdsfacgt  48181  muldvdsfacm1  48182  iccpartipre  48228  iccpartiltu  48229  iccpartigtl  48230  icceuelpartlem  48242  fmtno4prmfac  48382  lighneallem4b  48419  nprmdvdsfacm1lem2  48431  nprmdvdsfacm1lem4  48433  dfeven3  48481  dfodd4  48482  nn0o1gt2ALTV  48517  nnoALTV  48518  fpprel2  48564  gbegt5  48584  gbowgt5  48585  sbgoldbwt  48600  nnsum3primesle9  48617  nnsum4primesodd  48619  nnsum4primesoddALTV  48620  evengpop3  48621  evengpoap3  48622  nnsum4primesevenALTV  48624  bgoldbtbndlem1  48628  bgoldbtbndlem2  48629  bgoldbtbndlem3  48630  bgoldbtbndlem4  48631  gpgprismgriedgdmss  48875  gpgusgralem  48879  gpgedgvtx1  48885  gpg5nbgrvtx03starlem2  48892  gpg5nbgrvtx13starlem2  48895  gpg3nbgrvtx0  48899  cznnring  49084  elfzolborelfzop1  49356  zgtp1leeq  49358  rege1logbzge0  49396  fllog2  49405  dignn0ldlem  49439  dignn0flhalflem1  49452  dignn0flhalflem2  49453