Theorem zre 12562

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

Syntax hints:   → wi 4   ∨ w3o 1087   = wceq 1542   ∈ wcel 2107  ℝcr 11109  0cc0 11110  -cneg 11445  ℕcn 12212  ℤcz 12558

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 2704

This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3or 1089  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-rab 3434  df-v 3477  df-dif 3952  df-un 3954  df-in 3956  df-ss 3966  df-nul 4324  df-if 4530  df-sn 4630  df-pr 4632  df-op 4636  df-uni 4910  df-br 5150  df-iota 6496  df-fv 6552  df-ov 7412  df-neg 11447  df-z 12559

This theorem is referenced by:  zcn  12563  zrei  12564  zssre  12565  elnn0z  12571  elnnz1  12588  znnnlt1  12589  zletr  12606  znnsub  12608  znn0sub  12609  nzadd  12610  zltp1le  12612  zleltp1  12613  nn0ge0div  12631  zextle  12635  btwnnz  12638  suprzcl  12642  msqznn  12644  peano2uz2  12650  uzind  12654  fzind  12660  fnn0ind  12661  eluzuzle  12831  uzid  12837  uzneg  12842  uztric  12846  uz11  12847  eluzp1m1  12848  eluzp1p1  12850  eluzadd  12851  eluzsub  12852  eluzaddiOLD  12854  eluzsubiOLD  12856  subeluzsub  12859  uzin  12862  uz3m2nn  12875  peano2uz  12885  nn0pzuz  12889  uzwo  12895  eluz2b2  12905  uz2mulcl  12910  uzinfi  12912  eqreznegel  12918  lbzbi  12920  uzsupss  12924  nn01to3  12925  zmin  12928  zmax  12929  zbtwnre  12930  rebtwnz  12931  qre  12937  elpq  12959  rpnnen1lem2  12961  rpnnen1lem1  12962  rpnnen1lem3  12963  rpnnen1lem5  12965  z2ge  13177  qbtwnre  13178  zltaddlt1le  13482  elfz1eq  13512  fzn  13517  fzen  13518  uzsubsubfz  13523  fzaddel  13535  fzadd2  13536  ssfzunsnext  13546  ssfzunsn  13547  fzsuc2  13559  fzrev  13564  elfz1b  13570  fznuz  13583  uznfz  13584  fzp1nel  13585  elfz0fzfz0  13606  fz0fzelfz0  13607  fznn0sub2  13608  fz0fzdiffz0  13610  elfzmlbp  13612  difelfznle  13615  nelfzo  13637  elfzouz2  13647  fzo0n  13654  fzonlt0  13655  fzossrbm1  13661  fzospliti  13664  elfzo0z  13674  fzofzim  13679  fzo1fzo0n0  13683  eluzgtdifelfzo  13694  fzossfzop1  13710  ssfzoulel  13726  ssfzo12bi  13727  elfzonelfzo  13734  elfzomelpfzo  13736  elfznelfzob  13738  fzostep1  13748  fllt  13771  flid  13773  flbi2  13782  2tnp1ge0ge0  13794  flhalf  13795  fldiv4p1lem1div2  13800  fldiv4lem1div2uz2  13801  dfceil2  13804  ceile  13814  ceilid  13816  quoremz  13820  intfracq  13824  uzsup  13828  mulmod0  13842  zmod10  13852  zmodcl  13856  zmodfz  13858  zmodid2  13864  modcyc  13871  mulp1mod1  13877  modmuladd  13878  modmuladdim  13879  modmul1  13889  modaddmodup  13899  modaddmodlo  13900  modaddmulmod  13903  zsqcl2  14103  leexp2  14136  iexpcyc  14171  fi1uzind  14458  ccatsymb  14532  ccatval21sw  14535  lswccatn0lsw  14541  swrdnd  14604  swrdnnn0nd  14606  swrd0  14608  swrdswrdlem  14654  swrdswrd  14655  swrdccatin2  14679  pfxccatin12lem2  14681  pfxccatin12lem3  14682  repswswrd  14734  cshwmodn  14745  cshwsublen  14746  cshwidxmod  14753  cshwidxmodr  14754  cshwidxm1  14757  repswcshw  14762  2cshw  14763  cshweqrep  14771  cshw1  14772  swrd2lsw  14903  nn0abscl  15259  rexuzre  15299  dvdsval3  16201  p1modz1  16204  moddvds  16208  absdvdsb  16218  dvdsabsb  16219  dvdsle  16253  alzdvds  16263  mod2eq1n2dvds  16290  evennn02n  16293  evennn2n  16294  ltoddhalfle  16304  divalgmod  16349  fldivndvdslt  16357  flodddiv4t2lthalf  16359  bitsp1o  16374  gcdabs1  16470  gcdabsOLD  16473  modgcd  16474  bezoutlem1  16481  dfgcd2  16488  algcvga  16516  lcmabs  16542  isprm3  16620  dvdsnprmd  16627  2mulprm  16630  oddprmgt2  16636  sqnprm  16639  zgcdsq  16689  hashdvds  16708  vfermltlALT  16735  powm2modprm  16736  modprm0  16738  modprmn0modprm0  16740  fldivp1  16830  zgz  16866  4sqlem4  16885  prmgaplem5  16988  prmgaplem7  16990  cshwshashlem2  17030  setsstruct  17109  mulgmodid  18993  gexdvds  19452  zringunit  21036  prmirred  21044  znf1o  21107  chfacfscmul0  22360  chfacfscmulgsum  22362  chfacfpmmul0  22364  chfacfpmmulgsum  22366  dyadf  25108  dyadovol  25110  degltlem1  25590  coskpi  26032  cosne0  26038  relogexp  26104  cxpeq  26265  relogbzexp  26281  ppival2  26632  ppival2g  26633  ppiprm  26655  chtprm  26657  chtnprm  26658  ppip1le  26665  efexple  26784  zabsle1  26799  lgsdir2lem4  26831  lgsne0  26838  gausslemma2dlem1a  26868  gausslemma2dlem3  26871  gausslemma2dlem4  26872  lgsquadlem1  26883  lgsquadlem2  26884  2lgslem1a1  26892  2lgslem1a2  26893  2sqlem2  26921  rplogsumlem2  26988  pntrsumbnd  27069  axlowdim  28219  crctcshwlkn0lem3  29066  crctcshwlkn0lem5  29068  crctcshwlkn0  29075  crctcsh  29078  clwlkclwwlklem2fv2  29249  clwlkclwwlklem2a  29251  clwwisshclwwslemlem  29266  clwwlkinwwlk  29293  clwwlkext2edg  29309  wwlksubclwwlk  29311  numclwwlk5  29641  topnfbey  29722  uzssico  31995  1fldgenq  32412  znfermltl  32479  rezh  32951  zrhre  32999  hashf2  33082  ballotlemfc0  33491  ballotlemfcc  33492  chpvalz  33640  chtvalz  33641  zltp1ne  34099  0nn0m1nnn0  34102  elfzm12  34660  nn0prpwlem  35207  poimirlem24  36512  mblfinlem1  36525  mblfinlem2  36526  itg2addnclem2  36540  fzmul  36609  incsequz2  36617  ellz1  41505  lzunuz  41506  lzenom  41508  nerabdioph  41547  pell14qrgt0  41597  rmxycomplete  41656  monotuz  41680  monotoddzzfi  41681  oddcomabszz  41683  zindbi  41685  jm2.24  41702  congrep  41712  fzneg  41721  jm2.19  41732  fzunt  42206  fzunt1d  42208  fzuntgd  42209  oddfl  43987  fzdifsuc2  44020  climsuse  44324  stoweidlem26  44742  stoweidlem34  44750  fourierdlem20  44843  fourierdlem42  44865  fourierdlem51  44873  fourierdlem64  44886  fourierdlem76  44898  fourierdlem94  44916  fourierdlem97  44919  fourierdlem113  44935  natlocalincr  45590  natglobalincr  45591  zm1nn  46010  zgeltp1eq  46017  eluzge0nn0  46020  elfz2z  46023  2elfz2melfz  46026  elfzlble  46028  elfzelfzlble  46029  fzopredsuc  46031  smonoord  46039  fsummmodsndifre  46042  iccpartipre  46089  iccpartiltu  46090  iccpartigtl  46091  icceuelpartlem  46103  fmtno4prmfac  46240  lighneallem4b  46277  dfeven3  46326  dfodd4  46327  nn0o1gt2ALTV  46362  nnoALTV  46363  fpprel2  46409  gbegt5  46429  gbowgt5  46430  sbgoldbwt  46445  nnsum3primesle9  46462  nnsum4primesodd  46464  nnsum4primesoddALTV  46465  evengpop3  46466  evengpoap3  46467  nnsum4primesevenALTV  46469  bgoldbtbndlem1  46473  bgoldbtbndlem2  46474  bgoldbtbndlem3  46475  bgoldbtbndlem4  46476  cznnring  46854  elfzolborelfzop1  47200  zgtp1leeq  47202  mod0mul  47205  modn0mul  47206  m1modmmod  47207  difmodm1lt  47208  rege1logbzge0  47245  fllog2  47254  dignn0ldlem  47288  dignn0flhalflem1  47301  dignn0flhalflem2  47302