Theorem zre 12595

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

Syntax hints:   → wi 4   ∨ w3o 1083   = wceq 1533   ∈ wcel 2098  ℝcr 11139  0cc0 11140  -cneg 11477  ℕcn 12245  ℤcz 12591

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-ext 2696

This theorem depends on definitions:  df-bi 206  df-an 395  df-or 846  df-3or 1085  df-3an 1086  df-tru 1536  df-fal 1546  df-ex 1774  df-sb 2060  df-clab 2703  df-cleq 2717  df-clel 2802  df-rab 3419  df-v 3463  df-dif 3947  df-un 3949  df-ss 3961  df-nul 4323  df-if 4531  df-sn 4631  df-pr 4633  df-op 4637  df-uni 4910  df-br 5150  df-iota 6501  df-fv 6557  df-ov 7422  df-neg 11479  df-z 12592

This theorem is referenced by:  zcn  12596  zrei  12597  zssre  12598  elnn0z  12604  elnnz1  12621  znnnlt1  12622  zletr  12639  znnsub  12641  znn0sub  12642  nzadd  12643  zltp1le  12645  zleltp1  12646  nn0ge0div  12664  zextle  12668  btwnnz  12671  suprzcl  12675  msqznn  12677  peano2uz2  12683  uzind  12687  fzind  12693  fnn0ind  12694  eluzuzle  12864  uzid  12870  uzneg  12875  uztric  12879  uz11  12880  eluzp1m1  12881  eluzp1p1  12883  eluzadd  12884  eluzsub  12885  eluzaddiOLD  12887  eluzsubiOLD  12889  subeluzsub  12892  uzin  12895  uz3m2nn  12908  peano2uz  12918  nn0pzuz  12922  uzwo  12928  eluz2b2  12938  uz2mulcl  12943  uzinfi  12945  eqreznegel  12951  lbzbi  12953  uzsupss  12957  nn01to3  12958  zmin  12961  zmax  12962  zbtwnre  12963  rebtwnz  12964  qre  12970  elpq  12992  rpnnen1lem2  12994  rpnnen1lem1  12995  rpnnen1lem3  12996  rpnnen1lem5  12998  z2ge  13212  qbtwnre  13213  zltaddlt1le  13517  elfz1eq  13547  fzn  13552  fzen  13553  uzsubsubfz  13558  fzaddel  13570  fzadd2  13571  ssfzunsnext  13581  ssfzunsn  13582  fzsuc2  13594  fzrev  13599  elfz1b  13605  fznuz  13618  uznfz  13619  fzp1nel  13620  elfz0fzfz0  13641  fz0fzelfz0  13642  fznn0sub2  13643  fz0fzdiffz0  13645  elfzmlbp  13647  difelfznle  13650  nelfzo  13672  elfzouz2  13682  fzo0n  13689  fzonlt0  13690  fzossrbm1  13696  fzospliti  13699  elfzo0z  13709  fzofzim  13714  fzo1fzo0n0  13718  eluzgtdifelfzo  13729  fzossfzop1  13745  ssfzoulel  13761  ssfzo12bi  13762  elfzonelfzo  13770  elfzomelpfzo  13772  elfznelfzob  13774  fzostep1  13784  fllt  13807  flid  13809  flbi2  13818  2tnp1ge0ge0  13830  flhalf  13831  fldiv4p1lem1div2  13836  fldiv4lem1div2uz2  13837  dfceil2  13840  ceile  13850  ceilid  13852  quoremz  13856  intfracq  13860  uzsup  13864  mulmod0  13878  zmod10  13888  zmodcl  13892  zmodfz  13894  zmodid2  13900  modcyc  13907  mulp1mod1  13913  modmuladd  13914  modmuladdim  13915  modmul1  13925  modaddmodup  13935  modaddmodlo  13936  modaddmulmod  13939  zsqcl2  14138  leexp2  14171  iexpcyc  14206  fi1uzind  14494  ccatsymb  14568  ccatval21sw  14571  lswccatn0lsw  14577  swrdnd  14640  swrdnnn0nd  14642  swrd0  14644  swrdswrdlem  14690  swrdswrd  14691  swrdccatin2  14715  pfxccatin12lem2  14717  pfxccatin12lem3  14718  repswswrd  14770  cshwmodn  14781  cshwsublen  14782  cshwidxmod  14789  cshwidxmodr  14790  cshwidxm1  14793  repswcshw  14798  2cshw  14799  cshweqrep  14807  cshw1  14808  swrd2lsw  14939  nn0abscl  15295  rexuzre  15335  dvdsval3  16238  p1modz1  16241  moddvds  16245  absdvdsb  16255  dvdsabsb  16256  dvdsle  16290  alzdvds  16300  mod2eq1n2dvds  16327  evennn02n  16330  evennn2n  16331  ltoddhalfle  16341  divalgmod  16386  fldivndvdslt  16394  flodddiv4t2lthalf  16396  bitsp1o  16411  gcdabs1  16507  gcdabsOLD  16510  modgcd  16511  bezoutlem1  16518  dfgcd2  16525  algcvga  16553  lcmabs  16579  isprm3  16657  dvdsnprmd  16664  2mulprm  16667  oddprmgt2  16673  sqnprm  16676  zgcdsq  16728  hashdvds  16747  vfermltlALT  16774  powm2modprm  16775  modprm0  16777  modprmn0modprm0  16779  fldivp1  16869  zgz  16905  4sqlem4  16924  prmgaplem5  17027  prmgaplem7  17029  cshwshashlem2  17069  setsstruct  17148  mulgmodid  19076  gexdvds  19551  zringunit  21409  prmirred  21417  znf1o  21502  chfacfscmul0  22804  chfacfscmulgsum  22806  chfacfpmmul0  22808  chfacfpmmulgsum  22810  dyadf  25564  dyadovol  25566  degltlem1  26052  coskpi  26502  cosne0  26508  relogexp  26575  cxpeq  26737  relogbzexp  26753  ppival2  27105  ppival2g  27106  ppiprm  27128  chtprm  27130  chtnprm  27131  ppip1le  27138  efexple  27259  zabsle1  27274  lgsdir2lem4  27306  lgsne0  27313  gausslemma2dlem1a  27343  gausslemma2dlem3  27346  gausslemma2dlem4  27347  lgsquadlem1  27358  lgsquadlem2  27359  2lgslem1a1  27367  2lgslem1a2  27368  2sqlem2  27396  rplogsumlem2  27463  pntrsumbnd  27544  axlowdim  28844  crctcshwlkn0lem3  29695  crctcshwlkn0lem5  29697  crctcshwlkn0  29704  crctcsh  29707  clwlkclwwlklem2fv2  29878  clwlkclwwlklem2a  29880  clwwisshclwwslemlem  29895  clwwlkinwwlk  29922  clwwlkext2edg  29938  wwlksubclwwlk  29940  numclwwlk5  30270  topnfbey  30351  uzssico  32634  1fldgenq  33108  znfermltl  33177  rezh  33703  zrhre  33751  hashf2  33834  ballotlemfc0  34243  ballotlemfcc  34244  chpvalz  34391  chtvalz  34392  zltp1ne  34850  0nn0m1nnn0  34853  elfzm12  35410  nn0prpwlem  35937  poimirlem24  37248  mblfinlem1  37261  mblfinlem2  37262  itg2addnclem2  37276  fzmul  37345  incsequz2  37353  ellz1  42329  lzunuz  42330  lzenom  42332  nerabdioph  42371  pell14qrgt0  42421  rmxycomplete  42480  monotuz  42504  monotoddzzfi  42505  oddcomabszz  42507  zindbi  42509  jm2.24  42526  congrep  42536  fzneg  42545  jm2.19  42556  fzunt  43027  fzunt1d  43029  fzuntgd  43030  oddfl  44797  fzdifsuc2  44830  climsuse  45134  stoweidlem26  45552  stoweidlem34  45560  fourierdlem20  45653  fourierdlem42  45675  fourierdlem51  45683  fourierdlem64  45696  fourierdlem76  45708  fourierdlem94  45726  fourierdlem97  45729  fourierdlem113  45745  natlocalincr  46400  natglobalincr  46401  zm1nn  46820  zgeltp1eq  46827  eluzge0nn0  46830  elfz2z  46833  2elfz2melfz  46836  elfzlble  46838  elfzelfzlble  46839  fzopredsuc  46841  smonoord  46848  fsummmodsndifre  46851  iccpartipre  46898  iccpartiltu  46899  iccpartigtl  46900  icceuelpartlem  46912  fmtno4prmfac  47049  lighneallem4b  47086  dfeven3  47135  dfodd4  47136  nn0o1gt2ALTV  47171  nnoALTV  47172  fpprel2  47218  gbegt5  47238  gbowgt5  47239  sbgoldbwt  47254  nnsum3primesle9  47271  nnsum4primesodd  47273  nnsum4primesoddALTV  47274  evengpop3  47275  evengpoap3  47276  nnsum4primesevenALTV  47278  bgoldbtbndlem1  47282  bgoldbtbndlem2  47283  bgoldbtbndlem3  47284  bgoldbtbndlem4  47285  cznnring  47510  elfzolborelfzop1  47773  zgtp1leeq  47775  mod0mul  47778  modn0mul  47779  m1modmmod  47780  difmodm1lt  47781  rege1logbzge0  47818  fllog2  47827  dignn0ldlem  47861  dignn0flhalflem1  47874  dignn0flhalflem2  47875