Theorem zred 12633

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

Syntax hints:   → wi 4   ∈ wcel 2114  ℝcr 11037  ℤcz 12524

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3or 1088  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-sb 2069  df-clab 2715  df-cleq 2728  df-clel 2811  df-rab 3390  df-v 3431  df-dif 3892  df-un 3894  df-ss 3906  df-nul 4274  df-if 4467  df-sn 4568  df-pr 4570  df-op 4574  df-uni 4851  df-br 5086  df-iota 6454  df-fv 6506  df-ov 7370  df-neg 11380  df-z 12525

This theorem is referenced by:  zcnd  12634  suprfinzcl  12643  eluzmn  12795  eluzelre  12799  eluzadd  12817  subeluzsub  12821  uzm1  12822  zsupss  12887  suprzcl2  12888  uzwo3  12893  rpnnen1lem3  12929  rpnnen1lem5  12931  zltaddlt1le  13458  fzsplit2  13503  fzdisj  13505  ssfzunsnext  13523  fzpreddisj  13527  fznatpl1  13532  fzp1disj  13537  uzdisj  13551  fzdif1  13559  fzm1  13561  fz0fzdiffz0  13591  elfzmlbm  13592  elfzmlbp  13593  difelfznle  13596  nn0disj  13598  elfzolt3  13624  fzonel  13628  fzospliti  13646  fzodisj  13648  fzouzdisj  13650  fzodisjsn  13652  elfzo0subge1  13660  elfzo0suble  13661  fzonmapblen  13663  fzoaddel  13672  elincfzoext  13678  fzone1  13739  reflcl  13755  flge  13764  flwordi  13771  fladdz  13784  2tnp1ge0ge0  13788  flhalf  13789  fldiv4p1lem1div2  13794  fldiv4lem1div2uz2  13795  fldiv4lem1div2  13796  flleceil  13812  fleqceilz  13813  quoremz  13814  uzsup  13822  modaddid  13869  modmul12d  13887  modaddmodup  13896  modaddmodlo  13897  modfzo0difsn  13905  modsumfzodifsn  13906  addmodlteq  13908  om2uzlti  13912  om2uzf1oi  13915  seqf1olem1  14003  seqf1olem2  14004  bcval4  14269  bcp1nk  14279  bcval5  14280  fzsdom2  14390  seqcoll  14426  seqcoll2  14427  ccatrn  14552  ccatalpha  14556  cshwidxmodr  14766  fzomaxdiflem  15305  fzomaxdif  15306  rexuzre  15315  limsupgre  15443  rlimclim1  15507  isercoll  15630  iseralt  15647  fsumm1  15713  fsum1p  15715  fsum0diaglem  15738  modfsummods  15756  isumsplit  15805  climcndslem1  15814  mertenslem1  15849  ntrivcvgmul  15867  fprodntriv  15907  fprod1p  15933  fprodeq0  15940  fallfacval4  16008  bpoly4  16024  fzo0dvdseq  16292  dvdsmod  16298  oexpneg  16314  mod2eq1n2dvds  16316  ltoddhalfle  16330  flodddiv4t2lthalf  16387  bitsp1  16400  bitsfzolem  16403  bitsfzo  16404  bitsmod  16405  bitscmp  16407  bitsinv1lem  16410  sadaddlem  16435  bitsres  16442  bitsuz  16443  smumul  16462  gcd0id  16488  gcdneg  16491  dfgcd2  16515  nn0seqcvgd  16539  lcmgcdlem  16575  nprm  16657  prmdvdsfz  16675  isprm5  16677  isprm7  16678  coprm  16681  prmexpb  16689  prmfac1  16690  hashdvds  16745  crth  16748  eulerthlem2  16752  fermltl  16754  prmdiv  16755  prmdiveq  16756  hashgcdlem  16758  odzdvds  16766  vfermltlALT  16773  modprm0  16776  modprmn0modprm0  16778  prm23ge5  16786  pythagtriplem13  16798  pcxcl  16832  pcaddlem  16859  pcadd  16860  pcfac  16870  qexpz  16872  prmunb  16885  1arithlem4  16897  4sqlem5  16913  4sqlem6  16914  4sqlem7  16915  4sqlem10  16918  4sqlem11  16926  4sqlem12  16927  4sqlem15  16930  4sqlem16  16931  4sqlem17  16932  vdwnnlem3  16968  prmgaplem7  17028  cshwshashlem3  17068  chnub  18588  chnso  18590  chnccat  18592  chnpof1  18596  subgmulg  19116  mndodconglem  19516  odnncl  19520  odmod  19521  oddvds  19522  dfod2  19539  sylow1lem3  19575  efgsp1  19712  efgredleme  19718  telgsumfzs  19964  zringlpirlem1  21442  zringlpirlem3  21444  fermltlchr  21509  znf1o  21531  zcld  24779  ovoliunlem1  25469  ovoliunlem2  25470  dyadss  25561  dyaddisjlem  25562  dyadmaxlem  25564  dvfsumle  25988  dvfsumge  25989  dvfsumabs  25990  dvfsumlem1  25993  dvfsumlem3  25995  degltlem1  26037  plyco0  26157  plyeq0lem  26175  plydivex  26263  aannenlem1  26294  efif1olem2  26507  nnlogbexp  26745  logblt  26748  ang180lem1  26773  ang180lem3  26775  wilthlem2  27032  basellem3  27046  basellem4  27047  ppiprm  27114  chtdif  27121  ppidif  27126  chtub  27175  mersenne  27190  bcmono  27240  bcmax  27241  bposlem1  27247  bposlem3  27249  bposlem5  27251  bposlem6  27252  lgsval2lem  27270  lgsvalmod  27279  lgsneg  27284  lgsmod  27286  lgsdilem  27287  lgsdirprm  27294  lgsdilem2  27296  lgsne0  27298  lgssq  27300  lgssq2  27301  lgsqr  27314  lgsdchr  27318  gausslemma2dlem1a  27328  gausslemma2dlem3  27331  gausslemma2dlem5a  27333  gausslemma2dlem6  27335  gausslemma2d  27337  lgseisenlem1  27338  lgseisenlem2  27339  lgseisenlem3  27340  lgseisenlem4  27341  lgsquadlem1  27343  lgsquadlem2  27344  lgsquadlem3  27345  lgsquad3  27350  2lgslem1a2  27353  2lgslem1  27357  2lgslem2  27358  2sqlem3  27383  2sqlem8  27389  2sqblem  27394  2sqmod  27399  chebbnd1lem1  27432  chebbnd1lem2  27433  chebbnd1lem3  27434  dchrmusum2  27457  dchrvmasumlem1  27458  dchrvmasum2lem  27459  dchrvmasum2if  27460  dchrvmasumlem3  27462  dchrvmasumiflem2  27465  dchrisum0lem1  27479  dchrmusumlem  27485  mudivsum  27493  mulogsumlem  27494  mulogsum  27495  mulog2sumlem2  27498  mulog2sumlem3  27499  selberglem1  27508  selberglem2  27509  pntpbnd1  27549  pntlemg  27561  pntlemf  27568  qabvle  27588  padicabv  27593  padicabvcxp  27595  ostth2lem2  27597  axlowdimlem13  29023  axlowdimlem16  29026  pthdlem1  29834  crctcshwlkn0  29889  crctcsh  29892  clwwisshclwwslemlem  30083  eucrctshift  30313  nndiffz1  32859  fzsplit3  32866  bcm1n  32868  suppssnn0  32878  ltesubnnd  32896  wrdt2ind  33013  cshwrnid  33021  cycpmfv2  33175  cycpmco2lem6  33192  cycpmco2lem7  33193  cycpmrn  33204  cyc3conja  33218  pnfinf  33244  znfermltl  33426  constrext2chnlem  33894  cos9thpiminplylem1  33926  cos9thpiminplylem2  33927  dya2iocress  34418  dya2iocbrsiga  34419  dya2icobrsiga  34420  dya2icoseg  34421  dya2iocucvr  34428  sxbrsigalem2  34430  ballotlemfc0  34637  ballotlemfcc  34638  ballotlemodife  34642  ballotlemimin  34650  ballotlemsgt1  34655  ballotlemsel1i  34657  ballotlemsi  34659  ballotlemsima  34660  ballotlemrv2  34666  ballotlemfrceq  34673  ballotlemfrcn0  34674  ballotlemirc  34676  fsum2dsub  34751  reprlt  34763  reprgt  34765  breprexplemc  34776  tgoldbachgnn  34803  tgoldbachgt  34807  subfacval3  35371  erdszelem8  35380  erdszelem9  35381  supfz  35911  inffz  35912  dnizeq0  36735  dnizphlfeqhlf  36736  dnibndlem13  36750  knoppndvlem1  36772  knoppndvlem2  36773  knoppndvlem7  36778  knoppndvlem19  36790  knoppndvlem21  36792  ltflcei  37929  leceifl  37930  poimirlem1  37942  poimirlem2  37943  poimirlem6  37947  poimirlem7  37948  poimirlem8  37949  poimirlem15  37956  poimirlem16  37957  poimirlem17  37958  poimirlem19  37960  poimirlem20  37961  poimirlem23  37964  poimirlem24  37965  poimirlem27  37968  poimirlem29  37970  poimirlem31  37972  poimirlem32  37973  mblfinlem2  37979  itg2addnclem2  37993  mettrifi  38078  cntotbnd  38117  fzne2d  42419  aks4d1lem1  42501  aks4d1p1p3  42508  aks4d1p1p2  42509  aks4d1p1p4  42510  aks4d1p1  42515  aks4d1p2  42516  aks4d1p3  42517  aks4d1p5  42519  aks4d1p6  42520  aks4d1p7d1  42521  aks4d1p7  42522  aks4d1p8d3  42525  aks4d1p8  42526  aks4d1p9  42527  posbezout  42539  aks6d1c1  42555  hashscontpow1  42560  hashscontpow  42561  aks6d1c2  42569  aks6d1c5lem1  42575  2ap1caineq  42584  sticksstones6  42590  sticksstones7  42591  sticksstones10  42594  sticksstones12a  42596  sticksstones12  42597  sticksstones22  42607  bcled  42617  bcle2d  42618  aks6d1c7lem1  42619  aks6d1c7lem2  42620  aks6d1c7  42623  aks5lem6  42631  unitscyglem2  42635  unitscyglem4  42637  aks5lem8  42640  sumcubes  42745  frlmvscadiccat  42951  dffltz  43067  lzunuz  43200  lzenom  43202  diophin  43204  irrapxlem1  43250  irrapxlem2  43251  irrapxlem3  43252  irrapxlem4  43253  pellexlem5  43261  pellexlem6  43262  rmspecfund  43337  rmxypos  43375  ltrmynn0  43376  ltrmxnn0  43377  ltrmy  43380  rmyeq0  43381  rmyeq  43382  lermy  43383  rmyabs  43386  jm2.24nn  43387  jm2.17a  43388  jm2.17b  43389  jm2.17c  43390  jm2.24  43391  rmygeid  43392  acongrep  43408  fzmaxdif  43409  acongeq  43411  jm2.22  43423  jm2.23  43424  jm2.26lem3  43429  jm2.27a  43433  jm3.1lem1  43445  jm3.1lem3  43447  expdiophlem1  43449  fzuntd  43883  fzunt1d  43884  fzuntgd  43885  prmunb2  44738  nzprmdif  44746  hashnzfzclim  44749  binomcxplemnn0  44776  uzwo4  45484  ssinc  45517  ssdec  45518  zltlesub  45718  monoords  45730  fzisoeu  45733  fperiodmul  45737  fzdifsuc2  45743  iuneqfzuzlem  45764  uzublem  45858  zxrd  45881  uzinico  45989  uzubioo  45995  fmul01  46010  fmul01lt1lem1  46014  fmul01lt1lem2  46015  climsuselem1  46037  climsuse  46038  sumnnodd  46060  ltmod  46066  limsupresuz  46131  limsupubuzlem  46140  limsupequzlem  46150  limsupmnfuzlem  46154  limsupequzmptlem  46156  limsupre3uzlem  46163  supcnvlimsup  46168  limsup10exlem  46200  liminfresuz  46212  liminfvaluz  46220  limsupvaluz3  46226  ioodvbdlimc1lem2  46360  ioodvbdlimc2lem  46362  dvnmul  46371  dvnprodlem1  46374  dvnprodlem2  46375  iblspltprt  46401  itgspltprt  46407  stoweidlem3  46431  stoweidlem11  46439  stoweidlem20  46448  stoweidlem26  46454  stoweidlem34  46462  stoweidlem59  46487  stirlinglem5  46506  dirkertrigeqlem3  46528  dirkeritg  46530  dirkercncflem1  46531  dirkercncflem2  46532  dirkercncflem4  46534  fourierdlem4  46539  fourierdlem6  46541  fourierdlem7  46542  fourierdlem11  46546  fourierdlem12  46547  fourierdlem15  46550  fourierdlem19  46554  fourierdlem20  46555  fourierdlem25  46560  fourierdlem26  46561  fourierdlem34  46569  fourierdlem35  46570  fourierdlem41  46576  fourierdlem48  46582  fourierdlem49  46583  fourierdlem50  46584  fourierdlem51  46585  fourierdlem54  46588  fourierdlem63  46597  fourierdlem64  46598  fourierdlem65  46599  fourierdlem71  46605  fourierdlem79  46613  fourierdlem89  46623  fourierdlem90  46624  fourierdlem91  46625  fourierdlem102  46636  fourierdlem103  46637  fourierdlem104  46638  fourierdlem114  46648  fouriersw  46659  elaa2lem  46661  etransclem3  46665  etransclem4  46666  etransclem7  46669  etransclem10  46672  etransclem15  46677  etransclem19  46681  etransclem23  46685  etransclem24  46686  etransclem25  46687  etransclem27  46689  etransclem31  46693  etransclem32  46694  etransclem35  46697  etransclem41  46703  etransclem44  46706  etransclem46  46708  etransclem48  46710  iundjiun  46888  caratheodorylem1  46954  hoicvr  46976  smflimsuplem4  47251  smfliminflem  47258  ormklocald  47304  ormkglobd  47305  natglobalincr  47307  chnerlem3  47314  2elfz2melfz  47766  elfzelfzlble  47769  fzopredsuc  47772  nnmul2  47778  2ltceilhalf  47780  ceilhalfgt1  47781  ceilhalfnn  47788  submodlt  47804  m1modmmod  47812  difmodm1lt  47813  modmknepk  47816  mod2addne  47818  2timesltsq  47826  2timesltsqm1  47827  fsummsndifre  47828  iccpartgt  47887  icceuelpartlem  47895  icceuelpart  47896  iccpartnel  47898  nprmmul2  47988  nprmmul3  47989  lighneallem2  48069  proththd  48077  nprmdvdsfacm1lem4  48086  dfodd4  48135  oexpnegALTV  48153  nnoALTV  48171  evenltle  48193  fpprwppr  48215  gbowgt5  48238  gboge9  48240  stgoldbwt  48252  sbgoldbst  48254  sbgoldbalt  48257  sgoldbeven3prm  48259  mogoldbb  48261  bgoldbtbndlem1  48281  bgoldbtbndlem2  48282  bgoldbtbndlem3  48283  bgoldbtbnd  48285  bgoldbachlt  48289  tgblthelfgott  48291  tgoldbach  48293  upgrimpthslem2  48384  gpgprismgrusgra  48534  gpgedgvtx1  48538  gpgvtxedg0  48539  gpgvtxedg1  48540  gpg5nbgrvtx13starlem2  48548  gpg3nbgrvtx0  48552  gpg3kgrtriexlem1  48559  gpg3kgrtriexlem4  48562  gpg3kgrtriexlem6  48564  pw2m1lepw2m1  48996  fllogbd  49036  logbpw2m1  49043  fllog2  49044  nnpw2blen  49056  nnolog2flm1  49066  dignn0flhalflem1  49091  dignn0flhalflem2  49092