Theorem zred 12608

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

Syntax hints:   → wi 4   ∈ wcel 2114  ℝcr 11037  ℤcz 12500

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3or 1088  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-rab 3402  df-v 3444  df-dif 3906  df-un 3908  df-ss 3920  df-nul 4288  df-if 4482  df-sn 4583  df-pr 4585  df-op 4589  df-uni 4866  df-br 5101  df-iota 6456  df-fv 6508  df-ov 7371  df-neg 11379  df-z 12501

This theorem is referenced by:  zcnd  12609  suprfinzcl  12618  eluzmn  12770  eluzelre  12774  eluzadd  12792  subeluzsub  12796  uzm1  12797  zsupss  12862  suprzcl2  12863  uzwo3  12868  rpnnen1lem3  12904  rpnnen1lem5  12906  zltaddlt1le  13433  fzsplit2  13477  fzdisj  13479  ssfzunsnext  13497  fzpreddisj  13501  fznatpl1  13506  fzp1disj  13511  uzdisj  13525  fzdif1  13533  fzm1  13535  fz0fzdiffz0  13565  elfzmlbm  13566  elfzmlbp  13567  difelfznle  13570  nn0disj  13572  elfzolt3  13597  fzonel  13601  fzospliti  13619  fzodisj  13621  fzouzdisj  13623  fzodisjsn  13625  elfzo0subge1  13633  elfzo0suble  13634  fzonmapblen  13636  fzoaddel  13645  elincfzoext  13651  fzone1  13712  reflcl  13728  flge  13737  flwordi  13744  fladdz  13757  2tnp1ge0ge0  13761  flhalf  13762  fldiv4p1lem1div2  13767  fldiv4lem1div2uz2  13768  fldiv4lem1div2  13769  flleceil  13785  fleqceilz  13786  quoremz  13787  uzsup  13795  modaddid  13842  modmul12d  13860  modaddmodup  13869  modaddmodlo  13870  modfzo0difsn  13878  modsumfzodifsn  13879  addmodlteq  13881  om2uzlti  13885  om2uzf1oi  13888  seqf1olem1  13976  seqf1olem2  13977  bcval4  14242  bcp1nk  14252  bcval5  14253  fzsdom2  14363  seqcoll  14399  seqcoll2  14400  ccatrn  14525  ccatalpha  14529  cshwidxmodr  14739  fzomaxdiflem  15278  fzomaxdif  15279  rexuzre  15288  limsupgre  15416  rlimclim1  15480  isercoll  15603  iseralt  15620  fsumm1  15686  fsum1p  15688  fsum0diaglem  15711  modfsummods  15728  isumsplit  15775  climcndslem1  15784  mertenslem1  15819  ntrivcvgmul  15837  fprodntriv  15877  fprod1p  15903  fprodeq0  15910  fallfacval4  15978  bpoly4  15994  fzo0dvdseq  16262  dvdsmod  16268  oexpneg  16284  mod2eq1n2dvds  16286  ltoddhalfle  16300  flodddiv4t2lthalf  16357  bitsp1  16370  bitsfzolem  16373  bitsfzo  16374  bitsmod  16375  bitscmp  16377  bitsinv1lem  16380  sadaddlem  16405  bitsres  16412  bitsuz  16413  smumul  16432  gcd0id  16458  gcdneg  16461  dfgcd2  16485  nn0seqcvgd  16509  lcmgcdlem  16545  nprm  16627  prmdvdsfz  16644  isprm5  16646  isprm7  16647  coprm  16650  prmexpb  16658  prmfac1  16659  hashdvds  16714  crth  16717  eulerthlem2  16721  fermltl  16723  prmdiv  16724  prmdiveq  16725  hashgcdlem  16727  odzdvds  16735  vfermltlALT  16742  modprm0  16745  modprmn0modprm0  16747  prm23ge5  16755  pythagtriplem13  16767  pcxcl  16801  pcaddlem  16828  pcadd  16829  pcfac  16839  qexpz  16841  prmunb  16854  1arithlem4  16866  4sqlem5  16882  4sqlem6  16883  4sqlem7  16884  4sqlem10  16887  4sqlem11  16895  4sqlem12  16896  4sqlem15  16899  4sqlem16  16900  4sqlem17  16901  vdwnnlem3  16937  prmgaplem7  16997  cshwshashlem3  17037  chnub  18557  chnso  18559  chnccat  18561  chnpof1  18565  subgmulg  19082  mndodconglem  19482  odnncl  19486  odmod  19487  oddvds  19488  dfod2  19505  sylow1lem3  19541  efgsp1  19678  efgredleme  19684  telgsumfzs  19930  zringlpirlem1  21429  zringlpirlem3  21431  fermltlchr  21496  znf1o  21518  zcld  24770  ovoliunlem1  25471  ovoliunlem2  25472  dyadss  25563  dyaddisjlem  25564  dyadmaxlem  25566  dvfsumle  25994  dvfsumleOLD  25995  dvfsumge  25996  dvfsumabs  25997  dvfsumlem1  26000  dvfsumlem3  26003  degltlem1  26045  plyco0  26165  plyeq0lem  26183  plydivex  26273  aannenlem1  26304  efif1olem2  26520  nnlogbexp  26759  logblt  26762  ang180lem1  26787  ang180lem3  26789  wilthlem2  27047  basellem3  27061  basellem4  27062  ppiprm  27129  chtdif  27136  ppidif  27141  chtub  27191  mersenne  27206  bcmono  27256  bcmax  27257  bposlem1  27263  bposlem3  27265  bposlem5  27267  bposlem6  27268  lgsval2lem  27286  lgsvalmod  27295  lgsneg  27300  lgsmod  27302  lgsdilem  27303  lgsdirprm  27310  lgsdilem2  27312  lgsne0  27314  lgssq  27316  lgssq2  27317  lgsqr  27330  lgsdchr  27334  gausslemma2dlem1a  27344  gausslemma2dlem3  27347  gausslemma2dlem5a  27349  gausslemma2dlem6  27351  gausslemma2d  27353  lgseisenlem1  27354  lgseisenlem2  27355  lgseisenlem3  27356  lgseisenlem4  27357  lgsquadlem1  27359  lgsquadlem2  27360  lgsquadlem3  27361  lgsquad3  27366  2lgslem1a2  27369  2lgslem1  27373  2lgslem2  27374  2sqlem3  27399  2sqlem8  27405  2sqblem  27410  2sqmod  27415  chebbnd1lem1  27448  chebbnd1lem2  27449  chebbnd1lem3  27450  dchrmusum2  27473  dchrvmasumlem1  27474  dchrvmasum2lem  27475  dchrvmasum2if  27476  dchrvmasumlem3  27478  dchrvmasumiflem2  27481  dchrisum0lem1  27495  dchrmusumlem  27501  mudivsum  27509  mulogsumlem  27510  mulogsum  27511  mulog2sumlem2  27514  mulog2sumlem3  27515  selberglem1  27524  selberglem2  27525  pntpbnd1  27565  pntlemg  27577  pntlemf  27584  qabvle  27604  padicabv  27609  padicabvcxp  27611  ostth2lem2  27613  axlowdimlem13  29039  axlowdimlem16  29042  pthdlem1  29851  crctcshwlkn0  29906  crctcsh  29909  clwwisshclwwslemlem  30100  eucrctshift  30330  nndiffz1  32876  fzsplit3  32883  bcm1n  32885  suppssnn0  32895  ltesubnnd  32913  wrdt2ind  33045  cshwrnid  33053  cycpmfv2  33207  cycpmco2lem6  33224  cycpmco2lem7  33225  cycpmrn  33236  cyc3conja  33250  pnfinf  33276  znfermltl  33458  constrext2chnlem  33927  cos9thpiminplylem1  33959  cos9thpiminplylem2  33960  dya2iocress  34451  dya2iocbrsiga  34452  dya2icobrsiga  34453  dya2icoseg  34454  dya2iocucvr  34461  sxbrsigalem2  34463  ballotlemfc0  34670  ballotlemfcc  34671  ballotlemodife  34675  ballotlemimin  34683  ballotlemsgt1  34688  ballotlemsel1i  34690  ballotlemsi  34692  ballotlemsima  34693  ballotlemrv2  34699  ballotlemfrceq  34706  ballotlemfrcn0  34707  ballotlemirc  34709  fsum2dsub  34784  reprlt  34796  reprgt  34798  breprexplemc  34809  tgoldbachgnn  34836  tgoldbachgt  34840  subfacval3  35402  erdszelem8  35411  erdszelem9  35412  supfz  35942  inffz  35943  dnizeq0  36694  dnizphlfeqhlf  36695  dnibndlem13  36709  knoppndvlem1  36731  knoppndvlem2  36732  knoppndvlem7  36737  knoppndvlem19  36749  knoppndvlem21  36751  ltflcei  37856  leceifl  37857  poimirlem1  37869  poimirlem2  37870  poimirlem6  37874  poimirlem7  37875  poimirlem8  37876  poimirlem15  37883  poimirlem16  37884  poimirlem17  37885  poimirlem19  37887  poimirlem20  37888  poimirlem23  37891  poimirlem24  37892  poimirlem27  37895  poimirlem29  37897  poimirlem31  37899  poimirlem32  37900  mblfinlem2  37906  itg2addnclem2  37920  mettrifi  38005  cntotbnd  38044  fzne2d  42347  aks4d1lem1  42429  aks4d1p1p3  42436  aks4d1p1p2  42437  aks4d1p1p4  42438  aks4d1p1  42443  aks4d1p2  42444  aks4d1p3  42445  aks4d1p5  42447  aks4d1p6  42448  aks4d1p7d1  42449  aks4d1p7  42450  aks4d1p8d3  42453  aks4d1p8  42454  aks4d1p9  42455  posbezout  42467  aks6d1c1  42483  hashscontpow1  42488  hashscontpow  42489  aks6d1c2  42497  aks6d1c5lem1  42503  2ap1caineq  42512  sticksstones6  42518  sticksstones7  42519  sticksstones10  42522  sticksstones12a  42524  sticksstones12  42525  sticksstones22  42535  bcled  42545  bcle2d  42546  aks6d1c7lem1  42547  aks6d1c7lem2  42548  aks6d1c7  42551  aks5lem6  42559  unitscyglem2  42563  unitscyglem4  42565  aks5lem8  42568  sumcubes  42680  frlmvscadiccat  42873  dffltz  42989  lzunuz  43122  lzenom  43124  diophin  43126  irrapxlem1  43176  irrapxlem2  43177  irrapxlem3  43178  irrapxlem4  43179  pellexlem5  43187  pellexlem6  43188  rmspecfund  43263  rmxypos  43301  ltrmynn0  43302  ltrmxnn0  43303  ltrmy  43306  rmyeq0  43307  rmyeq  43308  lermy  43309  rmyabs  43312  jm2.24nn  43313  jm2.17a  43314  jm2.17b  43315  jm2.17c  43316  jm2.24  43317  rmygeid  43318  acongrep  43334  fzmaxdif  43335  acongeq  43337  jm2.22  43349  jm2.23  43350  jm2.26lem3  43355  jm2.27a  43359  jm3.1lem1  43371  jm3.1lem3  43373  expdiophlem1  43375  fzuntd  43809  fzunt1d  43810  fzuntgd  43811  prmunb2  44664  nzprmdif  44672  hashnzfzclim  44675  binomcxplemnn0  44702  uzwo4  45410  ssinc  45443  ssdec  45444  zltlesub  45644  monoords  45656  fzisoeu  45659  fperiodmul  45663  fzdifsuc2  45669  iuneqfzuzlem  45690  uzublem  45785  zxrd  45808  uzinico  45916  uzubioo  45922  fmul01  45937  fmul01lt1lem1  45941  fmul01lt1lem2  45942  climsuselem1  45964  climsuse  45965  sumnnodd  45987  ltmod  45993  limsupresuz  46058  limsupubuzlem  46067  limsupequzlem  46077  limsupmnfuzlem  46081  limsupequzmptlem  46083  limsupre3uzlem  46090  supcnvlimsup  46095  limsup10exlem  46127  liminfresuz  46139  liminfvaluz  46147  limsupvaluz3  46153  ioodvbdlimc1lem2  46287  ioodvbdlimc2lem  46289  dvnmul  46298  dvnprodlem1  46301  dvnprodlem2  46302  iblspltprt  46328  itgspltprt  46334  stoweidlem3  46358  stoweidlem11  46366  stoweidlem20  46375  stoweidlem26  46381  stoweidlem34  46389  stoweidlem59  46414  stirlinglem5  46433  dirkertrigeqlem3  46455  dirkeritg  46457  dirkercncflem1  46458  dirkercncflem2  46459  dirkercncflem4  46461  fourierdlem4  46466  fourierdlem6  46468  fourierdlem7  46469  fourierdlem11  46473  fourierdlem12  46474  fourierdlem15  46477  fourierdlem19  46481  fourierdlem20  46482  fourierdlem25  46487  fourierdlem26  46488  fourierdlem34  46496  fourierdlem35  46497  fourierdlem41  46503  fourierdlem48  46509  fourierdlem49  46510  fourierdlem50  46511  fourierdlem51  46512  fourierdlem54  46515  fourierdlem63  46524  fourierdlem64  46525  fourierdlem65  46526  fourierdlem71  46532  fourierdlem79  46540  fourierdlem89  46550  fourierdlem90  46551  fourierdlem91  46552  fourierdlem102  46563  fourierdlem103  46564  fourierdlem104  46565  fourierdlem114  46575  fouriersw  46586  elaa2lem  46588  etransclem3  46592  etransclem4  46593  etransclem7  46596  etransclem10  46599  etransclem15  46604  etransclem19  46608  etransclem23  46612  etransclem24  46613  etransclem25  46614  etransclem27  46616  etransclem31  46620  etransclem32  46621  etransclem35  46624  etransclem41  46630  etransclem44  46633  etransclem46  46635  etransclem48  46637  iundjiun  46815  caratheodorylem1  46881  smflimsuplem4  47178  smfliminflem  47185  ormklocald  47229  ormkglobd  47230  natglobalincr  47232  chnerlem3  47239  2elfz2melfz  47675  elfzelfzlble  47678  fzopredsuc  47680  2ltceilhalf  47685  ceilhalfgt1  47686  ceilhalfnn  47693  submodlt  47707  m1modmmod  47715  difmodm1lt  47716  modmknepk  47719  mod2addne  47721  fsummsndifre  47729  iccpartgt  47784  icceuelpartlem  47792  icceuelpart  47793  iccpartnel  47795  lighneallem2  47963  proththd  47971  dfodd4  48016  oexpnegALTV  48034  nnoALTV  48052  evenltle  48074  fpprwppr  48096  gbowgt5  48119  gboge9  48121  stgoldbwt  48133  sbgoldbst  48135  sbgoldbalt  48138  sgoldbeven3prm  48140  mogoldbb  48142  bgoldbtbndlem1  48162  bgoldbtbndlem2  48163  bgoldbtbndlem3  48164  bgoldbtbnd  48166  bgoldbachlt  48170  tgblthelfgott  48172  tgoldbach  48174  upgrimpthslem2  48265  gpgprismgrusgra  48415  gpgedgvtx1  48419  gpgvtxedg0  48420  gpgvtxedg1  48421  gpg5nbgrvtx13starlem2  48429  gpg3nbgrvtx0  48433  gpg3kgrtriexlem1  48440  gpg3kgrtriexlem4  48443  gpg3kgrtriexlem6  48445  pw2m1lepw2m1  48877  fllogbd  48917  logbpw2m1  48924  fllog2  48925  nnpw2blen  48937  nnolog2flm1  48947  dignn0flhalflem1  48972  dignn0flhalflem2  48973