Theorem zred 12435

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

Syntax hints:   → wi 4   ∈ wcel 2107  ℝcr 10879  ℤcz 12328

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2710

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3or 1087  df-3an 1088  df-tru 1542  df-fal 1552  df-ex 1783  df-sb 2069  df-clab 2717  df-cleq 2731  df-clel 2817  df-rab 3074  df-v 3435  df-dif 3891  df-un 3893  df-in 3895  df-ss 3905  df-nul 4258  df-if 4461  df-sn 4563  df-pr 4565  df-op 4569  df-uni 4841  df-br 5076  df-iota 6395  df-fv 6445  df-ov 7287  df-neg 11217  df-z 12329

This theorem is referenced by:  zcnd  12436  suprfinzcl  12445  eluzmn  12598  eluzelre  12602  subeluzsub  12624  uzm1  12625  zsupss  12686  suprzcl2  12687  uzwo3  12692  rpnnen1lem3  12728  rpnnen1lem5  12730  zltaddlt1le  13246  fzsplit2  13290  fzdisj  13292  ssfzunsnext  13310  fzpreddisj  13314  fznatpl1  13319  fzp1disj  13324  uzdisj  13338  fzm1  13345  fz0fzdiffz0  13374  elfzmlbm  13375  elfzmlbp  13376  difelfznle  13379  nn0disj  13381  elfzolt3  13406  fzonel  13410  fzospliti  13428  fzodisj  13430  fzouzdisj  13432  fzodisjsn  13434  fzonmapblen  13442  fzoaddel  13449  elincfzoext  13454  reflcl  13525  flge  13534  flwordi  13541  fladdz  13554  2tnp1ge0ge0  13558  flhalf  13559  fldiv4p1lem1div2  13564  fldiv4lem1div2uz2  13565  fldiv4lem1div2  13566  flleceil  13582  fleqceilz  13583  quoremz  13584  uzsup  13592  modmul12d  13654  modaddmodup  13663  modaddmodlo  13664  modfzo0difsn  13672  modsumfzodifsn  13673  addmodlteq  13675  om2uzlti  13679  om2uzf1oi  13682  seqf1olem1  13771  seqf1olem2  13772  bcval4  14030  bcp1nk  14040  bcval5  14041  fzsdom2  14152  seqcoll  14187  seqcoll2  14188  ccatrn  14303  ccatalpha  14307  cshwidxmodr  14526  fzomaxdiflem  15063  fzomaxdif  15064  rexuzre  15073  limsupgre  15199  rlimclim1  15263  isercoll  15388  iseralt  15405  fsumm1  15472  fsum1p  15474  fsum0diaglem  15497  modfsummods  15514  isumsplit  15561  climcndslem1  15570  mertenslem1  15605  ntrivcvgmul  15623  fprodntriv  15661  fprod1p  15687  fprodeq0  15694  fallfacval4  15762  bpoly4  15778  fzo0dvdseq  16041  dvdsmod  16047  oexpneg  16063  mod2eq1n2dvds  16065  ltoddhalfle  16079  flodddiv4t2lthalf  16134  bitsp1  16147  bitsfzolem  16150  bitsfzo  16151  bitsmod  16152  bitscmp  16154  bitsinv1lem  16157  sadaddlem  16182  bitsres  16189  bitsuz  16190  smumul  16209  gcd0id  16235  gcdneg  16238  dfgcd2  16263  nn0seqcvgd  16284  lcmgcdlem  16320  nprm  16402  prmdvdsfz  16419  isprm5  16421  isprm7  16422  coprm  16425  prmexpb  16434  prmfac1  16435  hashdvds  16485  crth  16488  eulerthlem2  16492  fermltl  16494  prmdiv  16495  prmdiveq  16496  hashgcdlem  16498  odzdvds  16505  vfermltlALT  16512  modprm0  16515  modprmn0modprm0  16517  prm23ge5  16525  pythagtriplem13  16537  pcxcl  16571  pcaddlem  16598  pcadd  16599  pcfac  16609  qexpz  16611  prmunb  16624  1arithlem4  16636  4sqlem5  16652  4sqlem6  16653  4sqlem7  16654  4sqlem10  16657  4sqlem11  16665  4sqlem12  16666  4sqlem15  16669  4sqlem16  16670  4sqlem17  16671  vdwnnlem3  16707  prmgaplem7  16767  cshwshashlem3  16808  subgmulg  18778  mndodconglem  19158  odnncl  19162  odmod  19163  oddvds  19164  dfod2  19180  sylow1lem3  19214  efgsp1  19352  efgredleme  19358  telgsumfzs  19599  zringlpirlem1  20693  zringlpirlem3  20695  znf1o  20768  zcld  23985  ovoliunlem1  24675  ovoliunlem2  24676  dyadss  24767  dyaddisjlem  24768  dyadmaxlem  24770  dvfsumle  25194  dvfsumge  25195  dvfsumabs  25196  dvfsumlem1  25199  dvfsumlem3  25201  degltlem1  25246  plyco0  25362  plyeq0lem  25380  plydivex  25466  aannenlem1  25497  efif1olem2  25708  nnlogbexp  25940  logblt  25943  ang180lem1  25968  ang180lem3  25970  wilthlem2  26227  basellem3  26241  basellem4  26242  ppiprm  26309  chtdif  26316  ppidif  26321  chtub  26369  mersenne  26384  bcmono  26434  bcmax  26435  bposlem1  26441  bposlem3  26443  bposlem5  26445  bposlem6  26446  lgsval2lem  26464  lgsvalmod  26473  lgsneg  26478  lgsmod  26480  lgsdilem  26481  lgsdirprm  26488  lgsdilem2  26490  lgsne0  26492  lgssq  26494  lgssq2  26495  lgsqr  26508  lgsdchr  26512  gausslemma2dlem1a  26522  gausslemma2dlem3  26525  gausslemma2dlem5a  26527  gausslemma2dlem6  26529  gausslemma2d  26531  lgseisenlem1  26532  lgseisenlem2  26533  lgseisenlem3  26534  lgseisenlem4  26535  lgsquadlem1  26537  lgsquadlem2  26538  lgsquadlem3  26539  lgsquad3  26544  2lgslem1a2  26547  2lgslem1  26551  2lgslem2  26552  2sqlem3  26577  2sqlem8  26583  2sqblem  26588  2sqmod  26593  chebbnd1lem1  26626  chebbnd1lem2  26627  chebbnd1lem3  26628  dchrmusum2  26651  dchrvmasumlem1  26652  dchrvmasum2lem  26653  dchrvmasum2if  26654  dchrvmasumlem3  26656  dchrvmasumiflem2  26659  dchrisum0lem1  26673  dchrmusumlem  26679  mudivsum  26687  mulogsumlem  26688  mulogsum  26689  mulog2sumlem2  26692  mulog2sumlem3  26693  selberglem1  26702  selberglem2  26703  pntpbnd1  26743  pntlemg  26755  pntlemf  26762  qabvle  26782  padicabv  26787  padicabvcxp  26789  ostth2lem2  26791  axlowdimlem13  27331  axlowdimlem16  27334  pthdlem1  28143  crctcshwlkn0  28195  crctcsh  28198  clwwisshclwwslemlem  28386  eucrctshift  28616  nndiffz1  31116  fzsplit3  31124  bcm1n  31125  fzone1  31130  ltesubnnd  31145  wrdt2ind  31234  cshwrnid  31242  cycpmfv2  31390  cycpmco2lem6  31407  cycpmco2lem7  31408  cycpmrn  31419  cyc3conja  31433  pnfinf  31446  znfermltl  31571  dya2iocress  32250  dya2iocbrsiga  32251  dya2icobrsiga  32252  dya2icoseg  32253  dya2iocucvr  32260  sxbrsigalem2  32262  ballotlemfc0  32468  ballotlemfcc  32469  ballotlemodife  32473  ballotlemimin  32481  ballotlemsgt1  32486  ballotlemsel1i  32488  ballotlemsi  32490  ballotlemsima  32491  ballotlemrv2  32497  ballotlemfrceq  32504  ballotlemfrcn0  32505  ballotlemirc  32507  fsum2dsub  32596  reprlt  32608  reprgt  32610  breprexplemc  32621  tgoldbachgnn  32648  tgoldbachgt  32652  subfacval3  33160  erdszelem8  33169  erdszelem9  33170  supfz  33703  inffz  33704  dnizeq0  34664  dnizphlfeqhlf  34665  dnibndlem13  34679  knoppndvlem1  34701  knoppndvlem2  34702  knoppndvlem7  34707  knoppndvlem19  34719  knoppndvlem21  34721  ltflcei  35774  leceifl  35775  poimirlem1  35787  poimirlem2  35788  poimirlem6  35792  poimirlem7  35793  poimirlem8  35794  poimirlem15  35801  poimirlem16  35802  poimirlem17  35803  poimirlem19  35805  poimirlem20  35806  poimirlem23  35809  poimirlem24  35810  poimirlem27  35813  poimirlem29  35815  poimirlem31  35817  poimirlem32  35818  mblfinlem2  35824  itg2addnclem2  35838  mettrifi  35924  cntotbnd  35963  fzne2d  39996  aks4d1lem1  40077  aks4d1p1p3  40084  aks4d1p1p2  40085  aks4d1p1p4  40086  aks4d1p1  40091  aks4d1p2  40092  aks4d1p3  40093  aks4d1p5  40095  aks4d1p6  40096  aks4d1p7d1  40097  aks4d1p7  40098  aks4d1p8d3  40101  aks4d1p8  40102  aks4d1p9  40103  2ap1caineq  40108  sticksstones6  40114  sticksstones7  40115  sticksstones10  40118  sticksstones12a  40120  sticksstones12  40121  sticksstones22  40131  metakunt7  40138  metakunt12  40143  metakunt15  40146  metakunt16  40147  metakunt22  40153  metakunt28  40159  prodsplit  40168  frlmvscadiccat  40244  dffltz  40478  lzunuz  40597  lzenom  40599  diophin  40601  irrapxlem1  40651  irrapxlem2  40652  irrapxlem3  40653  irrapxlem4  40654  pellexlem5  40662  pellexlem6  40663  rmspecfund  40738  rmxypos  40776  ltrmynn0  40777  ltrmxnn0  40778  ltrmy  40781  rmyeq0  40782  rmyeq  40783  lermy  40784  rmyabs  40787  jm2.24nn  40788  jm2.17a  40789  jm2.17b  40790  jm2.17c  40791  jm2.24  40792  rmygeid  40793  acongrep  40809  fzmaxdif  40810  acongeq  40812  jm2.22  40824  jm2.23  40825  jm2.26lem3  40830  jm2.27a  40834  jm3.1lem1  40846  jm3.1lem3  40848  expdiophlem1  40850  fzuntd  41070  fzunt1d  41071  fzuntgd  41072  prmunb2  41936  nzprmdif  41944  hashnzfzclim  41947  binomcxplemnn0  41974  uzwo4  42608  ssinc  42644  ssdec  42645  zltlesub  42831  monoords  42843  fzisoeu  42846  fperiodmul  42850  fzdifsuc2  42856  iuneqfzuzlem  42880  uzublem  42977  zxrd  43000  uzinico  43105  uzubioo  43112  fmul01  43128  fmul01lt1lem1  43132  fmul01lt1lem2  43133  climsuselem1  43155  climsuse  43156  sumnnodd  43178  ltmod  43186  limsupresuz  43251  limsupubuzlem  43260  limsupequzlem  43270  limsupmnfuzlem  43274  limsupequzmptlem  43276  limsupre3uzlem  43283  supcnvlimsup  43288  limsup10exlem  43320  liminfresuz  43332  liminfvaluz  43340  limsupvaluz3  43346  ioodvbdlimc1lem2  43480  ioodvbdlimc2lem  43482  dvnmul  43491  dvnprodlem1  43494  dvnprodlem2  43495  iblspltprt  43521  itgspltprt  43527  stoweidlem3  43551  stoweidlem11  43559  stoweidlem20  43568  stoweidlem26  43574  stoweidlem34  43582  stoweidlem59  43607  stirlinglem5  43626  dirkertrigeqlem3  43648  dirkeritg  43650  dirkercncflem1  43651  dirkercncflem2  43652  dirkercncflem4  43654  fourierdlem4  43659  fourierdlem6  43661  fourierdlem7  43662  fourierdlem11  43666  fourierdlem12  43667  fourierdlem15  43670  fourierdlem19  43674  fourierdlem20  43675  fourierdlem25  43680  fourierdlem26  43681  fourierdlem34  43689  fourierdlem35  43690  fourierdlem41  43696  fourierdlem48  43702  fourierdlem49  43703  fourierdlem50  43704  fourierdlem51  43705  fourierdlem54  43708  fourierdlem63  43717  fourierdlem64  43718  fourierdlem65  43719  fourierdlem71  43725  fourierdlem79  43733  fourierdlem89  43743  fourierdlem90  43744  fourierdlem91  43745  fourierdlem102  43756  fourierdlem103  43757  fourierdlem104  43758  fourierdlem114  43768  fouriersw  43779  elaa2lem  43781  etransclem3  43785  etransclem4  43786  etransclem7  43789  etransclem10  43792  etransclem15  43797  etransclem19  43801  etransclem23  43805  etransclem24  43806  etransclem25  43807  etransclem27  43809  etransclem31  43813  etransclem32  43814  etransclem35  43817  etransclem41  43823  etransclem44  43826  etransclem46  43828  etransclem48  43830  iundjiun  44005  caratheodorylem1  44071  smflimsuplem4  44367  smfliminflem  44374  2elfz2melfz  44821  elfzelfzlble  44824  fzopredsuc  44826  fsummsndifre  44835  iccpartgt  44890  icceuelpartlem  44898  icceuelpart  44899  iccpartnel  44901  lighneallem2  45069  proththd  45077  dfodd4  45122  oexpnegALTV  45140  nnoALTV  45158  evenltle  45180  fpprwppr  45202  gbowgt5  45225  gboge9  45227  stgoldbwt  45239  sbgoldbst  45241  sbgoldbalt  45244  sgoldbeven3prm  45246  mogoldbb  45248  bgoldbtbndlem1  45268  bgoldbtbndlem2  45269  bgoldbtbndlem3  45270  bgoldbtbnd  45272  bgoldbachlt  45276  tgblthelfgott  45278  tgoldbach  45280  pw2m1lepw2m1  45872  m1modmmod  45878  difmodm1lt  45879  fllogbd  45917  logbpw2m1  45924  fllog2  45925  nnpw2blen  45937  nnolog2flm1  45947  dignn0flhalflem1  45972  dignn0flhalflem2  45973  natglobalincr  46523