Theorem zred 12580

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

Syntax hints:   → wi 4   ∈ wcel 2109  ℝcr 11008  ℤcz 12471

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-rab 3395  df-v 3438  df-dif 3906  df-un 3908  df-ss 3920  df-nul 4285  df-if 4477  df-sn 4578  df-pr 4580  df-op 4584  df-uni 4859  df-br 5093  df-iota 6438  df-fv 6490  df-ov 7352  df-neg 11350  df-z 12472

This theorem is referenced by:  zcnd  12581  suprfinzcl  12590  eluzmn  12742  eluzelre  12746  eluzadd  12764  subeluzsub  12772  uzm1  12773  zsupss  12838  suprzcl2  12839  uzwo3  12844  rpnnen1lem3  12880  rpnnen1lem5  12882  zltaddlt1le  13408  fzsplit2  13452  fzdisj  13454  ssfzunsnext  13472  fzpreddisj  13476  fznatpl1  13481  fzp1disj  13486  uzdisj  13500  fzdif1  13508  fzm1  13510  fz0fzdiffz0  13540  elfzmlbm  13541  elfzmlbp  13542  difelfznle  13545  nn0disj  13547  elfzolt3  13572  fzonel  13576  fzospliti  13594  fzodisj  13596  fzouzdisj  13598  fzodisjsn  13600  elfzo0subge1  13608  elfzo0suble  13609  fzonmapblen  13611  fzoaddel  13620  elincfzoext  13626  reflcl  13700  flge  13709  flwordi  13716  fladdz  13729  2tnp1ge0ge0  13733  flhalf  13734  fldiv4p1lem1div2  13739  fldiv4lem1div2uz2  13740  fldiv4lem1div2  13741  flleceil  13757  fleqceilz  13758  quoremz  13759  uzsup  13767  modaddid  13814  modmul12d  13832  modaddmodup  13841  modaddmodlo  13842  modfzo0difsn  13850  modsumfzodifsn  13851  addmodlteq  13853  om2uzlti  13857  om2uzf1oi  13860  seqf1olem1  13948  seqf1olem2  13949  bcval4  14214  bcp1nk  14224  bcval5  14225  fzsdom2  14335  seqcoll  14371  seqcoll2  14372  ccatrn  14496  ccatalpha  14500  cshwidxmodr  14710  fzomaxdiflem  15250  fzomaxdif  15251  rexuzre  15260  limsupgre  15388  rlimclim1  15452  isercoll  15575  iseralt  15592  fsumm1  15658  fsum1p  15660  fsum0diaglem  15683  modfsummods  15700  isumsplit  15747  climcndslem1  15756  mertenslem1  15791  ntrivcvgmul  15809  fprodntriv  15849  fprod1p  15875  fprodeq0  15882  fallfacval4  15950  bpoly4  15966  fzo0dvdseq  16234  dvdsmod  16240  oexpneg  16256  mod2eq1n2dvds  16258  ltoddhalfle  16272  flodddiv4t2lthalf  16329  bitsp1  16342  bitsfzolem  16345  bitsfzo  16346  bitsmod  16347  bitscmp  16349  bitsinv1lem  16352  sadaddlem  16377  bitsres  16384  bitsuz  16385  smumul  16404  gcd0id  16430  gcdneg  16433  dfgcd2  16457  nn0seqcvgd  16481  lcmgcdlem  16517  nprm  16599  prmdvdsfz  16616  isprm5  16618  isprm7  16619  coprm  16622  prmexpb  16630  prmfac1  16631  hashdvds  16686  crth  16689  eulerthlem2  16693  fermltl  16695  prmdiv  16696  prmdiveq  16697  hashgcdlem  16699  odzdvds  16707  vfermltlALT  16714  modprm0  16717  modprmn0modprm0  16719  prm23ge5  16727  pythagtriplem13  16739  pcxcl  16773  pcaddlem  16800  pcadd  16801  pcfac  16811  qexpz  16813  prmunb  16826  1arithlem4  16838  4sqlem5  16854  4sqlem6  16855  4sqlem7  16856  4sqlem10  16859  4sqlem11  16867  4sqlem12  16868  4sqlem15  16871  4sqlem16  16872  4sqlem17  16873  vdwnnlem3  16909  prmgaplem7  16969  cshwshashlem3  17009  subgmulg  19019  mndodconglem  19420  odnncl  19424  odmod  19425  oddvds  19426  dfod2  19443  sylow1lem3  19479  efgsp1  19616  efgredleme  19622  telgsumfzs  19868  zringlpirlem1  21369  zringlpirlem3  21371  fermltlchr  21436  znf1o  21458  zcld  24700  ovoliunlem1  25401  ovoliunlem2  25402  dyadss  25493  dyaddisjlem  25494  dyadmaxlem  25496  dvfsumle  25924  dvfsumleOLD  25925  dvfsumge  25926  dvfsumabs  25927  dvfsumlem1  25930  dvfsumlem3  25933  degltlem1  25975  plyco0  26095  plyeq0lem  26113  plydivex  26203  aannenlem1  26234  efif1olem2  26450  nnlogbexp  26689  logblt  26692  ang180lem1  26717  ang180lem3  26719  wilthlem2  26977  basellem3  26991  basellem4  26992  ppiprm  27059  chtdif  27066  ppidif  27071  chtub  27121  mersenne  27136  bcmono  27186  bcmax  27187  bposlem1  27193  bposlem3  27195  bposlem5  27197  bposlem6  27198  lgsval2lem  27216  lgsvalmod  27225  lgsneg  27230  lgsmod  27232  lgsdilem  27233  lgsdirprm  27240  lgsdilem2  27242  lgsne0  27244  lgssq  27246  lgssq2  27247  lgsqr  27260  lgsdchr  27264  gausslemma2dlem1a  27274  gausslemma2dlem3  27277  gausslemma2dlem5a  27279  gausslemma2dlem6  27281  gausslemma2d  27283  lgseisenlem1  27284  lgseisenlem2  27285  lgseisenlem3  27286  lgseisenlem4  27287  lgsquadlem1  27289  lgsquadlem2  27290  lgsquadlem3  27291  lgsquad3  27296  2lgslem1a2  27299  2lgslem1  27303  2lgslem2  27304  2sqlem3  27329  2sqlem8  27335  2sqblem  27340  2sqmod  27345  chebbnd1lem1  27378  chebbnd1lem2  27379  chebbnd1lem3  27380  dchrmusum2  27403  dchrvmasumlem1  27404  dchrvmasum2lem  27405  dchrvmasum2if  27406  dchrvmasumlem3  27408  dchrvmasumiflem2  27411  dchrisum0lem1  27425  dchrmusumlem  27431  mudivsum  27439  mulogsumlem  27440  mulogsum  27441  mulog2sumlem2  27444  mulog2sumlem3  27445  selberglem1  27454  selberglem2  27455  pntpbnd1  27495  pntlemg  27507  pntlemf  27514  qabvle  27534  padicabv  27539  padicabvcxp  27541  ostth2lem2  27543  axlowdimlem13  28903  axlowdimlem16  28906  pthdlem1  29715  crctcshwlkn0  29770  crctcsh  29773  clwwisshclwwslemlem  29961  eucrctshift  30191  nndiffz1  32738  fzsplit3  32745  bcm1n  32747  fzone1  32752  suppssnn0  32759  ltesubnnd  32776  wrdt2ind  32904  cshwrnid  32912  chnub  32963  chnso  32965  cycpmfv2  33065  cycpmco2lem6  33082  cycpmco2lem7  33083  cycpmrn  33094  cyc3conja  33108  pnfinf  33134  znfermltl  33312  constrext2chnlem  33733  cos9thpiminplylem1  33765  cos9thpiminplylem2  33766  dya2iocress  34258  dya2iocbrsiga  34259  dya2icobrsiga  34260  dya2icoseg  34261  dya2iocucvr  34268  sxbrsigalem2  34270  ballotlemfc0  34477  ballotlemfcc  34478  ballotlemodife  34482  ballotlemimin  34490  ballotlemsgt1  34495  ballotlemsel1i  34497  ballotlemsi  34499  ballotlemsima  34500  ballotlemrv2  34506  ballotlemfrceq  34513  ballotlemfrcn0  34514  ballotlemirc  34516  fsum2dsub  34591  reprlt  34603  reprgt  34605  breprexplemc  34616  tgoldbachgnn  34643  tgoldbachgt  34647  subfacval3  35182  erdszelem8  35191  erdszelem9  35192  supfz  35722  inffz  35723  dnizeq0  36469  dnizphlfeqhlf  36470  dnibndlem13  36484  knoppndvlem1  36506  knoppndvlem2  36507  knoppndvlem7  36512  knoppndvlem19  36524  knoppndvlem21  36526  ltflcei  37608  leceifl  37609  poimirlem1  37621  poimirlem2  37622  poimirlem6  37626  poimirlem7  37627  poimirlem8  37628  poimirlem15  37635  poimirlem16  37636  poimirlem17  37637  poimirlem19  37639  poimirlem20  37640  poimirlem23  37643  poimirlem24  37644  poimirlem27  37647  poimirlem29  37649  poimirlem31  37651  poimirlem32  37652  mblfinlem2  37658  itg2addnclem2  37672  mettrifi  37757  cntotbnd  37796  fzne2d  41973  aks4d1lem1  42055  aks4d1p1p3  42062  aks4d1p1p2  42063  aks4d1p1p4  42064  aks4d1p1  42069  aks4d1p2  42070  aks4d1p3  42071  aks4d1p5  42073  aks4d1p6  42074  aks4d1p7d1  42075  aks4d1p7  42076  aks4d1p8d3  42079  aks4d1p8  42080  aks4d1p9  42081  posbezout  42093  aks6d1c1  42109  hashscontpow1  42114  hashscontpow  42115  aks6d1c2  42123  aks6d1c5lem1  42129  2ap1caineq  42138  sticksstones6  42144  sticksstones7  42145  sticksstones10  42148  sticksstones12a  42150  sticksstones12  42151  sticksstones22  42161  bcled  42171  bcle2d  42172  aks6d1c7lem1  42173  aks6d1c7lem2  42174  aks6d1c7  42177  aks5lem6  42185  unitscyglem2  42189  unitscyglem4  42191  aks5lem8  42194  sumcubes  42306  frlmvscadiccat  42499  dffltz  42627  lzunuz  42761  lzenom  42763  diophin  42765  irrapxlem1  42815  irrapxlem2  42816  irrapxlem3  42817  irrapxlem4  42818  pellexlem5  42826  pellexlem6  42827  rmspecfund  42902  rmxypos  42940  ltrmynn0  42941  ltrmxnn0  42942  ltrmy  42945  rmyeq0  42946  rmyeq  42947  lermy  42948  rmyabs  42951  jm2.24nn  42952  jm2.17a  42953  jm2.17b  42954  jm2.17c  42955  jm2.24  42956  rmygeid  42957  acongrep  42973  fzmaxdif  42974  acongeq  42976  jm2.22  42988  jm2.23  42989  jm2.26lem3  42994  jm2.27a  42998  jm3.1lem1  43010  jm3.1lem3  43012  expdiophlem1  43014  fzuntd  43449  fzunt1d  43450  fzuntgd  43451  prmunb2  44304  nzprmdif  44312  hashnzfzclim  44315  binomcxplemnn0  44342  uzwo4  45051  ssinc  45085  ssdec  45086  zltlesub  45287  monoords  45299  fzisoeu  45302  fperiodmul  45306  fzdifsuc2  45312  iuneqfzuzlem  45334  uzublem  45429  zxrd  45452  uzinico  45560  uzubioo  45566  fmul01  45581  fmul01lt1lem1  45585  fmul01lt1lem2  45586  climsuselem1  45608  climsuse  45609  sumnnodd  45631  ltmod  45639  limsupresuz  45704  limsupubuzlem  45713  limsupequzlem  45723  limsupmnfuzlem  45727  limsupequzmptlem  45729  limsupre3uzlem  45736  supcnvlimsup  45741  limsup10exlem  45773  liminfresuz  45785  liminfvaluz  45793  limsupvaluz3  45799  ioodvbdlimc1lem2  45933  ioodvbdlimc2lem  45935  dvnmul  45944  dvnprodlem1  45947  dvnprodlem2  45948  iblspltprt  45974  itgspltprt  45980  stoweidlem3  46004  stoweidlem11  46012  stoweidlem20  46021  stoweidlem26  46027  stoweidlem34  46035  stoweidlem59  46060  stirlinglem5  46079  dirkertrigeqlem3  46101  dirkeritg  46103  dirkercncflem1  46104  dirkercncflem2  46105  dirkercncflem4  46107  fourierdlem4  46112  fourierdlem6  46114  fourierdlem7  46115  fourierdlem11  46119  fourierdlem12  46120  fourierdlem15  46123  fourierdlem19  46127  fourierdlem20  46128  fourierdlem25  46133  fourierdlem26  46134  fourierdlem34  46142  fourierdlem35  46143  fourierdlem41  46149  fourierdlem48  46155  fourierdlem49  46156  fourierdlem50  46157  fourierdlem51  46158  fourierdlem54  46161  fourierdlem63  46170  fourierdlem64  46171  fourierdlem65  46172  fourierdlem71  46178  fourierdlem79  46186  fourierdlem89  46196  fourierdlem90  46197  fourierdlem91  46198  fourierdlem102  46209  fourierdlem103  46210  fourierdlem104  46211  fourierdlem114  46221  fouriersw  46232  elaa2lem  46234  etransclem3  46238  etransclem4  46239  etransclem7  46242  etransclem10  46245  etransclem15  46250  etransclem19  46254  etransclem23  46258  etransclem24  46259  etransclem25  46260  etransclem27  46262  etransclem31  46266  etransclem32  46267  etransclem35  46270  etransclem41  46276  etransclem44  46279  etransclem46  46281  etransclem48  46283  iundjiun  46461  caratheodorylem1  46527  smflimsuplem4  46824  smfliminflem  46831  ormklocald  46875  ormkglobd  46876  natglobalincr  46878  2elfz2melfz  47322  elfzelfzlble  47325  fzopredsuc  47327  2ltceilhalf  47332  ceilhalfgt1  47333  ceilhalfnn  47340  submodlt  47354  m1modmmod  47362  difmodm1lt  47363  modmknepk  47366  mod2addne  47368  fsummsndifre  47376  iccpartgt  47431  icceuelpartlem  47439  icceuelpart  47440  iccpartnel  47442  lighneallem2  47610  proththd  47618  dfodd4  47663  oexpnegALTV  47681  nnoALTV  47699  evenltle  47721  fpprwppr  47743  gbowgt5  47766  gboge9  47768  stgoldbwt  47780  sbgoldbst  47782  sbgoldbalt  47785  sgoldbeven3prm  47787  mogoldbb  47789  bgoldbtbndlem1  47809  bgoldbtbndlem2  47810  bgoldbtbndlem3  47811  bgoldbtbnd  47813  bgoldbachlt  47817  tgblthelfgott  47819  tgoldbach  47821  upgrimpthslem2  47912  gpgprismgrusgra  48062  gpgedgvtx1  48066  gpgvtxedg0  48067  gpgvtxedg1  48068  gpg5nbgrvtx13starlem2  48076  gpg3nbgrvtx0  48080  gpg3kgrtriexlem1  48087  gpg3kgrtriexlem4  48090  gpg3kgrtriexlem6  48092  pw2m1lepw2m1  48525  fllogbd  48565  logbpw2m1  48572  fllog2  48573  nnpw2blen  48585  nnolog2flm1  48595  dignn0flhalflem1  48620  dignn0flhalflem2  48621