Theorem zred 12702

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

Syntax hints:   → wi 4   ∈ wcel 2109  ℝcr 11133  ℤcz 12593

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 2708

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 2715  df-cleq 2728  df-clel 2810  df-rab 3421  df-v 3466  df-dif 3934  df-un 3936  df-ss 3948  df-nul 4314  df-if 4506  df-sn 4607  df-pr 4609  df-op 4613  df-uni 4889  df-br 5125  df-iota 6489  df-fv 6544  df-ov 7413  df-neg 11474  df-z 12594

This theorem is referenced by:  zcnd  12703  suprfinzcl  12712  eluzmn  12864  eluzelre  12868  eluzadd  12886  subeluzsub  12894  uzm1  12895  zsupss  12958  suprzcl2  12959  uzwo3  12964  rpnnen1lem3  13000  rpnnen1lem5  13002  zltaddlt1le  13527  fzsplit2  13571  fzdisj  13573  ssfzunsnext  13591  fzpreddisj  13595  fznatpl1  13600  fzp1disj  13605  uzdisj  13619  fzdif1  13627  fzm1  13629  fz0fzdiffz0  13659  elfzmlbm  13660  elfzmlbp  13661  difelfznle  13664  nn0disj  13666  elfzolt3  13691  fzonel  13695  fzospliti  13713  fzodisj  13715  fzouzdisj  13717  fzodisjsn  13719  elfzo0subge1  13727  elfzo0suble  13728  fzonmapblen  13730  fzoaddel  13738  elincfzoext  13744  reflcl  13818  flge  13827  flwordi  13834  fladdz  13847  2tnp1ge0ge0  13851  flhalf  13852  fldiv4p1lem1div2  13857  fldiv4lem1div2uz2  13858  fldiv4lem1div2  13859  flleceil  13875  fleqceilz  13876  quoremz  13877  uzsup  13885  modmul12d  13948  modaddmodup  13957  modaddmodlo  13958  modfzo0difsn  13966  modsumfzodifsn  13967  addmodlteq  13969  om2uzlti  13973  om2uzf1oi  13976  seqf1olem1  14064  seqf1olem2  14065  bcval4  14330  bcp1nk  14340  bcval5  14341  fzsdom2  14451  seqcoll  14487  seqcoll2  14488  ccatrn  14612  ccatalpha  14616  cshwidxmodr  14827  fzomaxdiflem  15366  fzomaxdif  15367  rexuzre  15376  limsupgre  15502  rlimclim1  15566  isercoll  15689  iseralt  15706  fsumm1  15772  fsum1p  15774  fsum0diaglem  15797  modfsummods  15814  isumsplit  15861  climcndslem1  15870  mertenslem1  15905  ntrivcvgmul  15923  fprodntriv  15963  fprod1p  15989  fprodeq0  15996  fallfacval4  16064  bpoly4  16080  fzo0dvdseq  16347  dvdsmod  16353  oexpneg  16369  mod2eq1n2dvds  16371  ltoddhalfle  16385  flodddiv4t2lthalf  16442  bitsp1  16455  bitsfzolem  16458  bitsfzo  16459  bitsmod  16460  bitscmp  16462  bitsinv1lem  16465  sadaddlem  16490  bitsres  16497  bitsuz  16498  smumul  16517  gcd0id  16543  gcdneg  16546  dfgcd2  16570  nn0seqcvgd  16594  lcmgcdlem  16630  nprm  16712  prmdvdsfz  16729  isprm5  16731  isprm7  16732  coprm  16735  prmexpb  16743  prmfac1  16744  hashdvds  16799  crth  16802  eulerthlem2  16806  fermltl  16808  prmdiv  16809  prmdiveq  16810  hashgcdlem  16812  odzdvds  16820  vfermltlALT  16827  modprm0  16830  modprmn0modprm0  16832  prm23ge5  16840  pythagtriplem13  16852  pcxcl  16886  pcaddlem  16913  pcadd  16914  pcfac  16924  qexpz  16926  prmunb  16939  1arithlem4  16951  4sqlem5  16967  4sqlem6  16968  4sqlem7  16969  4sqlem10  16972  4sqlem11  16980  4sqlem12  16981  4sqlem15  16984  4sqlem16  16985  4sqlem17  16986  vdwnnlem3  17022  prmgaplem7  17082  cshwshashlem3  17122  subgmulg  19128  mndodconglem  19527  odnncl  19531  odmod  19532  oddvds  19533  dfod2  19550  sylow1lem3  19586  efgsp1  19723  efgredleme  19729  telgsumfzs  19975  zringlpirlem1  21428  zringlpirlem3  21430  fermltlchr  21495  znf1o  21517  zcld  24758  ovoliunlem1  25460  ovoliunlem2  25461  dyadss  25552  dyaddisjlem  25553  dyadmaxlem  25555  dvfsumle  25983  dvfsumleOLD  25984  dvfsumge  25985  dvfsumabs  25986  dvfsumlem1  25989  dvfsumlem3  25992  degltlem1  26034  plyco0  26154  plyeq0lem  26172  plydivex  26262  aannenlem1  26293  efif1olem2  26509  nnlogbexp  26748  logblt  26751  ang180lem1  26776  ang180lem3  26778  wilthlem2  27036  basellem3  27050  basellem4  27051  ppiprm  27118  chtdif  27125  ppidif  27130  chtub  27180  mersenne  27195  bcmono  27245  bcmax  27246  bposlem1  27252  bposlem3  27254  bposlem5  27256  bposlem6  27257  lgsval2lem  27275  lgsvalmod  27284  lgsneg  27289  lgsmod  27291  lgsdilem  27292  lgsdirprm  27299  lgsdilem2  27301  lgsne0  27303  lgssq  27305  lgssq2  27306  lgsqr  27319  lgsdchr  27323  gausslemma2dlem1a  27333  gausslemma2dlem3  27336  gausslemma2dlem5a  27338  gausslemma2dlem6  27340  gausslemma2d  27342  lgseisenlem1  27343  lgseisenlem2  27344  lgseisenlem3  27345  lgseisenlem4  27346  lgsquadlem1  27348  lgsquadlem2  27349  lgsquadlem3  27350  lgsquad3  27355  2lgslem1a2  27358  2lgslem1  27362  2lgslem2  27363  2sqlem3  27388  2sqlem8  27394  2sqblem  27399  2sqmod  27404  chebbnd1lem1  27437  chebbnd1lem2  27438  chebbnd1lem3  27439  dchrmusum2  27462  dchrvmasumlem1  27463  dchrvmasum2lem  27464  dchrvmasum2if  27465  dchrvmasumlem3  27467  dchrvmasumiflem2  27470  dchrisum0lem1  27484  dchrmusumlem  27490  mudivsum  27498  mulogsumlem  27499  mulogsum  27500  mulog2sumlem2  27503  mulog2sumlem3  27504  selberglem1  27513  selberglem2  27514  pntpbnd1  27554  pntlemg  27566  pntlemf  27573  qabvle  27593  padicabv  27598  padicabvcxp  27600  ostth2lem2  27602  axlowdimlem13  28938  axlowdimlem16  28941  pthdlem1  29753  crctcshwlkn0  29808  crctcsh  29811  clwwisshclwwslemlem  29999  eucrctshift  30229  nndiffz1  32768  fzsplit3  32775  bcm1n  32777  fzone1  32782  suppssnn0  32789  ltesubnnd  32806  wrdt2ind  32934  cshwrnid  32942  chnub  32997  chnso  32999  cycpmfv2  33130  cycpmco2lem6  33147  cycpmco2lem7  33148  cycpmrn  33159  cyc3conja  33173  pnfinf  33186  znfermltl  33386  constrext2chnlem  33789  cos9thpiminplylem1  33821  cos9thpiminplylem2  33822  dya2iocress  34311  dya2iocbrsiga  34312  dya2icobrsiga  34313  dya2icoseg  34314  dya2iocucvr  34321  sxbrsigalem2  34323  ballotlemfc0  34530  ballotlemfcc  34531  ballotlemodife  34535  ballotlemimin  34543  ballotlemsgt1  34548  ballotlemsel1i  34550  ballotlemsi  34552  ballotlemsima  34553  ballotlemrv2  34559  ballotlemfrceq  34566  ballotlemfrcn0  34567  ballotlemirc  34569  fsum2dsub  34644  reprlt  34656  reprgt  34658  breprexplemc  34669  tgoldbachgnn  34696  tgoldbachgt  34700  subfacval3  35216  erdszelem8  35225  erdszelem9  35226  supfz  35751  inffz  35752  dnizeq0  36498  dnizphlfeqhlf  36499  dnibndlem13  36513  knoppndvlem1  36535  knoppndvlem2  36536  knoppndvlem7  36541  knoppndvlem19  36553  knoppndvlem21  36555  ltflcei  37637  leceifl  37638  poimirlem1  37650  poimirlem2  37651  poimirlem6  37655  poimirlem7  37656  poimirlem8  37657  poimirlem15  37664  poimirlem16  37665  poimirlem17  37666  poimirlem19  37668  poimirlem20  37669  poimirlem23  37672  poimirlem24  37673  poimirlem27  37676  poimirlem29  37678  poimirlem31  37680  poimirlem32  37681  mblfinlem2  37687  itg2addnclem2  37701  mettrifi  37786  cntotbnd  37825  fzne2d  41998  aks4d1lem1  42080  aks4d1p1p3  42087  aks4d1p1p2  42088  aks4d1p1p4  42089  aks4d1p1  42094  aks4d1p2  42095  aks4d1p3  42096  aks4d1p5  42098  aks4d1p6  42099  aks4d1p7d1  42100  aks4d1p7  42101  aks4d1p8d3  42104  aks4d1p8  42105  aks4d1p9  42106  posbezout  42118  aks6d1c1  42134  hashscontpow1  42139  hashscontpow  42140  aks6d1c2  42148  aks6d1c5lem1  42154  2ap1caineq  42163  sticksstones6  42169  sticksstones7  42170  sticksstones10  42173  sticksstones12a  42175  sticksstones12  42176  sticksstones22  42186  bcled  42196  bcle2d  42197  aks6d1c7lem1  42198  aks6d1c7lem2  42199  aks6d1c7  42202  aks5lem6  42210  unitscyglem2  42214  unitscyglem4  42216  aks5lem8  42219  sumcubes  42331  frlmvscadiccat  42504  dffltz  42632  lzunuz  42766  lzenom  42768  diophin  42770  irrapxlem1  42820  irrapxlem2  42821  irrapxlem3  42822  irrapxlem4  42823  pellexlem5  42831  pellexlem6  42832  rmspecfund  42907  rmxypos  42946  ltrmynn0  42947  ltrmxnn0  42948  ltrmy  42951  rmyeq0  42952  rmyeq  42953  lermy  42954  rmyabs  42957  jm2.24nn  42958  jm2.17a  42959  jm2.17b  42960  jm2.17c  42961  jm2.24  42962  rmygeid  42963  acongrep  42979  fzmaxdif  42980  acongeq  42982  jm2.22  42994  jm2.23  42995  jm2.26lem3  43000  jm2.27a  43004  jm3.1lem1  43016  jm3.1lem3  43018  expdiophlem1  43020  fzuntd  43455  fzunt1d  43456  fzuntgd  43457  prmunb2  44310  nzprmdif  44318  hashnzfzclim  44321  binomcxplemnn0  44348  uzwo4  45057  ssinc  45091  ssdec  45092  zltlesub  45294  monoords  45306  fzisoeu  45309  fperiodmul  45313  fzdifsuc2  45319  iuneqfzuzlem  45341  uzublem  45437  zxrd  45460  uzinico  45568  uzubioo  45574  fmul01  45589  fmul01lt1lem1  45593  fmul01lt1lem2  45594  climsuselem1  45616  climsuse  45617  sumnnodd  45639  ltmod  45647  limsupresuz  45712  limsupubuzlem  45721  limsupequzlem  45731  limsupmnfuzlem  45735  limsupequzmptlem  45737  limsupre3uzlem  45744  supcnvlimsup  45749  limsup10exlem  45781  liminfresuz  45793  liminfvaluz  45801  limsupvaluz3  45807  ioodvbdlimc1lem2  45941  ioodvbdlimc2lem  45943  dvnmul  45952  dvnprodlem1  45955  dvnprodlem2  45956  iblspltprt  45982  itgspltprt  45988  stoweidlem3  46012  stoweidlem11  46020  stoweidlem20  46029  stoweidlem26  46035  stoweidlem34  46043  stoweidlem59  46068  stirlinglem5  46087  dirkertrigeqlem3  46109  dirkeritg  46111  dirkercncflem1  46112  dirkercncflem2  46113  dirkercncflem4  46115  fourierdlem4  46120  fourierdlem6  46122  fourierdlem7  46123  fourierdlem11  46127  fourierdlem12  46128  fourierdlem15  46131  fourierdlem19  46135  fourierdlem20  46136  fourierdlem25  46141  fourierdlem26  46142  fourierdlem34  46150  fourierdlem35  46151  fourierdlem41  46157  fourierdlem48  46163  fourierdlem49  46164  fourierdlem50  46165  fourierdlem51  46166  fourierdlem54  46169  fourierdlem63  46178  fourierdlem64  46179  fourierdlem65  46180  fourierdlem71  46186  fourierdlem79  46194  fourierdlem89  46204  fourierdlem90  46205  fourierdlem91  46206  fourierdlem102  46217  fourierdlem103  46218  fourierdlem104  46219  fourierdlem114  46229  fouriersw  46240  elaa2lem  46242  etransclem3  46246  etransclem4  46247  etransclem7  46250  etransclem10  46253  etransclem15  46258  etransclem19  46262  etransclem23  46266  etransclem24  46267  etransclem25  46268  etransclem27  46270  etransclem31  46274  etransclem32  46275  etransclem35  46278  etransclem41  46284  etransclem44  46287  etransclem46  46289  etransclem48  46291  iundjiun  46469  caratheodorylem1  46535  smflimsuplem4  46832  smfliminflem  46839  ormklocald  46883  ormkglobd  46884  natglobalincr  46886  2elfz2melfz  47327  elfzelfzlble  47330  fzopredsuc  47332  2ltceilhalf  47337  ceilhalfgt1  47338  ceilhalfnn  47345  submodlt  47359  fsummsndifre  47366  iccpartgt  47421  icceuelpartlem  47429  icceuelpart  47430  iccpartnel  47432  lighneallem2  47600  proththd  47608  dfodd4  47653  oexpnegALTV  47671  nnoALTV  47689  evenltle  47711  fpprwppr  47733  gbowgt5  47756  gboge9  47758  stgoldbwt  47770  sbgoldbst  47772  sbgoldbalt  47775  sgoldbeven3prm  47777  mogoldbb  47779  bgoldbtbndlem1  47799  bgoldbtbndlem2  47800  bgoldbtbndlem3  47801  bgoldbtbnd  47803  bgoldbachlt  47807  tgblthelfgott  47809  tgoldbach  47811  upgrimpthslem2  47901  gpgprismgrusgra  48042  gpgedgvtx1  48046  gpgvtxedg0  48047  gpgvtxedg1  48048  gpg3nbgrvtxlem  48049  gpg5nbgrvtx13starlem2  48054  gpg3nbgrvtx0  48058  gpg3kgrtriexlem1  48065  gpg3kgrtriexlem4  48068  gpg3kgrtriexlem6  48070  pw2m1lepw2m1  48476  m1modmmod  48481  difmodm1lt  48482  fllogbd  48520  logbpw2m1  48527  fllog2  48528  nnpw2blen  48540  nnolog2flm1  48550  dignn0flhalflem1  48575  dignn0flhalflem2  48576