Theorem zre 11643

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

Syntax hints:   → wi 4   ∨ w3o 1099   = wceq 1637   ∈ wcel 2156  ℝcr 10216  0cc0 10217  -cneg 10548  ℕcn 11301  ℤcz 11639

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1877  ax-4 1894  ax-5 2001  ax-6 2068  ax-7 2104  ax-9 2165  ax-10 2185  ax-11 2201  ax-12 2214  ax-13 2420  ax-ext 2784

This theorem depends on definitions:  df-bi 198  df-an 385  df-or 866  df-3or 1101  df-3an 1102  df-tru 1641  df-ex 1860  df-nf 1864  df-sb 2061  df-clab 2793  df-cleq 2799  df-clel 2802  df-nfc 2937  df-rex 3102  df-rab 3105  df-v 3393  df-dif 3772  df-un 3774  df-in 3776  df-ss 3783  df-nul 4117  df-if 4280  df-sn 4371  df-pr 4373  df-op 4377  df-uni 4631  df-br 4845  df-iota 6060  df-fv 6105  df-ov 6873  df-neg 10550  df-z 11640

This theorem is referenced by:  zcn  11644  zrei  11645  zssre  11646  elnn0z  11652  elnnz1  11665  znnnlt1  11666  zletr  11683  znnsub  11685  znn0sub  11686  nzadd  11687  zltp1le  11689  zleltp1  11690  nn0ge0div  11708  zextle  11712  btwnnz  11715  suprzcl  11719  msqznn  11721  peano2uz2  11727  uzind  11731  fzind  11737  fnn0ind  11738  eluzuzle  11909  uzid  11915  uzneg  11919  uztric  11922  uz11  11923  eluzp1m1  11924  eluzp1p1  11926  eluzaddi  11927  eluzsubi  11928  subeluzsub  11931  uzin  11934  uz3m2nn  11945  peano2uz  11955  nn0pzuz  11959  uzwo  11966  eluz2b2  11976  uz2mulcl  11981  uzinfi  11983  eqreznegel  11989  lbzbi  11991  uzsupss  11995  nn01to3  11996  zmin  11999  zmax  12000  zbtwnre  12001  rebtwnz  12002  qre  12008  rpnnen1lem2  12029  rpnnen1lem1  12030  rpnnen1lem3  12031  rpnnen1lem5  12033  z2ge  12243  qbtwnre  12244  zltaddlt1le  12543  elfz1eq  12571  fzn  12576  fzen  12577  uzsubsubfz  12582  fzaddel  12594  fzadd2  12595  ssfzunsnext  12605  ssfzunsn  12606  fzsuc2  12617  fzrev  12622  elfz1b  12628  fznuz  12641  uznfz  12642  fzp1nel  12643  elfz0fzfz0  12664  fz0fzelfz0  12665  fznn0sub2  12666  fz0fzdiffz0  12668  elfzmlbp  12670  difelfznle  12673  nelfzo  12695  elfzouz2  12704  fzo0n  12710  fzonlt0  12711  fzossrbm1  12717  fzospliti  12720  elfzo0z  12730  fzofzim  12735  fzo1fzo0n0  12739  eluzgtdifelfzo  12750  fzossfzop1  12766  ssfzoulel  12782  ssfzo12bi  12783  elfzonelfzo  12790  elfzomelpfzo  12792  elfznelfzob  12794  fzostep1  12804  fllt  12827  flid  12829  flbi2  12838  2tnp1ge0ge0  12850  flhalf  12851  fldiv4p1lem1div2  12856  fldiv4lem1div2uz2  12857  dfceil2  12860  ceile  12868  ceilid  12870  quoremz  12874  intfracq  12878  uzsup  12882  mulmod0  12896  zmod10  12906  zmodcl  12910  zmodfz  12912  zmodid2  12918  modcyc  12925  mulp1mod1  12931  modmuladd  12932  modmuladdim  12933  modmul1  12943  modaddmodup  12953  modaddmodlo  12954  modaddmulmod  12957  leexp2  13134  zsqcl2  13160  iexpcyc  13188  fi1uzind  13492  ccatsymb  13575  ccatval21sw  13578  lswccatn0lsw  13584  swrdnd  13652  swrd0  13654  swrdswrdlem  13679  swrdswrd  13680  swrdccatin2  13707  swrdccatin12lem2  13709  swrdccatin12lem3  13710  repswswrd  13751  cshwmodn  13761  cshwsublen  13762  cshwidxmod  13769  cshwidxmodr  13770  cshwidxm1  13773  repswcshw  13778  2cshw  13779  cshweqrep  13787  cshw1  13788  swrd2lsw  13916  nn0abscl  14271  rexuzre  14311  znnenlemOLD  15156  dvdsval3  15203  p1modz1  15206  moddvds  15210  absdvdsb  15219  dvdsabsb  15220  dvdsle  15251  alzdvds  15261  mod2eq1n2dvds  15287  evennn02n  15290  evennn2n  15291  ltoddhalfle  15301  divalgmod  15345  fldivndvdslt  15353  flodddiv4t2lthalf  15355  bitsp1o  15370  gcdabs  15465  gcdabs1  15466  modgcd  15468  bezoutlem1  15471  dfgcd2  15478  algcvga  15507  lcmabs  15533  isprm3  15610  dvdsnprmd  15617  oddprmgt2  15625  sqnprm  15627  zgcdsq  15674  hashdvds  15693  vfermltlALT  15720  powm2modprm  15721  modprm0  15723  modprmn0modprm0  15725  fldivp1  15814  zgz  15850  4sqlem4  15869  prmgaplem5  15972  prmgaplem7  15974  cshwshashlem2  16011  setsstruct  16105  mulgmodid  17779  gexdvds  18196  zringunit  20040  prmirred  20047  znf1o  20103  chfacfscmul0  20873  chfacfscmulgsum  20875  chfacfpmmul0  20877  chfacfpmmulgsum  20879  dyadf  23571  dyadovol  23573  degltlem1  24045  coskpi  24486  cosne0  24490  relogexp  24555  cxpeq  24711  relogbzexp  24727  ppival2  25067  ppival2g  25068  ppiprm  25090  chtprm  25092  chtnprm  25093  ppip1le  25100  efexple  25219  zabsle1  25234  lgsdir2lem4  25266  lgsne0  25273  gausslemma2dlem1a  25303  gausslemma2dlem3  25306  gausslemma2dlem4  25307  lgsquadlem1  25318  lgsquadlem2  25319  2lgslem1a1  25327  2lgslem1a2  25328  2sqlem2  25356  rplogsumlem2  25387  pntrsumbnd  25468  axlowdim  26054  crctcshwlkn0lem3  26932  crctcshwlkn0lem5  26934  crctcshwlkn0  26941  crctcsh  26944  clwlkclwwlklem2fv2  27138  clwlkclwwlklem2a  27140  clwwisshclwwslemlem  27155  clwwlkinwwlk  27188  clwwlkext2edg  27205  wwlksubclwwlk  27208  clwlksfclwwlkOLD  27235  numclwwlk5  27575  topnfbey  27655  uzssico  29872  rezh  30339  zrhre  30387  hashf2  30470  ballotlemfc0  30878  ballotlemfcc  30879  chpvalz  31030  chtvalz  31031  elfzm12  31889  nn0prpwlem  32636  poimirlem24  33744  mblfinlem1  33757  mblfinlem2  33758  itg2addnclem2  33772  fzmul  33846  incsequz2  33854  ellz1  37829  lzunuz  37830  lzenom  37832  nerabdioph  37872  pell14qrgt0  37922  rmxycomplete  37980  monotuz  38004  monotoddzzfi  38005  oddcomabszz  38007  zindbi  38009  jm2.24  38028  congrep  38038  fzneg  38047  jm2.19  38058  oddfl  39968  fzdifsuc2  40002  climsuse  40317  stoweidlem26  40719  stoweidlem34  40727  fourierdlem20  40820  fourierdlem42  40842  fourierdlem51  40850  fourierdlem64  40863  fourierdlem76  40875  fourierdlem94  40893  fourierdlem97  40896  fourierdlem113  40912  zm1nn  41889  zgeltp1eq  41891  eluzge0nn0  41894  elfz2z  41897  2elfz2melfz  41900  elfzlble  41902  elfzelfzlble  41903  fzopredsuc  41905  smonoord  41913  fsummmodsndifre  41916  iccpartipre  41929  iccpartiltu  41930  iccpartigtl  41931  icceuelpartlem  41943  pfxccatin12lem2  41996  fmtno4prmfac  42056  lighneallem4b  42098  dfeven3  42142  dfodd4  42143  nn0o1gt2ALTV  42177  nnoALTV  42178  gbegt5  42221  gbowgt5  42222  sbgoldbwt  42237  nnsum3primesle9  42254  nnsum4primesodd  42256  nnsum4primesoddALTV  42257  evengpop3  42258  evengpoap3  42259  nnsum4primesevenALTV  42261  bgoldbtbndlem1  42265  bgoldbtbndlem2  42266  bgoldbtbndlem3  42267  bgoldbtbndlem4  42268  cznnring  42521  elfzolborelfzop1  42874  zgtp1leeq  42876  mod0mul  42879  modn0mul  42880  m1modmmod  42881  difmodm1lt  42882  rege1logbzge0  42918  fllog2  42927  dignn0ldlem  42961  dignn0flhalflem1  42974  dignn0flhalflem2  42975