Theorem zred 12673

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

Syntax hints:   → wi 4   ∈ wcel 2105  ℝcr 11115  ℤcz 12565

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1912  ax-6 1970  ax-7 2010  ax-8 2107  ax-9 2115  ax-ext 2702

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 845  df-3or 1087  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1781  df-sb 2067  df-clab 2709  df-cleq 2723  df-clel 2809  df-rab 3432  df-v 3475  df-dif 3951  df-un 3953  df-in 3955  df-ss 3965  df-nul 4323  df-if 4529  df-sn 4629  df-pr 4631  df-op 4635  df-uni 4909  df-br 5149  df-iota 6495  df-fv 6551  df-ov 7415  df-neg 11454  df-z 12566

This theorem is referenced by:  zcnd  12674  suprfinzcl  12683  eluzmn  12836  eluzelre  12840  eluzadd  12858  subeluzsub  12866  uzm1  12867  zsupss  12928  suprzcl2  12929  uzwo3  12934  rpnnen1lem3  12970  rpnnen1lem5  12972  zltaddlt1le  13489  fzsplit2  13533  fzdisj  13535  ssfzunsnext  13553  fzpreddisj  13557  fznatpl1  13562  fzp1disj  13567  uzdisj  13581  fzm1  13588  fz0fzdiffz0  13617  elfzmlbm  13618  elfzmlbp  13619  difelfznle  13622  nn0disj  13624  elfzolt3  13649  fzonel  13653  fzospliti  13671  fzodisj  13673  fzouzdisj  13675  fzodisjsn  13677  fzonmapblen  13685  fzoaddel  13692  elincfzoext  13697  reflcl  13768  flge  13777  flwordi  13784  fladdz  13797  2tnp1ge0ge0  13801  flhalf  13802  fldiv4p1lem1div2  13807  fldiv4lem1div2uz2  13808  fldiv4lem1div2  13809  flleceil  13825  fleqceilz  13826  quoremz  13827  uzsup  13835  modmul12d  13897  modaddmodup  13906  modaddmodlo  13907  modfzo0difsn  13915  modsumfzodifsn  13916  addmodlteq  13918  om2uzlti  13922  om2uzf1oi  13925  seqf1olem1  14014  seqf1olem2  14015  bcval4  14274  bcp1nk  14284  bcval5  14285  fzsdom2  14395  seqcoll  14432  seqcoll2  14433  ccatrn  14546  ccatalpha  14550  cshwidxmodr  14761  fzomaxdiflem  15296  fzomaxdif  15297  rexuzre  15306  limsupgre  15432  rlimclim1  15496  isercoll  15621  iseralt  15638  fsumm1  15704  fsum1p  15706  fsum0diaglem  15729  modfsummods  15746  isumsplit  15793  climcndslem1  15802  mertenslem1  15837  ntrivcvgmul  15855  fprodntriv  15893  fprod1p  15919  fprodeq0  15926  fallfacval4  15994  bpoly4  16010  fzo0dvdseq  16273  dvdsmod  16279  oexpneg  16295  mod2eq1n2dvds  16297  ltoddhalfle  16311  flodddiv4t2lthalf  16366  bitsp1  16379  bitsfzolem  16382  bitsfzo  16383  bitsmod  16384  bitscmp  16386  bitsinv1lem  16389  sadaddlem  16414  bitsres  16421  bitsuz  16422  smumul  16441  gcd0id  16467  gcdneg  16470  dfgcd2  16495  nn0seqcvgd  16514  lcmgcdlem  16550  nprm  16632  prmdvdsfz  16649  isprm5  16651  isprm7  16652  coprm  16655  prmexpb  16664  prmfac1  16665  hashdvds  16715  crth  16718  eulerthlem2  16722  fermltl  16724  prmdiv  16725  prmdiveq  16726  hashgcdlem  16728  odzdvds  16735  vfermltlALT  16742  modprm0  16745  modprmn0modprm0  16747  prm23ge5  16755  pythagtriplem13  16767  pcxcl  16801  pcaddlem  16828  pcadd  16829  pcfac  16839  qexpz  16841  prmunb  16854  1arithlem4  16866  4sqlem5  16882  4sqlem6  16883  4sqlem7  16884  4sqlem10  16887  4sqlem11  16895  4sqlem12  16896  4sqlem15  16899  4sqlem16  16900  4sqlem17  16901  vdwnnlem3  16937  prmgaplem7  16997  cshwshashlem3  17038  subgmulg  19060  mndodconglem  19454  odnncl  19458  odmod  19459  oddvds  19460  dfod2  19477  sylow1lem3  19513  efgsp1  19650  efgredleme  19656  telgsumfzs  19902  zringlpirlem1  21237  zringlpirlem3  21239  znf1o  21330  zcld  24562  ovoliunlem1  25264  ovoliunlem2  25265  dyadss  25356  dyaddisjlem  25357  dyadmaxlem  25359  dvfsumle  25787  dvfsumge  25788  dvfsumabs  25789  dvfsumlem1  25792  dvfsumlem3  25794  degltlem1  25839  plyco0  25955  plyeq0lem  25973  plydivex  26060  aannenlem1  26091  efif1olem2  26303  nnlogbexp  26537  logblt  26540  ang180lem1  26565  ang180lem3  26567  wilthlem2  26824  basellem3  26838  basellem4  26839  ppiprm  26906  chtdif  26913  ppidif  26918  chtub  26966  mersenne  26981  bcmono  27031  bcmax  27032  bposlem1  27038  bposlem3  27040  bposlem5  27042  bposlem6  27043  lgsval2lem  27061  lgsvalmod  27070  lgsneg  27075  lgsmod  27077  lgsdilem  27078  lgsdirprm  27085  lgsdilem2  27087  lgsne0  27089  lgssq  27091  lgssq2  27092  lgsqr  27105  lgsdchr  27109  gausslemma2dlem1a  27119  gausslemma2dlem3  27122  gausslemma2dlem5a  27124  gausslemma2dlem6  27126  gausslemma2d  27128  lgseisenlem1  27129  lgseisenlem2  27130  lgseisenlem3  27131  lgseisenlem4  27132  lgsquadlem1  27134  lgsquadlem2  27135  lgsquadlem3  27136  lgsquad3  27141  2lgslem1a2  27144  2lgslem1  27148  2lgslem2  27149  2sqlem3  27174  2sqlem8  27180  2sqblem  27185  2sqmod  27190  chebbnd1lem1  27223  chebbnd1lem2  27224  chebbnd1lem3  27225  dchrmusum2  27248  dchrvmasumlem1  27249  dchrvmasum2lem  27250  dchrvmasum2if  27251  dchrvmasumlem3  27253  dchrvmasumiflem2  27256  dchrisum0lem1  27270  dchrmusumlem  27276  mudivsum  27284  mulogsumlem  27285  mulogsum  27286  mulog2sumlem2  27289  mulog2sumlem3  27290  selberglem1  27299  selberglem2  27300  pntpbnd1  27340  pntlemg  27352  pntlemf  27359  qabvle  27379  padicabv  27384  padicabvcxp  27386  ostth2lem2  27388  axlowdimlem13  28494  axlowdimlem16  28497  pthdlem1  29305  crctcshwlkn0  29357  crctcsh  29360  clwwisshclwwslemlem  29548  eucrctshift  29778  nndiffz1  32279  fzsplit3  32287  bcm1n  32288  fzone1  32293  suppssnn0  32299  ltesubnnd  32310  wrdt2ind  32399  cshwrnid  32407  cycpmfv2  32558  cycpmco2lem6  32575  cycpmco2lem7  32576  cycpmrn  32587  cyc3conja  32601  pnfinf  32614  fermltlchr  32767  znfermltl  32768  dya2iocress  33586  dya2iocbrsiga  33587  dya2icobrsiga  33588  dya2icoseg  33589  dya2iocucvr  33596  sxbrsigalem2  33598  ballotlemfc0  33804  ballotlemfcc  33805  ballotlemodife  33809  ballotlemimin  33817  ballotlemsgt1  33822  ballotlemsel1i  33824  ballotlemsi  33826  ballotlemsima  33827  ballotlemrv2  33833  ballotlemfrceq  33840  ballotlemfrcn0  33841  ballotlemirc  33843  fsum2dsub  33932  reprlt  33944  reprgt  33946  breprexplemc  33957  tgoldbachgnn  33984  tgoldbachgt  33988  subfacval3  34493  erdszelem8  34502  erdszelem9  34503  supfz  35017  inffz  35018  gg-dvfsumle  35479  dnizeq0  35667  dnizphlfeqhlf  35668  dnibndlem13  35682  knoppndvlem1  35704  knoppndvlem2  35705  knoppndvlem7  35710  knoppndvlem19  35722  knoppndvlem21  35724  ltflcei  36792  leceifl  36793  poimirlem1  36805  poimirlem2  36806  poimirlem6  36810  poimirlem7  36811  poimirlem8  36812  poimirlem15  36819  poimirlem16  36820  poimirlem17  36821  poimirlem19  36823  poimirlem20  36824  poimirlem23  36827  poimirlem24  36828  poimirlem27  36831  poimirlem29  36833  poimirlem31  36835  poimirlem32  36836  mblfinlem2  36842  itg2addnclem2  36856  mettrifi  36941  cntotbnd  36980  fzne2d  41165  aks4d1lem1  41246  aks4d1p1p3  41253  aks4d1p1p2  41254  aks4d1p1p4  41255  aks4d1p1  41260  aks4d1p2  41261  aks4d1p3  41262  aks4d1p5  41264  aks4d1p6  41265  aks4d1p7d1  41266  aks4d1p7  41267  aks4d1p8d3  41270  aks4d1p8  41271  aks4d1p9  41272  2ap1caineq  41280  sticksstones6  41286  sticksstones7  41287  sticksstones10  41290  sticksstones12a  41292  sticksstones12  41293  sticksstones22  41303  metakunt7  41310  metakunt12  41315  metakunt15  41318  metakunt16  41319  metakunt22  41325  metakunt28  41331  prodsplit  41340  frlmvscadiccat  41399  sumcubes  41526  dffltz  41691  lzunuz  41821  lzenom  41823  diophin  41825  irrapxlem1  41875  irrapxlem2  41876  irrapxlem3  41877  irrapxlem4  41878  pellexlem5  41886  pellexlem6  41887  rmspecfund  41962  rmxypos  42001  ltrmynn0  42002  ltrmxnn0  42003  ltrmy  42006  rmyeq0  42007  rmyeq  42008  lermy  42009  rmyabs  42012  jm2.24nn  42013  jm2.17a  42014  jm2.17b  42015  jm2.17c  42016  jm2.24  42017  rmygeid  42018  acongrep  42034  fzmaxdif  42035  acongeq  42037  jm2.22  42049  jm2.23  42050  jm2.26lem3  42055  jm2.27a  42059  jm3.1lem1  42071  jm3.1lem3  42073  expdiophlem1  42075  fzuntd  42522  fzunt1d  42523  fzuntgd  42524  prmunb2  43385  nzprmdif  43393  hashnzfzclim  43396  binomcxplemnn0  43423  uzwo4  44054  ssinc  44090  ssdec  44091  zltlesub  44306  monoords  44318  fzisoeu  44321  fperiodmul  44325  fzdifsuc2  44331  iuneqfzuzlem  44355  uzublem  44451  zxrd  44474  uzinico  44584  uzubioo  44591  fmul01  44607  fmul01lt1lem1  44611  fmul01lt1lem2  44612  climsuselem1  44634  climsuse  44635  sumnnodd  44657  ltmod  44665  limsupresuz  44730  limsupubuzlem  44739  limsupequzlem  44749  limsupmnfuzlem  44753  limsupequzmptlem  44755  limsupre3uzlem  44762  supcnvlimsup  44767  limsup10exlem  44799  liminfresuz  44811  liminfvaluz  44819  limsupvaluz3  44825  ioodvbdlimc1lem2  44959  ioodvbdlimc2lem  44961  dvnmul  44970  dvnprodlem1  44973  dvnprodlem2  44974  iblspltprt  45000  itgspltprt  45006  stoweidlem3  45030  stoweidlem11  45038  stoweidlem20  45047  stoweidlem26  45053  stoweidlem34  45061  stoweidlem59  45086  stirlinglem5  45105  dirkertrigeqlem3  45127  dirkeritg  45129  dirkercncflem1  45130  dirkercncflem2  45131  dirkercncflem4  45133  fourierdlem4  45138  fourierdlem6  45140  fourierdlem7  45141  fourierdlem11  45145  fourierdlem12  45146  fourierdlem15  45149  fourierdlem19  45153  fourierdlem20  45154  fourierdlem25  45159  fourierdlem26  45160  fourierdlem34  45168  fourierdlem35  45169  fourierdlem41  45175  fourierdlem48  45181  fourierdlem49  45182  fourierdlem50  45183  fourierdlem51  45184  fourierdlem54  45187  fourierdlem63  45196  fourierdlem64  45197  fourierdlem65  45198  fourierdlem71  45204  fourierdlem79  45212  fourierdlem89  45222  fourierdlem90  45223  fourierdlem91  45224  fourierdlem102  45235  fourierdlem103  45236  fourierdlem104  45237  fourierdlem114  45247  fouriersw  45258  elaa2lem  45260  etransclem3  45264  etransclem4  45265  etransclem7  45268  etransclem10  45271  etransclem15  45276  etransclem19  45280  etransclem23  45284  etransclem24  45285  etransclem25  45286  etransclem27  45288  etransclem31  45292  etransclem32  45293  etransclem35  45296  etransclem41  45302  etransclem44  45305  etransclem46  45307  etransclem48  45309  iundjiun  45487  caratheodorylem1  45553  smflimsuplem4  45850  smfliminflem  45857  natglobalincr  45902  2elfz2melfz  46337  elfzelfzlble  46340  fzopredsuc  46342  fsummsndifre  46351  iccpartgt  46406  icceuelpartlem  46414  icceuelpart  46415  iccpartnel  46417  lighneallem2  46585  proththd  46593  dfodd4  46638  oexpnegALTV  46656  nnoALTV  46674  evenltle  46696  fpprwppr  46718  gbowgt5  46741  gboge9  46743  stgoldbwt  46755  sbgoldbst  46757  sbgoldbalt  46760  sgoldbeven3prm  46762  mogoldbb  46764  bgoldbtbndlem1  46784  bgoldbtbndlem2  46785  bgoldbtbndlem3  46786  bgoldbtbnd  46788  bgoldbachlt  46792  tgblthelfgott  46794  tgoldbach  46796  pw2m1lepw2m1  47301  m1modmmod  47307  difmodm1lt  47308  fllogbd  47346  logbpw2m1  47353  fllog2  47354  nnpw2blen  47366  nnolog2flm1  47376  dignn0flhalflem1  47401  dignn0flhalflem2  47402