Theorem zred 12674

Description: An integer is a real number. (Contributed by Mario Carneiro, 28-May-2016.)

Hypothesis

Ref	Expression
zred.1	⊢ (𝜑 → 𝐴 ∈ ℤ)

Assertion

Ref	Expression
zred	⊢ (𝜑 → 𝐴 ∈ ℝ)

Proof of Theorem zred

Step	Hyp	Ref	Expression
1		zssre 12572	. 2 ⊢ ℤ ⊆ ℝ
2		zred.1	. 2 ⊢ (𝜑 → 𝐴 ∈ ℤ)
3	1, 2	sselid 3934	1 ⊢ (𝜑 → 𝐴 ∈ ℝ)

Syntax hints:   → wi 4   ∈ wcel 2141  ℝcr 11069  ℤcz 12565

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1814  ax-4 1828  ax-5 1929  ax-6 1986  ax-7 2027  ax-8 2143  ax-9 2151  ax-ext 2733

This theorem depends on definitions:  df-bi 209  df-an 400  df-or 859  df-3or 1098  df-3an 1099  df-tru 1562  df-fal 1572  df-ex 1799  df-sb 2090  df-clab 2740  df-cleq 2753  df-clel 2836  df-rab 3414  df-v 3455  df-dif 3907  df-un 3909  df-ss 3921  df-nul 4286  df-if 4480  df-sn 4582  df-pr 4584  df-op 4588  df-uni 4865  df-br 5100  df-iota 6473  df-fv 6525  df-ov 7395  df-neg 11414  df-z 12566

