Theorem zred 12688

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 12586	. 2 ⊢ ℤ ⊆ ℝ
2		zred.1	. 2 ⊢ (𝜑 → 𝐴 ∈ ℤ)
3	1, 2	sselid 3937	1 ⊢ (𝜑 → 𝐴 ∈ ℝ)

Syntax hints:   → wi 4   ∈ wcel 2145  ℝcr 11087  ℤcz 12579

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1818  ax-4 1832  ax-5 1933  ax-6 1990  ax-7 2031  ax-8 2147  ax-9 2155  ax-ext 2737

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3or 1102  df-3an 1103  df-tru 1566  df-fal 1576  df-ex 1803  df-sb 2094  df-clab 2744  df-cleq 2757  df-clel 2840  df-rab 3418  df-v 3459  df-dif 3910  df-un 3912  df-ss 3924  df-nul 4289  df-if 4484  df-sn 4586  df-pr 4588  df-op 4592  df-uni 4868  df-br 5105  df-iota 6481  df-fv 6533  df-ov 7403  df-neg 11432  df-z 12580

This theorem is referenced by:  zcnd  12689  suprfinzcl  12698  eluzmn  12857  eluzelre  12861  eluzadd  12879  subeluzsub  12883  uzm1  12884  zsupss  12949  suprzcl2  12950  uzwo3  12955  rpnnen1lem3  12991  rpnnen1lem5  12993  zltaddlt1le  13520  fzsplit2  13565  fzdisj  13567  ssfzunsnext  13585  fzpreddisj  13589  fznatpl1  13594  fzp1disj  13599  uzdisj  13613  fzdif1  13621  fzm1  13623  fz0fzdiffz0  13653  elfzmlbm  13654  elfzmlbp  13655  difelfznle  13658  nn0disj  13660  elfzolt3  13686  fzonel  13690  fzospliti  13708  fzodisj  13710  fzouzdisj  13712  fzodisjsn  13714  elfzo0subge1  13722  elfzo0suble  13723  fzonmapblen  13725  fzoaddel  13734  elincfzoext  13740  fzone1  13801  reflcl  13817  flge  13826  flwordi  13833  fladdz  13846  2tnp1ge0ge0  13850  flhalf  13851  fldiv4p1lem1div2  13856  fldiv4lem1div2uz2  13857  fldiv4lem1div2  13858  flleceil  13874  fleqceilz  13875  quoremz  13876  uzsup  13884  modaddid  13931  modmul12d  13949  modaddmodup  13958  modaddmodlo  13959  modfzo0difsn  13967  modsumfzodifsn  13968  addmodlteq  13970  om2uzlti  13974  om2uzf1oi  13977  seqf1olem1  14065  seqf1olem2  14066  bcval4  14331  bcp1nk  14341  bcval5  14342  fzsdom2  14453  seqcoll  14489  seqcoll2  14490  ccatrn  14615  ccatalpha  14619  cshwidxmodr  14829  fzomaxdiflem  15382  fzomaxdif  15383  rexuzre  15392  limsupgre  15520  rlimclim1  15584  isercoll  15707  iseralt  15724  fsumm1  15790  fsum1p  15792  fsum0diaglem  15815  modfsummods  15833  isumsplit  15882  climcndslem1  15891  mertenslem1  15926  ntrivcvgmul  15944  fprodntriv  15984  fprod1p  16010  fprodeq0  16017  fallfacval4  16085  bpoly4  16101  fzo0dvdseq  16369  dvdsmod  16375  oexpneg  16391  mod2eq1n2dvds  16393  ltoddhalfle  16407  flodddiv4t2lthalf  16464  bitsp1  16477  bitsfzolem  16480  bitsfzo  16481  bitsmod  16482  bitscmp  16484  bitsinv1lem  16487  sadaddlem  16512  bitsres  16519  bitsuz  16520  smumul  16539  gcd0id  16565  gcdneg  16568  dfgcd2  16592  nn0seqcvgd  16616  lcmgcdlem  16652  nprm  16734  prmdvdsfz  16752  isprm5  16754  isprm7  16755  coprm  16758  prmexpb  16766  prmfac1  16767  hashdvds  16822  crth  16825  eulerthlem2  16829  fermltl  16831  prmdiv  16832  prmdiveq  16833  hashgcdlem  16835  odzdvds  16843  vfermltlALT  16850  modprm0  16853  modprmn0modprm0  16855  prm23ge5  16863  pythagtriplem13  16875  pcxcl  16909  pcaddlem  16936  pcadd  16937  pcfac  16947  qexpz  16949  prmunb  16962  1arithlem4  16974  4sqlem5  16990  4sqlem6  16991  4sqlem7  16992  4sqlem10  16995  4sqlem11  17003  4sqlem12  17004  4sqlem15  17007  4sqlem16  17008  4sqlem17  17009  vdwnnlem3  17045  prmgaplem7  17105  cshwshashlem3  17145  chnub  18666  chnso  18668  chnccat  18670  chnpof1  18674  subgmulg  19195  mndodconglem  19599  odnncl  19603  odmod  19604  oddvds  19605  dfod2  19622  sylow1lem3  19658  efgsp1  19795  efgredleme  19801  telgsumfzs  20047  zringlpirlem1  21569  zringlpirlem3  21571  fermltlchr  21636  znf1o  21658  zcld  24928  ovoliunlem1  25618  ovoliunlem2  25619  dyadss  25710  dyaddisjlem  25711  dyadmaxlem  25713  dvfsumle  26137  dvfsumge  26138  dvfsumabs  26139  dvfsumlem1  26142  dvfsumlem3  26144  degltlem1  26186  plyco0  26306  plyeq0lem  26324  plydivex  26415  aannenlem1  26446  efif1olem2  26662  nnlogbexp  26900  logblt  26903  ang180lem1  26928  ang180lem3  26930  wilthlem2  27187  basellem3  27201  basellem4  27202  ppiprm  27269  chtdif  27276  ppidif  27281  chtub  27330  mersenne  27345  bcmono  27395  bcmax  27396  bposlem1  27402  bposlem3  27404  bposlem5  27406  bposlem6  27407  lgsval2lem  27425  lgsvalmod  27434  lgsneg  27439  lgsmod  27441  lgsdilem  27442  lgsdirprm  27449  lgsdilem2  27451  lgsne0  27453  lgssq  27455  lgssq2  27456  lgsqr  27469  lgsdchr  27473  gausslemma2dlem1a  27483  gausslemma2dlem3  27486  gausslemma2dlem5a  27488  gausslemma2dlem6  27490  gausslemma2d  27492  lgseisenlem1  27493  lgseisenlem2  27494  lgseisenlem3  27495  lgseisenlem4  27496  lgsquadlem1  27498  lgsquadlem2  27499  lgsquadlem3  27500  lgsquad3  27505  2lgslem1a2  27508  2lgslem1  27512  2lgslem2  27513  2sqlem3  27538  2sqlem8  27544  2sqblem  27549  2sqmod  27554  chebbnd1lem1  27587  chebbnd1lem2  27588  chebbnd1lem3  27589  dchrmusum2  27612  dchrvmasumlem1  27613  dchrvmasum2lem  27614  dchrvmasum2if  27615  dchrvmasumlem3  27617  dchrvmasumiflem2  27620  dchrisum0lem1  27634  dchrmusumlem  27640  mudivsum  27648  mulogsumlem  27649  mulogsum  27650  mulog2sumlem2  27653  mulog2sumlem3  27654  selberglem1  27663  selberglem2  27664  pntpbnd1  27704  pntlemg  27716  pntlemf  27723  qabvle  27743  padicabv  27748  padicabvcxp  27750  ostth2lem2  27752  axlowdimlem13  29209  axlowdimlem16  29212  pthdlem1  30020  crctcshwlkn0  30075  crctcsh  30078  clwwisshclwwslemlem  30269  eucrctshift  30499  nndiffz1  33039  fzsplit3  33046  bcm1n  33048  suppssnn0  33058  ltesubnnd  33075  wrdt2ind  33181  cshwrnid  33189  cycpmfv2  33342  cycpmco2lem6  33359  cycpmco2lem7  33360  cycpmrn  33371  cyc3conja  33385  pnfinf  33411  znfermltl  33591  constrext2chnlem  34052  cos9thpiminplylem1  34084  cos9thpiminplylem2  34085  dya2iocress  34576  dya2iocbrsiga  34577  dya2icobrsiga  34578  dya2icoseg  34579  dya2iocucvr  34586  sxbrsigalem2  34588  ballotlemfc0  34795  ballotlemfcc  34796  ballotlemodife  34800  ballotlemimin  34808  ballotlemsgt1  34813  ballotlemsel1i  34815  ballotlemsi  34817  ballotlemsima  34818  ballotlemrv2  34824  ballotlemfrceq  34831  ballotlemfrcn0  34832  ballotlemirc  34834  fsum2dsub  34906  reprlt  34918  reprgt  34920  breprexplemc  34931  tgoldbachgnn  34958  tgoldbachgt  34962  subfacval3  35547  erdszelem8  35556  erdszelem9  35557  supfz  36087  inffz  36088  dnizeq0  36921  dnizphlfeqhlf  36922  dnibndlem13  36936  knoppndvlem1  36958  knoppndvlem2  36959  knoppndvlem7  36964  knoppndvlem19  36976  knoppndvlem21  36978  ltflcei  38114  leceifl  38115  poimirlem1  38127  poimirlem2  38128  poimirlem6  38132  poimirlem7  38133  poimirlem8  38134  poimirlem15  38141  poimirlem16  38142  poimirlem17  38143  poimirlem19  38145  poimirlem20  38146  poimirlem23  38149  poimirlem24  38150  poimirlem27  38153  poimirlem29  38155  poimirlem31  38157  poimirlem32  38158  mblfinlem2  38164  itg2addnclem2  38178  mettrifi  38263  cntotbnd  38302  fzne2d  42604  aks4d1lem1  42686  aks4d1p1p3  42693  aks4d1p1p2  42694  aks4d1p1p4  42695  aks4d1p1  42700  aks4d1p2  42701  aks4d1p3  42702  aks4d1p5  42704  aks4d1p6  42705  aks4d1p7d1  42706  aks4d1p7  42707  aks4d1p8d3  42710  aks4d1p8  42711  aks4d1p9  42712  posbezout  42724  aks6d1c1  42740  hashscontpow1  42745  hashscontpow  42746  aks6d1c2  42754  aks6d1c5lem1  42760  2ap1caineq  42769  sticksstones6  42775  sticksstones7  42776  sticksstones10  42779  sticksstones12a  42781  sticksstones12  42782  sticksstones22  42792  bcled  42802  bcle2d  42803  aks6d1c7lem1  42804  aks6d1c7lem2  42805  aks6d1c7  42808  aks5lem6  42816  unitscyglem2  42820  unitscyglem4  42822  aks5lem8  42825  sumcubes  42929  frlmvscadiccat  43135  dffltz  43223  lzunuz  43356  lzenom  43358  diophin  43360  irrapxlem1  43406  irrapxlem2  43407  irrapxlem3  43408  irrapxlem4  43409  pellexlem5  43417  pellexlem6  43418  rmspecfund  43493  rmxypos  43531  ltrmynn0  43532  ltrmxnn0  43533  ltrmy  43536  rmyeq0  43537  rmyeq  43538  lermy  43539  rmyabs  43542  jm2.24nn  43543  jm2.17a  43544  jm2.17b  43545  jm2.17c  43546  jm2.24  43547  rmygeid  43548  acongrep  43564  fzmaxdif  43565  acongeq  43567  jm2.22  43579  jm2.23  43580  jm2.26lem3  43585  jm2.27a  43589  jm3.1lem1  43601  jm3.1lem3  43603  expdiophlem1  43605  fzuntd  44039  fzunt1d  44040  fzuntgd  44041  prmunb2  44880  nzprmdif  44888  hashnzfzclim  44891  binomcxplemnn0  44918  uzwo4  45632  ssinc  45664  ssdec  45665  zltlesub  45863  monoords  45875  fzisoeu  45878  fperiodmul  45882  fzdifsuc2  45888  iuneqfzuzlem  45909  uzublem  46003  zxrd  46026  uzinico  46134  uzubioo  46140  fmul01  46155  fmul01lt1lem1  46159  fmul01lt1lem2  46160  climsuselem1  46182  climsuse  46183  sumnnodd  46205  ltmod  46211  limsupresuz  46276  limsupubuzlem  46285  limsupequzlem  46295  limsupmnfuzlem  46299  limsupequzmptlem  46301  limsupre3uzlem  46308  supcnvlimsup  46313  limsup10exlem  46345  liminfresuz  46357  liminfvaluz  46365  limsupvaluz3  46371  ioodvbdlimc1lem2  46505  ioodvbdlimc2lem  46507  dvnmul  46516  dvnprodlem1  46519  dvnprodlem2  46520  iblspltprt  46546  itgspltprt  46552  stoweidlem3  46576  stoweidlem11  46584  stoweidlem20  46593  stoweidlem26  46599  stoweidlem34  46607  stoweidlem59  46632  stirlinglem5  46651  dirkertrigeqlem3  46673  dirkeritg  46675  dirkercncflem1  46676  dirkercncflem2  46677  dirkercncflem4  46679  fourierdlem4  46684  fourierdlem6  46686  fourierdlem7  46687  fourierdlem11  46691  fourierdlem12  46692  fourierdlem15  46695  fourierdlem19  46699  fourierdlem20  46700  fourierdlem25  46705  fourierdlem26  46706  fourierdlem34  46714  fourierdlem35  46715  fourierdlem41  46721  fourierdlem48  46727  fourierdlem49  46728  fourierdlem50  46729  fourierdlem51  46730  fourierdlem54  46733  fourierdlem63  46742  fourierdlem64  46743  fourierdlem65  46744  fourierdlem71  46750  fourierdlem79  46758  fourierdlem89  46768  fourierdlem90  46769  fourierdlem91  46770  fourierdlem102  46781  fourierdlem103  46782  fourierdlem104  46783  fourierdlem114  46793  fouriersw  46804  elaa2lem  46806  etransclem3  46810  etransclem4  46811  etransclem7  46814  etransclem10  46817  etransclem15  46822  etransclem19  46826  etransclem23  46830  etransclem24  46831  etransclem25  46832  etransclem27  46834  etransclem31  46838  etransclem32  46839  etransclem35  46842  etransclem41  46848  etransclem44  46851  etransclem46  46853  etransclem48  46855  iundjiun  47033  caratheodorylem1  47099  hoicvr  47121  smflimsuplem4  47396  smfliminflem  47403  ormklocald  47449  ormkglobd  47450  natglobalincr  47452  chnerlem3  47459  2elfz2melfz  47911  elfzelfzlble  47914  fzopredsuc  47917  nnmul2  47923  2ltceilhalf  47925  ceilhalfgt1  47926  ceilhalfnn  47933  submodlt  47949  m1modmmod  47957  difmodm1lt  47958  modmknepk  47961  mod2addne  47963  2timesltsq  47971  2timesltsqm1  47972  fsummsndifre  47973  iccpartgt  48032  icceuelpartlem  48040  icceuelpart  48041  iccpartnel  48043  nprmmul2  48133  nprmmul3  48134  lighneallem2  48214  proththd  48222  nprmdvdsfacm1lem4  48231  dfodd4  48280  oexpnegALTV  48298  nnoALTV  48316  evenltle  48338  fpprwppr  48360  gbowgt5  48383  gboge9  48385  stgoldbwt  48397  sbgoldbst  48399  sbgoldbalt  48402  sgoldbeven3prm  48404  mogoldbb  48406  bgoldbtbndlem1  48426  bgoldbtbndlem2  48427  bgoldbtbndlem3  48428  bgoldbtbnd  48430  bgoldbachlt  48434  tgblthelfgott  48436  tgoldbach  48438  upgrimpthslem2  48529  gpgprismgrusgra  48679  gpgedgvtx1  48683  gpgvtxedg0  48684  gpgvtxedg1  48685  gpg5nbgrvtx13starlem2  48693  gpg3nbgrvtx0  48697  gpg3kgrtriexlem1  48704  gpg3kgrtriexlem4  48707  gpg3kgrtriexlem6  48709  pw2m1lepw2m1  49152  fllogbd  49192  logbpw2m1  49199  fllog2  49200  nnpw2blen  49212  nnolog2flm1  49222  dignn0flhalflem1  49247  dignn0flhalflem2  49248