Theorem zre 12492

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

Syntax hints:   → wi 4   ∨ w3o 1085   = wceq 1541   ∈ wcel 2113  ℝcr 11025  0cc0 11026  -cneg 11365  ℕcn 12145  ℤcz 12488

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-sb 2068  df-clab 2715  df-cleq 2728  df-clel 2811  df-rab 3400  df-v 3442  df-dif 3904  df-un 3906  df-ss 3918  df-nul 4286  df-if 4480  df-sn 4581  df-pr 4583  df-op 4587  df-uni 4864  df-br 5099  df-iota 6448  df-fv 6500  df-ov 7361  df-neg 11367  df-z 12489

This theorem is referenced by:  zcn  12493  zrei  12494  zssre  12495  elnn0z  12501  elnnz1  12517  znnnlt1  12518  zletr  12535  znnsub  12537  znn0sub  12538  nzadd  12539  zltp1le  12541  zleltp1  12542  nn0ge0div  12561  zextle  12565  btwnnz  12568  suprzcl  12572  msqznn  12574  peano2uz2  12580  uzind  12584  fzind  12590  fnn0ind  12591  eluzuzle  12760  uzid  12766  uzneg  12771  uztric  12775  uz11  12776  eluzp1m1  12777  eluzp1p1  12779  eluzadd  12780  eluzsub  12781  subeluzsub  12784  uzin  12787  uz3m2nn  12807  peano2uz  12814  nn0pzuz  12818  uzwo  12824  eluz2b2  12834  uz2mulcl  12839  uzinfi  12841  eqreznegel  12847  lbzbi  12849  uzsupss  12853  nn01to3  12854  zmin  12857  zmax  12858  zbtwnre  12859  rebtwnz  12860  qre  12866  elpq  12888  rpnnen1lem2  12890  rpnnen1lem1  12891  rpnnen1lem3  12892  rpnnen1lem5  12894  z2ge  13113  qbtwnre  13114  zltaddlt1le  13421  elfz1eq  13451  fzn  13456  fzen  13457  uzsubsubfz  13462  fzaddel  13474  fzadd2  13475  ssfzunsnext  13485  ssfzunsn  13486  fzsuc2  13498  fzrev  13503  elfz1b  13509  fznuz  13525  uznfz  13526  fzp1nel  13527  elfz0fzfz0  13549  fz0fzelfz0  13550  fznn0sub2  13551  fz0fzdiffz0  13553  elfzmlbp  13555  difelfznle  13558  nelfzo  13580  elfzouz2  13590  fzo0n  13597  fzonlt0  13598  fzossrbm1  13604  fzospliti  13607  elfzo0z  13617  fzofzim  13625  fzo1fzo0n0  13631  eluzgtdifelfzo  13643  fzossfzop1  13659  ssfzoulel  13676  ssfzo12bi  13677  elfzonelfzo  13685  elfzomelpfzo  13688  elfznelfzob  13690  fzostep1  13702  fllt  13726  flid  13728  flbi2  13737  2tnp1ge0ge0  13749  flhalf  13750  fldiv4p1lem1div2  13755  fldiv4lem1div2uz2  13756  dfceil2  13759  ceile  13769  ceilid  13771  quoremz  13775  intfracq  13779  uzsup  13783  mulmod0  13797  zmod10  13807  zmodcl  13811  zmodfz  13813  zmodid2  13819  modcyc  13826  modaddid  13830  mulp1mod1  13834  muladdmod  13835  modmuladd  13836  modmuladdim  13837  modmul1  13847  modaddmodup  13857  modaddmodlo  13858  modaddmulmod  13861  zsqcl2  14061  leexp2  14094  iexpcyc  14130  fi1uzind  14430  ccatsymb  14506  ccatval21sw  14509  lswccatn0lsw  14515  swrdnd  14578  swrdnnn0nd  14580  swrd0  14582  swrdswrdlem  14627  swrdswrd  14628  swrdccatin2  14652  pfxccatin12lem2  14654  pfxccatin12lem3  14655  repswswrd  14707  cshwmodn  14718  cshwsublen  14719  cshwidxmod  14726  cshwidxmodr  14727  cshwidxm1  14730  repswcshw  14735  2cshw  14736  cshweqrep  14744  cshw1  14745  swrd2lsw  14875  nn0abscl  15235  rexuzre  15276  dvdsval3  16183  p1modz1  16186  moddvds  16190  absdvdsb  16201  dvdsabsb  16202  dvdsle  16237  alzdvds  16247  mod2eq1n2dvds  16274  evennn02n  16277  evennn2n  16278  ltoddhalfle  16288  divalgmod  16333  fldivndvdslt  16343  flodddiv4t2lthalf  16345  bitsp1o  16360  gcdabs1  16456  modgcd  16459  bezoutlem1  16466  dfgcd2  16473  algcvga  16506  lcmabs  16532  isprm3  16610  dvdsnprmd  16617  2mulprm  16620  oddprmgt2  16626  sqnprm  16629  zgcdsq  16680  hashdvds  16702  vfermltlALT  16730  powm2modprm  16731  modprm0  16733  modprmn0modprm0  16735  fldivp1  16825  zgz  16861  4sqlem4  16880  prmgaplem5  16983  prmgaplem7  16985  cshwshashlem2  17024  setsstruct  17103  mulgmodid  19043  gexdvds  19513  zringunit  21421  prmirred  21429  znf1o  21506  chfacfscmul0  22802  chfacfscmulgsum  22804  chfacfpmmul0  22806  chfacfpmmulgsum  22808  dyadf  25548  dyadovol  25550  degltlem1  26033  coskpi  26488  cosne0  26494  relogexp  26561  cxpeq  26723  relogbzexp  26742  ppival2  27094  ppival2g  27095  ppiprm  27117  chtprm  27119  chtnprm  27120  ppip1le  27127  efexple  27248  zabsle1  27263  lgsdir2lem4  27295  lgsne0  27302  gausslemma2dlem1a  27332  gausslemma2dlem3  27335  gausslemma2dlem4  27336  lgsquadlem1  27347  lgsquadlem2  27348  2lgslem1a1  27356  2lgslem1a2  27357  2sqlem2  27385  rplogsumlem2  27452  pntrsumbnd  27533  axlowdim  29034  crctcshwlkn0lem3  29885  crctcshwlkn0lem5  29887  crctcshwlkn0  29894  crctcsh  29897  clwlkclwwlklem2fv2  30071  clwlkclwwlklem2a  30073  clwwisshclwwslemlem  30088  clwwlkinwwlk  30115  clwwlkext2edg  30131  wwlksubclwwlk  30133  numclwwlk5  30463  topnfbey  30544  uzssico  32864  1fldgenq  33404  znfermltl  33447  ply1coedeg  33670  rezh  34126  zrhre  34176  hashf2  34241  ballotlemfc0  34650  ballotlemfcc  34651  chpvalz  34785  chtvalz  34786  zltp1ne  35304  0nn0m1nnn0  35307  elfzm12  35869  nn0prpwlem  36516  poimirlem24  37845  mblfinlem1  37858  mblfinlem2  37859  itg2addnclem2  37873  fzmul  37942  incsequz2  37950  fimgmcyc  42789  ellz1  43009  lzunuz  43010  lzenom  43012  nerabdioph  43051  pell14qrgt0  43101  rmxycomplete  43159  monotuz  43183  monotoddzzfi  43184  oddcomabszz  43186  zindbi  43188  jm2.24  43205  congrep  43215  fzneg  43224  jm2.19  43235  fzunt  43696  fzunt1d  43698  fzuntgd  43699  oddfl  45526  fzdifsuc2  45558  climsuse  45854  stoweidlem26  46270  stoweidlem34  46278  fourierdlem20  46371  fourierdlem42  46393  fourierdlem51  46401  fourierdlem64  46414  fourierdlem76  46426  fourierdlem94  46444  fourierdlem97  46447  fourierdlem113  46463  natlocalincr  47120  natglobalincr  47121  zm1nn  47548  zgeltp1eq  47555  eluzge0nn0  47558  elfz2z  47561  2elfz2melfz  47564  elfzlble  47566  elfzelfzlble  47567  fzopredsuc  47569  ceilbi  47579  mod0mul  47602  modn0mul  47603  m1modmmod  47604  difmodm1lt  47605  mod2addne  47610  modm2nep1  47612  modp2nep1  47613  modm1nep2  47614  modm1nem2  47615  modm1p1ne  47616  smonoord  47617  fsummmodsndifre  47620  iccpartipre  47667  iccpartiltu  47668  iccpartigtl  47669  icceuelpartlem  47681  fmtno4prmfac  47818  lighneallem4b  47855  dfeven3  47904  dfodd4  47905  nn0o1gt2ALTV  47940  nnoALTV  47941  fpprel2  47987  gbegt5  48007  gbowgt5  48008  sbgoldbwt  48023  nnsum3primesle9  48040  nnsum4primesodd  48042  nnsum4primesoddALTV  48043  evengpop3  48044  evengpoap3  48045  nnsum4primesevenALTV  48047  bgoldbtbndlem1  48051  bgoldbtbndlem2  48052  bgoldbtbndlem3  48053  bgoldbtbndlem4  48054  gpgprismgriedgdmss  48298  gpgusgralem  48302  gpgedgvtx1  48308  gpg5nbgrvtx03starlem2  48315  gpg5nbgrvtx13starlem2  48318  gpg3nbgrvtx0  48322  cznnring  48508  elfzolborelfzop1  48765  zgtp1leeq  48767  rege1logbzge0  48805  fllog2  48814  dignn0ldlem  48848  dignn0flhalflem1  48861  dignn0flhalflem2  48862