Theorem zred 11834

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

Syntax hints:   → wi 4   ∈ wcel 2107  ℝcr 10271  ℤcz 11728

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1839  ax-4 1853  ax-5 1953  ax-6 2021  ax-7 2055  ax-9 2116  ax-10 2135  ax-11 2150  ax-12 2163  ax-13 2334  ax-ext 2754

This theorem depends on definitions:  df-bi 199  df-an 387  df-or 837  df-3or 1072  df-3an 1073  df-tru 1605  df-ex 1824  df-nf 1828  df-sb 2012  df-clab 2764  df-cleq 2770  df-clel 2774  df-nfc 2921  df-rex 3096  df-rab 3099  df-v 3400  df-dif 3795  df-un 3797  df-in 3799  df-ss 3806  df-nul 4142  df-if 4308  df-sn 4399  df-pr 4401  df-op 4405  df-uni 4672  df-br 4887  df-iota 6099  df-fv 6143  df-ov 6925  df-neg 10609  df-z 11729

This theorem is referenced by:  zcnd  11835  suprfinzcl  11844  eluzmn  11999  eluzelre  12003  subeluzsub  12023  uzm1  12024  zsupss  12084  suprzcl2  12085  uzwo3  12090  rpnnen1lem3  12126  rpnnen1lem5  12128  zltaddlt1le  12641  fzsplit2  12683  fzdisj  12685  ssfzunsnext  12703  fzpreddisj  12707  fznatpl1  12712  fzp1disj  12717  uzdisj  12731  fzm1  12738  fz0fzdiffz0  12767  elfzmlbm  12768  elfzmlbp  12769  difelfznle  12772  nn0disj  12774  elfzolt3  12799  fzonel  12802  fzospliti  12819  fzodisj  12821  fzouzdisj  12823  fzodisjsn  12825  fzonmapblen  12833  fzoaddel  12840  elincfzoext  12845  reflcl  12916  flge  12925  flwordi  12932  fladdz  12945  2tnp1ge0ge0  12949  flhalf  12950  fldiv4p1lem1div2  12955  fldiv4lem1div2uz2  12956  fldiv4lem1div2  12957  flleceil  12971  fleqceilz  12972  quoremz  12973  uzsup  12981  modmul12d  13043  modaddmodup  13052  modaddmodlo  13053  modfzo0difsn  13061  modsumfzodifsn  13062  addmodlteq  13064  om2uzlti  13068  om2uzf1oi  13071  seqf1olem1  13158  seqf1olem2  13159  bcval4  13412  bcp1nk  13422  bcval5  13423  fzsdom2  13529  seqcoll  13562  seqcoll2  13563  ccatrn  13679  ccatalpha  13683  cshwidxmodr  13955  fzomaxdiflem  14489  fzomaxdif  14490  rexuzre  14499  limsupgre  14620  rlimclim1  14684  isercoll  14806  iseralt  14823  fsumm1  14887  fsum1p  14889  fsum0diaglem  14912  modfsummods  14929  isumsplit  14976  climcndslem1  14985  mertenslem1  15019  ntrivcvgmul  15037  fprodntriv  15075  fprod1p  15101  fprodeq0  15108  fallfacval4  15176  bpoly4  15192  fzo0dvdseq  15452  dvdsmod  15457  oexpneg  15473  mod2eq1n2dvds  15475  ltoddhalfle  15489  flodddiv4t2lthalf  15546  bitsp1  15559  bitsfzolem  15562  bitsfzo  15563  bitsmod  15564  bitscmp  15566  bitsinv1lem  15569  sadaddlem  15594  bitsres  15601  bitsuz  15602  smumul  15621  gcd0id  15646  gcdneg  15649  dfgcd2  15669  nn0seqcvgd  15689  lcmgcdlem  15725  nprm  15806  prmdvdsfz  15821  isprm5  15823  isprm7  15824  coprm  15827  prmexpb  15834  prmfac1  15835  hashdvds  15884  crth  15887  eulerthlem2  15891  fermltl  15893  prmdiv  15894  prmdiveq  15895  hashgcdlem  15897  odzdvds  15904  vfermltlALT  15911  modprm0  15914  modprmn0modprm0  15916  prm23ge5  15924  pythagtriplem13  15936  pcxcl  15969  pcaddlem  15996  pcadd  15997  pcfac  16007  qexpz  16009  prmunb  16022  1arithlem4  16034  4sqlem5  16050  4sqlem6  16051  4sqlem7  16052  4sqlem10  16055  4sqlem11  16063  4sqlem12  16064  4sqlem15  16067  4sqlem16  16068  4sqlem17  16069  vdwnnlem3  16105  prmgaplem7  16165  cshwshashlem3  16203  subgmulg  17992  mndodconglem  18344  odnncl  18348  odmod  18349  oddvds  18350  dfod2  18365  sylow1lem3  18399  efgsp1  18534  efgredleme  18541  telgsumfzs  18773  zringlpirlem1  20228  zringlpirlem3  20230  znf1o  20295  zcld  23024  ovoliunlem1  23706  ovoliunlem2  23707  dyadss  23798  dyaddisjlem  23799  dyadmaxlem  23801  dvfsumle  24221  dvfsumge  24222  dvfsumabs  24223  dvfsumlem1  24226  dvfsumlem3  24228  degltlem1  24269  plyco0  24385  plyeq0lem  24403  plydivex  24489  aannenlem1  24520  efif1olem2  24727  nnlogbexp  24959  logblt  24962  ang180lem1  24987  ang180lem3  24989  wilthlem2  25247  basellem3  25261  basellem4  25262  ppiprm  25329  chtdif  25336  ppidif  25341  chtub  25389  mersenne  25404  bcmono  25454  bcmax  25455  bposlem1  25461  bposlem3  25463  bposlem5  25465  bposlem6  25466  lgsval2lem  25484  lgsvalmod  25493  lgsneg  25498  lgsmod  25500  lgsdilem  25501  lgsdirprm  25508  lgsdilem2  25510  lgsne0  25512  lgssq  25514  lgssq2  25515  lgsqr  25528  lgsdchr  25532  gausslemma2dlem1a  25542  gausslemma2dlem3  25545  gausslemma2dlem5a  25547  gausslemma2dlem6  25549  gausslemma2d  25551  lgseisenlem1  25552  lgseisenlem2  25553  lgseisenlem3  25554  lgseisenlem4  25555  lgsquadlem1  25557  lgsquadlem2  25558  lgsquadlem3  25559  lgsquad3  25564  2lgslem1a2  25567  2lgslem1  25571  2lgslem2  25572  2sqlem3  25597  2sqlem8  25603  2sqblem  25608  chebbnd1lem1  25610  chebbnd1lem2  25611  chebbnd1lem3  25612  dchrmusum2  25635  dchrvmasumlem1  25636  dchrvmasum2lem  25637  dchrvmasum2if  25638  dchrvmasumlem3  25640  dchrvmasumiflem2  25643  dchrisum0lem1  25657  dchrmusumlem  25663  mudivsum  25671  mulogsumlem  25672  mulogsum  25673  mulog2sumlem2  25676  mulog2sumlem3  25677  selberglem1  25686  selberglem2  25687  pntpbnd1  25727  pntlemg  25739  pntlemf  25746  qabvle  25766  padicabv  25771  padicabvcxp  25773  ostth2lem2  25775  axlowdimlem13  26303  axlowdimlem16  26306  pthdlem1  27118  crctcshwlkn0  27170  crctcsh  27173  clwwisshclwwslemlem  27402  eucrctshift  27647  nndiffz1  30112  fzsplit3  30117  bcm1n  30118  ltesubnnd  30132  2sqmod  30210  pnfinf  30299  dya2iocress  30934  dya2iocbrsiga  30935  dya2icobrsiga  30936  dya2icoseg  30937  dya2iocucvr  30944  sxbrsigalem2  30946  ballotlemfc0  31153  ballotlemfcc  31154  ballotlemodife  31158  ballotlemimin  31166  ballotlemsgt1  31171  ballotlemsel1i  31173  ballotlemsi  31175  ballotlemsima  31176  ballotlemrv2  31182  ballotlemfrceq  31189  ballotlemfrcn0  31190  ballotlemirc  31192  fsum2dsub  31287  reprlt  31299  reprgt  31301  breprexplemc  31312  tgoldbachgnn  31339  tgoldbachgt  31343  subfacval3  31770  erdszelem8  31779  erdszelem9  31780  supfz  32208  inffz  32209  dnizeq0  33048  dnizphlfeqhlf  33049  dnibndlem13  33063  knoppndvlem1  33085  knoppndvlem2  33086  knoppndvlem7  33091  knoppndvlem19  33103  knoppndvlem21  33105  ltflcei  34022  leceifl  34023  poimirlem1  34036  poimirlem2  34037  poimirlem6  34041  poimirlem7  34042  poimirlem8  34043  poimirlem15  34050  poimirlem16  34051  poimirlem17  34052  poimirlem19  34054  poimirlem20  34055  poimirlem23  34058  poimirlem24  34059  poimirlem27  34062  poimirlem29  34064  poimirlem31  34066  poimirlem32  34067  mblfinlem2  34073  itg2addnclem2  34087  mettrifi  34177  cntotbnd  34219  exp11d  38169  dffltz  38213  lzunuz  38291  lzenom  38293  diophin  38296  irrapxlem1  38346  irrapxlem2  38347  irrapxlem3  38348  irrapxlem4  38349  pellexlem5  38357  pellexlem6  38358  rmspecfund  38433  rmxypos  38473  ltrmynn0  38474  ltrmxnn0  38475  ltrmy  38478  rmyeq0  38479  rmyeq  38480  lermy  38481  rmyabs  38484  jm2.24nn  38485  jm2.17a  38486  jm2.17b  38487  jm2.17c  38488  jm2.24  38489  rmygeid  38490  acongrep  38506  fzmaxdif  38507  acongeq  38509  jm2.22  38521  jm2.23  38522  jm2.26lem3  38527  jm2.27a  38531  jm3.1lem1  38543  jm3.1lem3  38545  expdiophlem1  38547  prmunb2  39466  nzprmdif  39474  hashnzfzclim  39477  binomcxplemnn0  39504  uzwo4  40152  ssinc  40195  ssdec  40196  zltlesub  40407  monoords  40420  fzisoeu  40423  fperiodmul  40427  fzdifsuc2  40433  iuneqfzuzlem  40458  uzublem  40563  zxrd  40588  uzinico  40695  uzubioo  40702  fmul01  40720  fmul01lt1lem1  40724  fmul01lt1lem2  40725  climsuselem1  40747  climsuse  40748  sumnnodd  40770  ltmod  40778  limsupresuz  40843  limsupubuzlem  40852  limsupequzlem  40862  limsupmnfuzlem  40866  limsupequzmptlem  40868  limsupre3uzlem  40875  supcnvlimsup  40880  limsup10exlem  40912  liminfresuz  40924  liminfvaluz  40932  limsupvaluz3  40938  ioodvbdlimc1lem2  41075  ioodvbdlimc2lem  41077  dvnmul  41086  dvnprodlem1  41089  dvnprodlem2  41090  iblspltprt  41116  itgspltprt  41122  stoweidlem3  41147  stoweidlem11  41155  stoweidlem20  41164  stoweidlem26  41170  stoweidlem34  41178  stoweidlem59  41203  stirlinglem5  41222  dirkertrigeqlem3  41244  dirkeritg  41246  dirkercncflem1  41247  dirkercncflem2  41248  dirkercncflem4  41250  fourierdlem4  41255  fourierdlem6  41257  fourierdlem7  41258  fourierdlem11  41262  fourierdlem12  41263  fourierdlem15  41266  fourierdlem19  41270  fourierdlem20  41271  fourierdlem25  41276  fourierdlem26  41277  fourierdlem34  41285  fourierdlem35  41286  fourierdlem41  41292  fourierdlem48  41298  fourierdlem49  41299  fourierdlem50  41300  fourierdlem51  41301  fourierdlem54  41304  fourierdlem63  41313  fourierdlem64  41314  fourierdlem65  41315  fourierdlem71  41321  fourierdlem79  41329  fourierdlem89  41339  fourierdlem90  41340  fourierdlem91  41341  fourierdlem102  41352  fourierdlem103  41353  fourierdlem104  41354  fourierdlem114  41364  fouriersw  41375  elaa2lem  41377  etransclem3  41381  etransclem4  41382  etransclem7  41385  etransclem10  41388  etransclem15  41393  etransclem19  41397  etransclem23  41401  etransclem24  41402  etransclem25  41403  etransclem27  41405  etransclem31  41409  etransclem32  41410  etransclem35  41413  etransclem41  41419  etransclem44  41422  etransclem46  41424  etransclem48  41426  iundjiun  41601  caratheodorylem1  41667  smflimsuplem4  41956  smfliminflem  41963  2elfz2melfz  42360  elfzelfzlble  42363  fzopredsuc  42365  fsummsndifre  42374  iccpartgt  42395  icceuelpartlem  42403  icceuelpart  42404  iccpartnel  42406  lighneallem2  42544  proththd  42552  dfodd4  42596  oexpnegALTV  42613  nnoALTV  42631  evenltle  42651  gbowgt5  42675  gboge9  42677  stgoldbwt  42689  sbgoldbst  42691  sbgoldbalt  42694  sgoldbeven3prm  42696  mogoldbb  42698  bgoldbtbndlem1  42718  bgoldbtbndlem2  42719  bgoldbtbndlem3  42720  bgoldbtbnd  42722  bgoldbachlt  42726  tgblthelfgott  42728  tgoldbach  42730  pw2m1lepw2m1  43325  m1modmmod  43331  difmodm1lt  43332  fllogbd  43369  logbpw2m1  43376  fllog2  43377  nnpw2blen  43389  nnolog2flm1  43399  dignn0flhalflem1  43424  dignn0flhalflem2  43425