Theorem zre 12490

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

Syntax hints:   → wi 4   ∨ w3o 1085   = wceq 1541   ∈ wcel 2113  ℝcr 11023  0cc0 11024  -cneg 11363  ℕcn 12143  ℤcz 12486

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2706

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-sb 2068  df-clab 2713  df-cleq 2726  df-clel 2809  df-rab 3398  df-v 3440  df-dif 3902  df-un 3904  df-ss 3916  df-nul 4284  df-if 4478  df-sn 4579  df-pr 4581  df-op 4585  df-uni 4862  df-br 5097  df-iota 6446  df-fv 6498  df-ov 7359  df-neg 11365  df-z 12487

This theorem is referenced by:  zcn  12491  zrei  12492  zssre  12493  elnn0z  12499  elnnz1  12515  znnnlt1  12516  zletr  12533  znnsub  12535  znn0sub  12536  nzadd  12537  zltp1le  12539  zleltp1  12540  nn0ge0div  12559  zextle  12563  btwnnz  12566  suprzcl  12570  msqznn  12572  peano2uz2  12578  uzind  12582  fzind  12588  fnn0ind  12589  eluzuzle  12758  uzid  12764  uzneg  12769  uztric  12773  uz11  12774  eluzp1m1  12775  eluzp1p1  12777  eluzadd  12778  eluzsub  12779  subeluzsub  12782  uzin  12785  uz3m2nn  12805  peano2uz  12812  nn0pzuz  12816  uzwo  12822  eluz2b2  12832  uz2mulcl  12837  uzinfi  12839  eqreznegel  12845  lbzbi  12847  uzsupss  12851  nn01to3  12852  zmin  12855  zmax  12856  zbtwnre  12857  rebtwnz  12858  qre  12864  elpq  12886  rpnnen1lem2  12888  rpnnen1lem1  12889  rpnnen1lem3  12890  rpnnen1lem5  12892  z2ge  13111  qbtwnre  13112  zltaddlt1le  13419  elfz1eq  13449  fzn  13454  fzen  13455  uzsubsubfz  13460  fzaddel  13472  fzadd2  13473  ssfzunsnext  13483  ssfzunsn  13484  fzsuc2  13496  fzrev  13501  elfz1b  13507  fznuz  13523  uznfz  13524  fzp1nel  13525  elfz0fzfz0  13547  fz0fzelfz0  13548  fznn0sub2  13549  fz0fzdiffz0  13551  elfzmlbp  13553  difelfznle  13556  nelfzo  13578  elfzouz2  13588  fzo0n  13595  fzonlt0  13596  fzossrbm1  13602  fzospliti  13605  elfzo0z  13615  fzofzim  13623  fzo1fzo0n0  13629  eluzgtdifelfzo  13641  fzossfzop1  13657  ssfzoulel  13674  ssfzo12bi  13675  elfzonelfzo  13683  elfzomelpfzo  13686  elfznelfzob  13688  fzostep1  13700  fllt  13724  flid  13726  flbi2  13735  2tnp1ge0ge0  13747  flhalf  13748  fldiv4p1lem1div2  13753  fldiv4lem1div2uz2  13754  dfceil2  13757  ceile  13767  ceilid  13769  quoremz  13773  intfracq  13777  uzsup  13781  mulmod0  13795  zmod10  13805  zmodcl  13809  zmodfz  13811  zmodid2  13817  modcyc  13824  modaddid  13828  mulp1mod1  13832  muladdmod  13833  modmuladd  13834  modmuladdim  13835  modmul1  13845  modaddmodup  13855  modaddmodlo  13856  modaddmulmod  13859  zsqcl2  14059  leexp2  14092  iexpcyc  14128  fi1uzind  14428  ccatsymb  14504  ccatval21sw  14507  lswccatn0lsw  14513  swrdnd  14576  swrdnnn0nd  14578  swrd0  14580  swrdswrdlem  14625  swrdswrd  14626  swrdccatin2  14650  pfxccatin12lem2  14652  pfxccatin12lem3  14653  repswswrd  14705  cshwmodn  14716  cshwsublen  14717  cshwidxmod  14724  cshwidxmodr  14725  cshwidxm1  14728  repswcshw  14733  2cshw  14734  cshweqrep  14742  cshw1  14743  swrd2lsw  14873  nn0abscl  15233  rexuzre  15274  dvdsval3  16181  p1modz1  16184  moddvds  16188  absdvdsb  16199  dvdsabsb  16200  dvdsle  16235  alzdvds  16245  mod2eq1n2dvds  16272  evennn02n  16275  evennn2n  16276  ltoddhalfle  16286  divalgmod  16331  fldivndvdslt  16341  flodddiv4t2lthalf  16343  bitsp1o  16358  gcdabs1  16454  modgcd  16457  bezoutlem1  16464  dfgcd2  16471  algcvga  16504  lcmabs  16530  isprm3  16608  dvdsnprmd  16615  2mulprm  16618  oddprmgt2  16624  sqnprm  16627  zgcdsq  16678  hashdvds  16700  vfermltlALT  16728  powm2modprm  16729  modprm0  16731  modprmn0modprm0  16733  fldivp1  16823  zgz  16859  4sqlem4  16878  prmgaplem5  16981  prmgaplem7  16983  cshwshashlem2  17022  setsstruct  17101  mulgmodid  19041  gexdvds  19511  zringunit  21419  prmirred  21427  znf1o  21504  chfacfscmul0  22800  chfacfscmulgsum  22802  chfacfpmmul0  22804  chfacfpmmulgsum  22806  dyadf  25546  dyadovol  25548  degltlem1  26031  coskpi  26486  cosne0  26492  relogexp  26559  cxpeq  26721  relogbzexp  26740  ppival2  27092  ppival2g  27093  ppiprm  27115  chtprm  27117  chtnprm  27118  ppip1le  27125  efexple  27246  zabsle1  27261  lgsdir2lem4  27293  lgsne0  27300  gausslemma2dlem1a  27330  gausslemma2dlem3  27333  gausslemma2dlem4  27334  lgsquadlem1  27345  lgsquadlem2  27346  2lgslem1a1  27354  2lgslem1a2  27355  2sqlem2  27383  rplogsumlem2  27450  pntrsumbnd  27531  axlowdim  28983  crctcshwlkn0lem3  29834  crctcshwlkn0lem5  29836  crctcshwlkn0  29843  crctcsh  29846  clwlkclwwlklem2fv2  30020  clwlkclwwlklem2a  30022  clwwisshclwwslemlem  30037  clwwlkinwwlk  30064  clwwlkext2edg  30080  wwlksubclwwlk  30082  numclwwlk5  30412  topnfbey  30493  uzssico  32813  1fldgenq  33353  znfermltl  33396  ply1coedeg  33619  rezh  34075  zrhre  34125  hashf2  34190  ballotlemfc0  34599  ballotlemfcc  34600  chpvalz  34734  chtvalz  34735  zltp1ne  35253  0nn0m1nnn0  35256  elfzm12  35818  nn0prpwlem  36465  poimirlem24  37784  mblfinlem1  37797  mblfinlem2  37798  itg2addnclem2  37812  fzmul  37881  incsequz2  37889  fimgmcyc  42731  ellz1  42951  lzunuz  42952  lzenom  42954  nerabdioph  42993  pell14qrgt0  43043  rmxycomplete  43101  monotuz  43125  monotoddzzfi  43126  oddcomabszz  43128  zindbi  43130  jm2.24  43147  congrep  43157  fzneg  43166  jm2.19  43177  fzunt  43638  fzunt1d  43640  fzuntgd  43641  oddfl  45468  fzdifsuc2  45500  climsuse  45796  stoweidlem26  46212  stoweidlem34  46220  fourierdlem20  46313  fourierdlem42  46335  fourierdlem51  46343  fourierdlem64  46356  fourierdlem76  46368  fourierdlem94  46386  fourierdlem97  46389  fourierdlem113  46405  natlocalincr  47062  natglobalincr  47063  zm1nn  47490  zgeltp1eq  47497  eluzge0nn0  47500  elfz2z  47503  2elfz2melfz  47506  elfzlble  47508  elfzelfzlble  47509  fzopredsuc  47511  ceilbi  47521  mod0mul  47544  modn0mul  47545  m1modmmod  47546  difmodm1lt  47547  mod2addne  47552  modm2nep1  47554  modp2nep1  47555  modm1nep2  47556  modm1nem2  47557  modm1p1ne  47558  smonoord  47559  fsummmodsndifre  47562  iccpartipre  47609  iccpartiltu  47610  iccpartigtl  47611  icceuelpartlem  47623  fmtno4prmfac  47760  lighneallem4b  47797  dfeven3  47846  dfodd4  47847  nn0o1gt2ALTV  47882  nnoALTV  47883  fpprel2  47929  gbegt5  47949  gbowgt5  47950  sbgoldbwt  47965  nnsum3primesle9  47982  nnsum4primesodd  47984  nnsum4primesoddALTV  47985  evengpop3  47986  evengpoap3  47987  nnsum4primesevenALTV  47989  bgoldbtbndlem1  47993  bgoldbtbndlem2  47994  bgoldbtbndlem3  47995  bgoldbtbndlem4  47996  gpgprismgriedgdmss  48240  gpgusgralem  48244  gpgedgvtx1  48250  gpg5nbgrvtx03starlem2  48257  gpg5nbgrvtx13starlem2  48260  gpg3nbgrvtx0  48264  cznnring  48450  elfzolborelfzop1  48707  zgtp1leeq  48709  rege1logbzge0  48747  fllog2  48756  dignn0ldlem  48790  dignn0flhalflem1  48803  dignn0flhalflem2  48804