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

Theorem zred 11520
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 11422 . 2 ℤ ⊆ ℝ
2 zred.1 . 2 (𝜑𝐴 ∈ ℤ)
31, 2sseldi 3634 1 (𝜑𝐴 ∈ ℝ)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wcel 2030  cr 9973  cz 11415
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-9 2039  ax-10 2059  ax-11 2074  ax-12 2087  ax-13 2282  ax-ext 2631
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3or 1055  df-3an 1056  df-tru 1526  df-ex 1745  df-nf 1750  df-sb 1938  df-clab 2638  df-cleq 2644  df-clel 2647  df-nfc 2782  df-rex 2947  df-rab 2950  df-v 3233  df-dif 3610  df-un 3612  df-in 3614  df-ss 3621  df-nul 3949  df-if 4120  df-sn 4211  df-pr 4213  df-op 4217  df-uni 4469  df-br 4686  df-iota 5889  df-fv 5934  df-ov 6693  df-neg 10307  df-z 11416
This theorem is referenced by:  zcnd  11521  suprfinzcl  11530  eluzmn  11732  eluzelre  11736  uzm1  11756  zsupss  11815  suprzcl2  11816  uzwo3  11821  rpnnen1lem3  11854  rpnnen1lem5  11856  rpnnen1lem3OLD  11860  rpnnen1lem5OLD  11862  zltaddlt1le  12362  fzsplit2  12404  fzdisj  12406  ssfzunsnext  12424  fzpreddisj  12428  fznatpl1  12433  fzp1disj  12437  uzdisj  12451  fzm1  12458  fz0fzdiffz0  12487  elfzmlbm  12488  elfzmlbp  12489  difelfznle  12492  nn0disj  12494  elfzolt3  12519  fzonel  12522  fzospliti  12539  fzodisj  12541  fzouzdisj  12543  fzodisjsn  12545  fzonmapblen  12553  fzoaddel  12560  elincfzoext  12565  reflcl  12637  flge  12646  flwordi  12653  fladdz  12666  2tnp1ge0ge0  12670  flhalf  12671  fldiv4p1lem1div2  12676  fldiv4lem1div2uz2  12677  fldiv4lem1div2  12678  flleceil  12692  fleqceilz  12693  quoremz  12694  uzsup  12702  modmul12d  12764  modaddmodup  12773  modaddmodlo  12774  modfzo0difsn  12782  modsumfzodifsn  12783  addmodlteq  12785  om2uzlti  12789  om2uzf1oi  12792  seqf1olem1  12880  seqf1olem2  12881  bcval4  13134  bcp1nk  13144  bcval5  13145  fzsdom2  13253  seqcoll  13286  seqcoll2  13287  ccatrn  13407  ccatalpha  13411  cshwidxmodr  13596  fzomaxdiflem  14126  fzomaxdif  14127  rexuzre  14136  limsupgre  14256  rlimclim1  14320  isercoll  14442  iseralt  14459  fsumm1  14524  fsum1p  14526  fsum0diaglem  14552  modfsummods  14569  isumsplit  14616  climcndslem1  14625  mertenslem1  14660  ntrivcvgmul  14678  fprodntriv  14716  fprod1p  14742  fprodeq0  14749  fallfacval4  14818  bpoly4  14834  fzo0dvdseq  15092  dvdsmod  15097  oexpneg  15116  mod2eq1n2dvds  15118  ltoddhalfle  15132  flodddiv4t2lthalf  15187  bitsp1  15200  bitsfzolem  15203  bitsfzo  15204  bitsmod  15205  bitscmp  15207  bitsinv1lem  15210  sadaddlem  15235  bitsres  15242  bitsuz  15243  smumul  15262  gcd0id  15287  gcdneg  15290  dfgcd2  15310  nn0seqcvgd  15330  lcmgcdlem  15366  nprm  15448  prmdvdsfz  15464  isprm5  15466  isprm7  15467  coprm  15470  prmexpb  15477  prmfac1  15478  hashdvds  15527  crth  15530  eulerthlem2  15534  fermltl  15536  prmdiv  15537  prmdiveq  15538  hashgcdlem  15540  odzdvds  15547  vfermltlALT  15554  modprm0  15557  modprmn0modprm0  15559  prm23ge5  15567  pythagtriplem13  15579  pcxcl  15612  pcaddlem  15639  pcadd  15640  pcfac  15650  qexpz  15652  prmunb  15665  1arithlem4  15677  4sqlem5  15693  4sqlem6  15694  4sqlem7  15695  4sqlem10  15698  4sqlem11  15706  4sqlem12  15707  4sqlem15  15710  4sqlem16  15711  4sqlem17  15712  vdwnnlem3  15748  prmgaplem7  15808  cshwshashlem3  15851  subgmulg  17655  mndodconglem  18006  odnncl  18010  odmod  18011  oddvds  18012  dfod2  18027  sylow1lem3  18061  efgsp1  18196  efgredleme  18202  telgsumfzs  18432  zringlpirlem1  19880  zringlpirlem3  19882  znf1o  19948  zcld  22663  ovoliunlem1  23316  ovoliunlem2  23317  dyadss  23408  dyaddisjlem  23409  dyadmaxlem  23411  dvfsumle  23829  dvfsumge  23830  dvfsumabs  23831  dvfsumlem1  23834  dvfsumlem3  23836  degltlem1  23877  plyco0  23993  plyeq0lem  24011  plydivex  24097  aannenlem1  24128  efif1olem2  24334  nnlogbexp  24564  logblt  24567  ang180lem1  24584  ang180lem3  24586  wilthlem2  24840  basellem3  24854  basellem4  24855  ppiprm  24922  chtdif  24929  ppidif  24934  chtub  24982  mersenne  24997  bcmono  25047  bcmax  25048  bposlem1  25054  bposlem3  25056  bposlem5  25058  bposlem6  25059  lgsval2lem  25077  lgsvalmod  25086  lgsneg  25091  lgsmod  25093  lgsdilem  25094  lgsdirprm  25101  lgsdilem2  25103  lgsne0  25105  lgssq  25107  lgssq2  25108  lgsqr  25121  lgsdchr  25125  gausslemma2dlem1a  25135  gausslemma2dlem3  25138  gausslemma2dlem5a  25140  gausslemma2dlem6  25142  gausslemma2d  25144  lgseisenlem1  25145  lgseisenlem2  25146  lgseisenlem3  25147  lgseisenlem4  25148  lgsquadlem1  25150  lgsquadlem2  25151  lgsquadlem3  25152  lgsquad3  25157  2lgslem1a2  25160  2lgslem1  25164  2lgslem2  25165  2sqlem3  25190  2sqlem8  25196  2sqblem  25201  chebbnd1lem1  25203  chebbnd1lem2  25204  chebbnd1lem3  25205  dchrmusum2  25228  dchrvmasumlem1  25229  dchrvmasum2lem  25230  dchrvmasum2if  25231  dchrvmasumlem3  25233  dchrvmasumiflem2  25236  dchrisum0lem1  25250  dchrmusumlem  25256  mudivsum  25264  mulogsumlem  25265  mulogsum  25266  mulog2sumlem2  25269  mulog2sumlem3  25270  selberglem1  25279  selberglem2  25280  pntpbnd1  25320  pntlemg  25332  pntlemf  25339  qabvle  25359  padicabv  25364  padicabvcxp  25366  ostth2lem2  25368  axlowdimlem13  25879  axlowdimlem16  25882  pthdlem1  26718  crctcshwlkn0  26769  crctcsh  26772  clwwisshclwwslemlem  26970  eucrctshift  27221  nndiffz1  29676  fzsplit3  29681  bcm1n  29682  ltesubnnd  29696  2sqmod  29776  pnfinf  29865  dya2iocress  30464  dya2iocbrsiga  30465  dya2icobrsiga  30466  dya2icoseg  30467  dya2iocucvr  30474  sxbrsigalem2  30476  ballotlemfc0  30682  ballotlemfcc  30683  ballotlemodife  30687  ballotlemimin  30695  ballotlemsgt1  30700  ballotlemsel1i  30702  ballotlemsi  30704  ballotlemsima  30705  ballotlemrv2  30711  ballotlemfrceq  30718  ballotlemfrcn0  30719  ballotlemirc  30721  fsum2dsub  30813  reprlt  30825  reprgt  30827  breprexplemc  30838  tgoldbachgnn  30865  tgoldbachgt  30869  subfacval3  31297  erdszelem8  31306  erdszelem9  31307  supfz  31739  inffz  31740  inffzOLD  31741  dnizeq0  32590  dnizphlfeqhlf  32591  dnibndlem13  32605  knoppndvlem1  32628  knoppndvlem2  32629  knoppndvlem7  32634  knoppndvlem19  32646  knoppndvlem21  32648  ltflcei  33527  leceifl  33528  poimirlem1  33540  poimirlem2  33541  poimirlem6  33545  poimirlem7  33546  poimirlem8  33547  poimirlem15  33554  poimirlem16  33555  poimirlem17  33556  poimirlem19  33558  poimirlem20  33559  poimirlem23  33562  poimirlem24  33563  poimirlem27  33566  poimirlem29  33568  poimirlem31  33570  poimirlem32  33571  mblfinlem2  33577  itg2addnclem2  33592  mettrifi  33683  cntotbnd  33725  lzunuz  37648  lzenom  37650  diophin  37653  irrapxlem1  37703  irrapxlem2  37704  irrapxlem3  37705  irrapxlem4  37706  pellexlem5  37714  pellexlem6  37715  rmspecfund  37791  rmxypos  37831  ltrmynn0  37832  ltrmxnn0  37833  ltrmy  37836  rmyeq0  37837  rmyeq  37838  lermy  37839  rmyabs  37842  jm2.24nn  37843  jm2.17a  37844  jm2.17b  37845  jm2.17c  37846  jm2.24  37847  rmygeid  37848  acongrep  37864  fzmaxdif  37865  acongeq  37867  jm2.22  37879  jm2.23  37880  jm2.26lem3  37885  jm2.27a  37889  jm3.1lem1  37901  jm3.1lem3  37903  expdiophlem1  37905  prmunb2  38827  nzprmdif  38835  hashnzfzclim  38838  binomcxplemnn0  38865  uzwo4  39535  ssinc  39578  ssdec  39579  zltlesub  39811  monoords  39825  fzisoeu  39828  fperiodmul  39832  fzdifsuc2  39838  iuneqfzuzlem  39863  uzublem  39970  zxrd  39995  uzinico  40105  uzubioo  40112  fmul01  40130  fmul01lt1lem1  40134  fmul01lt1lem2  40135  climsuselem1  40157  climsuse  40158  sumnnodd  40180  ltmod  40188  limsupresuz  40253  limsupubuzlem  40262  limsupequzlem  40272  limsupmnfuzlem  40276  limsupequzmptlem  40278  limsupre3uzlem  40285  supcnvlimsup  40290  limsup10exlem  40322  liminfresuz  40334  liminfvaluz  40342  limsupvaluz3  40348  ioodvbdlimc1lem2  40465  ioodvbdlimc2lem  40467  dvnmul  40476  dvnprodlem1  40479  dvnprodlem2  40480  iblspltprt  40507  itgspltprt  40513  stoweidlem3  40538  stoweidlem11  40546  stoweidlem20  40555  stoweidlem26  40561  stoweidlem34  40569  stoweidlem59  40594  stirlinglem5  40613  dirkertrigeqlem3  40635  dirkeritg  40637  dirkercncflem1  40638  dirkercncflem2  40639  dirkercncflem4  40641  fourierdlem4  40646  fourierdlem6  40648  fourierdlem7  40649  fourierdlem11  40653  fourierdlem12  40654  fourierdlem15  40657  fourierdlem19  40661  fourierdlem20  40662  fourierdlem25  40667  fourierdlem26  40668  fourierdlem34  40676  fourierdlem35  40677  fourierdlem41  40683  fourierdlem48  40689  fourierdlem49  40690  fourierdlem50  40691  fourierdlem51  40692  fourierdlem54  40695  fourierdlem63  40704  fourierdlem64  40705  fourierdlem65  40706  fourierdlem71  40712  fourierdlem79  40720  fourierdlem89  40730  fourierdlem90  40731  fourierdlem91  40732  fourierdlem102  40743  fourierdlem103  40744  fourierdlem104  40745  fourierdlem114  40755  fouriersw  40766  elaa2lem  40768  etransclem3  40772  etransclem4  40773  etransclem7  40776  etransclem10  40779  etransclem15  40784  etransclem19  40788  etransclem23  40792  etransclem24  40793  etransclem25  40794  etransclem27  40796  etransclem31  40800  etransclem32  40801  etransclem35  40804  etransclem41  40810  etransclem44  40813  etransclem46  40815  etransclem48  40817  iundjiun  40995  caratheodorylem1  41061  smflimsuplem4  41350  smfliminflem  41357  2elfz2melfz  41653  elfzelfzlble  41656  fzopredsuc  41658  fsummsndifre  41667  iccpartgt  41688  icceuelpartlem  41696  icceuelpart  41697  iccpartnel  41699  lighneallem2  41848  proththd  41856  dfodd4  41896  oexpnegALTV  41913  nnoALTV  41931  evenltle  41951  gbowgt5  41975  gboge9  41977  stgoldbwt  41989  sbgoldbst  41991  sbgoldbalt  41994  sgoldbeven3prm  41996  mogoldbb  41998  bgoldbtbndlem1  42018  bgoldbtbndlem2  42019  bgoldbtbndlem3  42020  bgoldbtbnd  42022  bgoldbachlt  42026  tgblthelfgott  42028  tgoldbach  42030  bgoldbachltOLD  42032  tgblthelfgottOLD  42034  tgoldbachOLD  42037  pw2m1lepw2m1  42635  m1modmmod  42641  difmodm1lt  42642  fllogbd  42679  logbpw2m1  42686  fllog2  42687  nnpw2blen  42699  nnolog2flm1  42709  dignn0flhalflem1  42734  dignn0flhalflem2  42735
  Copyright terms: Public domain W3C validator