Theorem zred 12631

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

Syntax hints:   → wi 4   ∈ wcel 2119  ℝcr 11035  ℤcz 12522

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-ext 2712

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 854  df-3or 1093  df-3an 1094  df-tru 1550  df-fal 1560  df-ex 1787  df-sb 2074  df-clab 2719  df-cleq 2732  df-clel 2815  df-rab 3393  df-v 3434  df-dif 3893  df-un 3895  df-ss 3907  df-nul 4269  df-if 4462  df-sn 4563  df-pr 4565  df-op 4569  df-uni 4846  df-br 5080  df-iota 6448  df-fv 6500  df-ov 7366  df-neg 11378  df-z 12523

This theorem is referenced by:  zcnd  12632  suprfinzcl  12641  eluzmn  12793  eluzelre  12797  eluzadd  12815  subeluzsub  12819  uzm1  12820  zsupss  12885  suprzcl2  12886  uzwo3  12891  rpnnen1lem3  12927  rpnnen1lem5  12929  zltaddlt1le  13456  fzsplit2  13501  fzdisj  13503  ssfzunsnext  13521  fzpreddisj  13525  fznatpl1  13530  fzp1disj  13535  uzdisj  13549  fzdif1  13557  fzm1  13559  fz0fzdiffz0  13589  elfzmlbm  13590  elfzmlbp  13591  difelfznle  13594  nn0disj  13596  elfzolt3  13622  fzonel  13626  fzospliti  13644  fzodisj  13646  fzouzdisj  13648  fzodisjsn  13650  elfzo0subge1  13658  elfzo0suble  13659  fzonmapblen  13661  fzoaddel  13670  elincfzoext  13676  fzone1  13737  reflcl  13753  flge  13762  flwordi  13769  fladdz  13782  2tnp1ge0ge0  13786  flhalf  13787  fldiv4p1lem1div2  13792  fldiv4lem1div2uz2  13793  fldiv4lem1div2  13794  flleceil  13810  fleqceilz  13811  quoremz  13812  uzsup  13820  modaddid  13867  modmul12d  13885  modaddmodup  13894  modaddmodlo  13895  modfzo0difsn  13903  modsumfzodifsn  13904  addmodlteq  13906  om2uzlti  13910  om2uzf1oi  13913  seqf1olem1  14001  seqf1olem2  14002  bcval4  14267  bcp1nk  14277  bcval5  14278  fzsdom2  14388  seqcoll  14424  seqcoll2  14425  ccatrn  14550  ccatalpha  14554  cshwidxmodr  14764  fzomaxdiflem  15303  fzomaxdif  15304  rexuzre  15313  limsupgre  15441  rlimclim1  15505  isercoll  15628  iseralt  15645  fsumm1  15711  fsum1p  15713  fsum0diaglem  15736  modfsummods  15754  isumsplit  15803  climcndslem1  15812  mertenslem1  15847  ntrivcvgmul  15865  fprodntriv  15905  fprod1p  15931  fprodeq0  15938  fallfacval4  16006  bpoly4  16022  fzo0dvdseq  16290  dvdsmod  16296  oexpneg  16312  mod2eq1n2dvds  16314  ltoddhalfle  16328  flodddiv4t2lthalf  16385  bitsp1  16398  bitsfzolem  16401  bitsfzo  16402  bitsmod  16403  bitscmp  16405  bitsinv1lem  16408  sadaddlem  16433  bitsres  16440  bitsuz  16441  smumul  16460  gcd0id  16486  gcdneg  16489  dfgcd2  16513  nn0seqcvgd  16537  lcmgcdlem  16573  nprm  16655  prmdvdsfz  16673  isprm5  16675  isprm7  16676  coprm  16679  prmexpb  16687  prmfac1  16688  hashdvds  16743  crth  16746  eulerthlem2  16750  fermltl  16752  prmdiv  16753  prmdiveq  16754  hashgcdlem  16756  odzdvds  16764  vfermltlALT  16771  modprm0  16774  modprmn0modprm0  16776  prm23ge5  16784  pythagtriplem13  16796  pcxcl  16830  pcaddlem  16857  pcadd  16858  pcfac  16868  qexpz  16870  prmunb  16883  1arithlem4  16895  4sqlem5  16911  4sqlem6  16912  4sqlem7  16913  4sqlem10  16916  4sqlem11  16924  4sqlem12  16925  4sqlem15  16928  4sqlem16  16929  4sqlem17  16930  vdwnnlem3  16966  prmgaplem7  17026  cshwshashlem3  17066  chnub  18586  chnso  18588  chnccat  18590  chnpof1  18594  subgmulg  19114  mndodconglem  19514  odnncl  19518  odmod  19519  oddvds  19520  dfod2  19537  sylow1lem3  19573  efgsp1  19710  efgredleme  19716  telgsumfzs  19962  zringlpirlem1  21444  zringlpirlem3  21446  fermltlchr  21511  znf1o  21533  zcld  24804  ovoliunlem1  25494  ovoliunlem2  25495  dyadss  25586  dyaddisjlem  25587  dyadmaxlem  25589  dvfsumle  26013  dvfsumge  26014  dvfsumabs  26015  dvfsumlem1  26018  dvfsumlem3  26020  degltlem1  26062  plyco0  26182  plyeq0lem  26200  plydivex  26288  aannenlem1  26319  efif1olem2  26532  nnlogbexp  26770  logblt  26773  ang180lem1  26798  ang180lem3  26800  wilthlem2  27057  basellem3  27071  basellem4  27072  ppiprm  27139  chtdif  27146  ppidif  27151  chtub  27200  mersenne  27215  bcmono  27265  bcmax  27266  bposlem1  27272  bposlem3  27274  bposlem5  27276  bposlem6  27277  lgsval2lem  27295  lgsvalmod  27304  lgsneg  27309  lgsmod  27311  lgsdilem  27312  lgsdirprm  27319  lgsdilem2  27321  lgsne0  27323  lgssq  27325  lgssq2  27326  lgsqr  27339  lgsdchr  27343  gausslemma2dlem1a  27353  gausslemma2dlem3  27356  gausslemma2dlem5a  27358  gausslemma2dlem6  27360  gausslemma2d  27362  lgseisenlem1  27363  lgseisenlem2  27364  lgseisenlem3  27365  lgseisenlem4  27366  lgsquadlem1  27368  lgsquadlem2  27369  lgsquadlem3  27370  lgsquad3  27375  2lgslem1a2  27378  2lgslem1  27382  2lgslem2  27383  2sqlem3  27408  2sqlem8  27414  2sqblem  27419  2sqmod  27424  chebbnd1lem1  27457  chebbnd1lem2  27458  chebbnd1lem3  27459  dchrmusum2  27482  dchrvmasumlem1  27483  dchrvmasum2lem  27484  dchrvmasum2if  27485  dchrvmasumlem3  27487  dchrvmasumiflem2  27490  dchrisum0lem1  27504  dchrmusumlem  27510  mudivsum  27518  mulogsumlem  27519  mulogsum  27520  mulog2sumlem2  27523  mulog2sumlem3  27524  selberglem1  27533  selberglem2  27534  pntpbnd1  27574  pntlemg  27586  pntlemf  27593  qabvle  27613  padicabv  27618  padicabvcxp  27620  ostth2lem2  27622  axlowdimlem13  29048  axlowdimlem16  29051  pthdlem1  29859  crctcshwlkn0  29914  crctcsh  29917  clwwisshclwwslemlem  30108  eucrctshift  30338  nndiffz1  32885  fzsplit3  32892  bcm1n  32894  suppssnn0  32904  ltesubnnd  32922  wrdt2ind  33039  cshwrnid  33047  cycpmfv2  33202  cycpmco2lem6  33219  cycpmco2lem7  33220  cycpmrn  33231  cyc3conja  33245  pnfinf  33271  znfermltl  33456  constrext2chnlem  33941  cos9thpiminplylem1  33973  cos9thpiminplylem2  33974  dya2iocress  34465  dya2iocbrsiga  34466  dya2icobrsiga  34467  dya2icoseg  34468  dya2iocucvr  34475  sxbrsigalem2  34477  ballotlemfc0  34684  ballotlemfcc  34685  ballotlemodife  34689  ballotlemimin  34697  ballotlemsgt1  34702  ballotlemsel1i  34704  ballotlemsi  34706  ballotlemsima  34707  ballotlemrv2  34713  ballotlemfrceq  34720  ballotlemfrcn0  34721  ballotlemirc  34723  fsum2dsub  34798  reprlt  34810  reprgt  34812  breprexplemc  34823  tgoldbachgnn  34850  tgoldbachgt  34854  subfacval3  35424  erdszelem8  35433  erdszelem9  35434  supfz  35964  inffz  35965  dnizeq0  36788  dnizphlfeqhlf  36789  dnibndlem13  36803  knoppndvlem1  36825  knoppndvlem2  36826  knoppndvlem7  36831  knoppndvlem19  36843  knoppndvlem21  36845  ltflcei  37982  leceifl  37983  poimirlem1  37995  poimirlem2  37996  poimirlem6  38000  poimirlem7  38001  poimirlem8  38002  poimirlem15  38009  poimirlem16  38010  poimirlem17  38011  poimirlem19  38013  poimirlem20  38014  poimirlem23  38017  poimirlem24  38018  poimirlem27  38021  poimirlem29  38023  poimirlem31  38025  poimirlem32  38026  mblfinlem2  38032  itg2addnclem2  38046  mettrifi  38131  cntotbnd  38170  fzne2d  42472  aks4d1lem1  42554  aks4d1p1p3  42561  aks4d1p1p2  42562  aks4d1p1p4  42563  aks4d1p1  42568  aks4d1p2  42569  aks4d1p3  42570  aks4d1p5  42572  aks4d1p6  42573  aks4d1p7d1  42574  aks4d1p7  42575  aks4d1p8d3  42578  aks4d1p8  42579  aks4d1p9  42580  posbezout  42592  aks6d1c1  42608  hashscontpow1  42613  hashscontpow  42614  aks6d1c2  42622  aks6d1c5lem1  42628  2ap1caineq  42637  sticksstones6  42643  sticksstones7  42644  sticksstones10  42647  sticksstones12a  42649  sticksstones12  42650  sticksstones22  42660  bcled  42670  bcle2d  42671  aks6d1c7lem1  42672  aks6d1c7lem2  42673  aks6d1c7  42676  aks5lem6  42684  unitscyglem2  42688  unitscyglem4  42690  aks5lem8  42693  sumcubes  42797  frlmvscadiccat  43003  dffltz  43091  lzunuz  43224  lzenom  43226  diophin  43228  irrapxlem1  43274  irrapxlem2  43275  irrapxlem3  43276  irrapxlem4  43277  pellexlem5  43285  pellexlem6  43286  rmspecfund  43361  rmxypos  43399  ltrmynn0  43400  ltrmxnn0  43401  ltrmy  43404  rmyeq0  43405  rmyeq  43406  lermy  43407  rmyabs  43410  jm2.24nn  43411  jm2.17a  43412  jm2.17b  43413  jm2.17c  43414  jm2.24  43415  rmygeid  43416  acongrep  43432  fzmaxdif  43433  acongeq  43435  jm2.22  43447  jm2.23  43448  jm2.26lem3  43453  jm2.27a  43457  jm3.1lem1  43469  jm3.1lem3  43471  expdiophlem1  43473  fzuntd  43907  fzunt1d  43908  fzuntgd  43909  prmunb2  44762  nzprmdif  44770  hashnzfzclim  44773  binomcxplemnn0  44800  uzwo4  45508  ssinc  45541  ssdec  45542  zltlesub  45740  monoords  45752  fzisoeu  45755  fperiodmul  45759  fzdifsuc2  45765  iuneqfzuzlem  45786  uzublem  45880  zxrd  45903  uzinico  46011  uzubioo  46017  fmul01  46032  fmul01lt1lem1  46036  fmul01lt1lem2  46037  climsuselem1  46059  climsuse  46060  sumnnodd  46082  ltmod  46088  limsupresuz  46153  limsupubuzlem  46162  limsupequzlem  46172  limsupmnfuzlem  46176  limsupequzmptlem  46178  limsupre3uzlem  46185  supcnvlimsup  46190  limsup10exlem  46222  liminfresuz  46234  liminfvaluz  46242  limsupvaluz3  46248  ioodvbdlimc1lem2  46382  ioodvbdlimc2lem  46384  dvnmul  46393  dvnprodlem1  46396  dvnprodlem2  46397  iblspltprt  46423  itgspltprt  46429  stoweidlem3  46453  stoweidlem11  46461  stoweidlem20  46470  stoweidlem26  46476  stoweidlem34  46484  stoweidlem59  46509  stirlinglem5  46528  dirkertrigeqlem3  46550  dirkeritg  46552  dirkercncflem1  46553  dirkercncflem2  46554  dirkercncflem4  46556  fourierdlem4  46561  fourierdlem6  46563  fourierdlem7  46564  fourierdlem11  46568  fourierdlem12  46569  fourierdlem15  46572  fourierdlem19  46576  fourierdlem20  46577  fourierdlem25  46582  fourierdlem26  46583  fourierdlem34  46591  fourierdlem35  46592  fourierdlem41  46598  fourierdlem48  46604  fourierdlem49  46605  fourierdlem50  46606  fourierdlem51  46607  fourierdlem54  46610  fourierdlem63  46619  fourierdlem64  46620  fourierdlem65  46621  fourierdlem71  46627  fourierdlem79  46635  fourierdlem89  46645  fourierdlem90  46646  fourierdlem91  46647  fourierdlem102  46658  fourierdlem103  46659  fourierdlem104  46660  fourierdlem114  46670  fouriersw  46681  elaa2lem  46683  etransclem3  46687  etransclem4  46688  etransclem7  46691  etransclem10  46694  etransclem15  46699  etransclem19  46703  etransclem23  46707  etransclem24  46708  etransclem25  46709  etransclem27  46711  etransclem31  46715  etransclem32  46716  etransclem35  46719  etransclem41  46725  etransclem44  46728  etransclem46  46730  etransclem48  46732  iundjiun  46910  caratheodorylem1  46976  hoicvr  46998  smflimsuplem4  47273  smfliminflem  47280  ormklocald  47326  ormkglobd  47327  natglobalincr  47329  chnerlem3  47336  2elfz2melfz  47788  elfzelfzlble  47791  fzopredsuc  47794  nnmul2  47800  2ltceilhalf  47802  ceilhalfgt1  47803  ceilhalfnn  47810  submodlt  47826  m1modmmod  47834  difmodm1lt  47835  modmknepk  47838  mod2addne  47840  2timesltsq  47848  2timesltsqm1  47849  fsummsndifre  47850  iccpartgt  47909  icceuelpartlem  47917  icceuelpart  47918  iccpartnel  47920  nprmmul2  48010  nprmmul3  48011  lighneallem2  48091  proththd  48099  nprmdvdsfacm1lem4  48108  dfodd4  48157  oexpnegALTV  48175  nnoALTV  48193  evenltle  48215  fpprwppr  48237  gbowgt5  48260  gboge9  48262  stgoldbwt  48274  sbgoldbst  48276  sbgoldbalt  48279  sgoldbeven3prm  48281  mogoldbb  48283  bgoldbtbndlem1  48303  bgoldbtbndlem2  48304  bgoldbtbndlem3  48305  bgoldbtbnd  48307  bgoldbachlt  48311  tgblthelfgott  48313  tgoldbach  48315  upgrimpthslem2  48406  gpgprismgrusgra  48556  gpgedgvtx1  48560  gpgvtxedg0  48561  gpgvtxedg1  48562  gpg5nbgrvtx13starlem2  48570  gpg3nbgrvtx0  48574  gpg3kgrtriexlem1  48581  gpg3kgrtriexlem4  48584  gpg3kgrtriexlem6  48586  pw2m1lepw2m1  49018  fllogbd  49058  logbpw2m1  49065  fllog2  49066  nnpw2blen  49078  nnolog2flm1  49088  dignn0flhalflem1  49113  dignn0flhalflem2  49114