Theorem zre 12697

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

This proof depends on syntax axioms:   → wi 4   ∨ w3o 1102   = wceq 1570   ∈ wcel 2145  ℝcr 11199  0cc0 11200  -cneg 11542  ℕcn 12335  ℤcz 12693

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2733

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3or 1104  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-sb 2100  df-clab 2740  df-cleq 2753  df-clel 2836  df-rab 3414  df-v 3453  df-dif 3902  df-un 3904  df-ss 3916  df-nul 4280  df-if 4483  df-sn 4585  df-pr 4587  df-op 4591  df-uni 4868  df-br 5104  df-iota 6494  df-fv 6546  df-ov 7423  df-neg 11544  df-z 12694

This theorem is used by:  zcn  12698  zrei  12699  zssre  12700  elnn0z  12706  elnnz1  12722  znnnlt1  12723  zletr  12740  znnsub  12742  znn0sub  12743  nzadd  12744  zltp1le  12746  zleltp1  12747  0nn0m1nnn0  12753  nn0ge0div  12768  zextle  12772  btwnnz  12775  suprzcl  12779  msqznn  12781  peano2uz2  12787  uzind  12791  fzind  12797  fnn0ind  12798  eluzuzle  12974  uzid  12980  uzneg  12985  uztric  12989  uz11  12990  eluzp1m1  12991  eluzp1p1  12993  eluzadd  12994  eluzsub  12995  subeluzsub  12998  uzin  13001  uz3m2nn  13021  peano2uz  13028  nn0pzuz  13032  uzwo  13038  eluz2b2  13048  uz2mulcl  13053  uzinfi  13055  eqreznegel  13061  lbzbi  13063  uzsupss  13067  nn01to3  13068  zmin  13071  zmax  13072  zbtwnre  13073  rebtwnz  13074  qre  13080  elpq  13103  rpnnen1lem2  13105  rpnnen1lem1  13106  rpnnen1lem3  13107  rpnnen1lem5  13109  z2ge  13328  qbtwnre  13329  zltaddlt1le  13636  elfz1eq  13668  fzn  13673  fzen  13674  uzsubsubfz  13680  fzaddel  13692  fzadd2  13693  ssfzunsnext  13703  ssfzunsn  13704  fzsuc2  13716  fzrev  13721  elfz1b  13727  fznuz  13743  uznfz  13744  fzp1nel  13745  elfz0fzfz0  13767  fz0fzelfz0  13768  fznn0sub2  13769  fz0fzdiffz0  13771  elfzmlbp  13773  difelfznle  13776  nelfzo  13799  elfzouz2  13809  fzo0n  13816  fzonlt0  13817  fzossrbm1  13823  fzospliti  13826  elfzo0z  13836  fzofzim  13844  fzo1fzo0n0  13850  eluzgtdifelfzo  13862  fzossfzop1  13878  ssfzoulel  13895  ssfzo12bi  13896  elfzonelfzo  13904  elfzomelpfzo  13907  elfznelfzob  13909  fzostep1  13921  fllt  13946  flid  13948  flbi2  13957  2tnp1ge0ge0  13969  flhalf  13970  fldiv4p1lem1div2  13975  fldiv4lem1div2uz2  13976  dfceil2  13979  ceile  13989  ceilid  13991  quoremz  13995  intfracq  13999  uzsup  14003  mulmod0  14017  zmod10  14027  zmodcl  14031  zmodfz  14033  zmodid2  14039  modcyc  14046  modaddid  14050  mulp1mod1  14054  muladdmod  14055  modmuladd  14056  modmuladdim  14057  modmul1  14067  modaddmodup  14077  modaddmodlo  14078  modaddmulmod  14081  zsqcl2  14281  leexp2  14314  iexpcyc  14351  fi1uzind  14652  ccatsymb  14728  ccatval21sw  14731  lswccatn0lsw  14738  swrdnd  14804  swrdnnn0nd  14806  swrd0  14808  swrdswrdlem  14853  swrdswrd  14854  swrdccatin2  14878  pfxccatin12lem2  14880  pfxccatin12lem3  14881  repswswrd  14935  cshwmodn  14946  cshwsublen  14947  cshwidxmod  14954  cshwidxmodr  14955  cshwidxm1  14958  repswcshw  14963  2cshw  14964  cshweqrep  14972  cshw1  14973  swrd2lsw  15105  nn0abscl  15479  rexuzre  15520  dvdsval3  16426  p1modz1  16429  moddvds  16433  absdvdsb  16444  dvdsabsb  16445  dvdsle  16480  alzdvds  16490  mod2eq1n2dvds  16517  evennn02n  16520  evennn2n  16521  ltoddhalfle  16531  divalgmod  16576  fldivndvdslt  16586  flodddiv4t2lthalf  16588  bitsp1o  16603  gcdabs1  16702  modgcd  16705  bezoutlem1  16712  dfgcd2  16719  algcvga  16754  lcmabs  16780  isprm3  16858  dvdsnprmd  16865  2mulprm  16868  oddprmgt2  16875  sqnprm  16878  zgcdsq  16929  hashdvds  16952  vfermltlALT  16980  powm2modprm  16981  modprm0  16983  modprmn0modprm0  16985  fldivp1  17075  zgz  17111  4sqlem4  17130  prmgaplem5  17233  prmgaplem7  17235  cshwshashlem2  17274  setsstruct  17354  mulgmodid  19323  gexdvds  19798  zringunit  21772  prmirred  21780  znf1o  21857  chfacfscmul0  23176  chfacfscmulgsum  23178  chfacfpmmul0  23180  chfacfpmmulgsum  23182  dyadf  25912  dyadovol  25914  degltlem1  26390  coskpi  26851  cosne0  26857  relogexp  26924  cxpeq  27085  relogbzexp  27104  ppival2  27455  ppival2g  27456  ppiprm  27478  chtprm  27480  chtnprm  27481  ppip1le  27488  efexple  27608  zabsle1  27623  lgsdir2lem4  27655  lgsne0  27662  gausslemma2dlem1a  27692  gausslemma2dlem3  27695  gausslemma2dlem4  27696  lgsquadlem1  27707  lgsquadlem2  27708  2lgslem1a1  27716  2lgslem1a2  27717  2sqlem2  27745  rplogsumlem2  27812  pntrsumbnd  27893  fltoprmgt3  27996  axlowdim  29539  crctcshwlkn0lem3  30401  crctcshwlkn0lem5  30403  crctcshwlkn0  30410  crctcsh  30413  clwlkclwwlklem2fv2  30587  clwlkclwwlklem2a  30589  clwwisshclwwslemlem  30604  clwwlkinwwlk  30631  clwwlkext2edg  30647  wwlksubclwwlk  30649  numclwwlk5  30989  topnfbey  31070  uzssico  33376  1fldgenq  33884  znfermltl  33922  ply1coedeg  34121  rezh  34601  zrhre  34651  hashf2  34716  ballotlemfc0  35125  ballotlemfcc  35126  chpvalz  35257  chtvalz  35258  zltp1ne  35900  elfzm12  36440  nn0prpwlem  37110  poimirlem24  38562  mblfinlem1  38575  mblfinlem2  38576  itg2addnclem2  38590  fzmul  38675  incsequz2  38683  fimgmcyc  43598  ellz1  43777  lzunuz  43778  lzenom  43780  nerabdioph  43815  pell14qrgt0  43865  rmxycomplete  43923  monotuz  43947  monotoddzzfi  43948  oddcomabszz  43950  zindbi  43952  jm2.24  43969  congrep  43979  fzneg  43988  jm2.19  43999  fzunt  44455  fzunt1d  44457  fzuntgd  44458  oddfl  46293  fzdifsuc2  46325  climsuse  46619  stoweidlem26  47035  stoweidlem34  47043  fourierdlem20  47136  fourierdlem42  47158  fourierdlem51  47166  fourierdlem64  47179  fourierdlem76  47191  fourierdlem94  47209  fourierdlem97  47212  fourierdlem113  47228  zm1nn  48371  zgeltp1eq  48378  eluzge0nn0  48381  elfz2z  48384  2elfz2melfz  48387  elfzlble  48389  elfzelfzlble  48390  fzopredsuc  48393  ceilbi  48406  mod0mul  48431  modn0mul  48432  m1modmmod  48433  difmodm1lt  48434  mod2addne  48439  modm2nep1  48441  modp2nep1  48442  modm1nep2  48443  modm1nem2  48444  modm1p1ne  48445  smonoord  48446  2timesltsqm1  48448  fsummmodsndifre  48451  muldvdsfacgt  48455  muldvdsfacm1  48456  iccpartipre  48502  iccpartiltu  48503  iccpartigtl  48504  icceuelpartlem  48516  fmtno4prmfac  48656  lighneallem4b  48693  nprmdvdsfacm1lem2  48705  nprmdvdsfacm1lem4  48707  dfeven3  48755  dfodd4  48756  nn0o1gt2ALTV  48791  nnoALTV  48792  fpprel2  48838  gbegt5  48858  gbowgt5  48859  sbgoldbwt  48874  nnsum3primesle9  48891  nnsum4primesodd  48893  nnsum4primesoddALTV  48894  evengpop3  48895  evengpoap3  48896  nnsum4primesevenALTV  48898  bgoldbtbndlem1  48902  bgoldbtbndlem2  48903  bgoldbtbndlem3  48904  bgoldbtbndlem4  48905  gpgprismgriedgdmss  49149  gpgusgralem  49153  gpgedgvtx1  49159  gpg5nbgrvtx03starlem2  49166  gpg5nbgrvtx13starlem2  49169  gpg3nbgrvtx0  49173  cznnring  49358  elfzolborelfzop1  49630  zgtp1leeq  49632  rege1logbzge0  49670  fllog2  49679  dignn0ldlem  49713  dignn0flhalflem1  49726  dignn0flhalflem2  49727