Theorem zre 12643

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

Syntax hints:   → wi 4   ∨ w3o 1086   = wceq 1537   ∈ wcel 2108  ℝcr 11183  0cc0 11184  -cneg 11521  ℕcn 12293  ℤcz 12639

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2711

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 847  df-3or 1088  df-3an 1089  df-tru 1540  df-fal 1550  df-ex 1778  df-sb 2065  df-clab 2718  df-cleq 2732  df-clel 2819  df-rab 3444  df-v 3490  df-dif 3979  df-un 3981  df-ss 3993  df-nul 4353  df-if 4549  df-sn 4649  df-pr 4651  df-op 4655  df-uni 4932  df-br 5167  df-iota 6525  df-fv 6581  df-ov 7451  df-neg 11523  df-z 12640

This theorem is referenced by:  zcn  12644  zrei  12645  zssre  12646  elnn0z  12652  elnnz1  12669  znnnlt1  12670  zletr  12687  znnsub  12689  znn0sub  12690  nzadd  12691  zltp1le  12693  zleltp1  12694  nn0ge0div  12712  zextle  12716  btwnnz  12719  suprzcl  12723  msqznn  12725  peano2uz2  12731  uzind  12735  fzind  12741  fnn0ind  12742  eluzuzle  12912  uzid  12918  uzneg  12923  uztric  12927  uz11  12928  eluzp1m1  12929  eluzp1p1  12931  eluzadd  12932  eluzsub  12933  eluzaddiOLD  12935  eluzsubiOLD  12937  subeluzsub  12940  uzin  12943  uz3m2nn  12956  peano2uz  12966  nn0pzuz  12970  uzwo  12976  eluz2b2  12986  uz2mulcl  12991  uzinfi  12993  eqreznegel  12999  lbzbi  13001  uzsupss  13005  nn01to3  13006  zmin  13009  zmax  13010  zbtwnre  13011  rebtwnz  13012  qre  13018  elpq  13040  rpnnen1lem2  13042  rpnnen1lem1  13043  rpnnen1lem3  13044  rpnnen1lem5  13046  z2ge  13260  qbtwnre  13261  zltaddlt1le  13565  elfz1eq  13595  fzn  13600  fzen  13601  uzsubsubfz  13606  fzaddel  13618  fzadd2  13619  ssfzunsnext  13629  ssfzunsn  13630  fzsuc2  13642  fzrev  13647  elfz1b  13653  fznuz  13666  uznfz  13667  fzp1nel  13668  elfz0fzfz0  13690  fz0fzelfz0  13691  fznn0sub2  13692  fz0fzdiffz0  13694  elfzmlbp  13696  difelfznle  13699  nelfzo  13721  elfzouz2  13731  fzo0n  13738  fzonlt0  13739  fzossrbm1  13745  fzospliti  13748  elfzo0z  13758  fzofzim  13763  fzo1fzo0n0  13767  eluzgtdifelfzo  13778  fzossfzop1  13794  ssfzoulel  13810  ssfzo12bi  13811  elfzonelfzo  13819  elfzomelpfzo  13821  elfznelfzob  13823  fzostep1  13833  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  mulp1mod1  13963  modmuladd  13964  modmuladdim  13965  modmul1  13975  modaddmodup  13985  modaddmodlo  13986  modaddmulmod  13989  zsqcl2  14188  leexp2  14221  iexpcyc  14256  fi1uzind  14556  ccatsymb  14630  ccatval21sw  14633  lswccatn0lsw  14639  swrdnd  14702  swrdnnn0nd  14704  swrd0  14706  swrdswrdlem  14752  swrdswrd  14753  swrdccatin2  14777  pfxccatin12lem2  14779  pfxccatin12lem3  14780  repswswrd  14832  cshwmodn  14843  cshwsublen  14844  cshwidxmod  14851  cshwidxmodr  14852  cshwidxm1  14855  repswcshw  14860  2cshw  14861  cshweqrep  14869  cshw1  14870  swrd2lsw  15001  nn0abscl  15361  rexuzre  15401  dvdsval3  16306  p1modz1  16309  moddvds  16313  absdvdsb  16323  dvdsabsb  16324  dvdsle  16358  alzdvds  16368  mod2eq1n2dvds  16395  evennn02n  16398  evennn2n  16399  ltoddhalfle  16409  divalgmod  16454  fldivndvdslt  16462  flodddiv4t2lthalf  16464  bitsp1o  16479  gcdabs1  16575  gcdabsOLD  16578  modgcd  16579  bezoutlem1  16586  dfgcd2  16593  algcvga  16626  lcmabs  16652  isprm3  16730  dvdsnprmd  16737  2mulprm  16740  oddprmgt2  16746  sqnprm  16749  zgcdsq  16800  hashdvds  16822  vfermltlALT  16849  powm2modprm  16850  modprm0  16852  modprmn0modprm0  16854  fldivp1  16944  zgz  16980  4sqlem4  16999  prmgaplem5  17102  prmgaplem7  17104  cshwshashlem2  17144  setsstruct  17223  mulgmodid  19153  gexdvds  19626  zringunit  21500  prmirred  21508  znf1o  21593  chfacfscmul0  22885  chfacfscmulgsum  22887  chfacfpmmul0  22889  chfacfpmmulgsum  22891  dyadf  25645  dyadovol  25647  degltlem1  26131  coskpi  26583  cosne0  26589  relogexp  26656  cxpeq  26818  relogbzexp  26837  ppival2  27189  ppival2g  27190  ppiprm  27212  chtprm  27214  chtnprm  27215  ppip1le  27222  efexple  27343  zabsle1  27358  lgsdir2lem4  27390  lgsne0  27397  gausslemma2dlem1a  27427  gausslemma2dlem3  27430  gausslemma2dlem4  27431  lgsquadlem1  27442  lgsquadlem2  27443  2lgslem1a1  27451  2lgslem1a2  27452  2sqlem2  27480  rplogsumlem2  27547  pntrsumbnd  27628  axlowdim  28994  crctcshwlkn0lem3  29845  crctcshwlkn0lem5  29847  crctcshwlkn0  29854  crctcsh  29857  clwlkclwwlklem2fv2  30028  clwlkclwwlklem2a  30030  clwwisshclwwslemlem  30045  clwwlkinwwlk  30072  clwwlkext2edg  30088  wwlksubclwwlk  30090  numclwwlk5  30420  topnfbey  30501  uzssico  32789  1fldgenq  33289  znfermltl  33359  rezh  33917  zrhre  33965  hashf2  34048  ballotlemfc0  34457  ballotlemfcc  34458  chpvalz  34605  chtvalz  34606  zltp1ne  35077  0nn0m1nnn0  35080  elfzm12  35643  nn0prpwlem  36288  poimirlem24  37604  mblfinlem1  37617  mblfinlem2  37618  itg2addnclem2  37632  fzmul  37701  incsequz2  37709  fimgmcyc  42489  ellz1  42723  lzunuz  42724  lzenom  42726  nerabdioph  42765  pell14qrgt0  42815  rmxycomplete  42874  monotuz  42898  monotoddzzfi  42899  oddcomabszz  42901  zindbi  42903  jm2.24  42920  congrep  42930  fzneg  42939  jm2.19  42950  fzunt  43417  fzunt1d  43419  fzuntgd  43420  oddfl  45192  fzdifsuc2  45225  climsuse  45529  stoweidlem26  45947  stoweidlem34  45955  fourierdlem20  46048  fourierdlem42  46070  fourierdlem51  46078  fourierdlem64  46091  fourierdlem76  46103  fourierdlem94  46121  fourierdlem97  46124  fourierdlem113  46140  natlocalincr  46795  natglobalincr  46796  zm1nn  47217  zgeltp1eq  47224  eluzge0nn0  47227  elfz2z  47230  2elfz2melfz  47233  elfzlble  47235  elfzelfzlble  47236  fzopredsuc  47238  smonoord  47245  fsummmodsndifre  47248  iccpartipre  47295  iccpartiltu  47296  iccpartigtl  47297  icceuelpartlem  47309  fmtno4prmfac  47446  lighneallem4b  47483  dfeven3  47532  dfodd4  47533  nn0o1gt2ALTV  47568  nnoALTV  47569  fpprel2  47615  gbegt5  47635  gbowgt5  47636  sbgoldbwt  47651  nnsum3primesle9  47668  nnsum4primesodd  47670  nnsum4primesoddALTV  47671  evengpop3  47672  evengpoap3  47673  nnsum4primesevenALTV  47675  bgoldbtbndlem1  47679  bgoldbtbndlem2  47680  bgoldbtbndlem3  47681  bgoldbtbndlem4  47682  cznnring  47985  elfzolborelfzop1  48248  zgtp1leeq  48250  mod0mul  48253  modn0mul  48254  m1modmmod  48255  difmodm1lt  48256  rege1logbzge0  48293  fllog2  48302  dignn0ldlem  48336  dignn0flhalflem1  48349  dignn0flhalflem2  48350