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

Theorem zred 12076
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 11977 . 2 ℤ ⊆ ℝ
2 zred.1 . 2 (𝜑𝐴 ∈ ℤ)
31, 2sseldi 3964 1 (𝜑𝐴 ∈ ℝ)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wcel 2105  cr 10525  cz 11970
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1787  ax-4 1801  ax-5 1902  ax-6 1961  ax-7 2006  ax-8 2107  ax-9 2115  ax-10 2136  ax-11 2151  ax-12 2167  ax-ext 2793
This theorem depends on definitions:  df-bi 208  df-an 397  df-or 842  df-3or 1080  df-3an 1081  df-tru 1531  df-ex 1772  df-nf 1776  df-sb 2061  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-rex 3144  df-rab 3147  df-v 3497  df-dif 3938  df-un 3940  df-in 3942  df-ss 3951  df-nul 4291  df-if 4466  df-sn 4560  df-pr 4562  df-op 4566  df-uni 4833  df-br 5059  df-iota 6308  df-fv 6357  df-ov 7148  df-neg 10862  df-z 11971
This theorem is referenced by:  zcnd  12077  suprfinzcl  12086  eluzmn  12239  eluzelre  12243  subeluzsub  12264  uzm1  12265  zsupss  12326  suprzcl2  12327  uzwo3  12332  rpnnen1lem3  12368  rpnnen1lem5  12370  zltaddlt1le  12880  fzsplit2  12922  fzdisj  12924  ssfzunsnext  12942  fzpreddisj  12946  fznatpl1  12951  fzp1disj  12956  uzdisj  12970  fzm1  12977  fz0fzdiffz0  13006  elfzmlbm  13007  elfzmlbp  13008  difelfznle  13011  nn0disj  13013  elfzolt3  13038  fzonel  13041  fzospliti  13059  fzodisj  13061  fzouzdisj  13063  fzodisjsn  13065  fzonmapblen  13073  fzoaddel  13080  elincfzoext  13085  reflcl  13156  flge  13165  flwordi  13172  fladdz  13185  2tnp1ge0ge0  13189  flhalf  13190  fldiv4p1lem1div2  13195  fldiv4lem1div2uz2  13196  fldiv4lem1div2  13197  flleceil  13211  fleqceilz  13212  quoremz  13213  uzsup  13221  modmul12d  13283  modaddmodup  13292  modaddmodlo  13293  modfzo0difsn  13301  modsumfzodifsn  13302  addmodlteq  13304  om2uzlti  13308  om2uzf1oi  13311  seqf1olem1  13399  seqf1olem2  13400  bcval4  13657  bcp1nk  13667  bcval5  13668  fzsdom2  13779  seqcoll  13812  seqcoll2  13813  ccatrn  13933  ccatalpha  13937  cshwidxmodr  14156  fzomaxdiflem  14692  fzomaxdif  14693  rexuzre  14702  limsupgre  14828  rlimclim1  14892  isercoll  15014  iseralt  15031  fsumm1  15096  fsum1p  15098  fsum0diaglem  15121  modfsummods  15138  isumsplit  15185  climcndslem1  15194  mertenslem1  15230  ntrivcvgmul  15248  fprodntriv  15286  fprod1p  15312  fprodeq0  15319  fallfacval4  15387  bpoly4  15403  fzo0dvdseq  15663  dvdsmod  15668  oexpneg  15684  mod2eq1n2dvds  15686  ltoddhalfle  15700  flodddiv4t2lthalf  15757  bitsp1  15770  bitsfzolem  15773  bitsfzo  15774  bitsmod  15775  bitscmp  15777  bitsinv1lem  15780  sadaddlem  15805  bitsres  15812  bitsuz  15813  smumul  15832  gcd0id  15857  gcdneg  15860  dfgcd2  15884  nn0seqcvgd  15904  lcmgcdlem  15940  nprm  16022  prmdvdsfz  16039  isprm5  16041  isprm7  16042  coprm  16045  prmexpb  16052  prmfac1  16053  hashdvds  16102  crth  16105  eulerthlem2  16109  fermltl  16111  prmdiv  16112  prmdiveq  16113  hashgcdlem  16115  odzdvds  16122  vfermltlALT  16129  modprm0  16132  modprmn0modprm0  16134  prm23ge5  16142  pythagtriplem13  16154  pcxcl  16187  pcaddlem  16214  pcadd  16215  pcfac  16225  qexpz  16227  prmunb  16240  1arithlem4  16252  4sqlem5  16268  4sqlem6  16269  4sqlem7  16270  4sqlem10  16273  4sqlem11  16281  4sqlem12  16282  4sqlem15  16285  4sqlem16  16286  4sqlem17  16287  vdwnnlem3  16323  prmgaplem7  16383  cshwshashlem3  16421  subgmulg  18233  mndodconglem  18600  odnncl  18604  odmod  18605  oddvds  18606  dfod2  18622  sylow1lem3  18656  efgsp1  18794  efgredleme  18800  telgsumfzs  19040  zringlpirlem1  20561  zringlpirlem3  20563  znf1o  20628  zcld  23350  ovoliunlem1  24032  ovoliunlem2  24033  dyadss  24124  dyaddisjlem  24125  dyadmaxlem  24127  dvfsumle  24547  dvfsumge  24548  dvfsumabs  24549  dvfsumlem1  24552  dvfsumlem3  24554  degltlem1  24595  plyco0  24711  plyeq0lem  24729  plydivex  24815  aannenlem1  24846  efif1olem2  25054  nnlogbexp  25286  logblt  25289  ang180lem1  25314  ang180lem3  25316  wilthlem2  25574  basellem3  25588  basellem4  25589  ppiprm  25656  chtdif  25663  ppidif  25668  chtub  25716  mersenne  25731  bcmono  25781  bcmax  25782  bposlem1  25788  bposlem3  25790  bposlem5  25792  bposlem6  25793  lgsval2lem  25811  lgsvalmod  25820  lgsneg  25825  lgsmod  25827  lgsdilem  25828  lgsdirprm  25835  lgsdilem2  25837  lgsne0  25839  lgssq  25841  lgssq2  25842  lgsqr  25855  lgsdchr  25859  gausslemma2dlem1a  25869  gausslemma2dlem3  25872  gausslemma2dlem5a  25874  gausslemma2dlem6  25876  gausslemma2d  25878  lgseisenlem1  25879  lgseisenlem2  25880  lgseisenlem3  25881  lgseisenlem4  25882  lgsquadlem1  25884  lgsquadlem2  25885  lgsquadlem3  25886  lgsquad3  25891  2lgslem1a2  25894  2lgslem1  25898  2lgslem2  25899  2sqlem3  25924  2sqlem8  25930  2sqblem  25935  2sqmod  25940  chebbnd1lem1  25973  chebbnd1lem2  25974  chebbnd1lem3  25975  dchrmusum2  25998  dchrvmasumlem1  25999  dchrvmasum2lem  26000  dchrvmasum2if  26001  dchrvmasumlem3  26003  dchrvmasumiflem2  26006  dchrisum0lem1  26020  dchrmusumlem  26026  mudivsum  26034  mulogsumlem  26035  mulogsum  26036  mulog2sumlem2  26039  mulog2sumlem3  26040  selberglem1  26049  selberglem2  26050  pntpbnd1  26090  pntlemg  26102  pntlemf  26109  qabvle  26129  padicabv  26134  padicabvcxp  26136  ostth2lem2  26138  axlowdimlem13  26668  axlowdimlem16  26671  pthdlem1  27475  crctcshwlkn0  27527  crctcsh  27530  clwwisshclwwslemlem  27719  eucrctshift  27950  nndiffz1  30436  fzsplit3  30444  bcm1n  30445  fzone1  30450  ltesubnnd  30466  wrdt2ind  30555  cshwrnid  30563  cycpmfv2  30684  cycpmco2lem6  30701  cycpmco2lem7  30702  cycpmrn  30713  cyc3conja  30727  pnfinf  30740  dya2iocress  31432  dya2iocbrsiga  31433  dya2icobrsiga  31434  dya2icoseg  31435  dya2iocucvr  31442  sxbrsigalem2  31444  ballotlemfc0  31650  ballotlemfcc  31651  ballotlemodife  31655  ballotlemimin  31663  ballotlemsgt1  31668  ballotlemsel1i  31670  ballotlemsi  31672  ballotlemsima  31673  ballotlemrv2  31679  ballotlemfrceq  31686  ballotlemfrcn0  31687  ballotlemirc  31689  fsum2dsub  31778  reprlt  31790  reprgt  31792  breprexplemc  31803  tgoldbachgnn  31830  tgoldbachgt  31834  subfacval3  32334  erdszelem8  32343  erdszelem9  32344  supfz  32858  inffz  32859  dnizeq0  33712  dnizphlfeqhlf  33713  dnibndlem13  33727  knoppndvlem1  33749  knoppndvlem2  33750  knoppndvlem7  33755  knoppndvlem19  33767  knoppndvlem21  33769  ltflcei  34762  leceifl  34763  poimirlem1  34775  poimirlem2  34776  poimirlem6  34780  poimirlem7  34781  poimirlem8  34782  poimirlem15  34789  poimirlem16  34790  poimirlem17  34791  poimirlem19  34793  poimirlem20  34794  poimirlem23  34797  poimirlem24  34798  poimirlem27  34801  poimirlem29  34803  poimirlem31  34805  poimirlem32  34806  mblfinlem2  34812  itg2addnclem2  34826  mettrifi  34915  cntotbnd  34957  frlmvscadiccat  39025  exp11d  39069  dffltz  39151  lzunuz  39245  lzenom  39247  diophin  39249  irrapxlem1  39299  irrapxlem2  39300  irrapxlem3  39301  irrapxlem4  39302  pellexlem5  39310  pellexlem6  39311  rmspecfund  39386  rmxypos  39424  ltrmynn0  39425  ltrmxnn0  39426  ltrmy  39429  rmyeq0  39430  rmyeq  39431  lermy  39432  rmyabs  39435  jm2.24nn  39436  jm2.17a  39437  jm2.17b  39438  jm2.17c  39439  jm2.24  39440  rmygeid  39441  acongrep  39457  fzmaxdif  39458  acongeq  39460  jm2.22  39472  jm2.23  39473  jm2.26lem3  39478  jm2.27a  39482  jm3.1lem1  39494  jm3.1lem3  39496  expdiophlem1  39498  prmunb2  40523  nzprmdif  40531  hashnzfzclim  40534  binomcxplemnn0  40561  uzwo4  41195  ssinc  41233  ssdec  41234  zltlesub  41431  monoords  41444  fzisoeu  41447  fperiodmul  41451  fzdifsuc2  41457  iuneqfzuzlem  41482  uzublem  41584  zxrd  41609  uzinico  41716  uzubioo  41723  fmul01  41741  fmul01lt1lem1  41745  fmul01lt1lem2  41746  climsuselem1  41768  climsuse  41769  sumnnodd  41791  ltmod  41799  limsupresuz  41864  limsupubuzlem  41873  limsupequzlem  41883  limsupmnfuzlem  41887  limsupequzmptlem  41889  limsupre3uzlem  41896  supcnvlimsup  41901  limsup10exlem  41933  liminfresuz  41945  liminfvaluz  41953  limsupvaluz3  41959  ioodvbdlimc1lem2  42097  ioodvbdlimc2lem  42099  dvnmul  42108  dvnprodlem1  42111  dvnprodlem2  42112  iblspltprt  42138  itgspltprt  42144  stoweidlem3  42169  stoweidlem11  42177  stoweidlem20  42186  stoweidlem26  42192  stoweidlem34  42200  stoweidlem59  42225  stirlinglem5  42244  dirkertrigeqlem3  42266  dirkeritg  42268  dirkercncflem1  42269  dirkercncflem2  42270  dirkercncflem4  42272  fourierdlem4  42277  fourierdlem6  42279  fourierdlem7  42280  fourierdlem11  42284  fourierdlem12  42285  fourierdlem15  42288  fourierdlem19  42292  fourierdlem20  42293  fourierdlem25  42298  fourierdlem26  42299  fourierdlem34  42307  fourierdlem35  42308  fourierdlem41  42314  fourierdlem48  42320  fourierdlem49  42321  fourierdlem50  42322  fourierdlem51  42323  fourierdlem54  42326  fourierdlem63  42335  fourierdlem64  42336  fourierdlem65  42337  fourierdlem71  42343  fourierdlem79  42351  fourierdlem89  42361  fourierdlem90  42362  fourierdlem91  42363  fourierdlem102  42374  fourierdlem103  42375  fourierdlem104  42376  fourierdlem114  42386  fouriersw  42397  elaa2lem  42399  etransclem3  42403  etransclem4  42404  etransclem7  42407  etransclem10  42410  etransclem15  42415  etransclem19  42419  etransclem23  42423  etransclem24  42424  etransclem25  42425  etransclem27  42427  etransclem31  42431  etransclem32  42432  etransclem35  42435  etransclem41  42441  etransclem44  42444  etransclem46  42446  etransclem48  42448  iundjiun  42623  caratheodorylem1  42689  smflimsuplem4  42978  smfliminflem  42985  2elfz2melfz  43399  elfzelfzlble  43402  fzopredsuc  43404  fsummsndifre  43413  iccpartgt  43434  icceuelpartlem  43442  icceuelpart  43443  iccpartnel  43445  lighneallem2  43618  proththd  43626  dfodd4  43671  oexpnegALTV  43689  nnoALTV  43707  evenltle  43729  fpprwppr  43751  gbowgt5  43774  gboge9  43776  stgoldbwt  43788  sbgoldbst  43790  sbgoldbalt  43793  sgoldbeven3prm  43795  mogoldbb  43797  bgoldbtbndlem1  43817  bgoldbtbndlem2  43818  bgoldbtbndlem3  43819  bgoldbtbnd  43821  bgoldbachlt  43825  tgblthelfgott  43827  tgoldbach  43829  pw2m1lepw2m1  44473  m1modmmod  44479  difmodm1lt  44480  fllogbd  44518  logbpw2m1  44525  fllog2  44526  nnpw2blen  44538  nnolog2flm1  44548  dignn0flhalflem1  44573  dignn0flhalflem2  44574
  Copyright terms: Public domain W3C validator