This theorem is referenced by:  zcnd  12675  suprfinzcl  12684  eluzmn  12843  eluzelre  12847  eluzadd  12865  subeluzsub  12869  uzm1  12870  zsupss  12935  suprzcl2  12936  uzwo3  12941  rpnnen1lem3  12977  rpnnen1lem5  12979  zltaddlt1le  13506  fzsplit2  13551  fzdisj  13553  ssfzunsnext  13571  fzpreddisj  13575  fznatpl1  13580  fzp1disj  13585  uzdisj  13599  fzdif1  13607  fzm1  13609  fz0fzdiffz0  13639  elfzmlbm  13640  elfzmlbp  13641  difelfznle  13644  nn0disj  13646  elfzolt3  13672  fzonel  13676  fzospliti  13694  fzodisj  13696  fzouzdisj  13698  fzodisjsn  13700  elfzo0subge1  13708  elfzo0suble  13709  fzonmapblen  13711  fzoaddel  13720  elincfzoext  13726  fzone1  13787  reflcl  13803  flge  13812  flwordi  13819  fladdz  13832  2tnp1ge0ge0  13836  flhalf  13837  fldiv4p1lem1div2  13842  fldiv4lem1div2uz2  13843  fldiv4lem1div2  13844  flleceil  13860  fleqceilz  13861  quoremz  13862  uzsup  13870  modaddid  13917  modmul12d  13935  modaddmodup  13944  modaddmodlo  13945  modfzo0difsn  13953  modsumfzodifsn  13954  addmodlteq  13956  om2uzlti  13960  om2uzf1oi  13963  seqf1olem1  14051  seqf1olem2  14052  bcval4  14317  bcp1nk  14327  bcval5  14328  fzsdom2  14438  seqcoll  14474  seqcoll2  14475  ccatrn  14600  ccatalpha  14604  cshwidxmodr  14814  fzomaxdiflem  15353  fzomaxdif  15354  rexuzre  15363  limsupgre  15491  rlimclim1  15555  isercoll  15678  iseralt  15695  fsumm1  15761  fsum1p  15763  fsum0diaglem  15786  modfsummods  15804  isumsplit  15853  climcndslem1  15862  mertenslem1  15897  ntrivcvgmul  15915  fprodntriv  15955  fprod1p  15981  fprodeq0  15988  fallfacval4  16056  bpoly4  16072  fzo0dvdseq  16340  dvdsmod  16346  oexpneg  16362  mod2eq1n2dvds  16364  ltoddhalfle  16378  flodddiv4t2lthalf  16435  bitsp1  16448  bitsfzolem  16451  bitsfzo  16452  bitsmod  16453  bitscmp  16455  bitsinv1lem  16458  sadaddlem  16483  bitsres  16490  bitsuz  16491  smumul  16510  gcd0id  16536  gcdneg  16539  dfgcd2  16563  nn0seqcvgd  16587  lcmgcdlem  16623  nprm  16705  prmdvdsfz  16723  isprm5  16725  isprm7  16726  coprm  16729  prmexpb  16737  prmfac1  16738  hashdvds  16793  crth  16796  eulerthlem2  16800  fermltl  16802  prmdiv  16803  prmdiveq  16804  hashgcdlem  16806  odzdvds  16814  vfermltlALT  16821  modprm0  16824  modprmn0modprm0  16826  prm23ge5  16834  pythagtriplem13  16846  pcxcl  16880  pcaddlem  16907  pcadd  16908  pcfac  16918  qexpz  16920  prmunb  16933  1arithlem4  16945  4sqlem5  16961  4sqlem6  16962  4sqlem7  16963  4sqlem10  16966  4sqlem11  16974  4sqlem12  16975  4sqlem15  16978  4sqlem16  16979  4sqlem17  16980  vdwnnlem3  17016  prmgaplem7  17076  cshwshashlem3  17116  chnub  18637  chnso  18639  chnccat  18641  chnpof1  18645  subgmulg  19165  mndodconglem  19564  odnncl  19568  odmod  19569  oddvds  19570  dfod2  19587  sylow1lem3  19623  efgsp1  19760  efgredleme  19766  telgsumfzs  20012  zringlpirlem1  21494  zringlpirlem3  21496  fermltlchr  21561  znf1o  21583  zcld  24854  ovoliunlem1  25544  ovoliunlem2  25545  dyadss  25636  dyaddisjlem  25637  dyadmaxlem  25639  dvfsumle  26063  dvfsumge  26064  dvfsumabs  26065  dvfsumlem1  26068  dvfsumlem3  26070  degltlem1  26112  plyco0  26232  plyeq0lem  26250  plydivex  26338  aannenlem1  26369  efif1olem2  26585  nnlogbexp  26823  logblt  26826  ang180lem1  26851  ang180lem3  26853  wilthlem2  27110  basellem3  27124  basellem4  27125  ppiprm  27192  chtdif  27199  ppidif  27204  chtub  27253  mersenne  27268  bcmono  27318  bcmax  27319  bposlem1  27325  bposlem3  27327  bposlem5  27329  bposlem6  27330  lgsval2lem  27348  lgsvalmod  27357  lgsneg  27362  lgsmod  27364  lgsdilem  27365  lgsdirprm  27372  lgsdilem2  27374  lgsne0  27376  lgssq  27378  lgssq2  27379  lgsqr  27392  lgsdchr  27396  gausslemma2dlem1a  27406  gausslemma2dlem3  27409  gausslemma2dlem5a  27411  gausslemma2dlem6  27413  gausslemma2d  27415  lgseisenlem1  27416  lgseisenlem2  27417  lgseisenlem3  27418  lgseisenlem4  27419  lgsquadlem1  27421  lgsquadlem2  27422  lgsquadlem3  27423  lgsquad3  27428  2lgslem1a2  27431  2lgslem1  27435  2lgslem2  27436  2sqlem3  27461  2sqlem8  27467  2sqblem  27472  2sqmod  27477  chebbnd1lem1  27510  chebbnd1lem2  27511  chebbnd1lem3  27512  dchrmusum2  27535  dchrvmasumlem1  27536  dchrvmasum2lem  27537  dchrvmasum2if  27538  dchrvmasumlem3  27540  dchrvmasumiflem2  27543  dchrisum0lem1  27557  dchrmusumlem  27563  mudivsum  27571  mulogsumlem  27572  mulogsum  27573  mulog2sumlem2  27576  mulog2sumlem3  27577  selberglem1  27586  selberglem2  27587  pntpbnd1  27627  pntlemg  27639  pntlemf  27646  qabvle  27666  padicabv  27671  padicabvcxp  27673  ostth2lem2  27675  axlowdimlem13  29101  axlowdimlem16  29104  pthdlem1  29912  crctcshwlkn0  29967  crctcsh  29970  clwwisshclwwslemlem  30161  eucrctshift  30391  nndiffz1  32938  fzsplit3  32945  bcm1n  32947  suppssnn0  32957  ltesubnnd  32975  wrdt2ind  33092  cshwrnid  33100  cycpmfv2  33255  cycpmco2lem6  33272  cycpmco2lem7  33273  cycpmrn  33284  cyc3conja  33298  pnfinf  33324  znfermltl  33513  constrext2chnlem  34008  cos9thpiminplylem1  34040  cos9thpiminplylem2  34041  dya2iocress  34532  dya2iocbrsiga  34533  dya2icobrsiga  34534  dya2icoseg  34535  dya2iocucvr  34542  sxbrsigalem2  34544  ballotlemfc0  34751  ballotlemfcc  34752  ballotlemodife  34756  ballotlemimin  34764  ballotlemsgt1  34769  ballotlemsel1i  34771  ballotlemsi  34773  ballotlemsima  34774  ballotlemrv2  34780  ballotlemfrceq  34787  ballotlemfrcn0  34788  ballotlemirc  34790  fsum2dsub  34865  reprlt  34877  reprgt  34879  breprexplemc  34890  tgoldbachgnn  34917  tgoldbachgt  34921  subfacval3  35503  erdszelem8  35512  erdszelem9  35513  supfz  36043  inffz  36044  dnizeq0  36877  dnizphlfeqhlf  36878  dnibndlem13  36892  knoppndvlem1  36914  knoppndvlem2  36915  knoppndvlem7  36920  knoppndvlem19  36932  knoppndvlem21  36934  ltflcei  38071  leceifl  38072  poimirlem1  38084  poimirlem2  38085  poimirlem6  38089  poimirlem7  38090  poimirlem8  38091  poimirlem15  38098  poimirlem16  38099  poimirlem17  38100  poimirlem19  38102  poimirlem20  38103  poimirlem23  38106  poimirlem24  38107  poimirlem27  38110  poimirlem29  38112  poimirlem31  38114  poimirlem32  38115  mblfinlem2  38121  itg2addnclem2  38135  mettrifi  38220  cntotbnd  38259  fzne2d  42561  aks4d1lem1  42643  aks4d1p1p3  42650  aks4d1p1p2  42651  aks4d1p1p4  42652  aks4d1p1  42657  aks4d1p2  42658  aks4d1p3  42659  aks4d1p5  42661  aks4d1p6  42662  aks4d1p7d1  42663  aks4d1p7  42664  aks4d1p8d3  42667  aks4d1p8  42668  aks4d1p9  42669  posbezout  42681  aks6d1c1  42697  hashscontpow1  42702  hashscontpow  42703  aks6d1c2  42711  aks6d1c5lem1  42717  2ap1caineq  42726  sticksstones6  42732  sticksstones7  42733  sticksstones10  42736  sticksstones12a  42738  sticksstones12  42739  sticksstones22  42749  bcled  42759  bcle2d  42760  aks6d1c7lem1  42761  aks6d1c7lem2  42762  aks6d1c7  42765  aks5lem6  42773  unitscyglem2  42777  unitscyglem4  42779  aks5lem8  42782  sumcubes  42886  frlmvscadiccat  43092  dffltz  43180  lzunuz  43313  lzenom  43315  diophin  43317  irrapxlem1  43363  irrapxlem2  43364  irrapxlem3  43365  irrapxlem4  43366  pellexlem5  43374  pellexlem6  43375  rmspecfund  43450  rmxypos  43488  ltrmynn0  43489  ltrmxnn0  43490  ltrmy  43493  rmyeq0  43494  rmyeq  43495  lermy  43496  rmyabs  43499  jm2.24nn  43500  jm2.17a  43501  jm2.17b  43502  jm2.17c  43503  jm2.24  43504  rmygeid  43505  acongrep  43521  fzmaxdif  43522  acongeq  43524  jm2.22  43536  jm2.23  43537  jm2.26lem3  43542  jm2.27a  43546  jm3.1lem1  43558  jm3.1lem3  43560  expdiophlem1  43562  fzuntd  43996  fzunt1d  43997  fzuntgd  43998  prmunb2  44851  nzprmdif  44859  hashnzfzclim  44862  binomcxplemnn0  44889  uzwo4  45597  ssinc  45629  ssdec  45630  zltlesub  45828  monoords  45840  fzisoeu  45843  fperiodmul  45847  fzdifsuc2  45853  iuneqfzuzlem  45874  uzublem  45968  zxrd  45991  uzinico  46099  uzubioo  46105  fmul01  46120  fmul01lt1lem1  46124  fmul01lt1lem2  46125  climsuselem1  46147  climsuse  46148  sumnnodd  46170  ltmod  46176  limsupresuz  46241  limsupubuzlem  46250  limsupequzlem  46260  limsupmnfuzlem  46264  limsupequzmptlem  46266  limsupre3uzlem  46273  supcnvlimsup  46278  limsup10exlem  46310  liminfresuz  46322  liminfvaluz  46330  limsupvaluz3  46336  ioodvbdlimc1lem2  46470  ioodvbdlimc2lem  46472  dvnmul  46481  dvnprodlem1  46484  dvnprodlem2  46485  iblspltprt  46511  itgspltprt  46517  stoweidlem3  46541  stoweidlem11  46549  stoweidlem20  46558  stoweidlem26  46564  stoweidlem34  46572  stoweidlem59  46597  stirlinglem5  46616  dirkertrigeqlem3  46638  dirkeritg  46640  dirkercncflem1  46641  dirkercncflem2  46642  dirkercncflem4  46644  fourierdlem4  46649  fourierdlem6  46651  fourierdlem7  46652  fourierdlem11  46656  fourierdlem12  46657  fourierdlem15  46660  fourierdlem19  46664  fourierdlem20  46665  fourierdlem25  46670  fourierdlem26  46671  fourierdlem34  46679  fourierdlem35  46680  fourierdlem41  46686  fourierdlem48  46692  fourierdlem49  46693  fourierdlem50  46694  fourierdlem51  46695  fourierdlem54  46698  fourierdlem63  46707  fourierdlem64  46708  fourierdlem65  46709  fourierdlem71  46715  fourierdlem79  46723  fourierdlem89  46733  fourierdlem90  46734  fourierdlem91  46735  fourierdlem102  46746  fourierdlem103  46747  fourierdlem104  46748  fourierdlem114  46758  fouriersw  46769  elaa2lem  46771  etransclem3  46775  etransclem4  46776  etransclem7  46779  etransclem10  46782  etransclem15  46787  etransclem19  46791  etransclem23  46795  etransclem24  46796  etransclem25  46797  etransclem27  46799  etransclem31  46803  etransclem32  46804  etransclem35  46807  etransclem41  46813  etransclem44  46816  etransclem46  46818  etransclem48  46820  iundjiun  46998  caratheodorylem1  47064  hoicvr  47086  smflimsuplem4  47361  smfliminflem  47368  ormklocald  47414  ormkglobd  47415  natglobalincr  47417  chnerlem3  47424  2elfz2melfz  47876  elfzelfzlble  47879  fzopredsuc  47882  nnmul2  47888  2ltceilhalf  47890  ceilhalfgt1  47891  ceilhalfnn  47898  submodlt  47914  m1modmmod  47922  difmodm1lt  47923  modmknepk  47926  mod2addne  47928  2timesltsq  47936  2timesltsqm1  47937  fsummsndifre  47938  iccpartgt  47997  icceuelpartlem  48005  icceuelpart  48006  iccpartnel  48008  nprmmul2  48098  nprmmul3  48099  lighneallem2  48179  proththd  48187  nprmdvdsfacm1lem4  48196  dfodd4  48245  oexpnegALTV  48263  nnoALTV  48281  evenltle  48303  fpprwppr  48325  gbowgt5  48348  gboge9  48350  stgoldbwt  48362  sbgoldbst  48364  sbgoldbalt  48367  sgoldbeven3prm  48369  mogoldbb  48371  bgoldbtbndlem1  48391  bgoldbtbndlem2  48392  bgoldbtbndlem3  48393  bgoldbtbnd  48395  bgoldbachlt  48399  tgblthelfgott  48401  tgoldbach  48403  upgrimpthslem2  48494  gpgprismgrusgra  48644  gpgedgvtx1  48648  gpgvtxedg0  48649  gpgvtxedg1  48650  gpg5nbgrvtx13starlem2  48658  gpg3nbgrvtx0  48662  gpg3kgrtriexlem1  48669  gpg3kgrtriexlem4  48672  gpg3kgrtriexlem6  48674  pw2m1lepw2m1  49106  fllogbd  49146  logbpw2m1  49153  fllog2  49154  nnpw2blen  49166  nnolog2flm1  49176  dignn0flhalflem1  49201  dignn0flhalflem2  49202