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

Theorem zred 12079
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 11980 . 2 ℤ ⊆ ℝ
2 zred.1 . 2 (𝜑𝐴 ∈ ℤ)
31, 2sseldi 3963 1 (𝜑𝐴 ∈ ℝ)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wcel 2108  cr 10528  cz 11973
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1905  ax-6 1964  ax-7 2009  ax-8 2110  ax-9 2118  ax-10 2139  ax-11 2154  ax-12 2170  ax-ext 2791
This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3or 1083  df-3an 1084  df-tru 1534  df-ex 1775  df-nf 1779  df-sb 2064  df-clab 2798  df-cleq 2812  df-clel 2891  df-nfc 2961  df-rex 3142  df-rab 3145  df-v 3495  df-dif 3937  df-un 3939  df-in 3941  df-ss 3950  df-nul 4290  df-if 4466  df-sn 4560  df-pr 4562  df-op 4566  df-uni 4831  df-br 5058  df-iota 6307  df-fv 6356  df-ov 7151  df-neg 10865  df-z 11974
This theorem is referenced by:  zcnd  12080  suprfinzcl  12089  eluzmn  12242  eluzelre  12246  subeluzsub  12267  uzm1  12268  zsupss  12329  suprzcl2  12330  uzwo3  12335  rpnnen1lem3  12370  rpnnen1lem5  12372  zltaddlt1le  12882  fzsplit2  12924  fzdisj  12926  ssfzunsnext  12944  fzpreddisj  12948  fznatpl1  12953  fzp1disj  12958  uzdisj  12972  fzm1  12979  fz0fzdiffz0  13008  elfzmlbm  13009  elfzmlbp  13010  difelfznle  13013  nn0disj  13015  elfzolt3  13040  fzonel  13043  fzospliti  13061  fzodisj  13063  fzouzdisj  13065  fzodisjsn  13067  fzonmapblen  13075  fzoaddel  13082  elincfzoext  13087  reflcl  13158  flge  13167  flwordi  13174  fladdz  13187  2tnp1ge0ge0  13191  flhalf  13192  fldiv4p1lem1div2  13197  fldiv4lem1div2uz2  13198  fldiv4lem1div2  13199  flleceil  13213  fleqceilz  13214  quoremz  13215  uzsup  13223  modmul12d  13285  modaddmodup  13294  modaddmodlo  13295  modfzo0difsn  13303  modsumfzodifsn  13304  addmodlteq  13306  om2uzlti  13310  om2uzf1oi  13313  seqf1olem1  13401  seqf1olem2  13402  bcval4  13659  bcp1nk  13669  bcval5  13670  fzsdom2  13781  seqcoll  13814  seqcoll2  13815  ccatrn  13935  ccatalpha  13939  cshwidxmodr  14158  fzomaxdiflem  14694  fzomaxdif  14695  rexuzre  14704  limsupgre  14830  rlimclim1  14894  isercoll  15016  iseralt  15033  fsumm1  15098  fsum1p  15100  fsum0diaglem  15123  modfsummods  15140  isumsplit  15187  climcndslem1  15196  mertenslem1  15232  ntrivcvgmul  15250  fprodntriv  15288  fprod1p  15314  fprodeq0  15321  fallfacval4  15389  bpoly4  15405  fzo0dvdseq  15665  dvdsmod  15670  oexpneg  15686  mod2eq1n2dvds  15688  ltoddhalfle  15702  flodddiv4t2lthalf  15759  bitsp1  15772  bitsfzolem  15775  bitsfzo  15776  bitsmod  15777  bitscmp  15779  bitsinv1lem  15782  sadaddlem  15807  bitsres  15814  bitsuz  15815  smumul  15834  gcd0id  15859  gcdneg  15862  dfgcd2  15886  nn0seqcvgd  15906  lcmgcdlem  15942  nprm  16024  prmdvdsfz  16041  isprm5  16043  isprm7  16044  coprm  16047  prmexpb  16054  prmfac1  16055  hashdvds  16104  crth  16107  eulerthlem2  16111  fermltl  16113  prmdiv  16114  prmdiveq  16115  hashgcdlem  16117  odzdvds  16124  vfermltlALT  16131  modprm0  16134  modprmn0modprm0  16136  prm23ge5  16144  pythagtriplem13  16156  pcxcl  16189  pcaddlem  16216  pcadd  16217  pcfac  16227  qexpz  16229  prmunb  16242  1arithlem4  16254  4sqlem5  16270  4sqlem6  16271  4sqlem7  16272  4sqlem10  16275  4sqlem11  16283  4sqlem12  16284  4sqlem15  16287  4sqlem16  16288  4sqlem17  16289  vdwnnlem3  16325  prmgaplem7  16385  cshwshashlem3  16423  subgmulg  18285  mndodconglem  18661  odnncl  18665  odmod  18666  oddvds  18667  dfod2  18683  sylow1lem3  18717  efgsp1  18855  efgredleme  18861  telgsumfzs  19101  zringlpirlem1  20623  zringlpirlem3  20625  znf1o  20690  zcld  23413  ovoliunlem1  24095  ovoliunlem2  24096  dyadss  24187  dyaddisjlem  24188  dyadmaxlem  24190  dvfsumle  24610  dvfsumge  24611  dvfsumabs  24612  dvfsumlem1  24615  dvfsumlem3  24617  degltlem1  24658  plyco0  24774  plyeq0lem  24792  plydivex  24878  aannenlem1  24909  efif1olem2  25119  nnlogbexp  25351  logblt  25354  ang180lem1  25379  ang180lem3  25381  wilthlem2  25638  basellem3  25652  basellem4  25653  ppiprm  25720  chtdif  25727  ppidif  25732  chtub  25780  mersenne  25795  bcmono  25845  bcmax  25846  bposlem1  25852  bposlem3  25854  bposlem5  25856  bposlem6  25857  lgsval2lem  25875  lgsvalmod  25884  lgsneg  25889  lgsmod  25891  lgsdilem  25892  lgsdirprm  25899  lgsdilem2  25901  lgsne0  25903  lgssq  25905  lgssq2  25906  lgsqr  25919  lgsdchr  25923  gausslemma2dlem1a  25933  gausslemma2dlem3  25936  gausslemma2dlem5a  25938  gausslemma2dlem6  25940  gausslemma2d  25942  lgseisenlem1  25943  lgseisenlem2  25944  lgseisenlem3  25945  lgseisenlem4  25946  lgsquadlem1  25948  lgsquadlem2  25949  lgsquadlem3  25950  lgsquad3  25955  2lgslem1a2  25958  2lgslem1  25962  2lgslem2  25963  2sqlem3  25988  2sqlem8  25994  2sqblem  25999  2sqmod  26004  chebbnd1lem1  26037  chebbnd1lem2  26038  chebbnd1lem3  26039  dchrmusum2  26062  dchrvmasumlem1  26063  dchrvmasum2lem  26064  dchrvmasum2if  26065  dchrvmasumlem3  26067  dchrvmasumiflem2  26070  dchrisum0lem1  26084  dchrmusumlem  26090  mudivsum  26098  mulogsumlem  26099  mulogsum  26100  mulog2sumlem2  26103  mulog2sumlem3  26104  selberglem1  26113  selberglem2  26114  pntpbnd1  26154  pntlemg  26166  pntlemf  26173  qabvle  26193  padicabv  26198  padicabvcxp  26200  ostth2lem2  26202  axlowdimlem13  26732  axlowdimlem16  26735  pthdlem1  27539  crctcshwlkn0  27591  crctcsh  27594  clwwisshclwwslemlem  27783  eucrctshift  28014  nndiffz1  30501  fzsplit3  30509  bcm1n  30510  fzone1  30515  ltesubnnd  30531  wrdt2ind  30620  cshwrnid  30628  cycpmfv2  30749  cycpmco2lem6  30766  cycpmco2lem7  30767  cycpmrn  30778  cyc3conja  30792  pnfinf  30805  dya2iocress  31525  dya2iocbrsiga  31526  dya2icobrsiga  31527  dya2icoseg  31528  dya2iocucvr  31535  sxbrsigalem2  31537  ballotlemfc0  31743  ballotlemfcc  31744  ballotlemodife  31748  ballotlemimin  31756  ballotlemsgt1  31761  ballotlemsel1i  31763  ballotlemsi  31765  ballotlemsima  31766  ballotlemrv2  31772  ballotlemfrceq  31779  ballotlemfrcn0  31780  ballotlemirc  31782  fsum2dsub  31871  reprlt  31883  reprgt  31885  breprexplemc  31896  tgoldbachgnn  31923  tgoldbachgt  31927  subfacval3  32429  erdszelem8  32438  erdszelem9  32439  supfz  32953  inffz  32954  dnizeq0  33807  dnizphlfeqhlf  33808  dnibndlem13  33822  knoppndvlem1  33844  knoppndvlem2  33845  knoppndvlem7  33850  knoppndvlem19  33862  knoppndvlem21  33864  ltflcei  34872  leceifl  34873  poimirlem1  34885  poimirlem2  34886  poimirlem6  34890  poimirlem7  34891  poimirlem8  34892  poimirlem15  34899  poimirlem16  34900  poimirlem17  34901  poimirlem19  34903  poimirlem20  34904  poimirlem23  34907  poimirlem24  34908  poimirlem27  34911  poimirlem29  34913  poimirlem31  34915  poimirlem32  34916  mblfinlem2  34922  itg2addnclem2  34936  mettrifi  35024  cntotbnd  35066  frlmvscadiccat  39135  exp11d  39179  dffltz  39261  lzunuz  39355  lzenom  39357  diophin  39359  irrapxlem1  39409  irrapxlem2  39410  irrapxlem3  39411  irrapxlem4  39412  pellexlem5  39420  pellexlem6  39421  rmspecfund  39496  rmxypos  39534  ltrmynn0  39535  ltrmxnn0  39536  ltrmy  39539  rmyeq0  39540  rmyeq  39541  lermy  39542  rmyabs  39545  jm2.24nn  39546  jm2.17a  39547  jm2.17b  39548  jm2.17c  39549  jm2.24  39550  rmygeid  39551  acongrep  39567  fzmaxdif  39568  acongeq  39570  jm2.22  39582  jm2.23  39583  jm2.26lem3  39588  jm2.27a  39592  jm3.1lem1  39604  jm3.1lem3  39606  expdiophlem1  39608  prmunb2  40633  nzprmdif  40641  hashnzfzclim  40644  binomcxplemnn0  40671  uzwo4  41305  ssinc  41343  ssdec  41344  zltlesub  41540  monoords  41553  fzisoeu  41556  fperiodmul  41560  fzdifsuc2  41566  iuneqfzuzlem  41591  uzublem  41693  zxrd  41718  uzinico  41825  uzubioo  41832  fmul01  41850  fmul01lt1lem1  41854  fmul01lt1lem2  41855  climsuselem1  41877  climsuse  41878  sumnnodd  41900  ltmod  41908  limsupresuz  41973  limsupubuzlem  41982  limsupequzlem  41992  limsupmnfuzlem  41996  limsupequzmptlem  41998  limsupre3uzlem  42005  supcnvlimsup  42010  limsup10exlem  42042  liminfresuz  42054  liminfvaluz  42062  limsupvaluz3  42068  ioodvbdlimc1lem2  42206  ioodvbdlimc2lem  42208  dvnmul  42217  dvnprodlem1  42220  dvnprodlem2  42221  iblspltprt  42247  itgspltprt  42253  stoweidlem3  42278  stoweidlem11  42286  stoweidlem20  42295  stoweidlem26  42301  stoweidlem34  42309  stoweidlem59  42334  stirlinglem5  42353  dirkertrigeqlem3  42375  dirkeritg  42377  dirkercncflem1  42378  dirkercncflem2  42379  dirkercncflem4  42381  fourierdlem4  42386  fourierdlem6  42388  fourierdlem7  42389  fourierdlem11  42393  fourierdlem12  42394  fourierdlem15  42397  fourierdlem19  42401  fourierdlem20  42402  fourierdlem25  42407  fourierdlem26  42408  fourierdlem34  42416  fourierdlem35  42417  fourierdlem41  42423  fourierdlem48  42429  fourierdlem49  42430  fourierdlem50  42431  fourierdlem51  42432  fourierdlem54  42435  fourierdlem63  42444  fourierdlem64  42445  fourierdlem65  42446  fourierdlem71  42452  fourierdlem79  42460  fourierdlem89  42470  fourierdlem90  42471  fourierdlem91  42472  fourierdlem102  42483  fourierdlem103  42484  fourierdlem104  42485  fourierdlem114  42495  fouriersw  42506  elaa2lem  42508  etransclem3  42512  etransclem4  42513  etransclem7  42516  etransclem10  42519  etransclem15  42524  etransclem19  42528  etransclem23  42532  etransclem24  42533  etransclem25  42534  etransclem27  42536  etransclem31  42540  etransclem32  42541  etransclem35  42544  etransclem41  42550  etransclem44  42553  etransclem46  42555  etransclem48  42557  iundjiun  42732  caratheodorylem1  42798  smflimsuplem4  43087  smfliminflem  43094  2elfz2melfz  43508  elfzelfzlble  43511  fzopredsuc  43513  fsummsndifre  43522  iccpartgt  43577  icceuelpartlem  43585  icceuelpart  43586  iccpartnel  43588  lighneallem2  43761  proththd  43769  dfodd4  43814  oexpnegALTV  43832  nnoALTV  43850  evenltle  43872  fpprwppr  43894  gbowgt5  43917  gboge9  43919  stgoldbwt  43931  sbgoldbst  43933  sbgoldbalt  43936  sgoldbeven3prm  43938  mogoldbb  43940  bgoldbtbndlem1  43960  bgoldbtbndlem2  43961  bgoldbtbndlem3  43962  bgoldbtbnd  43964  bgoldbachlt  43968  tgblthelfgott  43970  tgoldbach  43972  pw2m1lepw2m1  44565  m1modmmod  44571  difmodm1lt  44572  fllogbd  44610  logbpw2m1  44617  fllog2  44618  nnpw2blen  44630  nnolog2flm1  44640  dignn0flhalflem1  44665  dignn0flhalflem2  44666
  Copyright terms: Public domain W3C validator