Theorem zre 12504

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

Syntax hints:   → wi 4   ∨ w3o 1086   = wceq 1542   ∈ wcel 2114  ℝcr 11037  0cc0 11038  -cneg 11377  ℕcn 12157  ℤcz 12500

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3or 1088  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-rab 3402  df-v 3444  df-dif 3906  df-un 3908  df-ss 3920  df-nul 4288  df-if 4482  df-sn 4583  df-pr 4585  df-op 4589  df-uni 4866  df-br 5101  df-iota 6456  df-fv 6508  df-ov 7371  df-neg 11379  df-z 12501

This theorem is referenced by:  zcn  12505  zrei  12506  zssre  12507  elnn0z  12513  elnnz1  12529  znnnlt1  12530  zletr  12547  znnsub  12549  znn0sub  12550  nzadd  12551  zltp1le  12553  zleltp1  12554  nn0ge0div  12573  zextle  12577  btwnnz  12580  suprzcl  12584  msqznn  12586  peano2uz2  12592  uzind  12596  fzind  12602  fnn0ind  12603  eluzuzle  12772  uzid  12778  uzneg  12783  uztric  12787  uz11  12788  eluzp1m1  12789  eluzp1p1  12791  eluzadd  12792  eluzsub  12793  subeluzsub  12796  uzin  12799  uz3m2nn  12819  peano2uz  12826  nn0pzuz  12830  uzwo  12836  eluz2b2  12846  uz2mulcl  12851  uzinfi  12853  eqreznegel  12859  lbzbi  12861  uzsupss  12865  nn01to3  12866  zmin  12869  zmax  12870  zbtwnre  12871  rebtwnz  12872  qre  12878  elpq  12900  rpnnen1lem2  12902  rpnnen1lem1  12903  rpnnen1lem3  12904  rpnnen1lem5  12906  z2ge  13125  qbtwnre  13126  zltaddlt1le  13433  elfz1eq  13463  fzn  13468  fzen  13469  uzsubsubfz  13474  fzaddel  13486  fzadd2  13487  ssfzunsnext  13497  ssfzunsn  13498  fzsuc2  13510  fzrev  13515  elfz1b  13521  fznuz  13537  uznfz  13538  fzp1nel  13539  elfz0fzfz0  13561  fz0fzelfz0  13562  fznn0sub2  13563  fz0fzdiffz0  13565  elfzmlbp  13567  difelfznle  13570  nelfzo  13592  elfzouz2  13602  fzo0n  13609  fzonlt0  13610  fzossrbm1  13616  fzospliti  13619  elfzo0z  13629  fzofzim  13637  fzo1fzo0n0  13643  eluzgtdifelfzo  13655  fzossfzop1  13671  ssfzoulel  13688  ssfzo12bi  13689  elfzonelfzo  13697  elfzomelpfzo  13700  elfznelfzob  13702  fzostep1  13714  fllt  13738  flid  13740  flbi2  13749  2tnp1ge0ge0  13761  flhalf  13762  fldiv4p1lem1div2  13767  fldiv4lem1div2uz2  13768  dfceil2  13771  ceile  13781  ceilid  13783  quoremz  13787  intfracq  13791  uzsup  13795  mulmod0  13809  zmod10  13819  zmodcl  13823  zmodfz  13825  zmodid2  13831  modcyc  13838  modaddid  13842  mulp1mod1  13846  muladdmod  13847  modmuladd  13848  modmuladdim  13849  modmul1  13859  modaddmodup  13869  modaddmodlo  13870  modaddmulmod  13873  zsqcl2  14073  leexp2  14106  iexpcyc  14142  fi1uzind  14442  ccatsymb  14518  ccatval21sw  14521  lswccatn0lsw  14527  swrdnd  14590  swrdnnn0nd  14592  swrd0  14594  swrdswrdlem  14639  swrdswrd  14640  swrdccatin2  14664  pfxccatin12lem2  14666  pfxccatin12lem3  14667  repswswrd  14719  cshwmodn  14730  cshwsublen  14731  cshwidxmod  14738  cshwidxmodr  14739  cshwidxm1  14742  repswcshw  14747  2cshw  14748  cshweqrep  14756  cshw1  14757  swrd2lsw  14887  nn0abscl  15247  rexuzre  15288  dvdsval3  16195  p1modz1  16198  moddvds  16202  absdvdsb  16213  dvdsabsb  16214  dvdsle  16249  alzdvds  16259  mod2eq1n2dvds  16286  evennn02n  16289  evennn2n  16290  ltoddhalfle  16300  divalgmod  16345  fldivndvdslt  16355  flodddiv4t2lthalf  16357  bitsp1o  16372  gcdabs1  16468  modgcd  16471  bezoutlem1  16478  dfgcd2  16485  algcvga  16518  lcmabs  16544  isprm3  16622  dvdsnprmd  16629  2mulprm  16632  oddprmgt2  16638  sqnprm  16641  zgcdsq  16692  hashdvds  16714  vfermltlALT  16742  powm2modprm  16743  modprm0  16745  modprmn0modprm0  16747  fldivp1  16837  zgz  16873  4sqlem4  16892  prmgaplem5  16995  prmgaplem7  16997  cshwshashlem2  17036  setsstruct  17115  mulgmodid  19055  gexdvds  19525  zringunit  21433  prmirred  21441  znf1o  21518  chfacfscmul0  22814  chfacfscmulgsum  22816  chfacfpmmul0  22818  chfacfpmmulgsum  22820  dyadf  25560  dyadovol  25562  degltlem1  26045  coskpi  26500  cosne0  26506  relogexp  26573  cxpeq  26735  relogbzexp  26754  ppival2  27106  ppival2g  27107  ppiprm  27129  chtprm  27131  chtnprm  27132  ppip1le  27139  efexple  27260  zabsle1  27275  lgsdir2lem4  27307  lgsne0  27314  gausslemma2dlem1a  27344  gausslemma2dlem3  27347  gausslemma2dlem4  27348  lgsquadlem1  27359  lgsquadlem2  27360  2lgslem1a1  27368  2lgslem1a2  27369  2sqlem2  27397  rplogsumlem2  27464  pntrsumbnd  27545  axlowdim  29046  crctcshwlkn0lem3  29897  crctcshwlkn0lem5  29899  crctcshwlkn0  29906  crctcsh  29909  clwlkclwwlklem2fv2  30083  clwlkclwwlklem2a  30085  clwwisshclwwslemlem  30100  clwwlkinwwlk  30127  clwwlkext2edg  30143  wwlksubclwwlk  30145  numclwwlk5  30475  topnfbey  30556  uzssico  32875  1fldgenq  33416  znfermltl  33459  ply1coedeg  33682  rezh  34147  zrhre  34197  hashf2  34262  ballotlemfc0  34671  ballotlemfcc  34672  chpvalz  34806  chtvalz  34807  zltp1ne  35326  0nn0m1nnn0  35329  elfzm12  35891  nn0prpwlem  36538  poimirlem24  37895  mblfinlem1  37908  mblfinlem2  37909  itg2addnclem2  37923  fzmul  37992  incsequz2  38000  fimgmcyc  42904  ellz1  43124  lzunuz  43125  lzenom  43127  nerabdioph  43166  pell14qrgt0  43216  rmxycomplete  43274  monotuz  43298  monotoddzzfi  43299  oddcomabszz  43301  zindbi  43303  jm2.24  43320  congrep  43330  fzneg  43339  jm2.19  43350  fzunt  43811  fzunt1d  43813  fzuntgd  43814  oddfl  45640  fzdifsuc2  45672  climsuse  45968  stoweidlem26  46384  stoweidlem34  46392  fourierdlem20  46485  fourierdlem42  46507  fourierdlem51  46515  fourierdlem64  46528  fourierdlem76  46540  fourierdlem94  46558  fourierdlem97  46561  fourierdlem113  46577  natlocalincr  47234  natglobalincr  47235  zm1nn  47662  zgeltp1eq  47669  eluzge0nn0  47672  elfz2z  47675  2elfz2melfz  47678  elfzlble  47680  elfzelfzlble  47681  fzopredsuc  47683  ceilbi  47693  mod0mul  47716  modn0mul  47717  m1modmmod  47718  difmodm1lt  47719  mod2addne  47724  modm2nep1  47726  modp2nep1  47727  modm1nep2  47728  modm1nem2  47729  modm1p1ne  47730  smonoord  47731  fsummmodsndifre  47734  iccpartipre  47781  iccpartiltu  47782  iccpartigtl  47783  icceuelpartlem  47795  fmtno4prmfac  47932  lighneallem4b  47969  dfeven3  48018  dfodd4  48019  nn0o1gt2ALTV  48054  nnoALTV  48055  fpprel2  48101  gbegt5  48121  gbowgt5  48122  sbgoldbwt  48137  nnsum3primesle9  48154  nnsum4primesodd  48156  nnsum4primesoddALTV  48157  evengpop3  48158  evengpoap3  48159  nnsum4primesevenALTV  48161  bgoldbtbndlem1  48165  bgoldbtbndlem2  48166  bgoldbtbndlem3  48167  bgoldbtbndlem4  48168  gpgprismgriedgdmss  48412  gpgusgralem  48416  gpgedgvtx1  48422  gpg5nbgrvtx03starlem2  48429  gpg5nbgrvtx13starlem2  48432  gpg3nbgrvtx0  48436  cznnring  48622  elfzolborelfzop1  48879  zgtp1leeq  48881  rege1logbzge0  48919  fllog2  48928  dignn0ldlem  48962  dignn0flhalflem1  48975  dignn0flhalflem2  48976