Theorem zre 12472

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

Syntax hints:   → wi 4   ∨ w3o 1085   = wceq 1541   ∈ wcel 2111  ℝcr 11005  0cc0 11006  -cneg 11345  ℕcn 12125  ℤcz 12468

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 2113  ax-9 2121  ax-ext 2703

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 2710  df-cleq 2723  df-clel 2806  df-rab 3396  df-v 3438  df-dif 3900  df-un 3902  df-ss 3914  df-nul 4281  df-if 4473  df-sn 4574  df-pr 4576  df-op 4580  df-uni 4857  df-br 5090  df-iota 6437  df-fv 6489  df-ov 7349  df-neg 11347  df-z 12469

This theorem is referenced by:  zcn  12473  zrei  12474  zssre  12475  elnn0z  12481  elnnz1  12498  znnnlt1  12499  zletr  12516  znnsub  12518  znn0sub  12519  nzadd  12520  zltp1le  12522  zleltp1  12523  nn0ge0div  12542  zextle  12546  btwnnz  12549  suprzcl  12553  msqznn  12555  peano2uz2  12561  uzind  12565  fzind  12571  fnn0ind  12572  eluzuzle  12741  uzid  12747  uzneg  12752  uztric  12756  uz11  12757  eluzp1m1  12758  eluzp1p1  12760  eluzadd  12761  eluzsub  12762  eluzaddiOLD  12764  eluzsubiOLD  12766  subeluzsub  12769  uzin  12772  uz3m2nn  12792  peano2uz  12799  nn0pzuz  12803  uzwo  12809  eluz2b2  12819  uz2mulcl  12824  uzinfi  12826  eqreznegel  12832  lbzbi  12834  uzsupss  12838  nn01to3  12839  zmin  12842  zmax  12843  zbtwnre  12844  rebtwnz  12845  qre  12851  elpq  12873  rpnnen1lem2  12875  rpnnen1lem1  12876  rpnnen1lem3  12877  rpnnen1lem5  12879  z2ge  13097  qbtwnre  13098  zltaddlt1le  13405  elfz1eq  13435  fzn  13440  fzen  13441  uzsubsubfz  13446  fzaddel  13458  fzadd2  13459  ssfzunsnext  13469  ssfzunsn  13470  fzsuc2  13482  fzrev  13487  elfz1b  13493  fznuz  13509  uznfz  13510  fzp1nel  13511  elfz0fzfz0  13533  fz0fzelfz0  13534  fznn0sub2  13535  fz0fzdiffz0  13537  elfzmlbp  13539  difelfznle  13542  nelfzo  13564  elfzouz2  13574  fzo0n  13581  fzonlt0  13582  fzossrbm1  13588  fzospliti  13591  elfzo0z  13601  fzofzim  13609  fzo1fzo0n0  13615  eluzgtdifelfzo  13627  fzossfzop1  13643  ssfzoulel  13660  ssfzo12bi  13661  elfzonelfzo  13669  elfzomelpfzo  13672  elfznelfzob  13674  fzostep1  13686  fllt  13710  flid  13712  flbi2  13721  2tnp1ge0ge0  13733  flhalf  13734  fldiv4p1lem1div2  13739  fldiv4lem1div2uz2  13740  dfceil2  13743  ceile  13753  ceilid  13755  quoremz  13759  intfracq  13763  uzsup  13767  mulmod0  13781  zmod10  13791  zmodcl  13795  zmodfz  13797  zmodid2  13803  modcyc  13810  modaddid  13814  mulp1mod1  13818  muladdmod  13819  modmuladd  13820  modmuladdim  13821  modmul1  13831  modaddmodup  13841  modaddmodlo  13842  modaddmulmod  13845  zsqcl2  14045  leexp2  14078  iexpcyc  14114  fi1uzind  14414  ccatsymb  14490  ccatval21sw  14493  lswccatn0lsw  14499  swrdnd  14562  swrdnnn0nd  14564  swrd0  14566  swrdswrdlem  14611  swrdswrd  14612  swrdccatin2  14636  pfxccatin12lem2  14638  pfxccatin12lem3  14639  repswswrd  14691  cshwmodn  14702  cshwsublen  14703  cshwidxmod  14710  cshwidxmodr  14711  cshwidxm1  14714  repswcshw  14719  2cshw  14720  cshweqrep  14728  cshw1  14729  swrd2lsw  14859  nn0abscl  15219  rexuzre  15260  dvdsval3  16167  p1modz1  16170  moddvds  16174  absdvdsb  16185  dvdsabsb  16186  dvdsle  16221  alzdvds  16231  mod2eq1n2dvds  16258  evennn02n  16261  evennn2n  16262  ltoddhalfle  16272  divalgmod  16317  fldivndvdslt  16327  flodddiv4t2lthalf  16329  bitsp1o  16344  gcdabs1  16440  modgcd  16443  bezoutlem1  16450  dfgcd2  16457  algcvga  16490  lcmabs  16516  isprm3  16594  dvdsnprmd  16601  2mulprm  16604  oddprmgt2  16610  sqnprm  16613  zgcdsq  16664  hashdvds  16686  vfermltlALT  16714  powm2modprm  16715  modprm0  16717  modprmn0modprm0  16719  fldivp1  16809  zgz  16845  4sqlem4  16864  prmgaplem5  16967  prmgaplem7  16969  cshwshashlem2  17008  setsstruct  17087  mulgmodid  19026  gexdvds  19496  zringunit  21403  prmirred  21411  znf1o  21488  chfacfscmul0  22773  chfacfscmulgsum  22775  chfacfpmmul0  22777  chfacfpmmulgsum  22779  dyadf  25519  dyadovol  25521  degltlem1  26004  coskpi  26459  cosne0  26465  relogexp  26532  cxpeq  26694  relogbzexp  26713  ppival2  27065  ppival2g  27066  ppiprm  27088  chtprm  27090  chtnprm  27091  ppip1le  27098  efexple  27219  zabsle1  27234  lgsdir2lem4  27266  lgsne0  27273  gausslemma2dlem1a  27303  gausslemma2dlem3  27306  gausslemma2dlem4  27307  lgsquadlem1  27318  lgsquadlem2  27319  2lgslem1a1  27327  2lgslem1a2  27328  2sqlem2  27356  rplogsumlem2  27423  pntrsumbnd  27504  axlowdim  28939  crctcshwlkn0lem3  29790  crctcshwlkn0lem5  29792  crctcshwlkn0  29799  crctcsh  29802  clwlkclwwlklem2fv2  29976  clwlkclwwlklem2a  29978  clwwisshclwwslemlem  29993  clwwlkinwwlk  30020  clwwlkext2edg  30036  wwlksubclwwlk  30038  numclwwlk5  30368  topnfbey  30449  uzssico  32767  1fldgenq  33288  znfermltl  33331  rezh  33982  zrhre  34032  hashf2  34097  ballotlemfc0  34506  ballotlemfcc  34507  chpvalz  34641  chtvalz  34642  zltp1ne  35154  0nn0m1nnn0  35157  elfzm12  35719  nn0prpwlem  36366  poimirlem24  37694  mblfinlem1  37707  mblfinlem2  37708  itg2addnclem2  37722  fzmul  37791  incsequz2  37799  fimgmcyc  42637  ellz1  42870  lzunuz  42871  lzenom  42873  nerabdioph  42912  pell14qrgt0  42962  rmxycomplete  43020  monotuz  43044  monotoddzzfi  43045  oddcomabszz  43047  zindbi  43049  jm2.24  43066  congrep  43076  fzneg  43085  jm2.19  43096  fzunt  43558  fzunt1d  43560  fzuntgd  43561  oddfl  45389  fzdifsuc2  45421  climsuse  45718  stoweidlem26  46134  stoweidlem34  46142  fourierdlem20  46235  fourierdlem42  46257  fourierdlem51  46265  fourierdlem64  46278  fourierdlem76  46290  fourierdlem94  46308  fourierdlem97  46311  fourierdlem113  46327  natlocalincr  46984  natglobalincr  46985  zm1nn  47412  zgeltp1eq  47419  eluzge0nn0  47422  elfz2z  47425  2elfz2melfz  47428  elfzlble  47430  elfzelfzlble  47431  fzopredsuc  47433  ceilbi  47443  mod0mul  47466  modn0mul  47467  m1modmmod  47468  difmodm1lt  47469  mod2addne  47474  modm2nep1  47476  modp2nep1  47477  modm1nep2  47478  modm1nem2  47479  modm1p1ne  47480  smonoord  47481  fsummmodsndifre  47484  iccpartipre  47531  iccpartiltu  47532  iccpartigtl  47533  icceuelpartlem  47545  fmtno4prmfac  47682  lighneallem4b  47719  dfeven3  47768  dfodd4  47769  nn0o1gt2ALTV  47804  nnoALTV  47805  fpprel2  47851  gbegt5  47871  gbowgt5  47872  sbgoldbwt  47887  nnsum3primesle9  47904  nnsum4primesodd  47906  nnsum4primesoddALTV  47907  evengpop3  47908  evengpoap3  47909  nnsum4primesevenALTV  47911  bgoldbtbndlem1  47915  bgoldbtbndlem2  47916  bgoldbtbndlem3  47917  bgoldbtbndlem4  47918  gpgprismgriedgdmss  48162  gpgusgralem  48166  gpgedgvtx1  48172  gpg5nbgrvtx03starlem2  48179  gpg5nbgrvtx13starlem2  48182  gpg3nbgrvtx0  48186  cznnring  48372  elfzolborelfzop1  48630  zgtp1leeq  48632  rege1logbzge0  48670  fllog2  48679  dignn0ldlem  48713  dignn0flhalflem1  48726  dignn0flhalflem2  48727