Theorem zre 12509

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

Syntax hints:   → wi 4   ∨ w3o 1085   = wceq 1540   ∈ wcel 2109  ℝcr 11043  0cc0 11044  -cneg 11382  ℕcn 12162  ℤcz 12505

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 2008  ax-8 2111  ax-9 2119  ax-ext 2701

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 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-rab 3403  df-v 3446  df-dif 3914  df-un 3916  df-ss 3928  df-nul 4293  df-if 4485  df-sn 4586  df-pr 4588  df-op 4592  df-uni 4868  df-br 5103  df-iota 6452  df-fv 6507  df-ov 7372  df-neg 11384  df-z 12506

This theorem is referenced by:  zcn  12510  zrei  12511  zssre  12512  elnn0z  12518  elnnz1  12535  znnnlt1  12536  zletr  12553  znnsub  12555  znn0sub  12556  nzadd  12557  zltp1le  12559  zleltp1  12560  nn0ge0div  12579  zextle  12583  btwnnz  12586  suprzcl  12590  msqznn  12592  peano2uz2  12598  uzind  12602  fzind  12608  fnn0ind  12609  eluzuzle  12778  uzid  12784  uzneg  12789  uztric  12793  uz11  12794  eluzp1m1  12795  eluzp1p1  12797  eluzadd  12798  eluzsub  12799  eluzaddiOLD  12801  eluzsubiOLD  12803  subeluzsub  12806  uzin  12809  uz3m2nn  12829  peano2uz  12836  nn0pzuz  12840  uzwo  12846  eluz2b2  12856  uz2mulcl  12861  uzinfi  12863  eqreznegel  12869  lbzbi  12871  uzsupss  12875  nn01to3  12876  zmin  12879  zmax  12880  zbtwnre  12881  rebtwnz  12882  qre  12888  elpq  12910  rpnnen1lem2  12912  rpnnen1lem1  12913  rpnnen1lem3  12914  rpnnen1lem5  12916  z2ge  13134  qbtwnre  13135  zltaddlt1le  13442  elfz1eq  13472  fzn  13477  fzen  13478  uzsubsubfz  13483  fzaddel  13495  fzadd2  13496  ssfzunsnext  13506  ssfzunsn  13507  fzsuc2  13519  fzrev  13524  elfz1b  13530  fznuz  13546  uznfz  13547  fzp1nel  13548  elfz0fzfz0  13570  fz0fzelfz0  13571  fznn0sub2  13572  fz0fzdiffz0  13574  elfzmlbp  13576  difelfznle  13579  nelfzo  13601  elfzouz2  13611  fzo0n  13618  fzonlt0  13619  fzossrbm1  13625  fzospliti  13628  elfzo0z  13638  fzofzim  13646  fzo1fzo0n0  13652  eluzgtdifelfzo  13664  fzossfzop1  13680  ssfzoulel  13697  ssfzo12bi  13698  elfzonelfzo  13706  elfzomelpfzo  13708  elfznelfzob  13710  fzostep1  13720  fllt  13744  flid  13746  flbi2  13755  2tnp1ge0ge0  13767  flhalf  13768  fldiv4p1lem1div2  13773  fldiv4lem1div2uz2  13774  dfceil2  13777  ceile  13787  ceilid  13789  quoremz  13793  intfracq  13797  uzsup  13801  mulmod0  13815  zmod10  13825  zmodcl  13829  zmodfz  13831  zmodid2  13837  modcyc  13844  modaddid  13848  mulp1mod1  13852  muladdmod  13853  modmuladd  13854  modmuladdim  13855  modmul1  13865  modaddmodup  13875  modaddmodlo  13876  modaddmulmod  13879  zsqcl2  14079  leexp2  14112  iexpcyc  14148  fi1uzind  14448  ccatsymb  14523  ccatval21sw  14526  lswccatn0lsw  14532  swrdnd  14595  swrdnnn0nd  14597  swrd0  14599  swrdswrdlem  14645  swrdswrd  14646  swrdccatin2  14670  pfxccatin12lem2  14672  pfxccatin12lem3  14673  repswswrd  14725  cshwmodn  14736  cshwsublen  14737  cshwidxmod  14744  cshwidxmodr  14745  cshwidxm1  14748  repswcshw  14753  2cshw  14754  cshweqrep  14762  cshw1  14763  swrd2lsw  14894  nn0abscl  15254  rexuzre  15295  dvdsval3  16202  p1modz1  16205  moddvds  16209  absdvdsb  16220  dvdsabsb  16221  dvdsle  16256  alzdvds  16266  mod2eq1n2dvds  16293  evennn02n  16296  evennn2n  16297  ltoddhalfle  16307  divalgmod  16352  fldivndvdslt  16362  flodddiv4t2lthalf  16364  bitsp1o  16379  gcdabs1  16475  modgcd  16478  bezoutlem1  16485  dfgcd2  16492  algcvga  16525  lcmabs  16551  isprm3  16629  dvdsnprmd  16636  2mulprm  16639  oddprmgt2  16645  sqnprm  16648  zgcdsq  16699  hashdvds  16721  vfermltlALT  16749  powm2modprm  16750  modprm0  16752  modprmn0modprm0  16754  fldivp1  16844  zgz  16880  4sqlem4  16899  prmgaplem5  17002  prmgaplem7  17004  cshwshashlem2  17043  setsstruct  17122  mulgmodid  19021  gexdvds  19490  zringunit  21352  prmirred  21360  znf1o  21437  chfacfscmul0  22721  chfacfscmulgsum  22723  chfacfpmmul0  22725  chfacfpmmulgsum  22727  dyadf  25468  dyadovol  25470  degltlem1  25953  coskpi  26408  cosne0  26414  relogexp  26481  cxpeq  26643  relogbzexp  26662  ppival2  27014  ppival2g  27015  ppiprm  27037  chtprm  27039  chtnprm  27040  ppip1le  27047  efexple  27168  zabsle1  27183  lgsdir2lem4  27215  lgsne0  27222  gausslemma2dlem1a  27252  gausslemma2dlem3  27255  gausslemma2dlem4  27256  lgsquadlem1  27267  lgsquadlem2  27268  2lgslem1a1  27276  2lgslem1a2  27277  2sqlem2  27305  rplogsumlem2  27372  pntrsumbnd  27453  axlowdim  28864  crctcshwlkn0lem3  29715  crctcshwlkn0lem5  29717  crctcshwlkn0  29724  crctcsh  29727  clwlkclwwlklem2fv2  29898  clwlkclwwlklem2a  29900  clwwisshclwwslemlem  29915  clwwlkinwwlk  29942  clwwlkext2edg  29958  wwlksubclwwlk  29960  numclwwlk5  30290  topnfbey  30371  uzssico  32680  1fldgenq  33245  znfermltl  33310  rezh  33932  zrhre  33982  hashf2  34047  ballotlemfc0  34457  ballotlemfcc  34458  chpvalz  34592  chtvalz  34593  zltp1ne  35070  0nn0m1nnn0  35073  elfzm12  35635  nn0prpwlem  36283  poimirlem24  37611  mblfinlem1  37624  mblfinlem2  37625  itg2addnclem2  37639  fzmul  37708  incsequz2  37716  fimgmcyc  42495  ellz1  42728  lzunuz  42729  lzenom  42731  nerabdioph  42770  pell14qrgt0  42820  rmxycomplete  42879  monotuz  42903  monotoddzzfi  42904  oddcomabszz  42906  zindbi  42908  jm2.24  42925  congrep  42935  fzneg  42944  jm2.19  42955  fzunt  43417  fzunt1d  43419  fzuntgd  43420  oddfl  45249  fzdifsuc2  45281  climsuse  45579  stoweidlem26  45997  stoweidlem34  46005  fourierdlem20  46098  fourierdlem42  46120  fourierdlem51  46128  fourierdlem64  46141  fourierdlem76  46153  fourierdlem94  46171  fourierdlem97  46174  fourierdlem113  46190  natlocalincr  46847  natglobalincr  46848  zm1nn  47276  zgeltp1eq  47283  eluzge0nn0  47286  elfz2z  47289  2elfz2melfz  47292  elfzlble  47294  elfzelfzlble  47295  fzopredsuc  47297  ceilbi  47307  mod0mul  47330  modn0mul  47331  m1modmmod  47332  difmodm1lt  47333  mod2addne  47338  modm2nep1  47340  modp2nep1  47341  modm1nep2  47342  modm1nem2  47343  modm1p1ne  47344  smonoord  47345  fsummmodsndifre  47348  iccpartipre  47395  iccpartiltu  47396  iccpartigtl  47397  icceuelpartlem  47409  fmtno4prmfac  47546  lighneallem4b  47583  dfeven3  47632  dfodd4  47633  nn0o1gt2ALTV  47668  nnoALTV  47669  fpprel2  47715  gbegt5  47735  gbowgt5  47736  sbgoldbwt  47751  nnsum3primesle9  47768  nnsum4primesodd  47770  nnsum4primesoddALTV  47771  evengpop3  47772  evengpoap3  47773  nnsum4primesevenALTV  47775  bgoldbtbndlem1  47779  bgoldbtbndlem2  47780  bgoldbtbndlem3  47781  bgoldbtbndlem4  47782  gpgprismgriedgdmss  48016  gpgusgralem  48020  gpgedgvtx1  48026  gpg5nbgrvtx03starlem2  48033  gpg5nbgrvtx13starlem2  48036  gpg3nbgrvtx0  48040  cznnring  48223  elfzolborelfzop1  48481  zgtp1leeq  48483  rege1logbzge0  48521  fllog2  48530  dignn0ldlem  48564  dignn0flhalflem1  48577  dignn0flhalflem2  48578