Theorem zred 12729

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

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2145  ℝcr 11127  ℤcz 12619

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 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2734

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 2100  df-clab 2741  df-cleq 2754  df-clel 2837  df-rab 3415  df-v 3455  df-dif 3905  df-un 3907  df-ss 3919  df-nul 4283  df-if 4486  df-sn 4588  df-pr 4590  df-op 4594  df-uni 4871  df-br 5108  df-iota 6493  df-fv 6545  df-ov 7420  df-neg 11472  df-z 12620

This theorem is used by:  zcnd  12730  suprfinzcl  12739  eluzmn  12898  eluzelre  12902  eluzadd  12920  subeluzsub  12924  uzm1  12925  zsupss  12990  suprzcl2  12991  uzwo3  12996  rpnnen1lem3  13033  rpnnen1lem5  13035  zltaddlt1le  13562  fzsplit2  13608  fzdisj  13610  ssfzunsnext  13628  fzpreddisj  13632  fznatpl1  13637  fzp1disj  13642  uzdisj  13656  fzdif1  13664  fzm1  13666  fz0fzdiffz0  13696  elfzmlbm  13697  elfzmlbp  13698  difelfznle  13701  nn0disj  13703  elfzolt3  13729  fzonel  13733  fzospliti  13751  fzodisj  13753  fzouzdisj  13755  fzodisjsn  13757  elfzo0subge1  13765  elfzo0suble  13766  fzonmapblen  13768  fzoaddel  13777  elincfzoext  13783  fzone1  13844  reflcl  13861  flge  13870  flwordi  13877  fladdz  13890  2tnp1ge0ge0  13894  flhalf  13895  fldiv4p1lem1div2  13900  fldiv4lem1div2uz2  13901  fldiv4lem1div2  13902  flleceil  13918  fleqceilz  13919  quoremz  13920  uzsup  13928  modaddid  13975  modmul12d  13993  modaddmodup  14002  modaddmodlo  14003  modfzo0difsn  14011  modsumfzodifsn  14012  addmodlteq  14014  om2uzlti  14018  om2uzf1oi  14021  seqf1olem1  14109  seqf1olem2  14110  bcval4  14375  bcp1nk  14385  bcval5  14386  fzsdom2  14497  seqcoll  14533  seqcoll2  14534  ccatrn  14659  ccatalpha  14664  cshwidxmodr  14879  fzomaxdiflem  15434  fzomaxdif  15435  rexuzre  15444  limsupgre  15572  rlimclim1  15636  isercoll  15759  iseralt  15776  fsumm1  15841  fsum1p  15843  fsum0diaglem  15866  modfsummods  15884  isumsplit  15933  climcndslem1  15942  mertenslem1  15977  ntrivcvgmul  15995  fprodntriv  16035  fprod1p  16061  fprodeq0  16068  fallfacval4  16135  bpoly4  16151  fzo0dvdseq  16419  dvdsmod  16425  oexpneg  16441  mod2eq1n2dvds  16443  ltoddhalfle  16457  flodddiv4t2lthalf  16514  bitsp1  16527  bitsfzolem  16530  bitsfzo  16531  bitsmod  16532  bitscmp  16534  bitsinv1lem  16537  sadaddlem  16562  bitsres  16569  bitsuz  16570  smumul  16589  gcd0id  16615  gcdneg  16618  dfgcd2  16642  nn0seqcvgd  16666  lcmgcdlem  16702  nprm  16784  prmdvdsfz  16802  isprm5  16804  isprm7  16805  coprm  16808  prmexpb  16816  prmfac1  16817  hashdvds  16872  crth  16875  eulerthlem2  16879  fermltl  16881  prmdiv  16882  prmdiveq  16883  hashgcdlem  16885  odzdvds  16893  vfermltlALT  16900  modprm0  16903  modprmn0modprm0  16905  prm23ge5  16913  pythagtriplem13  16925  pcxcl  16959  pcaddlem  16986  pcadd  16987  pcfac  16997  qexpz  16999  prmunb  17012  1arithlem4  17024  4sqlem5  17040  4sqlem6  17041  4sqlem7  17042  4sqlem10  17045  4sqlem11  17053  4sqlem12  17054  4sqlem15  17057  4sqlem16  17058  4sqlem17  17059  vdwnnlem3  17095  prmgaplem7  17155  cshwshashlem3  17195  chnub  18716  chnso  18718  chnccat  18720  chnpof1  18724  subgmulg  19270  mndodconglem  19674  odnncl  19678  odmod  19679  oddvds  19680  dfod2  19697  sylow1lem3  19733  efgsp1  19870  efgredleme  19876  telgsumfzs  20122  zringlpirlem1  21681  zringlpirlem3  21683  fermltlchr  21748  znf1o  21770  zcld  25046  ovoliunlem1  25736  ovoliunlem2  25737  dyadss  25828  dyaddisjlem  25829  dyadmaxlem  25831  dvfsumle  26255  dvfsumge  26256  dvfsumabs  26257  dvfsumlem1  26260  dvfsumlem3  26262  degltlem1  26304  plyco0  26424  plyeq0lem  26443  plydivex  26534  aannenlem1  26571  efif1olem2  26788  nnlogbexp  27026  logblt  27029  ang180lem1  27054  ang180lem3  27056  wilthlem2  27313  basellem3  27327  basellem4  27328  ppiprm  27395  chtdif  27402  ppidif  27407  chtub  27456  mersenne  27471  bcmono  27521  bcmax  27522  bposlem1  27528  bposlem3  27530  bposlem5  27532  bposlem6  27533  lgsval2lem  27551  lgsvalmod  27560  lgsneg  27565  lgsmod  27567  lgsdilem  27568  lgsdirprm  27575  lgsdilem2  27577  lgsne0  27579  lgssq  27581  lgssq2  27582  lgsqr  27595  lgsdchr  27599  gausslemma2dlem1a  27609  gausslemma2dlem3  27612  gausslemma2dlem5a  27614  gausslemma2dlem6  27616  gausslemma2d  27618  lgseisenlem1  27619  lgseisenlem2  27620  lgseisenlem3  27621  lgseisenlem4  27622  lgsquadlem1  27624  lgsquadlem2  27625  lgsquadlem3  27626  lgsquad3  27631  2lgslem1a2  27634  2lgslem1  27638  2lgslem2  27639  2sqlem3  27664  2sqlem8  27670  2sqblem  27675  2sqmod  27680  chebbnd1lem1  27713  chebbnd1lem2  27714  chebbnd1lem3  27715  dchrmusum2  27738  dchrvmasumlem1  27739  dchrvmasum2lem  27740  dchrvmasum2if  27741  dchrvmasumlem3  27743  dchrvmasumiflem2  27746  dchrisum0lem1  27760  dchrmusumlem  27766  mudivsum  27774  mulogsumlem  27775  mulogsum  27776  mulog2sumlem2  27779  mulog2sumlem3  27780  selberglem1  27789  selberglem2  27790  pntpbnd1  27830  pntlemg  27842  pntlemf  27849  qabvle  27869  padicabv  27874  padicabvcxp  27876  ostth2lem2  27878  axlowdimlem13  29419  axlowdimlem16  29422  pthdlem1  30239  crctcshwlkn0  30297  crctcsh  30300  clwwisshclwwslemlem  30491  eucrctshift  30731  nndiffz1  33265  fzsplit3  33272  bcm1n  33274  suppssnn0  33284  ltesubnnd  33301  wrdt2ind  33403  cshwrnid  33409  cycpmfv2  33562  cycpmco2lem6  33579  cycpmco2lem7  33580  cycpmrn  33591  cyc3conja  33605  pnfinf  33631  znfermltl  33809  constrext2chnlem  34268  cos9thpiminplylem1  34300  cos9thpiminplylem2  34301  dya2iocress  34793  dya2iocbrsiga  34794  dya2icobrsiga  34795  dya2icoseg  34796  dya2iocucvr  34803  sxbrsigalem2  34805  ballotlemfc0  35012  ballotlemfcc  35013  ballotlemodife  35017  ballotlemimin  35025  ballotlemsgt1  35030  ballotlemsel1i  35032  ballotlemsi  35034  ballotlemsima  35035  ballotlemrv2  35041  ballotlemfrceq  35048  ballotlemfrcn0  35049  ballotlemirc  35051  fsum2dsub  35123  reprlt  35135  reprgt  35137  breprexplemc  35148  tgoldbachgnn  35175  tgoldbachgt  35179  subfacval3  35776  erdszelem8  35785  erdszelem9  35786  supfz  36316  inffz  36317  dnizeq0  37180  dnizphlfeqhlf  37181  dnibndlem13  37195  knoppndvlem1  37217  knoppndvlem2  37218  knoppndvlem7  37223  knoppndvlem19  37235  knoppndvlem21  37237  ltflcei  38370  leceifl  38371  poimirlem1  38378  poimirlem2  38379  poimirlem6  38383  poimirlem7  38384  poimirlem8  38385  poimirlem15  38392  poimirlem16  38393  poimirlem17  38394  poimirlem19  38396  poimirlem20  38397  poimirlem23  38400  poimirlem24  38401  poimirlem27  38404  poimirlem29  38406  poimirlem31  38408  poimirlem32  38409  mblfinlem2  38415  itg2addnclem2  38429  mettrifi  38515  cntotbnd  38554  fzne2d  42854  aks4d1lem1  42936  aks4d1p1p3  42943  aks4d1p1p2  42944  aks4d1p1p4  42945  aks4d1p1  42950  aks4d1p2  42951  aks4d1p3  42952  aks4d1p5  42954  aks4d1p6  42955  aks4d1p7d1  42956  aks4d1p7  42957  aks4d1p8d3  42960  aks4d1p8  42961  aks4d1p9  42962  posbezout  42974  aks6d1c1  42990  hashscontpow1  42995  hashscontpow  42996  aks6d1c2  43004  aks6d1c5lem1  43010  2ap1caineq  43019  sticksstones6  43025  sticksstones7  43026  sticksstones10  43029  sticksstones12a  43031  sticksstones12  43032  sticksstones22  43042  bcled  43052  bcle2d  43053  aks6d1c7lem1  43054  aks6d1c7lem2  43055  aks6d1c7  43058  aks5lem6  43066  unitscyglem2  43070  unitscyglem4  43072  aks5lem8  43075  sumcubes  43196  frlmvscadiccat  43402  dffltz  43488  lzunuz  43621  lzenom  43623  diophin  43625  irrapxlem1  43671  irrapxlem2  43672  irrapxlem3  43673  irrapxlem4  43674  pellexlem5  43682  pellexlem6  43683  rmspecfund  43758  rmxypos  43796  ltrmynn0  43797  ltrmxnn0  43798  ltrmy  43801  rmyeq0  43802  rmyeq  43803  lermy  43804  rmyabs  43807  jm2.24nn  43808  jm2.17a  43809  jm2.17b  43810  jm2.17c  43811  jm2.24  43812  rmygeid  43813  acongrep  43829  fzmaxdif  43830  acongeq  43832  jm2.22  43844  jm2.23  43845  jm2.26lem3  43850  jm2.27a  43854  jm3.1lem1  43866  jm3.1lem3  43868  expdiophlem1  43870  fzuntd  44304  fzunt1d  44305  fzuntgd  44306  prmunb2  45143  nzprmdif  45151  hashnzfzclim  45154  binomcxplemnn0  45181  uzwo4  45895  ssinc  45927  ssdec  45928  zltlesub  46126  monoords  46138  fzisoeu  46141  fperiodmul  46145  fzdifsuc2  46151  iuneqfzuzlem  46172  uzublem  46266  zxrd  46289  uzinico  46397  uzubioo  46403  fmul01  46418  fmul01lt1lem1  46422  fmul01lt1lem2  46423  climsuselem1  46445  climsuse  46446  sumnnodd  46468  ltmod  46474  limsupresuz  46539  limsupubuzlem  46548  limsupequzlem  46558  limsupmnfuzlem  46562  limsupequzmptlem  46564  limsupre3uzlem  46571  supcnvlimsup  46576  limsup10exlem  46608  liminfresuz  46620  liminfvaluz  46628  limsupvaluz3  46634  ioodvbdlimc1lem2  46768  ioodvbdlimc2lem  46770  dvnmul  46779  dvnprodlem1  46782  dvnprodlem2  46783  iblspltprt  46809  itgspltprt  46815  stoweidlem3  46839  stoweidlem11  46847  stoweidlem20  46856  stoweidlem26  46862  stoweidlem34  46870  stoweidlem59  46895  stirlinglem5  46914  dirkertrigeqlem3  46936  dirkeritg  46938  dirkercncflem1  46939  dirkercncflem2  46940  dirkercncflem4  46942  fourierdlem4  46947  fourierdlem6  46949  fourierdlem7  46950  fourierdlem11  46954  fourierdlem12  46955  fourierdlem15  46958  fourierdlem19  46962  fourierdlem20  46963  fourierdlem25  46968  fourierdlem26  46969  fourierdlem34  46977  fourierdlem35  46978  fourierdlem41  46984  fourierdlem48  46990  fourierdlem49  46991  fourierdlem50  46992  fourierdlem51  46993  fourierdlem54  46996  fourierdlem63  47005  fourierdlem64  47006  fourierdlem65  47007  fourierdlem71  47013  fourierdlem79  47021  fourierdlem89  47031  fourierdlem90  47032  fourierdlem91  47033  fourierdlem102  47044  fourierdlem103  47045  fourierdlem104  47046  fourierdlem114  47056  fouriersw  47067  elaa2lem  47069  etransclem3  47073  etransclem4  47074  etransclem7  47077  etransclem10  47080  etransclem15  47085  etransclem19  47089  etransclem23  47093  etransclem24  47094  etransclem25  47095  etransclem27  47097  etransclem31  47101  etransclem32  47102  etransclem35  47105  etransclem41  47111  etransclem44  47114  etransclem46  47116  etransclem48  47118  iundjiun  47296  caratheodorylem1  47362  hoicvr  47384  smflimsuplem4  47659  smfliminflem  47666  ormklocald  47712  ormkglobd  47713  chnerlem3  47720  2elfz2melfz  48214  elfzelfzlble  48217  fzopredsuc  48220  nnmul2  48226  2ltceilhalf  48228  ceilhalfgt1  48229  ceilhalfnn  48236  submodlt  48252  m1modmmod  48260  difmodm1lt  48261  modmknepk  48264  mod2addne  48266  2timesltsq  48274  2timesltsqm1  48275  fsummsndifre  48276  iccpartgt  48335  icceuelpartlem  48343  icceuelpart  48344  iccpartnel  48346  nprmmul2  48436  nprmmul3  48437  lighneallem2  48517  proththd  48525  nprmdvdsfacm1lem4  48534  dfodd4  48583  oexpnegALTV  48601  nnoALTV  48619  evenltle  48641  fpprwppr  48663  gbowgt5  48686  gboge9  48688  stgoldbwt  48700  sbgoldbst  48702  sbgoldbalt  48705  sgoldbeven3prm  48707  mogoldbb  48709  bgoldbtbndlem1  48729  bgoldbtbndlem2  48730  bgoldbtbndlem3  48731  bgoldbtbnd  48733  bgoldbachlt  48737  tgblthelfgott  48739  tgoldbach  48741  upgrimpthslem2  48832  gpgprismgrusgra  48982  gpgedgvtx1  48986  gpgvtxedg0  48987  gpgvtxedg1  48988  gpg5nbgrvtx13starlem2  48996  gpg3nbgrvtx0  49000  gpg3kgrtriexlem1  49007  gpg3kgrtriexlem4  49010  gpg3kgrtriexlem6  49012  pw2m1lepw2m1  49458  fllogbd  49498  logbpw2m1  49505  fllog2  49506  nnpw2blen  49518  nnolog2flm1  49528  dignn0flhalflem1  49553  dignn0flhalflem2  49554