Theorem zred 12833

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

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2147  ℝcr 11229  ℤcz 12723

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-ext 2735

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3or 1104  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-sb 2102  df-clab 2742  df-cleq 2755  df-clel 2839  df-rab 3417  df-v 3456  df-ss 3901  df-dif 4050  df-un 4154  df-nul 4282  df-if 4486  df-sn 4589  df-pr 4591  df-op 4839  df-uni 4871  df-br 5107  df-iota 6515  df-fv 6569  df-ov 7449  df-neg 11574  df-z 12724

This theorem is used by:  zcnd  12834  suprfinzcl  12843  eluzmn  13002  eluzelre  13006  eluzadd  13024  subeluzsub  13028  uzm1  13029  zsupss  13094  suprzcl2  13095  uzwo3  13100  rpnnen1lem3  13137  rpnnen1lem5  13139  zltaddlt1le  13666  fzsplit2  13713  fzdisj  13715  ssfzunsnext  13733  fzpreddisj  13737  fznatpl1  13742  fzp1disj  13747  uzdisj  13761  fzdif1  13769  fzm1  13771  fz0fzdiffz0  13801  elfzmlbm  13802  elfzmlbp  13803  difelfznle  13806  nn0disj  13808  elfzolt3  13834  fzonel  13838  fzospliti  13856  fzodisj  13858  fzouzdisj  13860  fzodisjsn  13862  elfzo0subge1  13870  elfzo0suble  13871  fzonmapblen  13873  fzoaddel  13882  elincfzoext  13888  fzone1  13949  reflcl  13966  flge  13975  flwordi  13982  fladdz  13995  2tnp1ge0ge0  13999  flhalf  14000  fldiv4p1lem1div2  14005  fldiv4lem1div2uz2  14006  fldiv4lem1div2  14007  flleceil  14023  fleqceilz  14024  quoremz  14025  uzsup  14033  modaddid  14080  modmul12d  14098  modaddmodup  14107  modaddmodlo  14108  modfzo0difsn  14116  modsumfzodifsn  14117  addmodlteq  14119  om2uzlti  14123  om2uzf1oi  14126  seqf1olem1  14214  seqf1olem2  14215  bcval4  14481  bcp1nk  14491  bcval5  14492  fzsdom2  14603  seqcoll  14639  seqcoll2  14640  ccatrn  14765  ccatalpha  14770  cshwidxmodr  14986  fzomaxdiflem  15542  fzomaxdif  15543  rexuzre  15552  limsupgre  15680  rlimclim1  15744  isercoll  15867  iseralt  15884  fsumm1  15949  fsum1p  15951  fsum0diaglem  15974  modfsummods  15992  isumsplit  16041  climcndslem1  16050  mertenslem1  16085  ntrivcvgmul  16103  fprodntriv  16141  fprod1p  16167  fprodeq0  16174  fallfacval4  16241  bpoly4  16257  fzo0dvdseq  16525  dvdsmod  16531  oexpneg  16547  mod2eq1n2dvds  16549  ltoddhalfle  16563  flodddiv4t2lthalf  16620  bitsp1  16633  bitsfzolem  16636  bitsfzo  16637  bitsmod  16638  bitscmp  16640  bitsinv1lem  16643  sadaddlem  16668  bitsres  16675  bitsuz  16676  smumul  16695  gcd0id  16723  gcdneg  16726  dfgcd2  16751  nn0seqcvgd  16777  lcmgcdlem  16813  nprm  16895  prmdvdsfz  16913  isprm5  16915  isprm7  16916  coprm  16919  prmexpb  16927  prmfac1  16928  hashdvds  16984  crth  16987  eulerthlem2  16991  fermltl  16993  prmdiv  16994  prmdiveq  16995  hashgcdlem  16997  odzdvds  17005  vfermltlALT  17012  modprm0  17015  modprmn0modprm0  17017  prm23ge5  17025  pythagtriplem13  17037  pcxcl  17071  pcaddlem  17098  pcadd  17099  pcfac  17109  qexpz  17111  prmunb  17124  1arithlem4  17136  4sqlem5  17152  4sqlem6  17153  4sqlem7  17154  4sqlem10  17157  4sqlem11  17165  4sqlem12  17166  4sqlem15  17169  4sqlem16  17170  4sqlem17  17171  vdwnnlem3  17207  prmgaplem7  17267  cshwshashlem3  17307  chnub  18828  chnso  18830  chnccat  18832  chnpof1  18836  subgmulg  19383  mndodconglem  19788  odnncl  19792  odmod  19793  oddvds  19794  dfod2  19811  sylow1lem3  19847  efgsp1  19984  efgredleme  19990  telgsumfzs  20236  zringlpirlem1  21801  zringlpirlem3  21803  fermltlchr  21868  znf1o  21890  zcld  25166  ovoliunlem1  25856  ovoliunlem2  25857  dyadss  25948  dyaddisjlem  25949  dyadmaxlem  25951  dvfsumle  26374  dvfsumge  26375  dvfsumabs  26376  dvfsumlem1  26379  dvfsumlem3  26381  degltlem1  26423  plyco0  26543  plyeq0lem  26562  plydivex  26651  aannenlem1  26688  efif1olem2  26904  nnlogbexp  27142  logblt  27145  ang180lem1  27170  ang180lem3  27172  wilthlem2  27429  basellem3  27443  basellem4  27444  ppiprm  27511  chtdif  27518  ppidif  27523  chtub  27572  mersenne  27587  bcmono  27637  bcmax  27638  bposlem1  27644  bposlem3  27646  bposlem5  27648  bposlem6  27649  lgsval2lem  27667  lgsvalmod  27676  lgsneg  27681  lgsmod  27683  lgsdilem  27684  lgsdirprm  27691  lgsdilem2  27693  lgsne0  27695  lgssq  27697  lgssq2  27698  lgsqr  27711  lgsdchr  27715  gausslemma2dlem1a  27725  gausslemma2dlem3  27728  gausslemma2dlem5a  27730  gausslemma2dlem6  27732  gausslemma2d  27734  lgseisenlem1  27735  lgseisenlem2  27736  lgseisenlem3  27737  lgseisenlem4  27738  lgsquadlem1  27740  lgsquadlem2  27741  lgsquadlem3  27742  lgsquad3  27747  2lgslem1a2  27750  2lgslem1  27754  2lgslem2  27755  2sqlem3  27780  2sqlem8  27786  2sqblem  27791  2sqmod  27796  chebbnd1lem1  27829  chebbnd1lem2  27830  chebbnd1lem3  27831  dchrmusum2  27854  dchrvmasumlem1  27855  dchrvmasum2lem  27856  dchrvmasum2if  27857  dchrvmasumlem3  27859  dchrvmasumiflem2  27862  dchrisum0lem1  27876  dchrmusumlem  27882  mudivsum  27890  mulogsumlem  27891  mulogsum  27892  mulog2sumlem2  27895  mulog2sumlem3  27896  selberglem1  27905  selberglem2  27906  pntpbnd1  27946  pntlemg  27958  pntlemf  27965  qabvle  27985  padicabv  27990  padicabvcxp  27992  ostth2lem2  27994  axlowdimlem13  29565  axlowdimlem16  29568  pthdlem1  30385  crctcshwlkn0  30443  crctcsh  30446  clwwisshclwwslemlem  30637  eucrctshift  30877  nndiffz1  33451  fzsplit3  33458  bcm1n  33460  suppssnn0  33470  ltesubnnd  33487  wrdt2ind  33589  cshwrnid  33595  cycpmfv2  33751  cycpmco2lem6  33768  cycpmco2lem7  33769  cycpmrn  33780  cyc3conja  33794  pnfinf  33820  zzedom  33939  znfermltl  34006  constrext2chnlem  34465  cos9thpiminplylem1  34497  cos9thpiminplylem2  34498  dya2iocress  34989  dya2iocbrsiga  34990  dya2icobrsiga  34991  dya2icoseg  34992  dya2iocucvr  34999  sxbrsigalem2  35001  ballotlemfc0  35208  ballotlemfcc  35209  ballotlemodife  35213  ballotlemimin  35221  ballotlemsgt1  35226  ballotlemsel1i  35228  ballotlemsi  35230  ballotlemsima  35231  ballotlemrv2  35237  ballotlemfrceq  35244  ballotlemfrcn0  35245  ballotlemirc  35247  fsum2dsub  35319  reprlt  35331  reprgt  35333  breprexplemc  35344  tgoldbachgnn  35371  tgoldbachgt  35375  subfacval3  36134  erdszelem8  36143  erdszelem9  36144  supfz  36685  inffz  36686  dnizeq0  37532  dnizphlfeqhlf  37533  dnibndlem13  37547  knoppndvlem1  37569  knoppndvlem2  37570  knoppndvlem7  37575  knoppndvlem19  37587  knoppndvlem21  37589  ltflcei  38736  leceifl  38737  poimirlem1  38744  poimirlem2  38745  poimirlem6  38749  poimirlem7  38750  poimirlem8  38751  poimirlem15  38758  poimirlem16  38759  poimirlem17  38760  poimirlem19  38762  poimirlem20  38763  poimirlem23  38766  poimirlem24  38767  poimirlem27  38770  poimirlem29  38772  poimirlem31  38774  poimirlem32  38775  mblfinlem2  38781  itg2addnclem2  38795  mettrifi  38894  cntotbnd  38933  fzne2d  43233  aks4d1lem1  43315  aks4d1p1p3  43322  aks4d1p1p2  43323  aks4d1p1p4  43324  aks4d1p1  43329  aks4d1p2  43330  aks4d1p3  43331  aks4d1p5  43333  aks4d1p6  43334  aks4d1p7d1  43335  aks4d1p7  43336  aks4d1p8d3  43339  aks4d1p8  43340  aks4d1p9  43341  posbezout  43353  aks6d1c1  43369  hashscontpow1  43374  hashscontpow  43375  aks6d1c2  43383  aks6d1c5lem1  43389  2ap1caineq  43398  sticksstones6  43404  sticksstones7  43405  sticksstones10  43408  sticksstones12a  43410  sticksstones12  43411  sticksstones22  43421  bcled  43431  bcle2d  43432  aks6d1c7lem1  43433  aks6d1c7lem2  43434  aks6d1c7  43437  aks5lem6  43445  unitscyglem2  43449  unitscyglem4  43451  aks5lem8  43454  sumcubes  43574  frlmvscadiccat  43777  dffltz  43874  lzunuz  43983  lzenom  43985  diophin  43987  irrapxlem1  44033  irrapxlem2  44034  irrapxlem3  44035  irrapxlem4  44036  pellexlem5  44044  pellexlem6  44045  rmspecfund  44120  rmxypos  44158  ltrmynn0  44159  ltrmxnn0  44160  ltrmy  44163  rmyeq0  44164  rmyeq  44165  lermy  44166  rmyabs  44169  jm2.24nn  44170  jm2.17a  44171  jm2.17b  44172  jm2.17c  44173  jm2.24  44174  rmygeid  44175  acongrep  44191  fzmaxdif  44192  acongeq  44194  jm2.22  44206  jm2.23  44207  jm2.26lem3  44212  jm2.27a  44216  jm3.1lem1  44228  jm3.1lem3  44230  expdiophlem1  44232  fzuntd  44660  fzunt1d  44661  fzuntgd  44662  prmunb2  45498  nzprmdif  45506  hashnzfzclim  45509  binomcxplemnn0  45536  uzwo4  46286  ssinc  46317  ssdec  46318  zltlesub  46516  monoords  46528  fzisoeu  46531  fperiodmul  46535  fzdifsuc2  46541  iuneqfzuzlem  46561  uzublem  46655  zxrd  46678  uzinico  46786  uzubioo  46792  fmul01  46807  fmul01lt1lem1  46811  fmul01lt1lem2  46812  climsuselem1  46834  climsuse  46835  sumnnodd  46857  ltmod  46863  limsupresuz  46928  limsupubuzlem  46937  limsupequzlem  46947  limsupmnfuzlem  46951  limsupequzmptlem  46953  limsupre3uzlem  46960  supcnvlimsup  46965  limsup10exlem  46997  liminfresuz  47009  liminfvaluz  47017  limsupvaluz3  47023  ioodvbdlimc1lem2  47157  ioodvbdlimc2lem  47159  dvnmul  47168  dvnprodlem1  47171  dvnprodlem2  47172  iblspltprt  47198  itgspltprt  47204  stoweidlem3  47228  stoweidlem11  47236  stoweidlem20  47245  stoweidlem26  47251  stoweidlem34  47259  stoweidlem59  47284  stirlinglem5  47303  dirkertrigeqlem3  47325  dirkeritg  47327  dirkercncflem1  47328  dirkercncflem2  47329  dirkercncflem4  47331  fourierdlem4  47336  fourierdlem6  47338  fourierdlem7  47339  fourierdlem11  47343  fourierdlem12  47344  fourierdlem15  47347  fourierdlem19  47351  fourierdlem20  47352  fourierdlem25  47357  fourierdlem26  47358  fourierdlem34  47366  fourierdlem35  47367  fourierdlem41  47373  fourierdlem48  47379  fourierdlem49  47380  fourierdlem50  47381  fourierdlem51  47382  fourierdlem54  47385  fourierdlem63  47394  fourierdlem64  47395  fourierdlem65  47396  fourierdlem71  47402  fourierdlem79  47410  fourierdlem89  47420  fourierdlem90  47421  fourierdlem91  47422  fourierdlem102  47433  fourierdlem103  47434  fourierdlem104  47435  fourierdlem114  47445  fouriersw  47456  elaa2lem  47458  etransclem3  47462  etransclem4  47463  etransclem7  47466  etransclem10  47469  etransclem15  47474  etransclem19  47478  etransclem23  47482  etransclem24  47483  etransclem25  47484  etransclem27  47486  etransclem31  47490  etransclem32  47491  etransclem35  47494  etransclem41  47500  etransclem44  47503  etransclem46  47505  etransclem48  47507  iundjiun  47685  caratheodorylem1  47751  hoicvr  47773  smflimsuplem4  48048  smfliminflem  48055  ormklocald  48101  ormkglobd  48102  chnerlem3  48109  2elfz2melfz  48603  elfzelfzlble  48606  fzopredsuc  48609  nnmul2  48615  2ltceilhalf  48617  ceilhalfgt1  48618  ceilhalfnn  48625  submodlt  48641  m1modmmod  48649  difmodm1lt  48650  modmknepk  48653  mod2addne  48655  2timesltsq  48663  2timesltsqm1  48664  fsummsndifre  48665  iccpartgt  48724  icceuelpartlem  48732  icceuelpart  48733  iccpartnel  48735  nprmmul2  48825  nprmmul3  48826  lighneallem2  48906  proththd  48914  nprmdvdsfacm1lem4  48923  dfodd4  48972  oexpnegALTV  48990  nnoALTV  49008  evenltle  49030  fpprwppr  49052  gbowgt5  49075  gboge9  49077  stgoldbwt  49089  sbgoldbst  49091  sbgoldbalt  49094  sgoldbeven3prm  49096  mogoldbb  49098  bgoldbtbndlem1  49118  bgoldbtbndlem2  49119  bgoldbtbndlem3  49120  bgoldbtbnd  49122  bgoldbachlt  49126  tgblthelfgott  49128  tgoldbach  49130  upgrimpthslem2  49221  gpgprismgrusgra  49371  gpgedgvtx1  49375  gpgvtxedg0  49376  gpgvtxedg1  49377  gpg5nbgrvtx13starlem2  49385  gpg3nbgrvtx0  49389  gpg3kgrtriexlem1  49396  gpg3kgrtriexlem4  49399  gpg3kgrtriexlem6  49401  pw2m1lepw2m1  49847  fllogbd  49887  logbpw2m1  49894  fllog2  49895  nnpw2blen  49907  nnolog2flm1  49917  dignn0flhalflem1  49942  dignn0flhalflem2  49943