Theorem zred 12691

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

Syntax hints:   → wi 4   ∈ wcel 2145  ℝcr 11087  ℤcz 12582

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1818  ax-4 1832  ax-5 1933  ax-6 1990  ax-7 2031  ax-8 2147  ax-9 2155  ax-ext 2737

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3or 1102  df-3an 1103  df-tru 1566  df-fal 1576  df-ex 1803  df-sb 2094  df-clab 2744  df-cleq 2757  df-clel 2840  df-rab 3418  df-v 3459  df-dif 3910  df-un 3912  df-ss 3924  df-nul 4289  df-if 4484  df-sn 4586  df-pr 4588  df-op 4592  df-uni 4869  df-br 5106  df-iota 6481  df-fv 6533  df-ov 7403  df-neg 11432  df-z 12583

This theorem is referenced by:  zcnd  12692  suprfinzcl  12701  eluzmn  12860  eluzelre  12864  eluzadd  12882  subeluzsub  12886  uzm1  12887  zsupss  12952  suprzcl2  12953  uzwo3  12958  rpnnen1lem3  12994  rpnnen1lem5  12996  zltaddlt1le  13523  fzsplit2  13568  fzdisj  13570  ssfzunsnext  13588  fzpreddisj  13592  fznatpl1  13597  fzp1disj  13602  uzdisj  13616  fzdif1  13624  fzm1  13626  fz0fzdiffz0  13656  elfzmlbm  13657  elfzmlbp  13658  difelfznle  13661  nn0disj  13663  elfzolt3  13689  fzonel  13693  fzospliti  13711  fzodisj  13713  fzouzdisj  13715  fzodisjsn  13717  elfzo0subge1  13725  elfzo0suble  13726  fzonmapblen  13728  fzoaddel  13737  elincfzoext  13743  fzone1  13804  reflcl  13820  flge  13829  flwordi  13836  fladdz  13849  2tnp1ge0ge0  13853  flhalf  13854  fldiv4p1lem1div2  13859  fldiv4lem1div2uz2  13860  fldiv4lem1div2  13861  flleceil  13877  fleqceilz  13878  quoremz  13879  uzsup  13887  modaddid  13934  modmul12d  13952  modaddmodup  13961  modaddmodlo  13962  modfzo0difsn  13970  modsumfzodifsn  13971  addmodlteq  13973  om2uzlti  13977  om2uzf1oi  13980  seqf1olem1  14068  seqf1olem2  14069  bcval4  14334  bcp1nk  14344  bcval5  14345  fzsdom2  14455  seqcoll  14491  seqcoll2  14492  ccatrn  14617  ccatalpha  14621  cshwidxmodr  14831  fzomaxdiflem  15384  fzomaxdif  15385  rexuzre  15394  limsupgre  15522  rlimclim1  15586  isercoll  15709  iseralt  15726  fsumm1  15792  fsum1p  15794  fsum0diaglem  15817  modfsummods  15835  isumsplit  15884  climcndslem1  15893  mertenslem1  15928  ntrivcvgmul  15946  fprodntriv  15986  fprod1p  16012  fprodeq0  16019  fallfacval4  16087  bpoly4  16103  fzo0dvdseq  16371  dvdsmod  16377  oexpneg  16393  mod2eq1n2dvds  16395  ltoddhalfle  16409  flodddiv4t2lthalf  16466  bitsp1  16479  bitsfzolem  16482  bitsfzo  16483  bitsmod  16484  bitscmp  16486  bitsinv1lem  16489  sadaddlem  16514  bitsres  16521  bitsuz  16522  smumul  16541  gcd0id  16567  gcdneg  16570  dfgcd2  16594  nn0seqcvgd  16618  lcmgcdlem  16654  nprm  16736  prmdvdsfz  16754  isprm5  16756  isprm7  16757  coprm  16760  prmexpb  16768  prmfac1  16769  hashdvds  16824  crth  16827  eulerthlem2  16831  fermltl  16833  prmdiv  16834  prmdiveq  16835  hashgcdlem  16837  odzdvds  16845  vfermltlALT  16852  modprm0  16855  modprmn0modprm0  16857  prm23ge5  16865  pythagtriplem13  16877  pcxcl  16911  pcaddlem  16938  pcadd  16939  pcfac  16949  qexpz  16951  prmunb  16964  1arithlem4  16976  4sqlem5  16992  4sqlem6  16993  4sqlem7  16994  4sqlem10  16997  4sqlem11  17005  4sqlem12  17006  4sqlem15  17009  4sqlem16  17010  4sqlem17  17011  vdwnnlem3  17047  prmgaplem7  17107  cshwshashlem3  17147  chnub  18668  chnso  18670  chnccat  18672  chnpof1  18676  subgmulg  19198  mndodconglem  19602  odnncl  19606  odmod  19607  oddvds  19608  dfod2  19625  sylow1lem3  19661  efgsp1  19798  efgredleme  19804  telgsumfzs  20050  zringlpirlem1  21572  zringlpirlem3  21574  fermltlchr  21639  znf1o  21661  zcld  24932  ovoliunlem1  25622  ovoliunlem2  25623  dyadss  25714  dyaddisjlem  25715  dyadmaxlem  25717  dvfsumle  26141  dvfsumge  26142  dvfsumabs  26143  dvfsumlem1  26146  dvfsumlem3  26148  degltlem1  26190  plyco0  26310  plyeq0lem  26328  plydivex  26419  aannenlem1  26450  efif1olem2  26666  nnlogbexp  26904  logblt  26907  ang180lem1  26932  ang180lem3  26934  wilthlem2  27191  basellem3  27205  basellem4  27206  ppiprm  27273  chtdif  27280  ppidif  27285  chtub  27334  mersenne  27349  bcmono  27399  bcmax  27400  bposlem1  27406  bposlem3  27408  bposlem5  27410  bposlem6  27411  lgsval2lem  27429  lgsvalmod  27438  lgsneg  27443  lgsmod  27445  lgsdilem  27446  lgsdirprm  27453  lgsdilem2  27455  lgsne0  27457  lgssq  27459  lgssq2  27460  lgsqr  27473  lgsdchr  27477  gausslemma2dlem1a  27487  gausslemma2dlem3  27490  gausslemma2dlem5a  27492  gausslemma2dlem6  27494  gausslemma2d  27496  lgseisenlem1  27497  lgseisenlem2  27498  lgseisenlem3  27499  lgseisenlem4  27500  lgsquadlem1  27502  lgsquadlem2  27503  lgsquadlem3  27504  lgsquad3  27509  2lgslem1a2  27512  2lgslem1  27516  2lgslem2  27517  2sqlem3  27542  2sqlem8  27548  2sqblem  27553  2sqmod  27558  chebbnd1lem1  27591  chebbnd1lem2  27592  chebbnd1lem3  27593  dchrmusum2  27616  dchrvmasumlem1  27617  dchrvmasum2lem  27618  dchrvmasum2if  27619  dchrvmasumlem3  27621  dchrvmasumiflem2  27624  dchrisum0lem1  27638  dchrmusumlem  27644  mudivsum  27652  mulogsumlem  27653  mulogsum  27654  mulog2sumlem2  27657  mulog2sumlem3  27658  selberglem1  27667  selberglem2  27668  pntpbnd1  27708  pntlemg  27720  pntlemf  27727  qabvle  27747  padicabv  27752  padicabvcxp  27754  ostth2lem2  27756  axlowdimlem13  29213  axlowdimlem16  29216  pthdlem1  30024  crctcshwlkn0  30079  crctcsh  30082  clwwisshclwwslemlem  30273  eucrctshift  30503  nndiffz1  33043  fzsplit3  33050  bcm1n  33052  suppssnn0  33062  ltesubnnd  33080  wrdt2ind  33186  cshwrnid  33194  cycpmfv2  33347  cycpmco2lem6  33364  cycpmco2lem7  33365  cycpmrn  33376  cyc3conja  33390  pnfinf  33416  znfermltl  33596  constrext2chnlem  34057  cos9thpiminplylem1  34089  cos9thpiminplylem2  34090  dya2iocress  34581  dya2iocbrsiga  34582  dya2icobrsiga  34583  dya2icoseg  34584  dya2iocucvr  34591  sxbrsigalem2  34593  ballotlemfc0  34800  ballotlemfcc  34801  ballotlemodife  34805  ballotlemimin  34813  ballotlemsgt1  34818  ballotlemsel1i  34820  ballotlemsi  34822  ballotlemsima  34823  ballotlemrv2  34829  ballotlemfrceq  34836  ballotlemfrcn0  34837  ballotlemirc  34839  fsum2dsub  34911  reprlt  34923  reprgt  34925  breprexplemc  34936  tgoldbachgnn  34963  tgoldbachgt  34967  subfacval3  35552  erdszelem8  35561  erdszelem9  35562  supfz  36092  inffz  36093  dnizeq0  36926  dnizphlfeqhlf  36927  dnibndlem13  36941  knoppndvlem1  36963  knoppndvlem2  36964  knoppndvlem7  36969  knoppndvlem19  36981  knoppndvlem21  36983  ltflcei  38119  leceifl  38120  poimirlem1  38132  poimirlem2  38133  poimirlem6  38137  poimirlem7  38138  poimirlem8  38139  poimirlem15  38146  poimirlem16  38147  poimirlem17  38148  poimirlem19  38150  poimirlem20  38151  poimirlem23  38154  poimirlem24  38155  poimirlem27  38158  poimirlem29  38160  poimirlem31  38162  poimirlem32  38163  mblfinlem2  38169  itg2addnclem2  38183  mettrifi  38268  cntotbnd  38307  fzne2d  42609  aks4d1lem1  42691  aks4d1p1p3  42698  aks4d1p1p2  42699  aks4d1p1p4  42700  aks4d1p1  42705  aks4d1p2  42706  aks4d1p3  42707  aks4d1p5  42709  aks4d1p6  42710  aks4d1p7d1  42711  aks4d1p7  42712  aks4d1p8d3  42715  aks4d1p8  42716  aks4d1p9  42717  posbezout  42729  aks6d1c1  42745  hashscontpow1  42750  hashscontpow  42751  aks6d1c2  42759  aks6d1c5lem1  42765  2ap1caineq  42774  sticksstones6  42780  sticksstones7  42781  sticksstones10  42784  sticksstones12a  42786  sticksstones12  42787  sticksstones22  42797  bcled  42807  bcle2d  42808  aks6d1c7lem1  42809  aks6d1c7lem2  42810  aks6d1c7  42813  aks5lem6  42821  unitscyglem2  42825  unitscyglem4  42827  aks5lem8  42830  sumcubes  42934  frlmvscadiccat  43140  dffltz  43228  lzunuz  43361  lzenom  43363  diophin  43365  irrapxlem1  43411  irrapxlem2  43412  irrapxlem3  43413  irrapxlem4  43414  pellexlem5  43422  pellexlem6  43423  rmspecfund  43498  rmxypos  43536  ltrmynn0  43537  ltrmxnn0  43538  ltrmy  43541  rmyeq0  43542  rmyeq  43543  lermy  43544  rmyabs  43547  jm2.24nn  43548  jm2.17a  43549  jm2.17b  43550  jm2.17c  43551  jm2.24  43552  rmygeid  43553  acongrep  43569  fzmaxdif  43570  acongeq  43572  jm2.22  43584  jm2.23  43585  jm2.26lem3  43590  jm2.27a  43594  jm3.1lem1  43606  jm3.1lem3  43608  expdiophlem1  43610  fzuntd  44044  fzunt1d  44045  fzuntgd  44046  prmunb2  44885  nzprmdif  44893  hashnzfzclim  44896  binomcxplemnn0  44923  uzwo4  45631  ssinc  45663  ssdec  45664  zltlesub  45862  monoords  45874  fzisoeu  45877  fperiodmul  45881  fzdifsuc2  45887  iuneqfzuzlem  45908  uzublem  46002  zxrd  46025  uzinico  46133  uzubioo  46139  fmul01  46154  fmul01lt1lem1  46158  fmul01lt1lem2  46159  climsuselem1  46181  climsuse  46182  sumnnodd  46204  ltmod  46210  limsupresuz  46275  limsupubuzlem  46284  limsupequzlem  46294  limsupmnfuzlem  46298  limsupequzmptlem  46300  limsupre3uzlem  46307  supcnvlimsup  46312  limsup10exlem  46344  liminfresuz  46356  liminfvaluz  46364  limsupvaluz3  46370  ioodvbdlimc1lem2  46504  ioodvbdlimc2lem  46506  dvnmul  46515  dvnprodlem1  46518  dvnprodlem2  46519  iblspltprt  46545  itgspltprt  46551  stoweidlem3  46575  stoweidlem11  46583  stoweidlem20  46592  stoweidlem26  46598  stoweidlem34  46606  stoweidlem59  46631  stirlinglem5  46650  dirkertrigeqlem3  46672  dirkeritg  46674  dirkercncflem1  46675  dirkercncflem2  46676  dirkercncflem4  46678  fourierdlem4  46683  fourierdlem6  46685  fourierdlem7  46686  fourierdlem11  46690  fourierdlem12  46691  fourierdlem15  46694  fourierdlem19  46698  fourierdlem20  46699  fourierdlem25  46704  fourierdlem26  46705  fourierdlem34  46713  fourierdlem35  46714  fourierdlem41  46720  fourierdlem48  46726  fourierdlem49  46727  fourierdlem50  46728  fourierdlem51  46729  fourierdlem54  46732  fourierdlem63  46741  fourierdlem64  46742  fourierdlem65  46743  fourierdlem71  46749  fourierdlem79  46757  fourierdlem89  46767  fourierdlem90  46768  fourierdlem91  46769  fourierdlem102  46780  fourierdlem103  46781  fourierdlem104  46782  fourierdlem114  46792  fouriersw  46803  elaa2lem  46805  etransclem3  46809  etransclem4  46810  etransclem7  46813  etransclem10  46816  etransclem15  46821  etransclem19  46825  etransclem23  46829  etransclem24  46830  etransclem25  46831  etransclem27  46833  etransclem31  46837  etransclem32  46838  etransclem35  46841  etransclem41  46847  etransclem44  46850  etransclem46  46852  etransclem48  46854  iundjiun  47032  caratheodorylem1  47098  hoicvr  47120  smflimsuplem4  47395  smfliminflem  47402  ormklocald  47448  ormkglobd  47449  natglobalincr  47451  chnerlem3  47458  2elfz2melfz  47910  elfzelfzlble  47913  fzopredsuc  47916  nnmul2  47922  2ltceilhalf  47924  ceilhalfgt1  47925  ceilhalfnn  47932  submodlt  47948  m1modmmod  47956  difmodm1lt  47957  modmknepk  47960  mod2addne  47962  2timesltsq  47970  2timesltsqm1  47971  fsummsndifre  47972  iccpartgt  48031  icceuelpartlem  48039  icceuelpart  48040  iccpartnel  48042  nprmmul2  48132  nprmmul3  48133  lighneallem2  48213  proththd  48221  nprmdvdsfacm1lem4  48230  dfodd4  48279  oexpnegALTV  48297  nnoALTV  48315  evenltle  48337  fpprwppr  48359  gbowgt5  48382  gboge9  48384  stgoldbwt  48396  sbgoldbst  48398  sbgoldbalt  48401  sgoldbeven3prm  48403  mogoldbb  48405  bgoldbtbndlem1  48425  bgoldbtbndlem2  48426  bgoldbtbndlem3  48427  bgoldbtbnd  48429  bgoldbachlt  48433  tgblthelfgott  48435  tgoldbach  48437  upgrimpthslem2  48528  gpgprismgrusgra  48678  gpgedgvtx1  48682  gpgvtxedg0  48683  gpgvtxedg1  48684  gpg5nbgrvtx13starlem2  48692  gpg3nbgrvtx0  48696  gpg3kgrtriexlem1  48703  gpg3kgrtriexlem4  48706  gpg3kgrtriexlem6  48708  pw2m1lepw2m1  49151  fllogbd  49191  logbpw2m1  49198  fllog2  49199  nnpw2blen  49211  nnolog2flm1  49221  dignn0flhalflem1  49246  dignn0flhalflem2  49247