Theorem zred 12747

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

Syntax hints:   → wi 4   ∈ wcel 2108  ℝcr 11183  ℤcz 12639

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2711

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 847  df-3or 1088  df-3an 1089  df-tru 1540  df-fal 1550  df-ex 1778  df-sb 2065  df-clab 2718  df-cleq 2732  df-clel 2819  df-rab 3444  df-v 3490  df-dif 3979  df-un 3981  df-ss 3993  df-nul 4353  df-if 4549  df-sn 4649  df-pr 4651  df-op 4655  df-uni 4932  df-br 5167  df-iota 6525  df-fv 6581  df-ov 7451  df-neg 11523  df-z 12640

This theorem is referenced by:  zcnd  12748  suprfinzcl  12757  eluzmn  12910  eluzelre  12914  eluzadd  12932  subeluzsub  12940  uzm1  12941  zsupss  13002  suprzcl2  13003  uzwo3  13008  rpnnen1lem3  13044  rpnnen1lem5  13046  zltaddlt1le  13565  fzsplit2  13609  fzdisj  13611  ssfzunsnext  13629  fzpreddisj  13633  fznatpl1  13638  fzp1disj  13643  uzdisj  13657  fzm1  13664  fz0fzdiffz0  13694  elfzmlbm  13695  elfzmlbp  13696  difelfznle  13699  nn0disj  13701  elfzolt3  13726  fzonel  13730  fzospliti  13748  fzodisj  13750  fzouzdisj  13752  fzodisjsn  13754  fzonmapblen  13762  fzoaddel  13769  elincfzoext  13774  reflcl  13847  flge  13856  flwordi  13863  fladdz  13876  2tnp1ge0ge0  13880  flhalf  13881  fldiv4p1lem1div2  13886  fldiv4lem1div2uz2  13887  fldiv4lem1div2  13888  flleceil  13904  fleqceilz  13905  quoremz  13906  uzsup  13914  modmul12d  13976  modaddmodup  13985  modaddmodlo  13986  modfzo0difsn  13994  modsumfzodifsn  13995  addmodlteq  13997  om2uzlti  14001  om2uzf1oi  14004  seqf1olem1  14092  seqf1olem2  14093  bcval4  14356  bcp1nk  14366  bcval5  14367  fzsdom2  14477  seqcoll  14513  seqcoll2  14514  ccatrn  14637  ccatalpha  14641  cshwidxmodr  14852  fzomaxdiflem  15391  fzomaxdif  15392  rexuzre  15401  limsupgre  15527  rlimclim1  15591  isercoll  15716  iseralt  15733  fsumm1  15799  fsum1p  15801  fsum0diaglem  15824  modfsummods  15841  isumsplit  15888  climcndslem1  15897  mertenslem1  15932  ntrivcvgmul  15950  fprodntriv  15990  fprod1p  16016  fprodeq0  16023  fallfacval4  16091  bpoly4  16107  fzo0dvdseq  16371  dvdsmod  16377  oexpneg  16393  mod2eq1n2dvds  16395  ltoddhalfle  16409  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  16593  nn0seqcvgd  16617  lcmgcdlem  16653  nprm  16735  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  16842  vfermltlALT  16849  modprm0  16852  modprmn0modprm0  16854  prm23ge5  16862  pythagtriplem13  16874  pcxcl  16908  pcaddlem  16935  pcadd  16936  pcfac  16946  qexpz  16948  prmunb  16961  1arithlem4  16973  4sqlem5  16989  4sqlem6  16990  4sqlem7  16991  4sqlem10  16994  4sqlem11  17002  4sqlem12  17003  4sqlem15  17006  4sqlem16  17007  4sqlem17  17008  vdwnnlem3  17044  prmgaplem7  17104  cshwshashlem3  17145  subgmulg  19180  mndodconglem  19583  odnncl  19587  odmod  19588  oddvds  19589  dfod2  19606  sylow1lem3  19642  efgsp1  19779  efgredleme  19785  telgsumfzs  20031  zringlpirlem1  21496  zringlpirlem3  21498  fermltlchr  21567  znf1o  21593  zcld  24854  ovoliunlem1  25556  ovoliunlem2  25557  dyadss  25648  dyaddisjlem  25649  dyadmaxlem  25651  dvfsumle  26080  dvfsumleOLD  26081  dvfsumge  26082  dvfsumabs  26083  dvfsumlem1  26086  dvfsumlem3  26089  degltlem1  26131  plyco0  26251  plyeq0lem  26269  plydivex  26357  aannenlem1  26388  efif1olem2  26603  nnlogbexp  26842  logblt  26845  ang180lem1  26870  ang180lem3  26872  wilthlem2  27130  basellem3  27144  basellem4  27145  ppiprm  27212  chtdif  27219  ppidif  27224  chtub  27274  mersenne  27289  bcmono  27339  bcmax  27340  bposlem1  27346  bposlem3  27348  bposlem5  27350  bposlem6  27351  lgsval2lem  27369  lgsvalmod  27378  lgsneg  27383  lgsmod  27385  lgsdilem  27386  lgsdirprm  27393  lgsdilem2  27395  lgsne0  27397  lgssq  27399  lgssq2  27400  lgsqr  27413  lgsdchr  27417  gausslemma2dlem1a  27427  gausslemma2dlem3  27430  gausslemma2dlem5a  27432  gausslemma2dlem6  27434  gausslemma2d  27436  lgseisenlem1  27437  lgseisenlem2  27438  lgseisenlem3  27439  lgseisenlem4  27440  lgsquadlem1  27442  lgsquadlem2  27443  lgsquadlem3  27444  lgsquad3  27449  2lgslem1a2  27452  2lgslem1  27456  2lgslem2  27457  2sqlem3  27482  2sqlem8  27488  2sqblem  27493  2sqmod  27498  chebbnd1lem1  27531  chebbnd1lem2  27532  chebbnd1lem3  27533  dchrmusum2  27556  dchrvmasumlem1  27557  dchrvmasum2lem  27558  dchrvmasum2if  27559  dchrvmasumlem3  27561  dchrvmasumiflem2  27564  dchrisum0lem1  27578  dchrmusumlem  27584  mudivsum  27592  mulogsumlem  27593  mulogsum  27594  mulog2sumlem2  27597  mulog2sumlem3  27598  selberglem1  27607  selberglem2  27608  pntpbnd1  27648  pntlemg  27660  pntlemf  27667  qabvle  27687  padicabv  27692  padicabvcxp  27694  ostth2lem2  27696  axlowdimlem13  28987  axlowdimlem16  28990  pthdlem1  29802  crctcshwlkn0  29854  crctcsh  29857  clwwisshclwwslemlem  30045  eucrctshift  30275  nndiffz1  32791  fzsplit3  32799  bcm1n  32800  fzone1  32805  suppssnn0  32812  ltesubnnd  32826  wrdt2ind  32920  cshwrnid  32928  chnub  32984  chnso  32986  cycpmfv2  33107  cycpmco2lem6  33124  cycpmco2lem7  33125  cycpmrn  33136  cyc3conja  33150  pnfinf  33163  znfermltl  33359  dya2iocress  34239  dya2iocbrsiga  34240  dya2icobrsiga  34241  dya2icoseg  34242  dya2iocucvr  34249  sxbrsigalem2  34251  ballotlemfc0  34457  ballotlemfcc  34458  ballotlemodife  34462  ballotlemimin  34470  ballotlemsgt1  34475  ballotlemsel1i  34477  ballotlemsi  34479  ballotlemsima  34480  ballotlemrv2  34486  ballotlemfrceq  34493  ballotlemfrcn0  34494  ballotlemirc  34496  fsum2dsub  34584  reprlt  34596  reprgt  34598  breprexplemc  34609  tgoldbachgnn  34636  tgoldbachgt  34640  subfacval3  35157  erdszelem8  35166  erdszelem9  35167  supfz  35691  inffz  35692  dnizeq0  36441  dnizphlfeqhlf  36442  dnibndlem13  36456  knoppndvlem1  36478  knoppndvlem2  36479  knoppndvlem7  36484  knoppndvlem19  36496  knoppndvlem21  36498  ltflcei  37568  leceifl  37569  poimirlem1  37581  poimirlem2  37582  poimirlem6  37586  poimirlem7  37587  poimirlem8  37588  poimirlem15  37595  poimirlem16  37596  poimirlem17  37597  poimirlem19  37599  poimirlem20  37600  poimirlem23  37603  poimirlem24  37604  poimirlem27  37607  poimirlem29  37609  poimirlem31  37611  poimirlem32  37612  mblfinlem2  37618  itg2addnclem2  37632  mettrifi  37717  cntotbnd  37756  fzne2d  41937  aks4d1lem1  42019  aks4d1p1p3  42026  aks4d1p1p2  42027  aks4d1p1p4  42028  aks4d1p1  42033  aks4d1p2  42034  aks4d1p3  42035  aks4d1p5  42037  aks4d1p6  42038  aks4d1p7d1  42039  aks4d1p7  42040  aks4d1p8d3  42043  aks4d1p8  42044  aks4d1p9  42045  posbezout  42057  aks6d1c1  42073  hashscontpow1  42078  hashscontpow  42079  aks6d1c2  42087  aks6d1c5lem1  42093  2ap1caineq  42102  sticksstones6  42108  sticksstones7  42109  sticksstones10  42112  sticksstones12a  42114  sticksstones12  42115  sticksstones22  42125  bcled  42135  bcle2d  42136  aks6d1c7lem1  42137  aks6d1c7lem2  42138  aks6d1c7  42141  aks5lem6  42149  unitscyglem2  42153  unitscyglem4  42155  aks5lem8  42158  metakunt7  42168  metakunt12  42173  metakunt15  42176  metakunt16  42177  metakunt22  42183  metakunt28  42189  prodsplit  42197  sumcubes  42301  frlmvscadiccat  42461  dffltz  42589  lzunuz  42724  lzenom  42726  diophin  42728  irrapxlem1  42778  irrapxlem2  42779  irrapxlem3  42780  irrapxlem4  42781  pellexlem5  42789  pellexlem6  42790  rmspecfund  42865  rmxypos  42904  ltrmynn0  42905  ltrmxnn0  42906  ltrmy  42909  rmyeq0  42910  rmyeq  42911  lermy  42912  rmyabs  42915  jm2.24nn  42916  jm2.17a  42917  jm2.17b  42918  jm2.17c  42919  jm2.24  42920  rmygeid  42921  acongrep  42937  fzmaxdif  42938  acongeq  42940  jm2.22  42952  jm2.23  42953  jm2.26lem3  42958  jm2.27a  42962  jm3.1lem1  42974  jm3.1lem3  42976  expdiophlem1  42978  fzuntd  43418  fzunt1d  43419  fzuntgd  43420  prmunb2  44280  nzprmdif  44288  hashnzfzclim  44291  binomcxplemnn0  44318  uzwo4  44955  ssinc  44989  ssdec  44990  zltlesub  45200  monoords  45212  fzisoeu  45215  fperiodmul  45219  fzdifsuc2  45225  iuneqfzuzlem  45249  uzublem  45345  zxrd  45368  uzinico  45478  uzubioo  45485  fmul01  45501  fmul01lt1lem1  45505  fmul01lt1lem2  45506  climsuselem1  45528  climsuse  45529  sumnnodd  45551  ltmod  45559  limsupresuz  45624  limsupubuzlem  45633  limsupequzlem  45643  limsupmnfuzlem  45647  limsupequzmptlem  45649  limsupre3uzlem  45656  supcnvlimsup  45661  limsup10exlem  45693  liminfresuz  45705  liminfvaluz  45713  limsupvaluz3  45719  ioodvbdlimc1lem2  45853  ioodvbdlimc2lem  45855  dvnmul  45864  dvnprodlem1  45867  dvnprodlem2  45868  iblspltprt  45894  itgspltprt  45900  stoweidlem3  45924  stoweidlem11  45932  stoweidlem20  45941  stoweidlem26  45947  stoweidlem34  45955  stoweidlem59  45980  stirlinglem5  45999  dirkertrigeqlem3  46021  dirkeritg  46023  dirkercncflem1  46024  dirkercncflem2  46025  dirkercncflem4  46027  fourierdlem4  46032  fourierdlem6  46034  fourierdlem7  46035  fourierdlem11  46039  fourierdlem12  46040  fourierdlem15  46043  fourierdlem19  46047  fourierdlem20  46048  fourierdlem25  46053  fourierdlem26  46054  fourierdlem34  46062  fourierdlem35  46063  fourierdlem41  46069  fourierdlem48  46075  fourierdlem49  46076  fourierdlem50  46077  fourierdlem51  46078  fourierdlem54  46081  fourierdlem63  46090  fourierdlem64  46091  fourierdlem65  46092  fourierdlem71  46098  fourierdlem79  46106  fourierdlem89  46116  fourierdlem90  46117  fourierdlem91  46118  fourierdlem102  46129  fourierdlem103  46130  fourierdlem104  46131  fourierdlem114  46141  fouriersw  46152  elaa2lem  46154  etransclem3  46158  etransclem4  46159  etransclem7  46162  etransclem10  46165  etransclem15  46170  etransclem19  46174  etransclem23  46178  etransclem24  46179  etransclem25  46180  etransclem27  46182  etransclem31  46186  etransclem32  46187  etransclem35  46190  etransclem41  46196  etransclem44  46199  etransclem46  46201  etransclem48  46203  iundjiun  46381  caratheodorylem1  46447  smflimsuplem4  46744  smfliminflem  46751  natglobalincr  46796  2elfz2melfz  47233  elfzelfzlble  47236  fzopredsuc  47238  fsummsndifre  47246  iccpartgt  47301  icceuelpartlem  47309  icceuelpart  47310  iccpartnel  47312  lighneallem2  47480  proththd  47488  dfodd4  47533  oexpnegALTV  47551  nnoALTV  47569  evenltle  47591  fpprwppr  47613  gbowgt5  47636  gboge9  47638  stgoldbwt  47650  sbgoldbst  47652  sbgoldbalt  47655  sgoldbeven3prm  47657  mogoldbb  47659  bgoldbtbndlem1  47679  bgoldbtbndlem2  47680  bgoldbtbndlem3  47681  bgoldbtbnd  47683  bgoldbachlt  47687  tgblthelfgott  47689  tgoldbach  47691  pw2m1lepw2m1  48249  m1modmmod  48255  difmodm1lt  48256  fllogbd  48294  logbpw2m1  48301  fllog2  48302  nnpw2blen  48314  nnolog2flm1  48324  dignn0flhalflem1  48349  dignn0flhalflem2  48350