Theorem zred 12638

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

Syntax hints:   → wi 4   ∈ wcel 2109  ℝcr 11067  ℤcz 12529

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 3406  df-v 3449  df-dif 3917  df-un 3919  df-ss 3931  df-nul 4297  df-if 4489  df-sn 4590  df-pr 4592  df-op 4596  df-uni 4872  df-br 5108  df-iota 6464  df-fv 6519  df-ov 7390  df-neg 11408  df-z 12530

This theorem is referenced by:  zcnd  12639  suprfinzcl  12648  eluzmn  12800  eluzelre  12804  eluzadd  12822  subeluzsub  12830  uzm1  12831  zsupss  12896  suprzcl2  12897  uzwo3  12902  rpnnen1lem3  12938  rpnnen1lem5  12940  zltaddlt1le  13466  fzsplit2  13510  fzdisj  13512  ssfzunsnext  13530  fzpreddisj  13534  fznatpl1  13539  fzp1disj  13544  uzdisj  13558  fzdif1  13566  fzm1  13568  fz0fzdiffz0  13598  elfzmlbm  13599  elfzmlbp  13600  difelfznle  13603  nn0disj  13605  elfzolt3  13630  fzonel  13634  fzospliti  13652  fzodisj  13654  fzouzdisj  13656  fzodisjsn  13658  elfzo0subge1  13666  elfzo0suble  13667  fzonmapblen  13669  fzoaddel  13678  elincfzoext  13684  reflcl  13758  flge  13767  flwordi  13774  fladdz  13787  2tnp1ge0ge0  13791  flhalf  13792  fldiv4p1lem1div2  13797  fldiv4lem1div2uz2  13798  fldiv4lem1div2  13799  flleceil  13815  fleqceilz  13816  quoremz  13817  uzsup  13825  modaddid  13872  modmul12d  13890  modaddmodup  13899  modaddmodlo  13900  modfzo0difsn  13908  modsumfzodifsn  13909  addmodlteq  13911  om2uzlti  13915  om2uzf1oi  13918  seqf1olem1  14006  seqf1olem2  14007  bcval4  14272  bcp1nk  14282  bcval5  14283  fzsdom2  14393  seqcoll  14429  seqcoll2  14430  ccatrn  14554  ccatalpha  14558  cshwidxmodr  14769  fzomaxdiflem  15309  fzomaxdif  15310  rexuzre  15319  limsupgre  15447  rlimclim1  15511  isercoll  15634  iseralt  15651  fsumm1  15717  fsum1p  15719  fsum0diaglem  15742  modfsummods  15759  isumsplit  15806  climcndslem1  15815  mertenslem1  15850  ntrivcvgmul  15868  fprodntriv  15908  fprod1p  15934  fprodeq0  15941  fallfacval4  16009  bpoly4  16025  fzo0dvdseq  16293  dvdsmod  16299  oexpneg  16315  mod2eq1n2dvds  16317  ltoddhalfle  16331  flodddiv4t2lthalf  16388  bitsp1  16401  bitsfzolem  16404  bitsfzo  16405  bitsmod  16406  bitscmp  16408  bitsinv1lem  16411  sadaddlem  16436  bitsres  16443  bitsuz  16444  smumul  16463  gcd0id  16489  gcdneg  16492  dfgcd2  16516  nn0seqcvgd  16540  lcmgcdlem  16576  nprm  16658  prmdvdsfz  16675  isprm5  16677  isprm7  16678  coprm  16681  prmexpb  16689  prmfac1  16690  hashdvds  16745  crth  16748  eulerthlem2  16752  fermltl  16754  prmdiv  16755  prmdiveq  16756  hashgcdlem  16758  odzdvds  16766  vfermltlALT  16773  modprm0  16776  modprmn0modprm0  16778  prm23ge5  16786  pythagtriplem13  16798  pcxcl  16832  pcaddlem  16859  pcadd  16860  pcfac  16870  qexpz  16872  prmunb  16885  1arithlem4  16897  4sqlem5  16913  4sqlem6  16914  4sqlem7  16915  4sqlem10  16918  4sqlem11  16926  4sqlem12  16927  4sqlem15  16930  4sqlem16  16931  4sqlem17  16932  vdwnnlem3  16968  prmgaplem7  17028  cshwshashlem3  17068  subgmulg  19072  mndodconglem  19471  odnncl  19475  odmod  19476  oddvds  19477  dfod2  19494  sylow1lem3  19530  efgsp1  19667  efgredleme  19673  telgsumfzs  19919  zringlpirlem1  21372  zringlpirlem3  21374  fermltlchr  21439  znf1o  21461  zcld  24702  ovoliunlem1  25403  ovoliunlem2  25404  dyadss  25495  dyaddisjlem  25496  dyadmaxlem  25498  dvfsumle  25926  dvfsumleOLD  25927  dvfsumge  25928  dvfsumabs  25929  dvfsumlem1  25932  dvfsumlem3  25935  degltlem1  25977  plyco0  26097  plyeq0lem  26115  plydivex  26205  aannenlem1  26236  efif1olem2  26452  nnlogbexp  26691  logblt  26694  ang180lem1  26719  ang180lem3  26721  wilthlem2  26979  basellem3  26993  basellem4  26994  ppiprm  27061  chtdif  27068  ppidif  27073  chtub  27123  mersenne  27138  bcmono  27188  bcmax  27189  bposlem1  27195  bposlem3  27197  bposlem5  27199  bposlem6  27200  lgsval2lem  27218  lgsvalmod  27227  lgsneg  27232  lgsmod  27234  lgsdilem  27235  lgsdirprm  27242  lgsdilem2  27244  lgsne0  27246  lgssq  27248  lgssq2  27249  lgsqr  27262  lgsdchr  27266  gausslemma2dlem1a  27276  gausslemma2dlem3  27279  gausslemma2dlem5a  27281  gausslemma2dlem6  27283  gausslemma2d  27285  lgseisenlem1  27286  lgseisenlem2  27287  lgseisenlem3  27288  lgseisenlem4  27289  lgsquadlem1  27291  lgsquadlem2  27292  lgsquadlem3  27293  lgsquad3  27298  2lgslem1a2  27301  2lgslem1  27305  2lgslem2  27306  2sqlem3  27331  2sqlem8  27337  2sqblem  27342  2sqmod  27347  chebbnd1lem1  27380  chebbnd1lem2  27381  chebbnd1lem3  27382  dchrmusum2  27405  dchrvmasumlem1  27406  dchrvmasum2lem  27407  dchrvmasum2if  27408  dchrvmasumlem3  27410  dchrvmasumiflem2  27413  dchrisum0lem1  27427  dchrmusumlem  27433  mudivsum  27441  mulogsumlem  27442  mulogsum  27443  mulog2sumlem2  27446  mulog2sumlem3  27447  selberglem1  27456  selberglem2  27457  pntpbnd1  27497  pntlemg  27509  pntlemf  27516  qabvle  27536  padicabv  27541  padicabvcxp  27543  ostth2lem2  27545  axlowdimlem13  28881  axlowdimlem16  28884  pthdlem1  29696  crctcshwlkn0  29751  crctcsh  29754  clwwisshclwwslemlem  29942  eucrctshift  30172  nndiffz1  32709  fzsplit3  32716  bcm1n  32718  fzone1  32723  suppssnn0  32730  ltesubnnd  32747  wrdt2ind  32875  cshwrnid  32883  chnub  32938  chnso  32940  cycpmfv2  33071  cycpmco2lem6  33088  cycpmco2lem7  33089  cycpmrn  33100  cyc3conja  33114  pnfinf  33137  znfermltl  33337  constrext2chnlem  33740  cos9thpiminplylem1  33772  cos9thpiminplylem2  33773  dya2iocress  34265  dya2iocbrsiga  34266  dya2icobrsiga  34267  dya2icoseg  34268  dya2iocucvr  34275  sxbrsigalem2  34277  ballotlemfc0  34484  ballotlemfcc  34485  ballotlemodife  34489  ballotlemimin  34497  ballotlemsgt1  34502  ballotlemsel1i  34504  ballotlemsi  34506  ballotlemsima  34507  ballotlemrv2  34513  ballotlemfrceq  34520  ballotlemfrcn0  34521  ballotlemirc  34523  fsum2dsub  34598  reprlt  34610  reprgt  34612  breprexplemc  34623  tgoldbachgnn  34650  tgoldbachgt  34654  subfacval3  35176  erdszelem8  35185  erdszelem9  35186  supfz  35716  inffz  35717  dnizeq0  36463  dnizphlfeqhlf  36464  dnibndlem13  36478  knoppndvlem1  36500  knoppndvlem2  36501  knoppndvlem7  36506  knoppndvlem19  36518  knoppndvlem21  36520  ltflcei  37602  leceifl  37603  poimirlem1  37615  poimirlem2  37616  poimirlem6  37620  poimirlem7  37621  poimirlem8  37622  poimirlem15  37629  poimirlem16  37630  poimirlem17  37631  poimirlem19  37633  poimirlem20  37634  poimirlem23  37637  poimirlem24  37638  poimirlem27  37641  poimirlem29  37643  poimirlem31  37645  poimirlem32  37646  mblfinlem2  37652  itg2addnclem2  37666  mettrifi  37751  cntotbnd  37790  fzne2d  41968  aks4d1lem1  42050  aks4d1p1p3  42057  aks4d1p1p2  42058  aks4d1p1p4  42059  aks4d1p1  42064  aks4d1p2  42065  aks4d1p3  42066  aks4d1p5  42068  aks4d1p6  42069  aks4d1p7d1  42070  aks4d1p7  42071  aks4d1p8d3  42074  aks4d1p8  42075  aks4d1p9  42076  posbezout  42088  aks6d1c1  42104  hashscontpow1  42109  hashscontpow  42110  aks6d1c2  42118  aks6d1c5lem1  42124  2ap1caineq  42133  sticksstones6  42139  sticksstones7  42140  sticksstones10  42143  sticksstones12a  42145  sticksstones12  42146  sticksstones22  42156  bcled  42166  bcle2d  42167  aks6d1c7lem1  42168  aks6d1c7lem2  42169  aks6d1c7  42172  aks5lem6  42180  unitscyglem2  42184  unitscyglem4  42186  aks5lem8  42189  sumcubes  42301  frlmvscadiccat  42494  dffltz  42622  lzunuz  42756  lzenom  42758  diophin  42760  irrapxlem1  42810  irrapxlem2  42811  irrapxlem3  42812  irrapxlem4  42813  pellexlem5  42821  pellexlem6  42822  rmspecfund  42897  rmxypos  42936  ltrmynn0  42937  ltrmxnn0  42938  ltrmy  42941  rmyeq0  42942  rmyeq  42943  lermy  42944  rmyabs  42947  jm2.24nn  42948  jm2.17a  42949  jm2.17b  42950  jm2.17c  42951  jm2.24  42952  rmygeid  42953  acongrep  42969  fzmaxdif  42970  acongeq  42972  jm2.22  42984  jm2.23  42985  jm2.26lem3  42990  jm2.27a  42994  jm3.1lem1  43006  jm3.1lem3  43008  expdiophlem1  43010  fzuntd  43445  fzunt1d  43446  fzuntgd  43447  prmunb2  44300  nzprmdif  44308  hashnzfzclim  44311  binomcxplemnn0  44338  uzwo4  45047  ssinc  45081  ssdec  45082  zltlesub  45283  monoords  45295  fzisoeu  45298  fperiodmul  45302  fzdifsuc2  45308  iuneqfzuzlem  45330  uzublem  45426  zxrd  45449  uzinico  45557  uzubioo  45563  fmul01  45578  fmul01lt1lem1  45582  fmul01lt1lem2  45583  climsuselem1  45605  climsuse  45606  sumnnodd  45628  ltmod  45636  limsupresuz  45701  limsupubuzlem  45710  limsupequzlem  45720  limsupmnfuzlem  45724  limsupequzmptlem  45726  limsupre3uzlem  45733  supcnvlimsup  45738  limsup10exlem  45770  liminfresuz  45782  liminfvaluz  45790  limsupvaluz3  45796  ioodvbdlimc1lem2  45930  ioodvbdlimc2lem  45932  dvnmul  45941  dvnprodlem1  45944  dvnprodlem2  45945  iblspltprt  45971  itgspltprt  45977  stoweidlem3  46001  stoweidlem11  46009  stoweidlem20  46018  stoweidlem26  46024  stoweidlem34  46032  stoweidlem59  46057  stirlinglem5  46076  dirkertrigeqlem3  46098  dirkeritg  46100  dirkercncflem1  46101  dirkercncflem2  46102  dirkercncflem4  46104  fourierdlem4  46109  fourierdlem6  46111  fourierdlem7  46112  fourierdlem11  46116  fourierdlem12  46117  fourierdlem15  46120  fourierdlem19  46124  fourierdlem20  46125  fourierdlem25  46130  fourierdlem26  46131  fourierdlem34  46139  fourierdlem35  46140  fourierdlem41  46146  fourierdlem48  46152  fourierdlem49  46153  fourierdlem50  46154  fourierdlem51  46155  fourierdlem54  46158  fourierdlem63  46167  fourierdlem64  46168  fourierdlem65  46169  fourierdlem71  46175  fourierdlem79  46183  fourierdlem89  46193  fourierdlem90  46194  fourierdlem91  46195  fourierdlem102  46206  fourierdlem103  46207  fourierdlem104  46208  fourierdlem114  46218  fouriersw  46229  elaa2lem  46231  etransclem3  46235  etransclem4  46236  etransclem7  46239  etransclem10  46242  etransclem15  46247  etransclem19  46251  etransclem23  46255  etransclem24  46256  etransclem25  46257  etransclem27  46259  etransclem31  46263  etransclem32  46264  etransclem35  46267  etransclem41  46273  etransclem44  46276  etransclem46  46278  etransclem48  46280  iundjiun  46458  caratheodorylem1  46524  smflimsuplem4  46821  smfliminflem  46828  ormklocald  46872  ormkglobd  46873  natglobalincr  46875  2elfz2melfz  47319  elfzelfzlble  47322  fzopredsuc  47324  2ltceilhalf  47329  ceilhalfgt1  47330  ceilhalfnn  47337  submodlt  47351  m1modmmod  47359  difmodm1lt  47360  modmknepk  47363  mod2addne  47365  fsummsndifre  47373  iccpartgt  47428  icceuelpartlem  47436  icceuelpart  47437  iccpartnel  47439  lighneallem2  47607  proththd  47615  dfodd4  47660  oexpnegALTV  47678  nnoALTV  47696  evenltle  47718  fpprwppr  47740  gbowgt5  47763  gboge9  47765  stgoldbwt  47777  sbgoldbst  47779  sbgoldbalt  47782  sgoldbeven3prm  47784  mogoldbb  47786  bgoldbtbndlem1  47806  bgoldbtbndlem2  47807  bgoldbtbndlem3  47808  bgoldbtbnd  47810  bgoldbachlt  47814  tgblthelfgott  47816  tgoldbach  47818  upgrimpthslem2  47908  gpgprismgrusgra  48049  gpgedgvtx1  48053  gpgvtxedg0  48054  gpgvtxedg1  48055  gpg5nbgrvtx13starlem2  48063  gpg3nbgrvtx0  48067  gpg3kgrtriexlem1  48074  gpg3kgrtriexlem4  48077  gpg3kgrtriexlem6  48079  pw2m1lepw2m1  48509  fllogbd  48549  logbpw2m1  48556  fllog2  48557  nnpw2blen  48569  nnolog2flm1  48579  dignn0flhalflem1  48604  dignn0flhalflem2  48605