Theorem zred 11358

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

Syntax hints:   → wi 4   ∈ wcel 1977  ℝcr 9814  ℤcz 11254

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590

This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-3or 1032  df-3an 1033  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-rex 2902  df-rab 2905  df-v 3175  df-dif 3543  df-un 3545  df-in 3547  df-ss 3554  df-nul 3875  df-if 4037  df-sn 4126  df-pr 4128  df-op 4132  df-uni 4373  df-br 4584  df-iota 5768  df-fv 5812  df-ov 6552  df-neg 10148  df-z 11255

This theorem is referenced by:  zcnd  11359  suprfinzcl  11368  eluzmn  11570  eluzelre  11574  uzm1  11594  zsupss  11653  suprzcl2  11654  uzwo3  11659  rpnnen1lem3  11692  rpnnen1lem5  11694  rpnnen1lem3OLD  11698  rpnnen1lem5OLD  11700  zltaddlt1le  12195  fzsplit2  12237  fzdisj  12239  fzpreddisj  12260  fznatpl1  12265  fzp1disj  12269  uzdisj  12282  fzm1  12289  fz0fzdiffz0  12317  elfzmlbm  12318  elfzmlbp  12319  difelfznle  12322  nn0disj  12324  elfzolt3  12349  fzonel  12352  fzospliti  12369  fzodisj  12371  fzouzdisj  12373  fzodisjsn  12374  fzonmapblen  12381  fzoaddel  12388  elincfzoext  12393  reflcl  12459  flge  12468  flwordi  12475  fladdz  12488  2tnp1ge0ge0  12492  flhalf  12493  fldiv4p1lem1div2  12498  fldiv4lem1div2uz2  12499  fldiv4lem1div2  12500  flleceil  12514  fleqceilz  12515  quoremz  12516  uzsup  12524  modmul12d  12586  modaddmodup  12595  modaddmodlo  12596  modfzo0difsn  12604  modsumfzodifsn  12605  addmodlteq  12607  om2uzlti  12611  om2uzf1oi  12614  seqf1olem1  12702  seqf1olem2  12703  bcval4  12956  bcp1nk  12966  bcval5  12967  fzsdom2  13075  seqcoll  13105  seqcoll2  13106  ccatrn  13225  ccatalpha  13228  cshwidxmodr  13401  fzomaxdiflem  13930  fzomaxdif  13931  rexuzre  13940  limsupgre  14060  rlimclim1  14124  isercoll  14246  iseralt  14263  fsumm1  14324  fsum1p  14326  fsum0diaglem  14350  modfsummods  14366  isumsplit  14411  climcndslem1  14420  mertenslem1  14455  ntrivcvgmul  14473  fprodntriv  14511  fprod1p  14537  fprodeq0  14544  fallfacval4  14613  bpoly4  14629  fzo0dvdseq  14883  dvdsmod  14888  oexpneg  14907  mod2eq1n2dvds  14909  ltoddhalfle  14923  flodddiv4t2lthalf  14978  bitsp1  14991  bitsfzolem  14994  bitsfzo  14995  bitsmod  14996  bitscmp  14998  bitsinv1lem  15001  sadaddlem  15026  bitsres  15033  bitsuz  15034  smumul  15053  gcd0id  15078  gcdneg  15081  dfgcd2  15101  nn0seqcvgd  15121  lcmgcdlem  15157  nprm  15239  prmdvdsfz  15255  isprm5  15257  isprm7  15258  coprm  15261  prmexpb  15268  prmfac1  15269  hashdvds  15318  crth  15321  eulerthlem2  15325  fermltl  15327  prmdiv  15328  prmdiveq  15329  hashgcdlem  15331  odzdvds  15338  vfermltlALT  15345  modprm0  15348  modprmn0modprm0  15350  prm23ge5  15358  pythagtriplem13  15370  pcxcl  15403  pcaddlem  15430  pcadd  15431  pcfac  15441  qexpz  15443  prmunb  15456  1arithlem4  15468  4sqlem5  15484  4sqlem6  15485  4sqlem7  15486  4sqlem10  15489  4sqlem11  15497  4sqlem12  15498  4sqlem15  15501  4sqlem16  15502  4sqlem17  15503  vdwnnlem3  15539  prmgaplem7  15599  cshwshashlem3  15642  subgmulg  17431  mndodconglem  17783  odnncl  17787  odmod  17788  oddvds  17789  dfod2  17804  sylow1lem3  17838  efgsp1  17973  efgredleme  17979  telgsumfzs  18209  zringlpirlem1  19651  zringlpirlem3  19653  znf1o  19719  zcld  22424  ovoliunlem1  23077  ovoliunlem2  23078  dyadss  23168  dyaddisjlem  23169  dyadmaxlem  23171  dvfsumle  23588  dvfsumge  23589  dvfsumabs  23590  dvfsumlem1  23593  dvfsumlem3  23595  degltlem1  23636  plyco0  23752  plyeq0lem  23770  plydivex  23856  aannenlem1  23887  efif1olem2  24093  nnlogbexp  24319  logblt  24322  ang180lem1  24339  ang180lem3  24341  wilthlem2  24595  basellem3  24609  basellem4  24610  ppiprm  24677  chtdif  24684  ppidif  24689  chtub  24737  mersenne  24752  bcmono  24802  bcmax  24803  bposlem1  24809  bposlem3  24811  bposlem5  24813  bposlem6  24814  lgslem4  24825  lgsval2lem  24832  lgsvalmod  24841  lgsneg  24846  lgsmod  24848  lgsdilem  24849  lgsdirprm  24856  lgsdilem2  24858  lgsne0  24860  lgssq  24862  lgssq2  24863  lgsqr  24876  lgsdchr  24880  gausslemma2dlem1a  24890  gausslemma2dlem3  24893  gausslemma2dlem5a  24895  gausslemma2dlem6  24897  gausslemma2d  24899  lgseisenlem1  24900  lgseisenlem2  24901  lgseisenlem3  24902  lgseisenlem4  24903  lgsquadlem1  24905  lgsquadlem2  24906  lgsquadlem3  24907  lgsquad3  24912  2lgslem1a2  24915  2lgslem1  24919  2lgslem2  24920  2sqlem3  24945  2sqlem8  24951  2sqblem  24956  chebbnd1lem1  24958  chebbnd1lem2  24959  chebbnd1lem3  24960  dchrmusum2  24983  dchrvmasumlem1  24984  dchrvmasum2lem  24985  dchrvmasum2if  24986  dchrvmasumlem3  24988  dchrvmasumiflem2  24991  dchrisum0lem1  25005  dchrmusumlem  25011  mudivsum  25019  mulogsumlem  25020  mulogsum  25021  mulog2sumlem2  25024  mulog2sumlem3  25025  selberglem1  25034  selberglem2  25035  pntpbnd1  25075  pntlemg  25087  pntlemf  25094  qabvle  25114  padicabv  25119  padicabvcxp  25121  ostth2lem2  25123  axlowdimlem13  25634  axlowdimlem16  25637  clwwisshclwwlem1  26333  numclwwlk5  26639  nndiffz1  28936  fzsplit3  28940  bcm1n  28941  ltesubnnd  28955  2sqmod  28979  pnfinf  29068  dya2iocress  29663  dya2iocbrsiga  29664  dya2icobrsiga  29665  dya2icoseg  29666  dya2iocucvr  29673  sxbrsigalem2  29675  ballotlemfc0  29881  ballotlemfcc  29882  ballotlemodife  29886  ballotlemimin  29894  ballotlemsgt1  29899  ballotlemsel1i  29901  ballotlemsi  29903  ballotlemsima  29904  ballotlemrv2  29910  ballotlemfrceq  29917  ballotlemfrcn0  29918  ballotlemirc  29920  subfacval3  30425  erdszelem8  30434  erdszelem9  30435  supfz  30866  inffz  30867  inffzOLD  30868  dnizeq0  31635  dnizphlfeqhlf  31636  dnibndlem13  31650  knoppndvlem1  31673  knoppndvlem2  31674  knoppndvlem7  31679  knoppndvlem19  31691  knoppndvlem21  31693  ltflcei  32567  leceifl  32568  poimirlem1  32580  poimirlem2  32581  poimirlem6  32585  poimirlem7  32586  poimirlem8  32587  poimirlem15  32594  poimirlem16  32595  poimirlem17  32596  poimirlem19  32598  poimirlem20  32599  poimirlem23  32602  poimirlem24  32603  poimirlem27  32606  poimirlem29  32608  poimirlem31  32610  poimirlem32  32611  mblfinlem2  32617  itg2addnclem2  32632  mettrifi  32723  cntotbnd  32765  lzunuz  36349  lzenom  36351  diophin  36354  irrapxlem1  36404  irrapxlem2  36405  irrapxlem3  36406  irrapxlem4  36407  pellexlem5  36415  pellexlem6  36416  rmspecfund  36492  rmxypos  36532  ltrmynn0  36533  ltrmxnn0  36534  ltrmy  36537  rmyeq0  36538  rmyeq  36539  lermy  36540  rmyabs  36543  jm2.24nn  36544  jm2.17a  36545  jm2.17b  36546  jm2.17c  36547  jm2.24  36548  rmygeid  36549  acongrep  36565  fzmaxdif  36566  acongeq  36568  jm2.22  36580  jm2.23  36581  jm2.26lem3  36586  jm2.27a  36590  jm3.1lem1  36602  jm3.1lem3  36604  expdiophlem1  36606  prmunb2  37532  nzprmdif  37540  hashnzfzclim  37543  binomcxplemnn0  37570  uzwo4  38246  ssinc  38292  ssdec  38293  zltlesub  38438  monoords  38452  fzisoeu  38455  fperiodmul  38459  fzdifsuc2  38466  iuneqfzuzlem  38491  fmul01  38647  fmul01lt1lem1  38651  fmul01lt1lem2  38652  climsuselem1  38674  climsuse  38675  sumnnodd  38697  ltmod  38705  ioodvbdlimc1lem2  38822  ioodvbdlimc2lem  38824  dvnmul  38833  dvnprodlem1  38836  dvnprodlem2  38837  iblspltprt  38865  itgspltprt  38871  stoweidlem3  38896  stoweidlem11  38904  stoweidlem20  38913  stoweidlem26  38919  stoweidlem34  38927  stoweidlem59  38952  stirlinglem5  38971  dirkertrigeqlem3  38993  dirkeritg  38995  dirkercncflem1  38996  dirkercncflem2  38997  dirkercncflem4  38999  fourierdlem4  39004  fourierdlem6  39006  fourierdlem7  39007  fourierdlem11  39011  fourierdlem12  39012  fourierdlem15  39015  fourierdlem19  39019  fourierdlem20  39020  fourierdlem25  39025  fourierdlem26  39026  fourierdlem34  39034  fourierdlem35  39035  fourierdlem41  39041  fourierdlem48  39047  fourierdlem49  39048  fourierdlem50  39049  fourierdlem51  39050  fourierdlem54  39053  fourierdlem63  39062  fourierdlem64  39063  fourierdlem65  39064  fourierdlem71  39070  fourierdlem79  39078  fourierdlem89  39088  fourierdlem90  39089  fourierdlem91  39090  fourierdlem102  39101  fourierdlem103  39102  fourierdlem104  39103  fourierdlem114  39113  fouriersw  39124  elaa2lem  39126  etransclem3  39130  etransclem4  39131  etransclem7  39134  etransclem10  39137  etransclem15  39142  etransclem19  39146  etransclem23  39150  etransclem24  39151  etransclem25  39152  etransclem27  39154  etransclem31  39158  etransclem32  39159  etransclem35  39162  etransclem41  39168  etransclem44  39171  etransclem46  39173  etransclem48  39175  iundjiun  39353  caratheodorylem1  39416  fzopredsuc  39946  iccpartgt  39965  icceuelpartlem  39973  icceuelpart  39974  iccpartnel  39976  lighneallem2  40061  proththd  40069  dfodd4  40109  oexpnegALTV  40126  nnoALTV  40144  gbogt5  40184  gboage9  40186  stgoldbwt  40198  bgoldbst  40200  sgoldbalt  40203  bgoldbtbndlem1  40221  bgoldbtbndlem2  40222  bgoldbtbndlem3  40223  bgoldbtbnd  40225  bgoldbachlt  40227  tgblthelfgott  40229  tgoldbach  40232  bgoldbachltOLD  40234  tgblthelfgottOLD  40236  tgoldbachOLD  40239  2elfz2melfz  40355  elfzelfzlble  40358  fsummsndifre  40371  pthdlem1  40972  crctcsh1wlkn0  41024  crctcsh  41027  clwwisshclwwslemlem  41233  eucrctshift  41411  pw2m1lepw2m1  42104  m1modmmod  42110  difmodm1lt  42111  fllogbd  42152  logbpw2m1  42159  fllog2  42160  nnpw2blen  42172  nnolog2flm1  42182  dignn0flhalflem1  42207  dignn0flhalflem2  42208