Theorem zred 12577

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

Syntax hints:   → wi 4   ∈ wcel 2111  ℝcr 11005  ℤcz 12468

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2113  ax-9 2121  ax-ext 2703

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-sb 2068  df-clab 2710  df-cleq 2723  df-clel 2806  df-rab 3396  df-v 3438  df-dif 3905  df-un 3907  df-ss 3919  df-nul 4284  df-if 4476  df-sn 4577  df-pr 4579  df-op 4583  df-uni 4860  df-br 5092  df-iota 6437  df-fv 6489  df-ov 7349  df-neg 11347  df-z 12469

This theorem is referenced by:  zcnd  12578  suprfinzcl  12587  eluzmn  12739  eluzelre  12743  eluzadd  12761  subeluzsub  12769  uzm1  12770  zsupss  12835  suprzcl2  12836  uzwo3  12841  rpnnen1lem3  12877  rpnnen1lem5  12879  zltaddlt1le  13405  fzsplit2  13449  fzdisj  13451  ssfzunsnext  13469  fzpreddisj  13473  fznatpl1  13478  fzp1disj  13483  uzdisj  13497  fzdif1  13505  fzm1  13507  fz0fzdiffz0  13537  elfzmlbm  13538  elfzmlbp  13539  difelfznle  13542  nn0disj  13544  elfzolt3  13569  fzonel  13573  fzospliti  13591  fzodisj  13593  fzouzdisj  13595  fzodisjsn  13597  elfzo0subge1  13605  elfzo0suble  13606  fzonmapblen  13608  fzoaddel  13617  elincfzoext  13623  fzone1  13684  reflcl  13700  flge  13709  flwordi  13716  fladdz  13729  2tnp1ge0ge0  13733  flhalf  13734  fldiv4p1lem1div2  13739  fldiv4lem1div2uz2  13740  fldiv4lem1div2  13741  flleceil  13757  fleqceilz  13758  quoremz  13759  uzsup  13767  modaddid  13814  modmul12d  13832  modaddmodup  13841  modaddmodlo  13842  modfzo0difsn  13850  modsumfzodifsn  13851  addmodlteq  13853  om2uzlti  13857  om2uzf1oi  13860  seqf1olem1  13948  seqf1olem2  13949  bcval4  14214  bcp1nk  14224  bcval5  14225  fzsdom2  14335  seqcoll  14371  seqcoll2  14372  ccatrn  14497  ccatalpha  14501  cshwidxmodr  14711  fzomaxdiflem  15250  fzomaxdif  15251  rexuzre  15260  limsupgre  15388  rlimclim1  15452  isercoll  15575  iseralt  15592  fsumm1  15658  fsum1p  15660  fsum0diaglem  15683  modfsummods  15700  isumsplit  15747  climcndslem1  15756  mertenslem1  15791  ntrivcvgmul  15809  fprodntriv  15849  fprod1p  15875  fprodeq0  15882  fallfacval4  15950  bpoly4  15966  fzo0dvdseq  16234  dvdsmod  16240  oexpneg  16256  mod2eq1n2dvds  16258  ltoddhalfle  16272  flodddiv4t2lthalf  16329  bitsp1  16342  bitsfzolem  16345  bitsfzo  16346  bitsmod  16347  bitscmp  16349  bitsinv1lem  16352  sadaddlem  16377  bitsres  16384  bitsuz  16385  smumul  16404  gcd0id  16430  gcdneg  16433  dfgcd2  16457  nn0seqcvgd  16481  lcmgcdlem  16517  nprm  16599  prmdvdsfz  16616  isprm5  16618  isprm7  16619  coprm  16622  prmexpb  16630  prmfac1  16631  hashdvds  16686  crth  16689  eulerthlem2  16693  fermltl  16695  prmdiv  16696  prmdiveq  16697  hashgcdlem  16699  odzdvds  16707  vfermltlALT  16714  modprm0  16717  modprmn0modprm0  16719  prm23ge5  16727  pythagtriplem13  16739  pcxcl  16773  pcaddlem  16800  pcadd  16801  pcfac  16811  qexpz  16813  prmunb  16826  1arithlem4  16838  4sqlem5  16854  4sqlem6  16855  4sqlem7  16856  4sqlem10  16859  4sqlem11  16867  4sqlem12  16868  4sqlem15  16871  4sqlem16  16872  4sqlem17  16873  vdwnnlem3  16909  prmgaplem7  16969  cshwshashlem3  17009  chnub  18528  chnso  18530  chnccat  18532  chnpof1  18536  subgmulg  19053  mndodconglem  19454  odnncl  19458  odmod  19459  oddvds  19460  dfod2  19477  sylow1lem3  19513  efgsp1  19650  efgredleme  19656  telgsumfzs  19902  zringlpirlem1  21400  zringlpirlem3  21402  fermltlchr  21467  znf1o  21489  zcld  24730  ovoliunlem1  25431  ovoliunlem2  25432  dyadss  25523  dyaddisjlem  25524  dyadmaxlem  25526  dvfsumle  25954  dvfsumleOLD  25955  dvfsumge  25956  dvfsumabs  25957  dvfsumlem1  25960  dvfsumlem3  25963  degltlem1  26005  plyco0  26125  plyeq0lem  26143  plydivex  26233  aannenlem1  26264  efif1olem2  26480  nnlogbexp  26719  logblt  26722  ang180lem1  26747  ang180lem3  26749  wilthlem2  27007  basellem3  27021  basellem4  27022  ppiprm  27089  chtdif  27096  ppidif  27101  chtub  27151  mersenne  27166  bcmono  27216  bcmax  27217  bposlem1  27223  bposlem3  27225  bposlem5  27227  bposlem6  27228  lgsval2lem  27246  lgsvalmod  27255  lgsneg  27260  lgsmod  27262  lgsdilem  27263  lgsdirprm  27270  lgsdilem2  27272  lgsne0  27274  lgssq  27276  lgssq2  27277  lgsqr  27290  lgsdchr  27294  gausslemma2dlem1a  27304  gausslemma2dlem3  27307  gausslemma2dlem5a  27309  gausslemma2dlem6  27311  gausslemma2d  27313  lgseisenlem1  27314  lgseisenlem2  27315  lgseisenlem3  27316  lgseisenlem4  27317  lgsquadlem1  27319  lgsquadlem2  27320  lgsquadlem3  27321  lgsquad3  27326  2lgslem1a2  27329  2lgslem1  27333  2lgslem2  27334  2sqlem3  27359  2sqlem8  27365  2sqblem  27370  2sqmod  27375  chebbnd1lem1  27408  chebbnd1lem2  27409  chebbnd1lem3  27410  dchrmusum2  27433  dchrvmasumlem1  27434  dchrvmasum2lem  27435  dchrvmasum2if  27436  dchrvmasumlem3  27438  dchrvmasumiflem2  27441  dchrisum0lem1  27455  dchrmusumlem  27461  mudivsum  27469  mulogsumlem  27470  mulogsum  27471  mulog2sumlem2  27474  mulog2sumlem3  27475  selberglem1  27484  selberglem2  27485  pntpbnd1  27525  pntlemg  27537  pntlemf  27544  qabvle  27564  padicabv  27569  padicabvcxp  27571  ostth2lem2  27573  axlowdimlem13  28933  axlowdimlem16  28936  pthdlem1  29745  crctcshwlkn0  29800  crctcsh  29803  clwwisshclwwslemlem  29991  eucrctshift  30221  nndiffz1  32767  fzsplit3  32774  bcm1n  32775  suppssnn0  32785  ltesubnnd  32803  wrdt2ind  32932  cshwrnid  32940  cycpmfv2  33081  cycpmco2lem6  33098  cycpmco2lem7  33099  cycpmrn  33110  cyc3conja  33124  pnfinf  33150  znfermltl  33329  constrext2chnlem  33761  cos9thpiminplylem1  33793  cos9thpiminplylem2  33794  dya2iocress  34285  dya2iocbrsiga  34286  dya2icobrsiga  34287  dya2icoseg  34288  dya2iocucvr  34295  sxbrsigalem2  34297  ballotlemfc0  34504  ballotlemfcc  34505  ballotlemodife  34509  ballotlemimin  34517  ballotlemsgt1  34522  ballotlemsel1i  34524  ballotlemsi  34526  ballotlemsima  34527  ballotlemrv2  34533  ballotlemfrceq  34540  ballotlemfrcn0  34541  ballotlemirc  34543  fsum2dsub  34618  reprlt  34630  reprgt  34632  breprexplemc  34643  tgoldbachgnn  34670  tgoldbachgt  34674  subfacval3  35231  erdszelem8  35240  erdszelem9  35241  supfz  35771  inffz  35772  dnizeq0  36515  dnizphlfeqhlf  36516  dnibndlem13  36530  knoppndvlem1  36552  knoppndvlem2  36553  knoppndvlem7  36558  knoppndvlem19  36570  knoppndvlem21  36572  ltflcei  37654  leceifl  37655  poimirlem1  37667  poimirlem2  37668  poimirlem6  37672  poimirlem7  37673  poimirlem8  37674  poimirlem15  37681  poimirlem16  37682  poimirlem17  37683  poimirlem19  37685  poimirlem20  37686  poimirlem23  37689  poimirlem24  37690  poimirlem27  37693  poimirlem29  37695  poimirlem31  37697  poimirlem32  37698  mblfinlem2  37704  itg2addnclem2  37718  mettrifi  37803  cntotbnd  37842  fzne2d  42019  aks4d1lem1  42101  aks4d1p1p3  42108  aks4d1p1p2  42109  aks4d1p1p4  42110  aks4d1p1  42115  aks4d1p2  42116  aks4d1p3  42117  aks4d1p5  42119  aks4d1p6  42120  aks4d1p7d1  42121  aks4d1p7  42122  aks4d1p8d3  42125  aks4d1p8  42126  aks4d1p9  42127  posbezout  42139  aks6d1c1  42155  hashscontpow1  42160  hashscontpow  42161  aks6d1c2  42169  aks6d1c5lem1  42175  2ap1caineq  42184  sticksstones6  42190  sticksstones7  42191  sticksstones10  42194  sticksstones12a  42196  sticksstones12  42197  sticksstones22  42207  bcled  42217  bcle2d  42218  aks6d1c7lem1  42219  aks6d1c7lem2  42220  aks6d1c7  42223  aks5lem6  42231  unitscyglem2  42235  unitscyglem4  42237  aks5lem8  42240  sumcubes  42352  frlmvscadiccat  42545  dffltz  42673  lzunuz  42807  lzenom  42809  diophin  42811  irrapxlem1  42861  irrapxlem2  42862  irrapxlem3  42863  irrapxlem4  42864  pellexlem5  42872  pellexlem6  42873  rmspecfund  42948  rmxypos  42986  ltrmynn0  42987  ltrmxnn0  42988  ltrmy  42991  rmyeq0  42992  rmyeq  42993  lermy  42994  rmyabs  42997  jm2.24nn  42998  jm2.17a  42999  jm2.17b  43000  jm2.17c  43001  jm2.24  43002  rmygeid  43003  acongrep  43019  fzmaxdif  43020  acongeq  43022  jm2.22  43034  jm2.23  43035  jm2.26lem3  43040  jm2.27a  43044  jm3.1lem1  43056  jm3.1lem3  43058  expdiophlem1  43060  fzuntd  43495  fzunt1d  43496  fzuntgd  43497  prmunb2  44350  nzprmdif  44358  hashnzfzclim  44361  binomcxplemnn0  44388  uzwo4  45096  ssinc  45130  ssdec  45131  zltlesub  45332  monoords  45344  fzisoeu  45347  fperiodmul  45351  fzdifsuc2  45357  iuneqfzuzlem  45379  uzublem  45474  zxrd  45497  uzinico  45605  uzubioo  45611  fmul01  45626  fmul01lt1lem1  45630  fmul01lt1lem2  45631  climsuselem1  45653  climsuse  45654  sumnnodd  45676  ltmod  45682  limsupresuz  45747  limsupubuzlem  45756  limsupequzlem  45766  limsupmnfuzlem  45770  limsupequzmptlem  45772  limsupre3uzlem  45779  supcnvlimsup  45784  limsup10exlem  45816  liminfresuz  45828  liminfvaluz  45836  limsupvaluz3  45842  ioodvbdlimc1lem2  45976  ioodvbdlimc2lem  45978  dvnmul  45987  dvnprodlem1  45990  dvnprodlem2  45991  iblspltprt  46017  itgspltprt  46023  stoweidlem3  46047  stoweidlem11  46055  stoweidlem20  46064  stoweidlem26  46070  stoweidlem34  46078  stoweidlem59  46103  stirlinglem5  46122  dirkertrigeqlem3  46144  dirkeritg  46146  dirkercncflem1  46147  dirkercncflem2  46148  dirkercncflem4  46150  fourierdlem4  46155  fourierdlem6  46157  fourierdlem7  46158  fourierdlem11  46162  fourierdlem12  46163  fourierdlem15  46166  fourierdlem19  46170  fourierdlem20  46171  fourierdlem25  46176  fourierdlem26  46177  fourierdlem34  46185  fourierdlem35  46186  fourierdlem41  46192  fourierdlem48  46198  fourierdlem49  46199  fourierdlem50  46200  fourierdlem51  46201  fourierdlem54  46204  fourierdlem63  46213  fourierdlem64  46214  fourierdlem65  46215  fourierdlem71  46221  fourierdlem79  46229  fourierdlem89  46239  fourierdlem90  46240  fourierdlem91  46241  fourierdlem102  46252  fourierdlem103  46253  fourierdlem104  46254  fourierdlem114  46264  fouriersw  46275  elaa2lem  46277  etransclem3  46281  etransclem4  46282  etransclem7  46285  etransclem10  46288  etransclem15  46293  etransclem19  46297  etransclem23  46301  etransclem24  46302  etransclem25  46303  etransclem27  46305  etransclem31  46309  etransclem32  46310  etransclem35  46313  etransclem41  46319  etransclem44  46322  etransclem46  46324  etransclem48  46326  iundjiun  46504  caratheodorylem1  46570  smflimsuplem4  46867  smfliminflem  46874  ormklocald  46918  ormkglobd  46919  natglobalincr  46921  2elfz2melfz  47355  elfzelfzlble  47358  fzopredsuc  47360  2ltceilhalf  47365  ceilhalfgt1  47366  ceilhalfnn  47373  submodlt  47387  m1modmmod  47395  difmodm1lt  47396  modmknepk  47399  mod2addne  47401  fsummsndifre  47409  iccpartgt  47464  icceuelpartlem  47472  icceuelpart  47473  iccpartnel  47475  lighneallem2  47643  proththd  47651  dfodd4  47696  oexpnegALTV  47714  nnoALTV  47732  evenltle  47754  fpprwppr  47776  gbowgt5  47799  gboge9  47801  stgoldbwt  47813  sbgoldbst  47815  sbgoldbalt  47818  sgoldbeven3prm  47820  mogoldbb  47822  bgoldbtbndlem1  47842  bgoldbtbndlem2  47843  bgoldbtbndlem3  47844  bgoldbtbnd  47846  bgoldbachlt  47850  tgblthelfgott  47852  tgoldbach  47854  upgrimpthslem2  47945  gpgprismgrusgra  48095  gpgedgvtx1  48099  gpgvtxedg0  48100  gpgvtxedg1  48101  gpg5nbgrvtx13starlem2  48109  gpg3nbgrvtx0  48113  gpg3kgrtriexlem1  48120  gpg3kgrtriexlem4  48123  gpg3kgrtriexlem6  48125  pw2m1lepw2m1  48558  fllogbd  48598  logbpw2m1  48605  fllog2  48606  nnpw2blen  48618  nnolog2flm1  48628  dignn0flhalflem1  48653  dignn0flhalflem2  48654