Theorem zre 12590

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

Syntax hints:   → wi 4   ∨ w3o 1085   = wceq 1540   ∈ wcel 2108  ℝcr 11126  0cc0 11127  -cneg 11465  ℕcn 12238  ℤcz 12586

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 2007  ax-8 2110  ax-9 2118  ax-ext 2707

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 2065  df-clab 2714  df-cleq 2727  df-clel 2809  df-rab 3416  df-v 3461  df-dif 3929  df-un 3931  df-ss 3943  df-nul 4309  df-if 4501  df-sn 4602  df-pr 4604  df-op 4608  df-uni 4884  df-br 5120  df-iota 6483  df-fv 6538  df-ov 7406  df-neg 11467  df-z 12587

This theorem is referenced by:  zcn  12591  zrei  12592  zssre  12593  elnn0z  12599  elnnz1  12616  znnnlt1  12617  zletr  12634  znnsub  12636  znn0sub  12637  nzadd  12638  zltp1le  12640  zleltp1  12641  nn0ge0div  12660  zextle  12664  btwnnz  12667  suprzcl  12671  msqznn  12673  peano2uz2  12679  uzind  12683  fzind  12689  fnn0ind  12690  eluzuzle  12859  uzid  12865  uzneg  12870  uztric  12874  uz11  12875  eluzp1m1  12876  eluzp1p1  12878  eluzadd  12879  eluzsub  12880  eluzaddiOLD  12882  eluzsubiOLD  12884  subeluzsub  12887  uzin  12890  uz3m2nn  12905  peano2uz  12915  nn0pzuz  12919  uzwo  12925  eluz2b2  12935  uz2mulcl  12940  uzinfi  12942  eqreznegel  12948  lbzbi  12950  uzsupss  12954  nn01to3  12955  zmin  12958  zmax  12959  zbtwnre  12960  rebtwnz  12961  qre  12967  elpq  12989  rpnnen1lem2  12991  rpnnen1lem1  12992  rpnnen1lem3  12993  rpnnen1lem5  12995  z2ge  13212  qbtwnre  13213  zltaddlt1le  13520  elfz1eq  13550  fzn  13555  fzen  13556  uzsubsubfz  13561  fzaddel  13573  fzadd2  13574  ssfzunsnext  13584  ssfzunsn  13585  fzsuc2  13597  fzrev  13602  elfz1b  13608  fznuz  13624  uznfz  13625  fzp1nel  13626  elfz0fzfz0  13648  fz0fzelfz0  13649  fznn0sub2  13650  fz0fzdiffz0  13652  elfzmlbp  13654  difelfznle  13657  nelfzo  13679  elfzouz2  13689  fzo0n  13696  fzonlt0  13697  fzossrbm1  13703  fzospliti  13706  elfzo0z  13716  fzofzim  13724  fzo1fzo0n0  13729  eluzgtdifelfzo  13741  fzossfzop1  13757  ssfzoulel  13774  ssfzo12bi  13775  elfzonelfzo  13783  elfzomelpfzo  13785  elfznelfzob  13787  fzostep1  13797  fllt  13821  flid  13823  flbi2  13832  2tnp1ge0ge0  13844  flhalf  13845  fldiv4p1lem1div2  13850  fldiv4lem1div2uz2  13851  dfceil2  13854  ceile  13864  ceilid  13866  quoremz  13870  intfracq  13874  uzsup  13878  mulmod0  13892  zmod10  13902  zmodcl  13906  zmodfz  13908  zmodid2  13914  modcyc  13921  mulp1mod1  13927  muladdmod  13928  modmuladd  13929  modmuladdim  13930  modmul1  13940  modaddmodup  13950  modaddmodlo  13951  modaddmulmod  13954  zsqcl2  14154  leexp2  14187  iexpcyc  14223  fi1uzind  14523  ccatsymb  14598  ccatval21sw  14601  lswccatn0lsw  14607  swrdnd  14670  swrdnnn0nd  14672  swrd0  14674  swrdswrdlem  14720  swrdswrd  14721  swrdccatin2  14745  pfxccatin12lem2  14747  pfxccatin12lem3  14748  repswswrd  14800  cshwmodn  14811  cshwsublen  14812  cshwidxmod  14819  cshwidxmodr  14820  cshwidxm1  14823  repswcshw  14828  2cshw  14829  cshweqrep  14837  cshw1  14838  swrd2lsw  14969  nn0abscl  15329  rexuzre  15369  dvdsval3  16274  p1modz1  16277  moddvds  16281  absdvdsb  16292  dvdsabsb  16293  dvdsle  16327  alzdvds  16337  mod2eq1n2dvds  16364  evennn02n  16367  evennn2n  16368  ltoddhalfle  16378  divalgmod  16423  fldivndvdslt  16433  flodddiv4t2lthalf  16435  bitsp1o  16450  gcdabs1  16546  modgcd  16549  bezoutlem1  16556  dfgcd2  16563  algcvga  16596  lcmabs  16622  isprm3  16700  dvdsnprmd  16707  2mulprm  16710  oddprmgt2  16716  sqnprm  16719  zgcdsq  16770  hashdvds  16792  vfermltlALT  16820  powm2modprm  16821  modprm0  16823  modprmn0modprm0  16825  fldivp1  16915  zgz  16951  4sqlem4  16970  prmgaplem5  17073  prmgaplem7  17075  cshwshashlem2  17114  setsstruct  17193  mulgmodid  19094  gexdvds  19563  zringunit  21425  prmirred  21433  znf1o  21510  chfacfscmul0  22794  chfacfscmulgsum  22796  chfacfpmmul0  22798  chfacfpmmulgsum  22800  dyadf  25542  dyadovol  25544  degltlem1  26027  coskpi  26482  cosne0  26488  relogexp  26555  cxpeq  26717  relogbzexp  26736  ppival2  27088  ppival2g  27089  ppiprm  27111  chtprm  27113  chtnprm  27114  ppip1le  27121  efexple  27242  zabsle1  27257  lgsdir2lem4  27289  lgsne0  27296  gausslemma2dlem1a  27326  gausslemma2dlem3  27329  gausslemma2dlem4  27330  lgsquadlem1  27341  lgsquadlem2  27342  2lgslem1a1  27350  2lgslem1a2  27351  2sqlem2  27379  rplogsumlem2  27446  pntrsumbnd  27527  axlowdim  28886  crctcshwlkn0lem3  29740  crctcshwlkn0lem5  29742  crctcshwlkn0  29749  crctcsh  29752  clwlkclwwlklem2fv2  29923  clwlkclwwlklem2a  29925  clwwisshclwwslemlem  29940  clwwlkinwwlk  29967  clwwlkext2edg  29983  wwlksubclwwlk  29985  numclwwlk5  30315  topnfbey  30396  uzssico  32707  1fldgenq  33262  znfermltl  33327  rezh  33946  zrhre  33996  hashf2  34061  ballotlemfc0  34471  ballotlemfcc  34472  chpvalz  34606  chtvalz  34607  zltp1ne  35078  0nn0m1nnn0  35081  elfzm12  35643  nn0prpwlem  36286  poimirlem24  37614  mblfinlem1  37627  mblfinlem2  37628  itg2addnclem2  37642  fzmul  37711  incsequz2  37719  fimgmcyc  42504  ellz1  42737  lzunuz  42738  lzenom  42740  nerabdioph  42779  pell14qrgt0  42829  rmxycomplete  42888  monotuz  42912  monotoddzzfi  42913  oddcomabszz  42915  zindbi  42917  jm2.24  42934  congrep  42944  fzneg  42953  jm2.19  42964  fzunt  43426  fzunt1d  43428  fzuntgd  43429  oddfl  45254  fzdifsuc2  45287  climsuse  45585  stoweidlem26  46003  stoweidlem34  46011  fourierdlem20  46104  fourierdlem42  46126  fourierdlem51  46134  fourierdlem64  46147  fourierdlem76  46159  fourierdlem94  46177  fourierdlem97  46180  fourierdlem113  46196  natlocalincr  46853  natglobalincr  46854  zm1nn  47279  zgeltp1eq  47286  eluzge0nn0  47289  elfz2z  47292  2elfz2melfz  47295  elfzlble  47297  elfzelfzlble  47298  fzopredsuc  47300  ceilbi  47310  smonoord  47333  fsummmodsndifre  47336  iccpartipre  47383  iccpartiltu  47384  iccpartigtl  47385  icceuelpartlem  47397  fmtno4prmfac  47534  lighneallem4b  47571  dfeven3  47620  dfodd4  47621  nn0o1gt2ALTV  47656  nnoALTV  47657  fpprel2  47703  gbegt5  47723  gbowgt5  47724  sbgoldbwt  47739  nnsum3primesle9  47756  nnsum4primesodd  47758  nnsum4primesoddALTV  47759  evengpop3  47760  evengpoap3  47761  nnsum4primesevenALTV  47763  bgoldbtbndlem1  47767  bgoldbtbndlem2  47768  bgoldbtbndlem3  47769  bgoldbtbndlem4  47770  gpgprismgriedgdmss  48004  gpgusgralem  48008  gpgedgvtx1  48014  gpg5nbgrvtx03starlem2  48019  gpg5nbgrvtx13starlem2  48022  gpg3nbgrvtx0  48026  cznnring  48185  elfzolborelfzop1  48443  zgtp1leeq  48445  mod0mul  48447  modn0mul  48448  m1modmmod  48449  difmodm1lt  48450  rege1logbzge0  48487  fllog2  48496  dignn0ldlem  48530  dignn0flhalflem1  48543  dignn0flhalflem2  48544