Theorem zre 11258

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

Syntax hints:   → wi 4   ∨ w3o 1030   = wceq 1475   ∈ wcel 1977  ℝcr 9814  0cc0 9815  -cneg 10146  ℕcn 10897  ℤcz 11254

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590

This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-3or 1032  df-3an 1033  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-rex 2902  df-rab 2905  df-v 3175  df-dif 3543  df-un 3545  df-in 3547  df-ss 3554  df-nul 3875  df-if 4037  df-sn 4126  df-pr 4128  df-op 4132  df-uni 4373  df-br 4584  df-iota 5768  df-fv 5812  df-ov 6552  df-neg 10148  df-z 11255

This theorem is referenced by:  zcn  11259  zrei  11260  zssre  11261  elnn0z  11267  elnnz1  11280  znnnlt1  11281  zletr  11298  znnsub  11300  znn0sub  11301  nzadd  11302  zltp1le  11304  zleltp1  11305  nn0ge0div  11322  zextle  11326  btwnnz  11329  suprzcl  11333  msqznn  11335  peano2uz2  11341  uzind  11345  fzind  11351  fnn0ind  11352  eluzuzle  11572  uzid  11578  uzneg  11582  uztric  11585  uz11  11586  eluzp1m1  11587  eluzp1p1  11589  eluzaddi  11590  eluzsubi  11591  uzin  11596  uz3m2nn  11607  peano2uz  11617  nn0pzuz  11621  uzwo  11627  eluz2b2  11637  uz2mulcl  11642  uzinfi  11644  eqreznegel  11650  lbzbi  11652  uzsupss  11656  nn01to3  11657  zmin  11660  zmax  11661  zbtwnre  11662  rebtwnz  11663  qre  11669  rpnnen1lem2  11690  rpnnen1lem1  11691  rpnnen1lem3  11692  rpnnen1lem5  11694  rpnnen1lem1OLD  11697  rpnnen1lem3OLD  11698  rpnnen1lem5OLD  11700  z2ge  11903  qbtwnre  11904  zltaddlt1le  12195  elfz1eq  12223  fzn  12228  fzen  12229  uzsubsubfz  12234  fzaddel  12246  fzadd2  12247  ssfzunsn  12257  fzsuc2  12268  fzrev  12273  elfz1b  12279  fznuz  12291  uznfz  12292  fzp1nel  12293  elfz0fzfz0  12313  fz0fzelfz0  12314  fznn0sub2  12315  fz0fzdiffz0  12317  elfzmlbp  12319  difelfznle  12322  nelfzo  12344  elfzouz2  12353  fzo0n  12359  fzonlt0  12360  fzossrbm1  12366  fzospliti  12369  elfzo0z  12377  fzofzim  12382  fzo1fzo0n0  12386  eluzgtdifelfzo  12397  fzossfzop1  12412  ssfzoulel  12428  ssfzo12bi  12429  elfzonelfzo  12436  elfzomelpfzo  12438  elfznelfzob  12440  fzosplitprm1  12443  fzostep1  12446  fllt  12469  flid  12471  flbi2  12480  2tnp1ge0ge0  12492  flhalf  12493  fldiv4p1lem1div2  12498  fldiv4lem1div2uz2  12499  dfceil2  12502  ceile  12510  ceilid  12512  quoremz  12516  intfracq  12520  uzsup  12524  mulmod0  12538  zmod10  12548  zmodcl  12552  zmodfz  12554  zmodid2  12560  modcyc  12567  mulp1mod1  12573  modmuladd  12574  modmuladdim  12575  modmul1  12585  modaddmodup  12595  modaddmodlo  12596  modaddmulmod  12599  leexp2  12777  zsqcl2  12803  iexpcyc  12831  fi1uzind  13134  fi1uzindOLD  13140  ccatsymb  13219  lswccatn0lsw  13226  swrdnd  13284  swrd0  13286  swrdswrdlem  13311  swrdswrd  13312  swrdccatin2  13338  swrdccatin12lem2  13340  swrdccatin12lem3  13341  repswswrd  13382  cshwmodn  13392  cshwsublen  13393  cshwidxmod  13400  cshwidxmodr  13401  cshwidxm1  13404  repswcshw  13409  2cshw  13410  cshweqrep  13418  cshw1  13419  swrd2lsw  13543  nn0abscl  13900  rexuzre  13940  znnenlem  14779  dvdsval3  14825  moddvds  14829  absdvdsb  14838  dvdsabsb  14839  dvdsle  14870  alzdvds  14880  mulmoddvds  14889  mod2eq1n2dvds  14909  evennn02n  14912  evennn2n  14913  ltoddhalfle  14923  divalgmod  14967  divalgmodOLD  14968  fldivndvdslt  14976  flodddiv4t2lthalf  14978  bitsp1o  14993  gcdabs  15088  gcdabs1  15089  modgcd  15091  bezoutlem1  15094  dfgcd2  15101  algcvga  15130  lcmabs  15156  isprm3  15234  dvdsnprmd  15241  oddprmgt2  15249  sqnprm  15252  zgcdsq  15299  hashdvds  15318  vfermltlALT  15345  powm2modprm  15346  modprm0  15348  modprmn0modprm0  15350  fldivp1  15439  zgz  15475  4sqlem4  15494  prmgaplem5  15597  prmgaplem7  15599  cshwshashlem2  15641  mulgmodid  17404  gexdvds  17822  zringunit  19655  prmirred  19662  znf1o  19719  chfacfscmul0  20482  chfacfscmulgsum  20484  chfacfpmmul0  20486  chfacfpmmulgsum  20488  dyadf  23165  dyadovol  23167  degltlem1  23636  coskpi  24076  cosne0  24080  relogexp  24146  cxpeq  24298  relogbzexp  24314  ppival2  24654  ppival2g  24655  ppiprm  24677  chtprm  24679  chtnprm  24680  ppip1le  24687  efexple  24806  zabsle1  24821  lgsdir2lem4  24853  lgsne0  24860  gausslemma2dlem1a  24890  gausslemma2dlem3  24893  gausslemma2dlem4  24894  lgsquadlem1  24905  lgsquadlem2  24906  2lgslem1a1  24914  2lgslem1a2  24915  2sqlem2  24943  rplogsumlem2  24974  pntrsumbnd  25055  axlowdim  25641  clwlkisclwwlklem2fv2  26311  clwlkisclwwlklem2a  26313  clwwlkext2edg  26330  wwlksubclwwlk  26332  clwwisshclwwlem1  26333  usg2cwwkdifex  26349  clwlkfclwwlk  26371  extwwlkfablem2  26605  numclwwlkovf2ex  26613  numclwlk1lem2f1  26621  frgrareg  26644  frgraregord013  26645  topnfbey  26717  rezh  29343  zrhre  29391  hashf2  29473  ballotlemfc0  29881  ballotlemfcc  29882  elfzm12  30823  nn0prpwlem  31487  poimirlem24  32603  mblfinlem1  32616  mblfinlem2  32617  itg2addnclem2  32632  fzmul  32707  incsequz2  32715  ellz1  36348  lzunuz  36349  lzenom  36351  nerabdioph  36391  pell14qrgt0  36441  rmxycomplete  36500  monotuz  36524  monotoddzzfi  36525  oddcomabszz  36527  zindbi  36529  jm2.24  36548  congrep  36558  fzneg  36567  jm2.19  36578  oddfl  38430  fzdifsuc2  38466  climsuse  38675  stoweidlem26  38919  stoweidlem34  38927  fourierdlem20  39020  fourierdlem42  39042  fourierdlem51  39050  fourierdlem64  39063  fourierdlem76  39075  fourierdlem94  39093  fourierdlem97  39096  fourierdlem113  39112  zgeltp1eq  39943  smonoord  39944  fzopredsuc  39946  iccpartipre  39959  iccpartiltu  39960  iccpartigtl  39961  icceuelpartlem  39973  fmtno4prmfac  40022  lighneallem4b  40064  dfeven3  40108  dfodd4  40109  nn0o1gt2ALTV  40143  nnoALTV  40144  gbegt5  40183  gbogt5  40184  bgoldbwt  40199  nnsum3primesle9  40210  nnsum4primesodd  40212  nnsum4primesoddALTV  40213  evengpop3  40214  evengpoap3  40215  nnsum4primesevenALTV  40217  bgoldbtbndlem1  40221  bgoldbtbndlem2  40222  bgoldbtbndlem3  40223  bgoldbtbndlem4  40224  pfxccatin12lem2  40287  zm1nn  40348  eluzge0nn0  40350  elfz2z  40352  2elfz2melfz  40355  elfzlble  40357  elfzelfzlble  40358  fsummmodsndifre  40373  crctcsh1wlkn0lem3  41015  crctcsh1wlkn0lem5  41017  crctcsh1wlkn0  41024  crctcsh  41027  clwlkclwwlklem2fv2  41205  clwlkclwwlklem2a  41207  clwwlksext2edg  41230  wwlksubclwwlks  41232  clwwisshclwwslemlem  41233  clwlksfclwwlk  41269  av-numclwwlkovf2ex  41517  av-numclwlk1lem2f1  41524  av-numclwwlk5  41542  cznnring  41748  elfzolborelfzop1  42103  zgtp1leeq  42105  mod0mul  42108  modn0mul  42109  m1modmmod  42110  difmodm1lt  42111  rege1logbzge0  42151  fllog2  42160  dignn0ldlem  42194  dignn0flhalflem1  42207  dignn0flhalflem2  42208