Theorem zred 12706

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

Syntax hints:   → wi 4   ∈ wcel 2107  ℝcr 11137  ℤcz 12597

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1794  ax-4 1808  ax-5 1909  ax-6 1966  ax-7 2006  ax-8 2109  ax-9 2117  ax-ext 2706

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1542  df-fal 1552  df-ex 1779  df-sb 2064  df-clab 2713  df-cleq 2726  df-clel 2808  df-rab 3421  df-v 3466  df-dif 3936  df-un 3938  df-ss 3950  df-nul 4316  df-if 4508  df-sn 4609  df-pr 4611  df-op 4615  df-uni 4890  df-br 5126  df-iota 6495  df-fv 6550  df-ov 7417  df-neg 11478  df-z 12598

This theorem is referenced by:  zcnd  12707  suprfinzcl  12716  eluzmn  12868  eluzelre  12872  eluzadd  12890  subeluzsub  12898  uzm1  12899  zsupss  12962  suprzcl2  12963  uzwo3  12968  rpnnen1lem3  13004  rpnnen1lem5  13006  zltaddlt1le  13528  fzsplit2  13572  fzdisj  13574  ssfzunsnext  13592  fzpreddisj  13596  fznatpl1  13601  fzp1disj  13606  uzdisj  13620  fzdif1  13628  fzm1  13630  fz0fzdiffz0  13660  elfzmlbm  13661  elfzmlbp  13662  difelfznle  13665  nn0disj  13667  elfzolt3  13692  fzonel  13696  fzospliti  13714  fzodisj  13716  fzouzdisj  13718  fzodisjsn  13720  elfzo0subge1  13728  elfzo0suble  13729  fzonmapblen  13731  fzoaddel  13739  elincfzoext  13745  reflcl  13819  flge  13828  flwordi  13835  fladdz  13848  2tnp1ge0ge0  13852  flhalf  13853  fldiv4p1lem1div2  13858  fldiv4lem1div2uz2  13859  fldiv4lem1div2  13860  flleceil  13876  fleqceilz  13877  quoremz  13878  uzsup  13886  modmul12d  13949  modaddmodup  13958  modaddmodlo  13959  modfzo0difsn  13967  modsumfzodifsn  13968  addmodlteq  13970  om2uzlti  13974  om2uzf1oi  13977  seqf1olem1  14065  seqf1olem2  14066  bcval4  14329  bcp1nk  14339  bcval5  14340  fzsdom2  14450  seqcoll  14486  seqcoll2  14487  ccatrn  14610  ccatalpha  14614  cshwidxmodr  14825  fzomaxdiflem  15364  fzomaxdif  15365  rexuzre  15374  limsupgre  15500  rlimclim1  15564  isercoll  15687  iseralt  15704  fsumm1  15770  fsum1p  15772  fsum0diaglem  15795  modfsummods  15812  isumsplit  15859  climcndslem1  15868  mertenslem1  15903  ntrivcvgmul  15921  fprodntriv  15961  fprod1p  15987  fprodeq0  15994  fallfacval4  16062  bpoly4  16078  fzo0dvdseq  16343  dvdsmod  16349  oexpneg  16365  mod2eq1n2dvds  16367  ltoddhalfle  16381  flodddiv4t2lthalf  16438  bitsp1  16451  bitsfzolem  16454  bitsfzo  16455  bitsmod  16456  bitscmp  16458  bitsinv1lem  16461  sadaddlem  16486  bitsres  16493  bitsuz  16494  smumul  16513  gcd0id  16539  gcdneg  16542  dfgcd2  16566  nn0seqcvgd  16590  lcmgcdlem  16626  nprm  16708  prmdvdsfz  16725  isprm5  16727  isprm7  16728  coprm  16731  prmexpb  16739  prmfac1  16740  hashdvds  16795  crth  16798  eulerthlem2  16802  fermltl  16804  prmdiv  16805  prmdiveq  16806  hashgcdlem  16808  odzdvds  16816  vfermltlALT  16823  modprm0  16826  modprmn0modprm0  16828  prm23ge5  16836  pythagtriplem13  16848  pcxcl  16882  pcaddlem  16909  pcadd  16910  pcfac  16920  qexpz  16922  prmunb  16935  1arithlem4  16947  4sqlem5  16963  4sqlem6  16964  4sqlem7  16965  4sqlem10  16968  4sqlem11  16976  4sqlem12  16977  4sqlem15  16980  4sqlem16  16981  4sqlem17  16982  vdwnnlem3  17018  prmgaplem7  17078  cshwshashlem3  17118  subgmulg  19132  mndodconglem  19532  odnncl  19536  odmod  19537  oddvds  19538  dfod2  19555  sylow1lem3  19591  efgsp1  19728  efgredleme  19734  telgsumfzs  19980  zringlpirlem1  21440  zringlpirlem3  21442  fermltlchr  21511  znf1o  21537  zcld  24790  ovoliunlem1  25492  ovoliunlem2  25493  dyadss  25584  dyaddisjlem  25585  dyadmaxlem  25587  dvfsumle  26015  dvfsumleOLD  26016  dvfsumge  26017  dvfsumabs  26018  dvfsumlem1  26021  dvfsumlem3  26024  degltlem1  26066  plyco0  26186  plyeq0lem  26204  plydivex  26294  aannenlem1  26325  efif1olem2  26540  nnlogbexp  26779  logblt  26782  ang180lem1  26807  ang180lem3  26809  wilthlem2  27067  basellem3  27081  basellem4  27082  ppiprm  27149  chtdif  27156  ppidif  27161  chtub  27211  mersenne  27226  bcmono  27276  bcmax  27277  bposlem1  27283  bposlem3  27285  bposlem5  27287  bposlem6  27288  lgsval2lem  27306  lgsvalmod  27315  lgsneg  27320  lgsmod  27322  lgsdilem  27323  lgsdirprm  27330  lgsdilem2  27332  lgsne0  27334  lgssq  27336  lgssq2  27337  lgsqr  27350  lgsdchr  27354  gausslemma2dlem1a  27364  gausslemma2dlem3  27367  gausslemma2dlem5a  27369  gausslemma2dlem6  27371  gausslemma2d  27373  lgseisenlem1  27374  lgseisenlem2  27375  lgseisenlem3  27376  lgseisenlem4  27377  lgsquadlem1  27379  lgsquadlem2  27380  lgsquadlem3  27381  lgsquad3  27386  2lgslem1a2  27389  2lgslem1  27393  2lgslem2  27394  2sqlem3  27419  2sqlem8  27425  2sqblem  27430  2sqmod  27435  chebbnd1lem1  27468  chebbnd1lem2  27469  chebbnd1lem3  27470  dchrmusum2  27493  dchrvmasumlem1  27494  dchrvmasum2lem  27495  dchrvmasum2if  27496  dchrvmasumlem3  27498  dchrvmasumiflem2  27501  dchrisum0lem1  27515  dchrmusumlem  27521  mudivsum  27529  mulogsumlem  27530  mulogsum  27531  mulog2sumlem2  27534  mulog2sumlem3  27535  selberglem1  27544  selberglem2  27545  pntpbnd1  27585  pntlemg  27597  pntlemf  27604  qabvle  27624  padicabv  27629  padicabvcxp  27631  ostth2lem2  27633  axlowdimlem13  28918  axlowdimlem16  28921  pthdlem1  29733  crctcshwlkn0  29788  crctcsh  29791  clwwisshclwwslemlem  29979  eucrctshift  30209  nndiffz1  32735  fzsplit3  32742  bcm1n  32744  fzone1  32749  suppssnn0  32756  ltesubnnd  32771  wrdt2ind  32885  cshwrnid  32893  chnub  32948  chnso  32950  cycpmfv2  33080  cycpmco2lem6  33097  cycpmco2lem7  33098  cycpmrn  33109  cyc3conja  33123  pnfinf  33136  znfermltl  33335  dya2iocress  34217  dya2iocbrsiga  34218  dya2icobrsiga  34219  dya2icoseg  34220  dya2iocucvr  34227  sxbrsigalem2  34229  ballotlemfc0  34436  ballotlemfcc  34437  ballotlemodife  34441  ballotlemimin  34449  ballotlemsgt1  34454  ballotlemsel1i  34456  ballotlemsi  34458  ballotlemsima  34459  ballotlemrv2  34465  ballotlemfrceq  34472  ballotlemfrcn0  34473  ballotlemirc  34475  fsum2dsub  34563  reprlt  34575  reprgt  34577  breprexplemc  34588  tgoldbachgnn  34615  tgoldbachgt  34619  subfacval3  35135  erdszelem8  35144  erdszelem9  35145  supfz  35670  inffz  35671  dnizeq0  36417  dnizphlfeqhlf  36418  dnibndlem13  36432  knoppndvlem1  36454  knoppndvlem2  36455  knoppndvlem7  36460  knoppndvlem19  36472  knoppndvlem21  36474  ltflcei  37556  leceifl  37557  poimirlem1  37569  poimirlem2  37570  poimirlem6  37574  poimirlem7  37575  poimirlem8  37576  poimirlem15  37583  poimirlem16  37584  poimirlem17  37585  poimirlem19  37587  poimirlem20  37588  poimirlem23  37591  poimirlem24  37592  poimirlem27  37595  poimirlem29  37597  poimirlem31  37599  poimirlem32  37600  mblfinlem2  37606  itg2addnclem2  37620  mettrifi  37705  cntotbnd  37744  fzne2d  41922  aks4d1lem1  42004  aks4d1p1p3  42011  aks4d1p1p2  42012  aks4d1p1p4  42013  aks4d1p1  42018  aks4d1p2  42019  aks4d1p3  42020  aks4d1p5  42022  aks4d1p6  42023  aks4d1p7d1  42024  aks4d1p7  42025  aks4d1p8d3  42028  aks4d1p8  42029  aks4d1p9  42030  posbezout  42042  aks6d1c1  42058  hashscontpow1  42063  hashscontpow  42064  aks6d1c2  42072  aks6d1c5lem1  42078  2ap1caineq  42087  sticksstones6  42093  sticksstones7  42094  sticksstones10  42097  sticksstones12a  42099  sticksstones12  42100  sticksstones22  42110  bcled  42120  bcle2d  42121  aks6d1c7lem1  42122  aks6d1c7lem2  42123  aks6d1c7  42126  aks5lem6  42134  unitscyglem2  42138  unitscyglem4  42140  aks5lem8  42143  metakunt7  42153  metakunt12  42158  metakunt15  42161  metakunt16  42162  metakunt22  42168  metakunt28  42174  prodsplit  42182  sumcubes  42292  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  43414  fzunt1d  43415  fzuntgd  43416  prmunb2  44275  nzprmdif  44283  hashnzfzclim  44286  binomcxplemnn0  44313  uzwo4  45003  ssinc  45037  ssdec  45038  zltlesub  45242  monoords  45254  fzisoeu  45257  fperiodmul  45261  fzdifsuc2  45267  iuneqfzuzlem  45290  uzublem  45386  zxrd  45409  uzinico  45518  uzubioo  45525  fmul01  45540  fmul01lt1lem1  45544  fmul01lt1lem2  45545  climsuselem1  45567  climsuse  45568  sumnnodd  45590  ltmod  45598  limsupresuz  45663  limsupubuzlem  45672  limsupequzlem  45682  limsupmnfuzlem  45686  limsupequzmptlem  45688  limsupre3uzlem  45695  supcnvlimsup  45700  limsup10exlem  45732  liminfresuz  45744  liminfvaluz  45752  limsupvaluz3  45758  ioodvbdlimc1lem2  45892  ioodvbdlimc2lem  45894  dvnmul  45903  dvnprodlem1  45906  dvnprodlem2  45907  iblspltprt  45933  itgspltprt  45939  stoweidlem3  45963  stoweidlem11  45971  stoweidlem20  45980  stoweidlem26  45986  stoweidlem34  45994  stoweidlem59  46019  stirlinglem5  46038  dirkertrigeqlem3  46060  dirkeritg  46062  dirkercncflem1  46063  dirkercncflem2  46064  dirkercncflem4  46066  fourierdlem4  46071  fourierdlem6  46073  fourierdlem7  46074  fourierdlem11  46078  fourierdlem12  46079  fourierdlem15  46082  fourierdlem19  46086  fourierdlem20  46087  fourierdlem25  46092  fourierdlem26  46093  fourierdlem34  46101  fourierdlem35  46102  fourierdlem41  46108  fourierdlem48  46114  fourierdlem49  46115  fourierdlem50  46116  fourierdlem51  46117  fourierdlem54  46120  fourierdlem63  46129  fourierdlem64  46130  fourierdlem65  46131  fourierdlem71  46137  fourierdlem79  46145  fourierdlem89  46155  fourierdlem90  46156  fourierdlem91  46157  fourierdlem102  46168  fourierdlem103  46169  fourierdlem104  46170  fourierdlem114  46180  fouriersw  46191  elaa2lem  46193  etransclem3  46197  etransclem4  46198  etransclem7  46201  etransclem10  46204  etransclem15  46209  etransclem19  46213  etransclem23  46217  etransclem24  46218  etransclem25  46219  etransclem27  46221  etransclem31  46225  etransclem32  46226  etransclem35  46229  etransclem41  46235  etransclem44  46238  etransclem46  46240  etransclem48  46242  iundjiun  46420  caratheodorylem1  46486  smflimsuplem4  46783  smfliminflem  46790  ormklocald  46834  ormkglobd  46835  natglobalincr  46837  2elfz2melfz  47276  elfzelfzlble  47279  fzopredsuc  47281  submodlt  47298  fsummsndifre  47305  iccpartgt  47360  icceuelpartlem  47368  icceuelpart  47369  iccpartnel  47371  lighneallem2  47539  proththd  47547  dfodd4  47592  oexpnegALTV  47610  nnoALTV  47628  evenltle  47650  fpprwppr  47672  gbowgt5  47695  gboge9  47697  stgoldbwt  47709  sbgoldbst  47711  sbgoldbalt  47714  sgoldbeven3prm  47716  mogoldbb  47718  bgoldbtbndlem1  47738  bgoldbtbndlem2  47739  bgoldbtbndlem3  47740  bgoldbtbnd  47742  bgoldbachlt  47746  tgblthelfgott  47748  tgoldbach  47750  2ltceilhalf  47961  gpgedgvtx1  47966  gpgvtxedg0  47967  gpgvtxedg1  47968  gpg3nbgrvtxlem  47969  gpg5nbgrvtx13starlem2  47974  gpg3nbgrvtx0  47978  gpg3kgrtriexlem1  47985  gpg3kgrtriexlem4  47988  gpg3kgrtriexlem6  47990  pw2m1lepw2m1  48383  m1modmmod  48388  difmodm1lt  48389  fllogbd  48427  logbpw2m1  48434  fllog2  48435  nnpw2blen  48447  nnolog2flm1  48457  dignn0flhalflem1  48482  dignn0flhalflem2  48483