Theorem zred 12701

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

Syntax hints:   → wi 4   ∈ wcel 2143  ℝcr 11100  ℤcz 12592

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-ext 2735

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3or 1104  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1810  df-sb 2097  df-clab 2742  df-cleq 2755  df-clel 2838  df-rab 3417  df-v 3457  df-dif 3909  df-un 3911  df-ss 3923  df-nul 4288  df-if 4489  df-sn 4591  df-pr 4593  df-op 4597  df-uni 4874  df-br 5111  df-iota 6494  df-fv 6546  df-ov 7415  df-neg 11445  df-z 12593

This theorem is referenced by:  zcnd  12702  suprfinzcl  12711  eluzmn  12870  eluzelre  12874  eluzadd  12892  subeluzsub  12896  uzm1  12897  zsupss  12962  suprzcl2  12963  uzwo3  12968  rpnnen1lem3  13004  rpnnen1lem5  13006  zltaddlt1le  13533  fzsplit2  13579  fzdisj  13581  ssfzunsnext  13599  fzpreddisj  13603  fznatpl1  13608  fzp1disj  13613  uzdisj  13627  fzdif1  13635  fzm1  13637  fz0fzdiffz0  13667  elfzmlbm  13668  elfzmlbp  13669  difelfznle  13672  nn0disj  13674  elfzolt3  13700  fzonel  13704  fzospliti  13722  fzodisj  13724  fzouzdisj  13726  fzodisjsn  13728  elfzo0subge1  13736  elfzo0suble  13737  fzonmapblen  13739  fzoaddel  13748  elincfzoext  13754  fzone1  13815  reflcl  13831  flge  13840  flwordi  13847  fladdz  13860  2tnp1ge0ge0  13864  flhalf  13865  fldiv4p1lem1div2  13870  fldiv4lem1div2uz2  13871  fldiv4lem1div2  13872  flleceil  13888  fleqceilz  13889  quoremz  13890  uzsup  13898  modaddid  13945  modmul12d  13963  modaddmodup  13972  modaddmodlo  13973  modfzo0difsn  13981  modsumfzodifsn  13982  addmodlteq  13984  om2uzlti  13988  om2uzf1oi  13991  seqf1olem1  14079  seqf1olem2  14080  bcval4  14345  bcp1nk  14355  bcval5  14356  fzsdom2  14467  seqcoll  14503  seqcoll2  14504  ccatrn  14629  ccatalpha  14633  cshwidxmodr  14843  fzomaxdiflem  15396  fzomaxdif  15397  rexuzre  15406  limsupgre  15534  rlimclim1  15598  isercoll  15721  iseralt  15738  fsumm1  15804  fsum1p  15806  fsum0diaglem  15829  modfsummods  15847  isumsplit  15896  climcndslem1  15905  mertenslem1  15940  ntrivcvgmul  15958  fprodntriv  15998  fprod1p  16024  fprodeq0  16031  fallfacval4  16098  bpoly4  16114  fzo0dvdseq  16382  dvdsmod  16388  oexpneg  16404  mod2eq1n2dvds  16406  ltoddhalfle  16420  flodddiv4t2lthalf  16477  bitsp1  16490  bitsfzolem  16493  bitsfzo  16494  bitsmod  16495  bitscmp  16497  bitsinv1lem  16500  sadaddlem  16525  bitsres  16532  bitsuz  16533  smumul  16552  gcd0id  16578  gcdneg  16581  dfgcd2  16605  nn0seqcvgd  16629  lcmgcdlem  16665  nprm  16747  prmdvdsfz  16765  isprm5  16767  isprm7  16768  coprm  16771  prmexpb  16779  prmfac1  16780  hashdvds  16835  crth  16838  eulerthlem2  16842  fermltl  16844  prmdiv  16845  prmdiveq  16846  hashgcdlem  16848  odzdvds  16856  vfermltlALT  16863  modprm0  16866  modprmn0modprm0  16868  prm23ge5  16876  pythagtriplem13  16888  pcxcl  16922  pcaddlem  16949  pcadd  16950  pcfac  16960  qexpz  16962  prmunb  16975  1arithlem4  16987  4sqlem5  17003  4sqlem6  17004  4sqlem7  17005  4sqlem10  17008  4sqlem11  17016  4sqlem12  17017  4sqlem15  17020  4sqlem16  17021  4sqlem17  17022  vdwnnlem3  17058  prmgaplem7  17118  cshwshashlem3  17158  chnub  18679  chnso  18681  chnccat  18683  chnpof1  18687  subgmulg  19208  mndodconglem  19612  odnncl  19616  odmod  19617  oddvds  19618  dfod2  19635  sylow1lem3  19671  efgsp1  19808  efgredleme  19814  telgsumfzs  20060  zringlpirlem1  21593  zringlpirlem3  21595  fermltlchr  21660  znf1o  21682  zcld  24952  ovoliunlem1  25642  ovoliunlem2  25643  dyadss  25734  dyaddisjlem  25735  dyadmaxlem  25737  dvfsumle  26161  dvfsumge  26162  dvfsumabs  26163  dvfsumlem1  26166  dvfsumlem3  26168  degltlem1  26210  plyco0  26330  plyeq0lem  26348  plydivex  26439  aannenlem1  26472  efif1olem2  26689  nnlogbexp  26927  logblt  26930  ang180lem1  26955  ang180lem3  26957  wilthlem2  27214  basellem3  27228  basellem4  27229  ppiprm  27296  chtdif  27303  ppidif  27308  chtub  27357  mersenne  27372  bcmono  27422  bcmax  27423  bposlem1  27429  bposlem3  27431  bposlem5  27433  bposlem6  27434  lgsval2lem  27452  lgsvalmod  27461  lgsneg  27466  lgsmod  27468  lgsdilem  27469  lgsdirprm  27476  lgsdilem2  27478  lgsne0  27480  lgssq  27482  lgssq2  27483  lgsqr  27496  lgsdchr  27500  gausslemma2dlem1a  27510  gausslemma2dlem3  27513  gausslemma2dlem5a  27515  gausslemma2dlem6  27517  gausslemma2d  27519  lgseisenlem1  27520  lgseisenlem2  27521  lgseisenlem3  27522  lgseisenlem4  27523  lgsquadlem1  27525  lgsquadlem2  27526  lgsquadlem3  27527  lgsquad3  27532  2lgslem1a2  27535  2lgslem1  27539  2lgslem2  27540  2sqlem3  27565  2sqlem8  27571  2sqblem  27576  2sqmod  27581  chebbnd1lem1  27614  chebbnd1lem2  27615  chebbnd1lem3  27616  dchrmusum2  27639  dchrvmasumlem1  27640  dchrvmasum2lem  27641  dchrvmasum2if  27642  dchrvmasumlem3  27644  dchrvmasumiflem2  27647  dchrisum0lem1  27661  dchrmusumlem  27667  mudivsum  27675  mulogsumlem  27676  mulogsum  27677  mulog2sumlem2  27680  mulog2sumlem3  27681  selberglem1  27690  selberglem2  27691  pntpbnd1  27731  pntlemg  27743  pntlemf  27750  qabvle  27770  padicabv  27775  padicabvcxp  27777  ostth2lem2  27779  axlowdimlem13  29285  axlowdimlem16  29288  pthdlem1  30096  crctcshwlkn0  30151  crctcsh  30154  clwwisshclwwslemlem  30345  eucrctshift  30575  nndiffz1  33112  fzsplit3  33119  bcm1n  33121  suppssnn0  33131  ltesubnnd  33148  wrdt2ind  33254  cshwrnid  33262  cycpmfv2  33415  cycpmco2lem6  33432  cycpmco2lem7  33433  cycpmrn  33444  cyc3conja  33458  pnfinf  33484  znfermltl  33662  constrext2chnlem  34121  cos9thpiminplylem1  34153  cos9thpiminplylem2  34154  dya2iocress  34645  dya2iocbrsiga  34646  dya2icobrsiga  34647  dya2icoseg  34648  dya2iocucvr  34655  sxbrsigalem2  34657  ballotlemfc0  34864  ballotlemfcc  34865  ballotlemodife  34869  ballotlemimin  34877  ballotlemsgt1  34882  ballotlemsel1i  34884  ballotlemsi  34886  ballotlemsima  34887  ballotlemrv2  34893  ballotlemfrceq  34900  ballotlemfrcn0  34901  ballotlemirc  34903  fsum2dsub  34975  reprlt  34987  reprgt  34989  breprexplemc  35000  tgoldbachgnn  35027  tgoldbachgt  35031  subfacval3  35662  erdszelem8  35671  erdszelem9  35672  supfz  36202  inffz  36203  dnizeq0  37045  dnizphlfeqhlf  37046  dnibndlem13  37060  knoppndvlem1  37082  knoppndvlem2  37083  knoppndvlem7  37088  knoppndvlem19  37100  knoppndvlem21  37102  ltflcei  38240  leceifl  38241  poimirlem1  38253  poimirlem2  38254  poimirlem6  38258  poimirlem7  38259  poimirlem8  38260  poimirlem15  38267  poimirlem16  38268  poimirlem17  38269  poimirlem19  38271  poimirlem20  38272  poimirlem23  38275  poimirlem24  38276  poimirlem27  38279  poimirlem29  38281  poimirlem31  38283  poimirlem32  38284  mblfinlem2  38290  itg2addnclem2  38304  mettrifi  38389  cntotbnd  38428  fzne2d  42728  aks4d1lem1  42810  aks4d1p1p3  42817  aks4d1p1p2  42818  aks4d1p1p4  42819  aks4d1p1  42824  aks4d1p2  42825  aks4d1p3  42826  aks4d1p5  42828  aks4d1p6  42829  aks4d1p7d1  42830  aks4d1p7  42831  aks4d1p8d3  42834  aks4d1p8  42835  aks4d1p9  42836  posbezout  42848  aks6d1c1  42864  hashscontpow1  42869  hashscontpow  42870  aks6d1c2  42878  aks6d1c5lem1  42884  2ap1caineq  42893  sticksstones6  42899  sticksstones7  42900  sticksstones10  42903  sticksstones12a  42905  sticksstones12  42906  sticksstones22  42916  bcled  42926  bcle2d  42927  aks6d1c7lem1  42928  aks6d1c7lem2  42929  aks6d1c7  42932  aks5lem6  42940  unitscyglem2  42944  unitscyglem4  42946  aks5lem8  42949  sumcubes  43055  frlmvscadiccat  43261  dffltz  43349  lzunuz  43482  lzenom  43484  diophin  43486  irrapxlem1  43532  irrapxlem2  43533  irrapxlem3  43534  irrapxlem4  43535  pellexlem5  43543  pellexlem6  43544  rmspecfund  43619  rmxypos  43657  ltrmynn0  43658  ltrmxnn0  43659  ltrmy  43662  rmyeq0  43663  rmyeq  43664  lermy  43665  rmyabs  43668  jm2.24nn  43669  jm2.17a  43670  jm2.17b  43671  jm2.17c  43672  jm2.24  43673  rmygeid  43674  acongrep  43690  fzmaxdif  43691  acongeq  43693  jm2.22  43705  jm2.23  43706  jm2.26lem3  43711  jm2.27a  43715  jm3.1lem1  43727  jm3.1lem3  43729  expdiophlem1  43731  fzuntd  44165  fzunt1d  44166  fzuntgd  44167  prmunb2  45004  nzprmdif  45012  hashnzfzclim  45015  binomcxplemnn0  45042  uzwo4  45756  ssinc  45788  ssdec  45789  zltlesub  45987  monoords  45999  fzisoeu  46002  fperiodmul  46006  fzdifsuc2  46012  iuneqfzuzlem  46033  uzublem  46127  zxrd  46150  uzinico  46258  uzubioo  46264  fmul01  46279  fmul01lt1lem1  46283  fmul01lt1lem2  46284  climsuselem1  46306  climsuse  46307  sumnnodd  46329  ltmod  46335  limsupresuz  46400  limsupubuzlem  46409  limsupequzlem  46419  limsupmnfuzlem  46423  limsupequzmptlem  46425  limsupre3uzlem  46432  supcnvlimsup  46437  limsup10exlem  46469  liminfresuz  46481  liminfvaluz  46489  limsupvaluz3  46495  ioodvbdlimc1lem2  46629  ioodvbdlimc2lem  46631  dvnmul  46640  dvnprodlem1  46643  dvnprodlem2  46644  iblspltprt  46670  itgspltprt  46676  stoweidlem3  46700  stoweidlem11  46708  stoweidlem20  46717  stoweidlem26  46723  stoweidlem34  46731  stoweidlem59  46756  stirlinglem5  46775  dirkertrigeqlem3  46797  dirkeritg  46799  dirkercncflem1  46800  dirkercncflem2  46801  dirkercncflem4  46803  fourierdlem4  46808  fourierdlem6  46810  fourierdlem7  46811  fourierdlem11  46815  fourierdlem12  46816  fourierdlem15  46819  fourierdlem19  46823  fourierdlem20  46824  fourierdlem25  46829  fourierdlem26  46830  fourierdlem34  46838  fourierdlem35  46839  fourierdlem41  46845  fourierdlem48  46851  fourierdlem49  46852  fourierdlem50  46853  fourierdlem51  46854  fourierdlem54  46857  fourierdlem63  46866  fourierdlem64  46867  fourierdlem65  46868  fourierdlem71  46874  fourierdlem79  46882  fourierdlem89  46892  fourierdlem90  46893  fourierdlem91  46894  fourierdlem102  46905  fourierdlem103  46906  fourierdlem104  46907  fourierdlem114  46917  fouriersw  46928  elaa2lem  46930  etransclem3  46934  etransclem4  46935  etransclem7  46938  etransclem10  46941  etransclem15  46946  etransclem19  46950  etransclem23  46954  etransclem24  46955  etransclem25  46956  etransclem27  46958  etransclem31  46962  etransclem32  46963  etransclem35  46966  etransclem41  46972  etransclem44  46975  etransclem46  46977  etransclem48  46979  iundjiun  47157  caratheodorylem1  47223  hoicvr  47245  smflimsuplem4  47520  smfliminflem  47527  ormklocald  47573  ormkglobd  47574  natglobalincr  47576  chnerlem3  47583  2elfz2melfz  48038  elfzelfzlble  48041  fzopredsuc  48044  nnmul2  48050  2ltceilhalf  48052  ceilhalfgt1  48053  ceilhalfnn  48060  submodlt  48076  m1modmmod  48084  difmodm1lt  48085  modmknepk  48088  mod2addne  48090  2timesltsq  48098  2timesltsqm1  48099  fsummsndifre  48100  iccpartgt  48159  icceuelpartlem  48167  icceuelpart  48168  iccpartnel  48170  nprmmul2  48260  nprmmul3  48261  lighneallem2  48341  proththd  48349  nprmdvdsfacm1lem4  48358  dfodd4  48407  oexpnegALTV  48425  nnoALTV  48443  evenltle  48465  fpprwppr  48487  gbowgt5  48510  gboge9  48512  stgoldbwt  48524  sbgoldbst  48526  sbgoldbalt  48529  sgoldbeven3prm  48531  mogoldbb  48533  bgoldbtbndlem1  48553  bgoldbtbndlem2  48554  bgoldbtbndlem3  48555  bgoldbtbnd  48557  bgoldbachlt  48561  tgblthelfgott  48563  tgoldbach  48565  upgrimpthslem2  48656  gpgprismgrusgra  48806  gpgedgvtx1  48810  gpgvtxedg0  48811  gpgvtxedg1  48812  gpg5nbgrvtx13starlem2  48820  gpg3nbgrvtx0  48824  gpg3kgrtriexlem1  48831  gpg3kgrtriexlem4  48834  gpg3kgrtriexlem6  48836  pw2m1lepw2m1  49283  fllogbd  49323  logbpw2m1  49330  fllog2  49331  nnpw2blen  49343  nnolog2flm1  49353  dignn0flhalflem1  49378  dignn0flhalflem2  49379