Theorem zre 12509

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

Syntax hints:   → wi 4   ∨ w3o 1085   = wceq 1540   ∈ wcel 2109  ℝcr 11043  0cc0 11044  -cneg 11382  ℕcn 12162  ℤcz 12505

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 3403  df-v 3446  df-dif 3914  df-un 3916  df-ss 3928  df-nul 4293  df-if 4485  df-sn 4586  df-pr 4588  df-op 4592  df-uni 4868  df-br 5103  df-iota 6452  df-fv 6507  df-ov 7372  df-neg 11384  df-z 12506

This theorem is referenced by:  zcn  12510  zrei  12511  zssre  12512  elnn0z  12518  elnnz1  12535  znnnlt1  12536  zletr  12553  znnsub  12555  znn0sub  12556  nzadd  12557  zltp1le  12559  zleltp1  12560  nn0ge0div  12579  zextle  12583  btwnnz  12586  suprzcl  12590  msqznn  12592  peano2uz2  12598  uzind  12602  fzind  12608  fnn0ind  12609  eluzuzle  12778  uzid  12784  uzneg  12789  uztric  12793  uz11  12794  eluzp1m1  12795  eluzp1p1  12797  eluzadd  12798  eluzsub  12799  eluzaddiOLD  12801  eluzsubiOLD  12803  subeluzsub  12806  uzin  12809  uz3m2nn  12829  peano2uz  12836  nn0pzuz  12840  uzwo  12846  eluz2b2  12856  uz2mulcl  12861  uzinfi  12863  eqreznegel  12869  lbzbi  12871  uzsupss  12875  nn01to3  12876  zmin  12879  zmax  12880  zbtwnre  12881  rebtwnz  12882  qre  12888  elpq  12910  rpnnen1lem2  12912  rpnnen1lem1  12913  rpnnen1lem3  12914  rpnnen1lem5  12916  z2ge  13134  qbtwnre  13135  zltaddlt1le  13442  elfz1eq  13472  fzn  13477  fzen  13478  uzsubsubfz  13483  fzaddel  13495  fzadd2  13496  ssfzunsnext  13506  ssfzunsn  13507  fzsuc2  13519  fzrev  13524  elfz1b  13530  fznuz  13546  uznfz  13547  fzp1nel  13548  elfz0fzfz0  13570  fz0fzelfz0  13571  fznn0sub2  13572  fz0fzdiffz0  13574  elfzmlbp  13576  difelfznle  13579  nelfzo  13601  elfzouz2  13611  fzo0n  13618  fzonlt0  13619  fzossrbm1  13625  fzospliti  13628  elfzo0z  13638  fzofzim  13646  fzo1fzo0n0  13652  eluzgtdifelfzo  13664  fzossfzop1  13680  ssfzoulel  13697  ssfzo12bi  13698  elfzonelfzo  13706  elfzomelpfzo  13708  elfznelfzob  13710  fzostep1  13720  fllt  13744  flid  13746  flbi2  13755  2tnp1ge0ge0  13767  flhalf  13768  fldiv4p1lem1div2  13773  fldiv4lem1div2uz2  13774  dfceil2  13777  ceile  13787  ceilid  13789  quoremz  13793  intfracq  13797  uzsup  13801  mulmod0  13815  zmod10  13825  zmodcl  13829  zmodfz  13831  zmodid2  13837  modcyc  13844  modaddid  13848  mulp1mod1  13852  muladdmod  13853  modmuladd  13854  modmuladdim  13855  modmul1  13865  modaddmodup  13875  modaddmodlo  13876  modaddmulmod  13879  zsqcl2  14079  leexp2  14112  iexpcyc  14148  fi1uzind  14448  ccatsymb  14523  ccatval21sw  14526  lswccatn0lsw  14532  swrdnd  14595  swrdnnn0nd  14597  swrd0  14599  swrdswrdlem  14645  swrdswrd  14646  swrdccatin2  14670  pfxccatin12lem2  14672  pfxccatin12lem3  14673  repswswrd  14725  cshwmodn  14736  cshwsublen  14737  cshwidxmod  14744  cshwidxmodr  14745  cshwidxm1  14748  repswcshw  14753  2cshw  14754  cshweqrep  14762  cshw1  14763  swrd2lsw  14894  nn0abscl  15254  rexuzre  15295  dvdsval3  16202  p1modz1  16205  moddvds  16209  absdvdsb  16220  dvdsabsb  16221  dvdsle  16256  alzdvds  16266  mod2eq1n2dvds  16293  evennn02n  16296  evennn2n  16297  ltoddhalfle  16307  divalgmod  16352  fldivndvdslt  16362  flodddiv4t2lthalf  16364  bitsp1o  16379  gcdabs1  16475  modgcd  16478  bezoutlem1  16485  dfgcd2  16492  algcvga  16525  lcmabs  16551  isprm3  16629  dvdsnprmd  16636  2mulprm  16639  oddprmgt2  16645  sqnprm  16648  zgcdsq  16699  hashdvds  16721  vfermltlALT  16749  powm2modprm  16750  modprm0  16752  modprmn0modprm0  16754  fldivp1  16844  zgz  16880  4sqlem4  16899  prmgaplem5  17002  prmgaplem7  17004  cshwshashlem2  17043  setsstruct  17122  mulgmodid  19027  gexdvds  19498  zringunit  21408  prmirred  21416  znf1o  21493  chfacfscmul0  22778  chfacfscmulgsum  22780  chfacfpmmul0  22782  chfacfpmmulgsum  22784  dyadf  25525  dyadovol  25527  degltlem1  26010  coskpi  26465  cosne0  26471  relogexp  26538  cxpeq  26700  relogbzexp  26719  ppival2  27071  ppival2g  27072  ppiprm  27094  chtprm  27096  chtnprm  27097  ppip1le  27104  efexple  27225  zabsle1  27240  lgsdir2lem4  27272  lgsne0  27279  gausslemma2dlem1a  27309  gausslemma2dlem3  27312  gausslemma2dlem4  27313  lgsquadlem1  27324  lgsquadlem2  27325  2lgslem1a1  27333  2lgslem1a2  27334  2sqlem2  27362  rplogsumlem2  27429  pntrsumbnd  27510  axlowdim  28941  crctcshwlkn0lem3  29792  crctcshwlkn0lem5  29794  crctcshwlkn0  29801  crctcsh  29804  clwlkclwwlklem2fv2  29975  clwlkclwwlklem2a  29977  clwwisshclwwslemlem  29992  clwwlkinwwlk  30019  clwwlkext2edg  30035  wwlksubclwwlk  30037  numclwwlk5  30367  topnfbey  30448  uzssico  32757  1fldgenq  33288  znfermltl  33330  rezh  33952  zrhre  34002  hashf2  34067  ballotlemfc0  34477  ballotlemfcc  34478  chpvalz  34612  chtvalz  34613  zltp1ne  35090  0nn0m1nnn0  35093  elfzm12  35655  nn0prpwlem  36303  poimirlem24  37631  mblfinlem1  37644  mblfinlem2  37645  itg2addnclem2  37659  fzmul  37728  incsequz2  37736  fimgmcyc  42515  ellz1  42748  lzunuz  42749  lzenom  42751  nerabdioph  42790  pell14qrgt0  42840  rmxycomplete  42899  monotuz  42923  monotoddzzfi  42924  oddcomabszz  42926  zindbi  42928  jm2.24  42945  congrep  42955  fzneg  42964  jm2.19  42975  fzunt  43437  fzunt1d  43439  fzuntgd  43440  oddfl  45269  fzdifsuc2  45301  climsuse  45599  stoweidlem26  46017  stoweidlem34  46025  fourierdlem20  46118  fourierdlem42  46140  fourierdlem51  46148  fourierdlem64  46161  fourierdlem76  46173  fourierdlem94  46191  fourierdlem97  46194  fourierdlem113  46210  natlocalincr  46867  natglobalincr  46868  zm1nn  47296  zgeltp1eq  47303  eluzge0nn0  47306  elfz2z  47309  2elfz2melfz  47312  elfzlble  47314  elfzelfzlble  47315  fzopredsuc  47317  ceilbi  47327  mod0mul  47350  modn0mul  47351  m1modmmod  47352  difmodm1lt  47353  mod2addne  47358  modm2nep1  47360  modp2nep1  47361  modm1nep2  47362  modm1nem2  47363  modm1p1ne  47364  smonoord  47365  fsummmodsndifre  47368  iccpartipre  47415  iccpartiltu  47416  iccpartigtl  47417  icceuelpartlem  47429  fmtno4prmfac  47566  lighneallem4b  47603  dfeven3  47652  dfodd4  47653  nn0o1gt2ALTV  47688  nnoALTV  47689  fpprel2  47735  gbegt5  47755  gbowgt5  47756  sbgoldbwt  47771  nnsum3primesle9  47788  nnsum4primesodd  47790  nnsum4primesoddALTV  47791  evengpop3  47792  evengpoap3  47793  nnsum4primesevenALTV  47795  bgoldbtbndlem1  47799  bgoldbtbndlem2  47800  bgoldbtbndlem3  47801  bgoldbtbndlem4  47802  gpgprismgriedgdmss  48036  gpgusgralem  48040  gpgedgvtx1  48046  gpg5nbgrvtx03starlem2  48053  gpg5nbgrvtx13starlem2  48056  gpg3nbgrvtx0  48060  cznnring  48243  elfzolborelfzop1  48501  zgtp1leeq  48503  rege1logbzge0  48541  fllog2  48550  dignn0ldlem  48584  dignn0flhalflem1  48597  dignn0flhalflem2  48598