Theorem zre 12029

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

Syntax hints:   → wi 4   ∨ w3o 1083   = wceq 1538   ∈ wcel 2111  ℝcr 10579  0cc0 10580  -cneg 10914  ℕcn 11679  ℤcz 12025

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-10 2142  ax-11 2158  ax-12 2175  ax-ext 2729

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3or 1085  df-3an 1086  df-tru 1541  df-ex 1782  df-nf 1786  df-sb 2070  df-clab 2736  df-cleq 2750  df-clel 2830  df-nfc 2901  df-rab 3079  df-v 3411  df-un 3865  df-in 3867  df-ss 3877  df-sn 4526  df-pr 4528  df-op 4532  df-uni 4802  df-br 5036  df-iota 6298  df-fv 6347  df-ov 7158  df-neg 10916  df-z 12026

This theorem is referenced by:  zcn  12030  zrei  12031  zssre  12032  elnn0z  12038  elnnz1  12052  znnnlt1  12053  zletr  12070  znnsub  12072  znn0sub  12073  nzadd  12074  zltp1le  12076  zleltp1  12077  nn0ge0div  12095  zextle  12099  btwnnz  12102  suprzcl  12106  msqznn  12108  peano2uz2  12114  uzind  12118  fzind  12124  fnn0ind  12125  eluzuzle  12296  uzid  12302  uzneg  12307  uztric  12311  uz11  12312  eluzp1m1  12313  eluzp1p1  12315  eluzaddi  12316  eluzsubi  12317  subeluzsub  12320  uzin  12323  uz3m2nn  12336  peano2uz  12346  nn0pzuz  12350  uzwo  12356  eluz2b2  12366  uz2mulcl  12371  uzinfi  12373  eqreznegel  12379  lbzbi  12381  uzsupss  12385  nn01to3  12386  zmin  12389  zmax  12390  zbtwnre  12391  rebtwnz  12392  qre  12398  elpq  12420  rpnnen1lem2  12422  rpnnen1lem1  12423  rpnnen1lem3  12424  rpnnen1lem5  12426  z2ge  12637  qbtwnre  12638  zltaddlt1le  12942  elfz1eq  12972  fzn  12977  fzen  12978  uzsubsubfz  12983  fzaddel  12995  fzadd2  12996  ssfzunsnext  13006  ssfzunsn  13007  fzsuc2  13019  fzrev  13024  elfz1b  13030  fznuz  13043  uznfz  13044  fzp1nel  13045  elfz0fzfz0  13066  fz0fzelfz0  13067  fznn0sub2  13068  fz0fzdiffz0  13070  elfzmlbp  13072  difelfznle  13075  nelfzo  13097  elfzouz2  13106  fzo0n  13113  fzonlt0  13114  fzossrbm1  13120  fzospliti  13123  elfzo0z  13133  fzofzim  13138  fzo1fzo0n0  13142  eluzgtdifelfzo  13153  fzossfzop1  13169  ssfzoulel  13185  ssfzo12bi  13186  elfzonelfzo  13193  elfzomelpfzo  13195  elfznelfzob  13197  fzostep1  13207  fllt  13230  flid  13232  flbi2  13241  2tnp1ge0ge0  13253  flhalf  13254  fldiv4p1lem1div2  13259  fldiv4lem1div2uz2  13260  dfceil2  13263  ceile  13271  ceilid  13273  quoremz  13277  intfracq  13281  uzsup  13285  mulmod0  13299  zmod10  13309  zmodcl  13313  zmodfz  13315  zmodid2  13321  modcyc  13328  mulp1mod1  13334  modmuladd  13335  modmuladdim  13336  modmul1  13346  modaddmodup  13356  modaddmodlo  13357  modaddmulmod  13360  zsqcl2  13557  leexp2  13590  iexpcyc  13624  fi1uzind  13912  ccatsymb  13988  ccatval21sw  13991  lswccatn0lsw  13997  swrdnd  14068  swrdnnn0nd  14070  swrd0  14072  swrdswrdlem  14118  swrdswrd  14119  swrdccatin2  14143  pfxccatin12lem2  14145  pfxccatin12lem3  14146  repswswrd  14198  cshwmodn  14209  cshwsublen  14210  cshwidxmod  14217  cshwidxmodr  14218  cshwidxm1  14221  repswcshw  14226  2cshw  14227  cshweqrep  14235  cshw1  14236  swrd2lsw  14366  nn0abscl  14725  rexuzre  14765  dvdsval3  15664  p1modz1  15667  moddvds  15671  absdvdsb  15681  dvdsabsb  15682  dvdsle  15716  alzdvds  15726  mod2eq1n2dvds  15753  evennn02n  15756  evennn2n  15757  ltoddhalfle  15767  divalgmod  15812  fldivndvdslt  15820  flodddiv4t2lthalf  15822  bitsp1o  15837  gcdabs  15933  gcdabs1  15934  modgcd  15936  bezoutlem1  15943  dfgcd2  15950  algcvga  15980  lcmabs  16006  isprm3  16084  dvdsnprmd  16091  2mulprm  16094  oddprmgt2  16100  sqnprm  16103  zgcdsq  16153  hashdvds  16172  vfermltlALT  16199  powm2modprm  16200  modprm0  16202  modprmn0modprm0  16204  fldivp1  16293  zgz  16329  4sqlem4  16348  prmgaplem5  16451  prmgaplem7  16453  cshwshashlem2  16493  setsstruct  16586  mulgmodid  18338  gexdvds  18781  zringunit  20261  prmirred  20269  znf1o  20324  chfacfscmul0  21563  chfacfscmulgsum  21565  chfacfpmmul0  21567  chfacfpmmulgsum  21569  dyadf  24296  dyadovol  24298  degltlem1  24777  coskpi  25219  cosne0  25225  relogexp  25291  cxpeq  25450  relogbzexp  25466  ppival2  25817  ppival2g  25818  ppiprm  25840  chtprm  25842  chtnprm  25843  ppip1le  25850  efexple  25969  zabsle1  25984  lgsdir2lem4  26016  lgsne0  26023  gausslemma2dlem1a  26053  gausslemma2dlem3  26056  gausslemma2dlem4  26057  lgsquadlem1  26068  lgsquadlem2  26069  2lgslem1a1  26077  2lgslem1a2  26078  2sqlem2  26106  rplogsumlem2  26173  pntrsumbnd  26254  axlowdim  26859  crctcshwlkn0lem3  27702  crctcshwlkn0lem5  27704  crctcshwlkn0  27711  crctcsh  27714  clwlkclwwlklem2fv2  27885  clwlkclwwlklem2a  27887  clwwisshclwwslemlem  27902  clwwlkinwwlk  27929  clwwlkext2edg  27945  wwlksubclwwlk  27947  numclwwlk5  28277  topnfbey  28358  uzssico  30633  znfermltl  31087  rezh  31444  zrhre  31492  hashf2  31575  ballotlemfc0  31982  ballotlemfcc  31983  chpvalz  32131  chtvalz  32132  zltp1ne  32588  0nn0m1nnn0  32591  elfzm12  33153  nn0prpwlem  34086  poimirlem24  35387  mblfinlem1  35400  mblfinlem2  35401  itg2addnclem2  35415  fzmul  35485  incsequz2  35493  ellz1  40109  lzunuz  40110  lzenom  40112  nerabdioph  40151  pell14qrgt0  40201  rmxycomplete  40259  monotuz  40283  monotoddzzfi  40284  oddcomabszz  40286  zindbi  40288  jm2.24  40305  congrep  40315  fzneg  40324  jm2.19  40335  oddfl  42304  fzdifsuc2  42338  climsuse  42644  stoweidlem26  43062  stoweidlem34  43070  fourierdlem20  43163  fourierdlem42  43185  fourierdlem51  43193  fourierdlem64  43206  fourierdlem76  43218  fourierdlem94  43236  fourierdlem97  43239  fourierdlem113  43255  zm1nn  44255  zgeltp1eq  44262  eluzge0nn0  44265  elfz2z  44268  2elfz2melfz  44271  elfzlble  44273  elfzelfzlble  44274  fzopredsuc  44276  smonoord  44284  fsummmodsndifre  44287  iccpartipre  44334  iccpartiltu  44335  iccpartigtl  44336  icceuelpartlem  44348  fmtno4prmfac  44485  lighneallem4b  44522  dfeven3  44571  dfodd4  44572  nn0o1gt2ALTV  44607  nnoALTV  44608  fpprel2  44654  gbegt5  44674  gbowgt5  44675  sbgoldbwt  44690  nnsum3primesle9  44707  nnsum4primesodd  44709  nnsum4primesoddALTV  44710  evengpop3  44711  evengpoap3  44712  nnsum4primesevenALTV  44714  bgoldbtbndlem1  44718  bgoldbtbndlem2  44719  bgoldbtbndlem3  44720  bgoldbtbndlem4  44721  cznnring  44975  elfzolborelfzop1  45321  zgtp1leeq  45323  mod0mul  45326  modn0mul  45327  m1modmmod  45328  difmodm1lt  45329  rege1logbzge0  45366  fllog2  45375  dignn0ldlem  45409  dignn0flhalflem1  45422  dignn0flhalflem2  45423