MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  zred Structured version   Visualization version   GIF version

Theorem zred 12608
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
StepHypRef Expression
1 zssre 12507 . 2 ℤ ⊆ ℝ
2 zred.1 . 2 (𝜑𝐴 ∈ ℤ)
31, 2sselid 3943 1 (𝜑𝐴 ∈ ℝ)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wcel 2107  cr 11051  cz 12500
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 2708
This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3or 1089  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-sb 2069  df-clab 2715  df-cleq 2729  df-clel 2815  df-rab 3409  df-v 3448  df-dif 3914  df-un 3916  df-in 3918  df-ss 3928  df-nul 4284  df-if 4488  df-sn 4588  df-pr 4590  df-op 4594  df-uni 4867  df-br 5107  df-iota 6449  df-fv 6505  df-ov 7361  df-neg 11389  df-z 12501
This theorem is referenced by:  zcnd  12609  suprfinzcl  12618  eluzmn  12771  eluzelre  12775  eluzadd  12793  subeluzsub  12801  uzm1  12802  zsupss  12863  suprzcl2  12864  uzwo3  12869  rpnnen1lem3  12905  rpnnen1lem5  12907  zltaddlt1le  13423  fzsplit2  13467  fzdisj  13469  ssfzunsnext  13487  fzpreddisj  13491  fznatpl1  13496  fzp1disj  13501  uzdisj  13515  fzm1  13522  fz0fzdiffz0  13551  elfzmlbm  13552  elfzmlbp  13553  difelfznle  13556  nn0disj  13558  elfzolt3  13583  fzonel  13587  fzospliti  13605  fzodisj  13607  fzouzdisj  13609  fzodisjsn  13611  fzonmapblen  13619  fzoaddel  13626  elincfzoext  13631  reflcl  13702  flge  13711  flwordi  13718  fladdz  13731  2tnp1ge0ge0  13735  flhalf  13736  fldiv4p1lem1div2  13741  fldiv4lem1div2uz2  13742  fldiv4lem1div2  13743  flleceil  13759  fleqceilz  13760  quoremz  13761  uzsup  13769  modmul12d  13831  modaddmodup  13840  modaddmodlo  13841  modfzo0difsn  13849  modsumfzodifsn  13850  addmodlteq  13852  om2uzlti  13856  om2uzf1oi  13859  seqf1olem1  13948  seqf1olem2  13949  bcval4  14208  bcp1nk  14218  bcval5  14219  fzsdom2  14329  seqcoll  14364  seqcoll2  14365  ccatrn  14478  ccatalpha  14482  cshwidxmodr  14693  fzomaxdiflem  15228  fzomaxdif  15229  rexuzre  15238  limsupgre  15364  rlimclim1  15428  isercoll  15553  iseralt  15570  fsumm1  15637  fsum1p  15639  fsum0diaglem  15662  modfsummods  15679  isumsplit  15726  climcndslem1  15735  mertenslem1  15770  ntrivcvgmul  15788  fprodntriv  15826  fprod1p  15852  fprodeq0  15859  fallfacval4  15927  bpoly4  15943  fzo0dvdseq  16206  dvdsmod  16212  oexpneg  16228  mod2eq1n2dvds  16230  ltoddhalfle  16244  flodddiv4t2lthalf  16299  bitsp1  16312  bitsfzolem  16315  bitsfzo  16316  bitsmod  16317  bitscmp  16319  bitsinv1lem  16322  sadaddlem  16347  bitsres  16354  bitsuz  16355  smumul  16374  gcd0id  16400  gcdneg  16403  dfgcd2  16428  nn0seqcvgd  16447  lcmgcdlem  16483  nprm  16565  prmdvdsfz  16582  isprm5  16584  isprm7  16585  coprm  16588  prmexpb  16597  prmfac1  16598  hashdvds  16648  crth  16651  eulerthlem2  16655  fermltl  16657  prmdiv  16658  prmdiveq  16659  hashgcdlem  16661  odzdvds  16668  vfermltlALT  16675  modprm0  16678  modprmn0modprm0  16680  prm23ge5  16688  pythagtriplem13  16700  pcxcl  16734  pcaddlem  16761  pcadd  16762  pcfac  16772  qexpz  16774  prmunb  16787  1arithlem4  16799  4sqlem5  16815  4sqlem6  16816  4sqlem7  16817  4sqlem10  16820  4sqlem11  16828  4sqlem12  16829  4sqlem15  16832  4sqlem16  16833  4sqlem17  16834  vdwnnlem3  16870  prmgaplem7  16930  cshwshashlem3  16971  subgmulg  18943  mndodconglem  19324  odnncl  19328  odmod  19329  oddvds  19330  dfod2  19347  sylow1lem3  19383  efgsp1  19520  efgredleme  19526  telgsumfzs  19767  zringlpirlem1  20886  zringlpirlem3  20888  znf1o  20961  zcld  24179  ovoliunlem1  24869  ovoliunlem2  24870  dyadss  24961  dyaddisjlem  24962  dyadmaxlem  24964  dvfsumle  25388  dvfsumge  25389  dvfsumabs  25390  dvfsumlem1  25393  dvfsumlem3  25395  degltlem1  25440  plyco0  25556  plyeq0lem  25574  plydivex  25660  aannenlem1  25691  efif1olem2  25902  nnlogbexp  26134  logblt  26137  ang180lem1  26162  ang180lem3  26164  wilthlem2  26421  basellem3  26435  basellem4  26436  ppiprm  26503  chtdif  26510  ppidif  26515  chtub  26563  mersenne  26578  bcmono  26628  bcmax  26629  bposlem1  26635  bposlem3  26637  bposlem5  26639  bposlem6  26640  lgsval2lem  26658  lgsvalmod  26667  lgsneg  26672  lgsmod  26674  lgsdilem  26675  lgsdirprm  26682  lgsdilem2  26684  lgsne0  26686  lgssq  26688  lgssq2  26689  lgsqr  26702  lgsdchr  26706  gausslemma2dlem1a  26716  gausslemma2dlem3  26719  gausslemma2dlem5a  26721  gausslemma2dlem6  26723  gausslemma2d  26725  lgseisenlem1  26726  lgseisenlem2  26727  lgseisenlem3  26728  lgseisenlem4  26729  lgsquadlem1  26731  lgsquadlem2  26732  lgsquadlem3  26733  lgsquad3  26738  2lgslem1a2  26741  2lgslem1  26745  2lgslem2  26746  2sqlem3  26771  2sqlem8  26777  2sqblem  26782  2sqmod  26787  chebbnd1lem1  26820  chebbnd1lem2  26821  chebbnd1lem3  26822  dchrmusum2  26845  dchrvmasumlem1  26846  dchrvmasum2lem  26847  dchrvmasum2if  26848  dchrvmasumlem3  26850  dchrvmasumiflem2  26853  dchrisum0lem1  26867  dchrmusumlem  26873  mudivsum  26881  mulogsumlem  26882  mulogsum  26883  mulog2sumlem2  26886  mulog2sumlem3  26887  selberglem1  26896  selberglem2  26897  pntpbnd1  26937  pntlemg  26949  pntlemf  26956  qabvle  26976  padicabv  26981  padicabvcxp  26983  ostth2lem2  26985  axlowdimlem13  27906  axlowdimlem16  27909  pthdlem1  28717  crctcshwlkn0  28769  crctcsh  28772  clwwisshclwwslemlem  28960  eucrctshift  29190  nndiffz1  31692  fzsplit3  31700  bcm1n  31701  fzone1  31706  ltesubnnd  31721  wrdt2ind  31810  cshwrnid  31818  cycpmfv2  31966  cycpmco2lem6  31983  cycpmco2lem7  31984  cycpmrn  31995  cyc3conja  32009  pnfinf  32022  fermltlchr  32157  znfermltl  32158  dya2iocress  32877  dya2iocbrsiga  32878  dya2icobrsiga  32879  dya2icoseg  32880  dya2iocucvr  32887  sxbrsigalem2  32889  ballotlemfc0  33095  ballotlemfcc  33096  ballotlemodife  33100  ballotlemimin  33108  ballotlemsgt1  33113  ballotlemsel1i  33115  ballotlemsi  33117  ballotlemsima  33118  ballotlemrv2  33124  ballotlemfrceq  33131  ballotlemfrcn0  33132  ballotlemirc  33134  fsum2dsub  33223  reprlt  33235  reprgt  33237  breprexplemc  33248  tgoldbachgnn  33275  tgoldbachgt  33279  subfacval3  33786  erdszelem8  33795  erdszelem9  33796  supfz  34304  inffz  34305  dnizeq0  34941  dnizphlfeqhlf  34942  dnibndlem13  34956  knoppndvlem1  34978  knoppndvlem2  34979  knoppndvlem7  34984  knoppndvlem19  34996  knoppndvlem21  34998  ltflcei  36069  leceifl  36070  poimirlem1  36082  poimirlem2  36083  poimirlem6  36087  poimirlem7  36088  poimirlem8  36089  poimirlem15  36096  poimirlem16  36097  poimirlem17  36098  poimirlem19  36100  poimirlem20  36101  poimirlem23  36104  poimirlem24  36105  poimirlem27  36108  poimirlem29  36110  poimirlem31  36112  poimirlem32  36113  mblfinlem2  36119  itg2addnclem2  36133  mettrifi  36219  cntotbnd  36258  fzne2d  40441  aks4d1lem1  40522  aks4d1p1p3  40529  aks4d1p1p2  40530  aks4d1p1p4  40531  aks4d1p1  40536  aks4d1p2  40537  aks4d1p3  40538  aks4d1p5  40540  aks4d1p6  40541  aks4d1p7d1  40542  aks4d1p7  40543  aks4d1p8d3  40546  aks4d1p8  40547  aks4d1p9  40548  2ap1caineq  40556  sticksstones6  40562  sticksstones7  40563  sticksstones10  40566  sticksstones12a  40568  sticksstones12  40569  sticksstones22  40579  metakunt7  40586  metakunt12  40591  metakunt15  40594  metakunt16  40595  metakunt22  40601  metakunt28  40607  prodsplit  40616  frlmvscadiccat  40684  dffltz  40975  lzunuz  41094  lzenom  41096  diophin  41098  irrapxlem1  41148  irrapxlem2  41149  irrapxlem3  41150  irrapxlem4  41151  pellexlem5  41159  pellexlem6  41160  rmspecfund  41235  rmxypos  41274  ltrmynn0  41275  ltrmxnn0  41276  ltrmy  41279  rmyeq0  41280  rmyeq  41281  lermy  41282  rmyabs  41285  jm2.24nn  41286  jm2.17a  41287  jm2.17b  41288  jm2.17c  41289  jm2.24  41290  rmygeid  41291  acongrep  41307  fzmaxdif  41308  acongeq  41310  jm2.22  41322  jm2.23  41323  jm2.26lem3  41328  jm2.27a  41332  jm3.1lem1  41344  jm3.1lem3  41346  expdiophlem1  41348  fzuntd  41735  fzunt1d  41736  fzuntgd  41737  prmunb2  42598  nzprmdif  42606  hashnzfzclim  42609  binomcxplemnn0  42636  uzwo4  43268  ssinc  43304  ssdec  43305  zltlesub  43526  monoords  43538  fzisoeu  43541  fperiodmul  43545  fzdifsuc2  43551  iuneqfzuzlem  43575  uzublem  43672  zxrd  43695  uzinico  43805  uzubioo  43812  fmul01  43828  fmul01lt1lem1  43832  fmul01lt1lem2  43833  climsuselem1  43855  climsuse  43856  sumnnodd  43878  ltmod  43886  limsupresuz  43951  limsupubuzlem  43960  limsupequzlem  43970  limsupmnfuzlem  43974  limsupequzmptlem  43976  limsupre3uzlem  43983  supcnvlimsup  43988  limsup10exlem  44020  liminfresuz  44032  liminfvaluz  44040  limsupvaluz3  44046  ioodvbdlimc1lem2  44180  ioodvbdlimc2lem  44182  dvnmul  44191  dvnprodlem1  44194  dvnprodlem2  44195  iblspltprt  44221  itgspltprt  44227  stoweidlem3  44251  stoweidlem11  44259  stoweidlem20  44268  stoweidlem26  44274  stoweidlem34  44282  stoweidlem59  44307  stirlinglem5  44326  dirkertrigeqlem3  44348  dirkeritg  44350  dirkercncflem1  44351  dirkercncflem2  44352  dirkercncflem4  44354  fourierdlem4  44359  fourierdlem6  44361  fourierdlem7  44362  fourierdlem11  44366  fourierdlem12  44367  fourierdlem15  44370  fourierdlem19  44374  fourierdlem20  44375  fourierdlem25  44380  fourierdlem26  44381  fourierdlem34  44389  fourierdlem35  44390  fourierdlem41  44396  fourierdlem48  44402  fourierdlem49  44403  fourierdlem50  44404  fourierdlem51  44405  fourierdlem54  44408  fourierdlem63  44417  fourierdlem64  44418  fourierdlem65  44419  fourierdlem71  44425  fourierdlem79  44433  fourierdlem89  44443  fourierdlem90  44444  fourierdlem91  44445  fourierdlem102  44456  fourierdlem103  44457  fourierdlem104  44458  fourierdlem114  44468  fouriersw  44479  elaa2lem  44481  etransclem3  44485  etransclem4  44486  etransclem7  44489  etransclem10  44492  etransclem15  44497  etransclem19  44501  etransclem23  44505  etransclem24  44506  etransclem25  44507  etransclem27  44509  etransclem31  44513  etransclem32  44514  etransclem35  44517  etransclem41  44523  etransclem44  44526  etransclem46  44528  etransclem48  44530  iundjiun  44708  caratheodorylem1  44774  smflimsuplem4  45071  smfliminflem  45078  natglobalincr  45123  2elfz2melfz  45557  elfzelfzlble  45560  fzopredsuc  45562  fsummsndifre  45571  iccpartgt  45626  icceuelpartlem  45634  icceuelpart  45635  iccpartnel  45637  lighneallem2  45805  proththd  45813  dfodd4  45858  oexpnegALTV  45876  nnoALTV  45894  evenltle  45916  fpprwppr  45938  gbowgt5  45961  gboge9  45963  stgoldbwt  45975  sbgoldbst  45977  sbgoldbalt  45980  sgoldbeven3prm  45982  mogoldbb  45984  bgoldbtbndlem1  46004  bgoldbtbndlem2  46005  bgoldbtbndlem3  46006  bgoldbtbnd  46008  bgoldbachlt  46012  tgblthelfgott  46014  tgoldbach  46016  pw2m1lepw2m1  46608  m1modmmod  46614  difmodm1lt  46615  fllogbd  46653  logbpw2m1  46660  fllog2  46661  nnpw2blen  46673  nnolog2flm1  46683  dignn0flhalflem1  46708  dignn0flhalflem2  46709
  Copyright terms: Public domain W3C validator