Theorem zre 12253

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

Syntax hints:   → wi 4   ∨ w3o 1084   = wceq 1539   ∈ wcel 2108  ℝcr 10801  0cc0 10802  -cneg 11136  ℕcn 11903  ℤcz 12249

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 844  df-3or 1086  df-3an 1087  df-tru 1542  df-fal 1552  df-ex 1784  df-sb 2069  df-clab 2716  df-cleq 2730  df-clel 2817  df-rab 3072  df-v 3424  df-dif 3886  df-un 3888  df-in 3890  df-ss 3900  df-nul 4254  df-if 4457  df-sn 4559  df-pr 4561  df-op 4565  df-uni 4837  df-br 5071  df-iota 6376  df-fv 6426  df-ov 7258  df-neg 11138  df-z 12250

This theorem is referenced by:  zcn  12254  zrei  12255  zssre  12256  elnn0z  12262  elnnz1  12276  znnnlt1  12277  zletr  12294  znnsub  12296  znn0sub  12297  nzadd  12298  zltp1le  12300  zleltp1  12301  nn0ge0div  12319  zextle  12323  btwnnz  12326  suprzcl  12330  msqznn  12332  peano2uz2  12338  uzind  12342  fzind  12348  fnn0ind  12349  eluzuzle  12520  uzid  12526  uzneg  12531  uztric  12535  uz11  12536  eluzp1m1  12537  eluzp1p1  12539  eluzaddi  12540  eluzsubi  12541  subeluzsub  12544  uzin  12547  uz3m2nn  12560  peano2uz  12570  nn0pzuz  12574  uzwo  12580  eluz2b2  12590  uz2mulcl  12595  uzinfi  12597  eqreznegel  12603  lbzbi  12605  uzsupss  12609  nn01to3  12610  zmin  12613  zmax  12614  zbtwnre  12615  rebtwnz  12616  qre  12622  elpq  12644  rpnnen1lem2  12646  rpnnen1lem1  12647  rpnnen1lem3  12648  rpnnen1lem5  12650  z2ge  12861  qbtwnre  12862  zltaddlt1le  13166  elfz1eq  13196  fzn  13201  fzen  13202  uzsubsubfz  13207  fzaddel  13219  fzadd2  13220  ssfzunsnext  13230  ssfzunsn  13231  fzsuc2  13243  fzrev  13248  elfz1b  13254  fznuz  13267  uznfz  13268  fzp1nel  13269  elfz0fzfz0  13290  fz0fzelfz0  13291  fznn0sub2  13292  fz0fzdiffz0  13294  elfzmlbp  13296  difelfznle  13299  nelfzo  13321  elfzouz2  13330  fzo0n  13337  fzonlt0  13338  fzossrbm1  13344  fzospliti  13347  elfzo0z  13357  fzofzim  13362  fzo1fzo0n0  13366  eluzgtdifelfzo  13377  fzossfzop1  13393  ssfzoulel  13409  ssfzo12bi  13410  elfzonelfzo  13417  elfzomelpfzo  13419  elfznelfzob  13421  fzostep1  13431  fllt  13454  flid  13456  flbi2  13465  2tnp1ge0ge0  13477  flhalf  13478  fldiv4p1lem1div2  13483  fldiv4lem1div2uz2  13484  dfceil2  13487  ceile  13497  ceilid  13499  quoremz  13503  intfracq  13507  uzsup  13511  mulmod0  13525  zmod10  13535  zmodcl  13539  zmodfz  13541  zmodid2  13547  modcyc  13554  mulp1mod1  13560  modmuladd  13561  modmuladdim  13562  modmul1  13572  modaddmodup  13582  modaddmodlo  13583  modaddmulmod  13586  zsqcl2  13784  leexp2  13817  iexpcyc  13851  fi1uzind  14139  ccatsymb  14215  ccatval21sw  14218  lswccatn0lsw  14224  swrdnd  14295  swrdnnn0nd  14297  swrd0  14299  swrdswrdlem  14345  swrdswrd  14346  swrdccatin2  14370  pfxccatin12lem2  14372  pfxccatin12lem3  14373  repswswrd  14425  cshwmodn  14436  cshwsublen  14437  cshwidxmod  14444  cshwidxmodr  14445  cshwidxm1  14448  repswcshw  14453  2cshw  14454  cshweqrep  14462  cshw1  14463  swrd2lsw  14593  nn0abscl  14952  rexuzre  14992  dvdsval3  15895  p1modz1  15898  moddvds  15902  absdvdsb  15912  dvdsabsb  15913  dvdsle  15947  alzdvds  15957  mod2eq1n2dvds  15984  evennn02n  15987  evennn2n  15988  ltoddhalfle  15998  divalgmod  16043  fldivndvdslt  16051  flodddiv4t2lthalf  16053  bitsp1o  16068  gcdabs1  16164  gcdabsOLD  16167  modgcd  16168  bezoutlem1  16175  dfgcd2  16182  algcvga  16212  lcmabs  16238  isprm3  16316  dvdsnprmd  16323  2mulprm  16326  oddprmgt2  16332  sqnprm  16335  zgcdsq  16385  hashdvds  16404  vfermltlALT  16431  powm2modprm  16432  modprm0  16434  modprmn0modprm0  16436  fldivp1  16526  zgz  16562  4sqlem4  16581  prmgaplem5  16684  prmgaplem7  16686  cshwshashlem2  16726  setsstruct  16805  mulgmodid  18657  gexdvds  19104  zringunit  20600  prmirred  20608  znf1o  20671  chfacfscmul0  21915  chfacfscmulgsum  21917  chfacfpmmul0  21919  chfacfpmmulgsum  21921  dyadf  24660  dyadovol  24662  degltlem1  25142  coskpi  25584  cosne0  25590  relogexp  25656  cxpeq  25815  relogbzexp  25831  ppival2  26182  ppival2g  26183  ppiprm  26205  chtprm  26207  chtnprm  26208  ppip1le  26215  efexple  26334  zabsle1  26349  lgsdir2lem4  26381  lgsne0  26388  gausslemma2dlem1a  26418  gausslemma2dlem3  26421  gausslemma2dlem4  26422  lgsquadlem1  26433  lgsquadlem2  26434  2lgslem1a1  26442  2lgslem1a2  26443  2sqlem2  26471  rplogsumlem2  26538  pntrsumbnd  26619  axlowdim  27232  crctcshwlkn0lem3  28078  crctcshwlkn0lem5  28080  crctcshwlkn0  28087  crctcsh  28090  clwlkclwwlklem2fv2  28261  clwlkclwwlklem2a  28263  clwwisshclwwslemlem  28278  clwwlkinwwlk  28305  clwwlkext2edg  28321  wwlksubclwwlk  28323  numclwwlk5  28653  topnfbey  28734  uzssico  31007  znfermltl  31464  rezh  31821  zrhre  31869  hashf2  31952  ballotlemfc0  32359  ballotlemfcc  32360  chpvalz  32508  chtvalz  32509  zltp1ne  32968  0nn0m1nnn0  32971  elfzm12  33533  nn0prpwlem  34438  poimirlem24  35728  mblfinlem1  35741  mblfinlem2  35742  itg2addnclem2  35756  fzmul  35826  incsequz2  35834  ellz1  40505  lzunuz  40506  lzenom  40508  nerabdioph  40547  pell14qrgt0  40597  rmxycomplete  40655  monotuz  40679  monotoddzzfi  40680  oddcomabszz  40682  zindbi  40684  jm2.24  40701  congrep  40711  fzneg  40720  jm2.19  40731  oddfl  42705  fzdifsuc2  42739  climsuse  43039  stoweidlem26  43457  stoweidlem34  43465  fourierdlem20  43558  fourierdlem42  43580  fourierdlem51  43588  fourierdlem64  43601  fourierdlem76  43613  fourierdlem94  43631  fourierdlem97  43634  fourierdlem113  43650  zm1nn  44682  zgeltp1eq  44689  eluzge0nn0  44692  elfz2z  44695  2elfz2melfz  44698  elfzlble  44700  elfzelfzlble  44701  fzopredsuc  44703  smonoord  44711  fsummmodsndifre  44714  iccpartipre  44761  iccpartiltu  44762  iccpartigtl  44763  icceuelpartlem  44775  fmtno4prmfac  44912  lighneallem4b  44949  dfeven3  44998  dfodd4  44999  nn0o1gt2ALTV  45034  nnoALTV  45035  fpprel2  45081  gbegt5  45101  gbowgt5  45102  sbgoldbwt  45117  nnsum3primesle9  45134  nnsum4primesodd  45136  nnsum4primesoddALTV  45137  evengpop3  45138  evengpoap3  45139  nnsum4primesevenALTV  45141  bgoldbtbndlem1  45145  bgoldbtbndlem2  45146  bgoldbtbndlem3  45147  bgoldbtbndlem4  45148  cznnring  45402  elfzolborelfzop1  45748  zgtp1leeq  45750  mod0mul  45753  modn0mul  45754  m1modmmod  45755  difmodm1lt  45756  rege1logbzge0  45793  fllog2  45802  dignn0ldlem  45836  dignn0flhalflem1  45849  dignn0flhalflem2  45850