Theorem zre 12332

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

Syntax hints:   → wi 4   ∨ w3o 1085   = wceq 1539   ∈ wcel 2107  ℝcr 10879  0cc0 10880  -cneg 11215  ℕcn 11982  ℤcz 12328

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2710

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3or 1087  df-3an 1088  df-tru 1542  df-fal 1552  df-ex 1783  df-sb 2069  df-clab 2717  df-cleq 2731  df-clel 2817  df-rab 3074  df-v 3435  df-dif 3891  df-un 3893  df-in 3895  df-ss 3905  df-nul 4258  df-if 4461  df-sn 4563  df-pr 4565  df-op 4569  df-uni 4841  df-br 5076  df-iota 6395  df-fv 6445  df-ov 7287  df-neg 11217  df-z 12329

This theorem is referenced by:  zcn  12333  zrei  12334  zssre  12335  elnn0z  12341  elnnz1  12355  znnnlt1  12356  zletr  12373  znnsub  12375  znn0sub  12376  nzadd  12377  zltp1le  12379  zleltp1  12380  nn0ge0div  12398  zextle  12402  btwnnz  12405  suprzcl  12409  msqznn  12411  peano2uz2  12417  uzind  12421  fzind  12427  fnn0ind  12428  eluzuzle  12600  uzid  12606  uzneg  12611  uztric  12615  uz11  12616  eluzp1m1  12617  eluzp1p1  12619  eluzaddi  12620  eluzsubi  12621  subeluzsub  12624  uzin  12627  uz3m2nn  12640  peano2uz  12650  nn0pzuz  12654  uzwo  12660  eluz2b2  12670  uz2mulcl  12675  uzinfi  12677  eqreznegel  12683  lbzbi  12685  uzsupss  12689  nn01to3  12690  zmin  12693  zmax  12694  zbtwnre  12695  rebtwnz  12696  qre  12702  elpq  12724  rpnnen1lem2  12726  rpnnen1lem1  12727  rpnnen1lem3  12728  rpnnen1lem5  12730  z2ge  12941  qbtwnre  12942  zltaddlt1le  13246  elfz1eq  13276  fzn  13281  fzen  13282  uzsubsubfz  13287  fzaddel  13299  fzadd2  13300  ssfzunsnext  13310  ssfzunsn  13311  fzsuc2  13323  fzrev  13328  elfz1b  13334  fznuz  13347  uznfz  13348  fzp1nel  13349  elfz0fzfz0  13370  fz0fzelfz0  13371  fznn0sub2  13372  fz0fzdiffz0  13374  elfzmlbp  13376  difelfznle  13379  nelfzo  13401  elfzouz2  13411  fzo0n  13418  fzonlt0  13419  fzossrbm1  13425  fzospliti  13428  elfzo0z  13438  fzofzim  13443  fzo1fzo0n0  13447  eluzgtdifelfzo  13458  fzossfzop1  13474  ssfzoulel  13490  ssfzo12bi  13491  elfzonelfzo  13498  elfzomelpfzo  13500  elfznelfzob  13502  fzostep1  13512  fllt  13535  flid  13537  flbi2  13546  2tnp1ge0ge0  13558  flhalf  13559  fldiv4p1lem1div2  13564  fldiv4lem1div2uz2  13565  dfceil2  13568  ceile  13578  ceilid  13580  quoremz  13584  intfracq  13588  uzsup  13592  mulmod0  13606  zmod10  13616  zmodcl  13620  zmodfz  13622  zmodid2  13628  modcyc  13635  mulp1mod1  13641  modmuladd  13642  modmuladdim  13643  modmul1  13653  modaddmodup  13663  modaddmodlo  13664  modaddmulmod  13667  zsqcl2  13865  leexp2  13898  iexpcyc  13932  fi1uzind  14220  ccatsymb  14296  ccatval21sw  14299  lswccatn0lsw  14305  swrdnd  14376  swrdnnn0nd  14378  swrd0  14380  swrdswrdlem  14426  swrdswrd  14427  swrdccatin2  14451  pfxccatin12lem2  14453  pfxccatin12lem3  14454  repswswrd  14506  cshwmodn  14517  cshwsublen  14518  cshwidxmod  14525  cshwidxmodr  14526  cshwidxm1  14529  repswcshw  14534  2cshw  14535  cshweqrep  14543  cshw1  14544  swrd2lsw  14674  nn0abscl  15033  rexuzre  15073  dvdsval3  15976  p1modz1  15979  moddvds  15983  absdvdsb  15993  dvdsabsb  15994  dvdsle  16028  alzdvds  16038  mod2eq1n2dvds  16065  evennn02n  16068  evennn2n  16069  ltoddhalfle  16079  divalgmod  16124  fldivndvdslt  16132  flodddiv4t2lthalf  16134  bitsp1o  16149  gcdabs1  16245  gcdabsOLD  16248  modgcd  16249  bezoutlem1  16256  dfgcd2  16263  algcvga  16293  lcmabs  16319  isprm3  16397  dvdsnprmd  16404  2mulprm  16407  oddprmgt2  16413  sqnprm  16416  zgcdsq  16466  hashdvds  16485  vfermltlALT  16512  powm2modprm  16513  modprm0  16515  modprmn0modprm0  16517  fldivp1  16607  zgz  16643  4sqlem4  16662  prmgaplem5  16765  prmgaplem7  16767  cshwshashlem2  16807  setsstruct  16886  mulgmodid  18751  gexdvds  19198  zringunit  20697  prmirred  20705  znf1o  20768  chfacfscmul0  22016  chfacfscmulgsum  22018  chfacfpmmul0  22020  chfacfpmmulgsum  22022  dyadf  24764  dyadovol  24766  degltlem1  25246  coskpi  25688  cosne0  25694  relogexp  25760  cxpeq  25919  relogbzexp  25935  ppival2  26286  ppival2g  26287  ppiprm  26309  chtprm  26311  chtnprm  26312  ppip1le  26319  efexple  26438  zabsle1  26453  lgsdir2lem4  26485  lgsne0  26492  gausslemma2dlem1a  26522  gausslemma2dlem3  26525  gausslemma2dlem4  26526  lgsquadlem1  26537  lgsquadlem2  26538  2lgslem1a1  26546  2lgslem1a2  26547  2sqlem2  26575  rplogsumlem2  26642  pntrsumbnd  26723  axlowdim  27338  crctcshwlkn0lem3  28186  crctcshwlkn0lem5  28188  crctcshwlkn0  28195  crctcsh  28198  clwlkclwwlklem2fv2  28369  clwlkclwwlklem2a  28371  clwwisshclwwslemlem  28386  clwwlkinwwlk  28413  clwwlkext2edg  28429  wwlksubclwwlk  28431  numclwwlk5  28761  topnfbey  28842  uzssico  31114  znfermltl  31571  rezh  31930  zrhre  31978  hashf2  32061  ballotlemfc0  32468  ballotlemfcc  32469  chpvalz  32617  chtvalz  32618  zltp1ne  33077  0nn0m1nnn0  33080  elfzm12  33642  nn0prpwlem  34520  poimirlem24  35810  mblfinlem1  35823  mblfinlem2  35824  itg2addnclem2  35838  fzmul  35908  incsequz2  35916  ellz1  40596  lzunuz  40597  lzenom  40599  nerabdioph  40638  pell14qrgt0  40688  rmxycomplete  40746  monotuz  40770  monotoddzzfi  40771  oddcomabszz  40773  zindbi  40775  jm2.24  40792  congrep  40802  fzneg  40811  jm2.19  40822  fzunt  41069  fzunt1d  41071  fzuntgd  41072  oddfl  42823  fzdifsuc2  42856  climsuse  43156  stoweidlem26  43574  stoweidlem34  43582  fourierdlem20  43675  fourierdlem42  43697  fourierdlem51  43705  fourierdlem64  43718  fourierdlem76  43730  fourierdlem94  43748  fourierdlem97  43751  fourierdlem113  43767  zm1nn  44805  zgeltp1eq  44812  eluzge0nn0  44815  elfz2z  44818  2elfz2melfz  44821  elfzlble  44823  elfzelfzlble  44824  fzopredsuc  44826  smonoord  44834  fsummmodsndifre  44837  iccpartipre  44884  iccpartiltu  44885  iccpartigtl  44886  icceuelpartlem  44898  fmtno4prmfac  45035  lighneallem4b  45072  dfeven3  45121  dfodd4  45122  nn0o1gt2ALTV  45157  nnoALTV  45158  fpprel2  45204  gbegt5  45224  gbowgt5  45225  sbgoldbwt  45240  nnsum3primesle9  45257  nnsum4primesodd  45259  nnsum4primesoddALTV  45260  evengpop3  45261  evengpoap3  45262  nnsum4primesevenALTV  45264  bgoldbtbndlem1  45268  bgoldbtbndlem2  45269  bgoldbtbndlem3  45270  bgoldbtbndlem4  45271  cznnring  45525  elfzolborelfzop1  45871  zgtp1leeq  45873  mod0mul  45876  modn0mul  45877  m1modmmod  45878  difmodm1lt  45879  rege1logbzge0  45916  fllog2  45925  dignn0ldlem  45959  dignn0flhalflem1  45972  dignn0flhalflem2  45973  natlocalincr  46522  natglobalincr  46523