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

Theorem zred 11748
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 11650 . 2 ℤ ⊆ ℝ
2 zred.1 . 2 (𝜑𝐴 ∈ ℤ)
31, 2sseldi 3796 1 (𝜑𝐴 ∈ ℝ)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wcel 2156  cr 10220  cz 11643
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1877  ax-4 1894  ax-5 2001  ax-6 2068  ax-7 2104  ax-9 2165  ax-10 2185  ax-11 2201  ax-12 2214  ax-13 2420  ax-ext 2784
This theorem depends on definitions:  df-bi 198  df-an 385  df-or 866  df-3or 1101  df-3an 1102  df-tru 1641  df-ex 1860  df-nf 1864  df-sb 2061  df-clab 2793  df-cleq 2799  df-clel 2802  df-nfc 2937  df-rex 3102  df-rab 3105  df-v 3393  df-dif 3772  df-un 3774  df-in 3776  df-ss 3783  df-nul 4117  df-if 4280  df-sn 4371  df-pr 4373  df-op 4377  df-uni 4631  df-br 4845  df-iota 6064  df-fv 6109  df-ov 6877  df-neg 10554  df-z 11644
This theorem is referenced by:  zcnd  11749  suprfinzcl  11758  eluzmn  11911  eluzelre  11915  subeluzsub  11935  uzm1  11936  zsupss  11996  suprzcl2  11997  uzwo3  12002  rpnnen1lem3  12035  rpnnen1lem5  12037  zltaddlt1le  12547  fzsplit2  12589  fzdisj  12591  ssfzunsnext  12609  fzpreddisj  12613  fznatpl1  12618  fzp1disj  12622  uzdisj  12636  fzm1  12643  fz0fzdiffz0  12672  elfzmlbm  12673  elfzmlbp  12674  difelfznle  12677  nn0disj  12679  elfzolt3  12704  fzonel  12707  fzospliti  12724  fzodisj  12726  fzouzdisj  12728  fzodisjsn  12730  fzonmapblen  12738  fzoaddel  12745  elincfzoext  12750  reflcl  12821  flge  12830  flwordi  12837  fladdz  12850  2tnp1ge0ge0  12854  flhalf  12855  fldiv4p1lem1div2  12860  fldiv4lem1div2uz2  12861  fldiv4lem1div2  12862  flleceil  12876  fleqceilz  12877  quoremz  12878  uzsup  12886  modmul12d  12948  modaddmodup  12957  modaddmodlo  12958  modfzo0difsn  12966  modsumfzodifsn  12967  addmodlteq  12969  om2uzlti  12973  om2uzf1oi  12976  seqf1olem1  13063  seqf1olem2  13064  bcval4  13314  bcp1nk  13324  bcval5  13325  fzsdom2  13432  seqcoll  13465  seqcoll2  13466  ccatrn  13586  ccatalpha  13590  cshwidxmodr  13774  fzomaxdiflem  14305  fzomaxdif  14306  rexuzre  14315  limsupgre  14435  rlimclim1  14499  isercoll  14621  iseralt  14638  fsumm1  14703  fsum1p  14705  fsum0diaglem  14730  modfsummods  14747  isumsplit  14794  climcndslem1  14803  mertenslem1  14837  ntrivcvgmul  14855  fprodntriv  14893  fprod1p  14919  fprodeq0  14926  fallfacval4  14994  bpoly4  15010  fzo0dvdseq  15268  dvdsmod  15273  oexpneg  15289  mod2eq1n2dvds  15291  ltoddhalfle  15305  flodddiv4t2lthalf  15359  bitsp1  15372  bitsfzolem  15375  bitsfzo  15376  bitsmod  15377  bitscmp  15379  bitsinv1lem  15382  sadaddlem  15407  bitsres  15414  bitsuz  15415  smumul  15434  gcd0id  15459  gcdneg  15462  dfgcd2  15482  nn0seqcvgd  15502  lcmgcdlem  15538  nprm  15619  prmdvdsfz  15634  isprm5  15636  isprm7  15637  coprm  15640  prmexpb  15647  prmfac1  15648  hashdvds  15697  crth  15700  eulerthlem2  15704  fermltl  15706  prmdiv  15707  prmdiveq  15708  hashgcdlem  15710  odzdvds  15717  vfermltlALT  15724  modprm0  15727  modprmn0modprm0  15729  prm23ge5  15737  pythagtriplem13  15749  pcxcl  15782  pcaddlem  15809  pcadd  15810  pcfac  15820  qexpz  15822  prmunb  15835  1arithlem4  15847  4sqlem5  15863  4sqlem6  15864  4sqlem7  15865  4sqlem10  15868  4sqlem11  15876  4sqlem12  15877  4sqlem15  15880  4sqlem16  15881  4sqlem17  15882  vdwnnlem3  15918  prmgaplem7  15978  cshwshashlem3  16016  subgmulg  17810  mndodconglem  18161  odnncl  18165  odmod  18166  oddvds  18167  dfod2  18182  sylow1lem3  18216  efgsp1  18351  efgredleme  18357  telgsumfzs  18588  zringlpirlem1  20040  zringlpirlem3  20042  znf1o  20107  zcld  22829  ovoliunlem1  23483  ovoliunlem2  23484  dyadss  23575  dyaddisjlem  23576  dyadmaxlem  23578  dvfsumle  23998  dvfsumge  23999  dvfsumabs  24000  dvfsumlem1  24003  dvfsumlem3  24005  degltlem1  24046  plyco0  24162  plyeq0lem  24180  plydivex  24266  aannenlem1  24297  efif1olem2  24504  nnlogbexp  24733  logblt  24736  ang180lem1  24753  ang180lem3  24755  wilthlem2  25009  basellem3  25023  basellem4  25024  ppiprm  25091  chtdif  25098  ppidif  25103  chtub  25151  mersenne  25166  bcmono  25216  bcmax  25217  bposlem1  25223  bposlem3  25225  bposlem5  25227  bposlem6  25228  lgsval2lem  25246  lgsvalmod  25255  lgsneg  25260  lgsmod  25262  lgsdilem  25263  lgsdirprm  25270  lgsdilem2  25272  lgsne0  25274  lgssq  25276  lgssq2  25277  lgsqr  25290  lgsdchr  25294  gausslemma2dlem1a  25304  gausslemma2dlem3  25307  gausslemma2dlem5a  25309  gausslemma2dlem6  25311  gausslemma2d  25313  lgseisenlem1  25314  lgseisenlem2  25315  lgseisenlem3  25316  lgseisenlem4  25317  lgsquadlem1  25319  lgsquadlem2  25320  lgsquadlem3  25321  lgsquad3  25326  2lgslem1a2  25329  2lgslem1  25333  2lgslem2  25334  2sqlem3  25359  2sqlem8  25365  2sqblem  25370  chebbnd1lem1  25372  chebbnd1lem2  25373  chebbnd1lem3  25374  dchrmusum2  25397  dchrvmasumlem1  25398  dchrvmasum2lem  25399  dchrvmasum2if  25400  dchrvmasumlem3  25402  dchrvmasumiflem2  25405  dchrisum0lem1  25419  dchrmusumlem  25425  mudivsum  25433  mulogsumlem  25434  mulogsum  25435  mulog2sumlem2  25438  mulog2sumlem3  25439  selberglem1  25448  selberglem2  25449  pntpbnd1  25489  pntlemg  25501  pntlemf  25508  qabvle  25528  padicabv  25533  padicabvcxp  25535  ostth2lem2  25537  axlowdimlem13  26048  axlowdimlem16  26051  pthdlem1  26890  crctcshwlkn0  26942  crctcsh  26945  clwwisshclwwslemlem  27156  eucrctshift  27416  nndiffz1  29875  fzsplit3  29880  bcm1n  29881  ltesubnnd  29895  2sqmod  29973  pnfinf  30062  dya2iocress  30661  dya2iocbrsiga  30662  dya2icobrsiga  30663  dya2icoseg  30664  dya2iocucvr  30671  sxbrsigalem2  30673  ballotlemfc0  30879  ballotlemfcc  30880  ballotlemodife  30884  ballotlemimin  30892  ballotlemsgt1  30897  ballotlemsel1i  30899  ballotlemsi  30901  ballotlemsima  30902  ballotlemrv2  30908  ballotlemfrceq  30915  ballotlemfrcn0  30916  ballotlemirc  30918  fsum2dsub  31010  reprlt  31022  reprgt  31024  breprexplemc  31035  tgoldbachgnn  31062  tgoldbachgt  31066  subfacval3  31494  erdszelem8  31503  erdszelem9  31504  supfz  31935  inffz  31936  inffzOLD  31937  dnizeq0  32782  dnizphlfeqhlf  32783  dnibndlem13  32797  knoppndvlem1  32820  knoppndvlem2  32821  knoppndvlem7  32826  knoppndvlem19  32838  knoppndvlem21  32840  ltflcei  33710  leceifl  33711  poimirlem1  33723  poimirlem2  33724  poimirlem6  33728  poimirlem7  33729  poimirlem8  33730  poimirlem15  33737  poimirlem16  33738  poimirlem17  33739  poimirlem19  33741  poimirlem20  33742  poimirlem23  33745  poimirlem24  33746  poimirlem27  33749  poimirlem29  33751  poimirlem31  33753  poimirlem32  33754  mblfinlem2  33760  itg2addnclem2  33774  mettrifi  33864  cntotbnd  33906  lzunuz  37833  lzenom  37835  diophin  37838  irrapxlem1  37888  irrapxlem2  37889  irrapxlem3  37890  irrapxlem4  37891  pellexlem5  37899  pellexlem6  37900  rmspecfund  37975  rmxypos  38015  ltrmynn0  38016  ltrmxnn0  38017  ltrmy  38020  rmyeq0  38021  rmyeq  38022  lermy  38023  rmyabs  38026  jm2.24nn  38027  jm2.17a  38028  jm2.17b  38029  jm2.17c  38030  jm2.24  38031  rmygeid  38032  acongrep  38048  fzmaxdif  38049  acongeq  38051  jm2.22  38063  jm2.23  38064  jm2.26lem3  38069  jm2.27a  38073  jm3.1lem1  38085  jm3.1lem3  38087  expdiophlem1  38089  prmunb2  39010  nzprmdif  39018  hashnzfzclim  39021  binomcxplemnn0  39048  uzwo4  39714  ssinc  39757  ssdec  39758  zltlesub  39979  monoords  39992  fzisoeu  39995  fperiodmul  39999  fzdifsuc2  40005  iuneqfzuzlem  40030  uzublem  40136  zxrd  40161  uzinico  40267  uzubioo  40274  fmul01  40292  fmul01lt1lem1  40296  fmul01lt1lem2  40297  climsuselem1  40319  climsuse  40320  sumnnodd  40342  ltmod  40350  limsupresuz  40415  limsupubuzlem  40424  limsupequzlem  40434  limsupmnfuzlem  40438  limsupequzmptlem  40440  limsupre3uzlem  40447  supcnvlimsup  40452  limsup10exlem  40484  liminfresuz  40496  liminfvaluz  40504  limsupvaluz3  40510  ioodvbdlimc1lem2  40627  ioodvbdlimc2lem  40629  dvnmul  40638  dvnprodlem1  40641  dvnprodlem2  40642  iblspltprt  40668  itgspltprt  40674  stoweidlem3  40699  stoweidlem11  40707  stoweidlem20  40716  stoweidlem26  40722  stoweidlem34  40730  stoweidlem59  40755  stirlinglem5  40774  dirkertrigeqlem3  40796  dirkeritg  40798  dirkercncflem1  40799  dirkercncflem2  40800  dirkercncflem4  40802  fourierdlem4  40807  fourierdlem6  40809  fourierdlem7  40810  fourierdlem11  40814  fourierdlem12  40815  fourierdlem15  40818  fourierdlem19  40822  fourierdlem20  40823  fourierdlem25  40828  fourierdlem26  40829  fourierdlem34  40837  fourierdlem35  40838  fourierdlem41  40844  fourierdlem48  40850  fourierdlem49  40851  fourierdlem50  40852  fourierdlem51  40853  fourierdlem54  40856  fourierdlem63  40865  fourierdlem64  40866  fourierdlem65  40867  fourierdlem71  40873  fourierdlem79  40881  fourierdlem89  40891  fourierdlem90  40892  fourierdlem91  40893  fourierdlem102  40904  fourierdlem103  40905  fourierdlem104  40906  fourierdlem114  40916  fouriersw  40927  elaa2lem  40929  etransclem3  40933  etransclem4  40934  etransclem7  40937  etransclem10  40940  etransclem15  40945  etransclem19  40949  etransclem23  40953  etransclem24  40954  etransclem25  40955  etransclem27  40957  etransclem31  40961  etransclem32  40962  etransclem35  40965  etransclem41  40971  etransclem44  40974  etransclem46  40976  etransclem48  40978  iundjiun  41156  caratheodorylem1  41222  smflimsuplem4  41511  smfliminflem  41518  2elfz2melfz  41903  elfzelfzlble  41906  fzopredsuc  41908  fsummsndifre  41917  iccpartgt  41938  icceuelpartlem  41946  icceuelpart  41947  iccpartnel  41949  lighneallem2  42098  proththd  42106  dfodd4  42146  oexpnegALTV  42163  nnoALTV  42181  evenltle  42201  gbowgt5  42225  gboge9  42227  stgoldbwt  42239  sbgoldbst  42241  sbgoldbalt  42244  sgoldbeven3prm  42246  mogoldbb  42248  bgoldbtbndlem1  42268  bgoldbtbndlem2  42269  bgoldbtbndlem3  42270  bgoldbtbnd  42272  bgoldbachlt  42276  tgblthelfgott  42278  tgoldbach  42280  pw2m1lepw2m1  42878  m1modmmod  42884  difmodm1lt  42885  fllogbd  42922  logbpw2m1  42929  fllog2  42930  nnpw2blen  42942  nnolog2flm1  42952  dignn0flhalflem1  42977  dignn0flhalflem2  42978
  Copyright terms: Public domain W3C validator