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

Theorem zred 11314
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 11217 . 2 ℤ ⊆ ℝ
2 zred.1 . 2 (𝜑𝐴 ∈ ℤ)
31, 2sseldi 3565 1 (𝜑𝐴 ∈ ℝ)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wcel 1976  cr 9791  cz 11210
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1712  ax-4 1727  ax-5 1826  ax-6 1874  ax-7 1921  ax-10 2005  ax-11 2020  ax-12 2033  ax-13 2233  ax-ext 2589
This theorem depends on definitions:  df-bi 195  df-or 383  df-an 384  df-3or 1031  df-3an 1032  df-tru 1477  df-ex 1695  df-nf 1700  df-sb 1867  df-clab 2596  df-cleq 2602  df-clel 2605  df-nfc 2739  df-rex 2901  df-rab 2904  df-v 3174  df-dif 3542  df-un 3544  df-in 3546  df-ss 3553  df-nul 3874  df-if 4036  df-sn 4125  df-pr 4127  df-op 4131  df-uni 4367  df-br 4578  df-iota 5754  df-fv 5798  df-ov 6530  df-neg 10120  df-z 11211
This theorem is referenced by:  zcnd  11315  suprfinzcl  11324  eluzmn  11526  eluzelre  11530  uzm1  11550  zsupss  11609  suprzcl2  11610  uzwo3  11615  rpnnen1lem3  11648  rpnnen1lem5  11650  rpnnen1lem3OLD  11654  rpnnen1lem5OLD  11656  zltaddlt1le  12151  fzsplit2  12192  fzdisj  12194  fzpreddisj  12215  fznatpl1  12220  fzp1disj  12224  uzdisj  12237  fzm1  12244  fz0fzdiffz0  12272  elfzmlbm  12273  elfzmlbp  12274  difelfznle  12277  nn0disj  12279  elfzolt3  12304  fzonel  12307  fzospliti  12324  fzodisj  12326  fzouzdisj  12328  fzodisjsn  12329  fzonmapblen  12336  fzoaddel  12343  elincfzoext  12348  reflcl  12414  flge  12423  flwordi  12430  fladdz  12443  2tnp1ge0ge0  12447  flhalf  12448  fldiv4p1lem1div2  12453  fldiv4lem1div2uz2  12454  fldiv4lem1div2  12455  flleceil  12469  fleqceilz  12470  quoremz  12471  uzsup  12479  modmul12d  12541  modaddmodup  12550  modaddmodlo  12551  modfzo0difsn  12559  modsumfzodifsn  12560  addmodlteq  12562  om2uzlti  12566  om2uzf1oi  12569  seqf1olem1  12657  seqf1olem2  12658  bcval4  12911  bcp1nk  12921  bcval5  12922  fzsdom2  13027  seqcoll  13057  seqcoll2  13058  ccatrn  13171  ccatalpha  13174  cshwidxmodr  13347  fzomaxdiflem  13876  fzomaxdif  13877  rexuzre  13886  limsupgre  14006  rlimclim1  14070  isercoll  14192  iseralt  14209  fsumm1  14270  fsum1p  14272  fsum0diaglem  14296  modfsummods  14312  isumsplit  14357  climcndslem1  14366  mertenslem1  14401  ntrivcvgmul  14419  fprodntriv  14457  fprod1p  14483  fprodeq0  14490  fallfacval4  14559  bpoly4  14575  fzo0dvdseq  14829  dvdsmod  14834  oexpneg  14853  mod2eq1n2dvds  14855  ltoddhalfle  14869  flodddiv4t2lthalf  14924  bitsp1  14937  bitsfzolem  14940  bitsfzo  14941  bitsmod  14942  bitscmp  14944  bitsinv1lem  14947  sadaddlem  14972  bitsres  14979  bitsuz  14980  smumul  14999  gcd0id  15024  gcdneg  15027  dfgcd2  15047  nn0seqcvgd  15067  lcmgcdlem  15103  nprm  15185  prmdvdsfz  15201  isprm5  15203  isprm7  15204  coprm  15207  prmexpb  15214  prmfac1  15215  hashdvds  15264  crth  15267  eulerthlem2  15271  fermltl  15273  prmdiv  15274  prmdiveq  15275  hashgcdlem  15277  odzdvds  15284  vfermltlALT  15291  modprm0  15294  modprmn0modprm0  15296  prm23ge5  15304  pythagtriplem13  15316  pcxcl  15349  pcaddlem  15376  pcadd  15377  pcfac  15387  qexpz  15389  prmunb  15402  1arithlem4  15414  4sqlem5  15430  4sqlem6  15431  4sqlem7  15432  4sqlem10  15435  4sqlem11  15443  4sqlem12  15444  4sqlem15  15447  4sqlem16  15448  4sqlem17  15449  vdwnnlem3  15485  prmgaplem7  15545  cshwshashlem3  15588  subgmulg  17377  mndodconglem  17729  odnncl  17733  odmod  17734  oddvds  17735  dfod2  17750  sylow1lem3  17784  efgsp1  17919  efgredleme  17925  telgsumfzs  18155  zringlpirlem1  19597  zringlpirlem3  19599  znf1o  19664  zcld  22356  ovoliunlem1  22994  ovoliunlem2  22995  dyadss  23085  dyaddisjlem  23086  dyadmaxlem  23088  dvfsumle  23505  dvfsumge  23506  dvfsumabs  23507  dvfsumlem1  23510  dvfsumlem3  23512  degltlem1  23553  plyco0  23669  plyeq0lem  23687  plydivex  23773  aannenlem1  23804  efif1olem2  24010  nnlogbexp  24236  logblt  24239  ang180lem1  24256  ang180lem3  24258  wilthlem2  24512  basellem3  24526  basellem4  24527  ppiprm  24594  chtdif  24601  ppidif  24606  chtub  24654  mersenne  24669  bcmono  24719  bcmax  24720  bposlem1  24726  bposlem3  24728  bposlem5  24730  bposlem6  24731  lgslem4  24742  lgsval2lem  24749  lgsvalmod  24758  lgsneg  24763  lgsmod  24765  lgsdilem  24766  lgsdirprm  24773  lgsdilem2  24775  lgsne0  24777  lgssq  24779  lgssq2  24780  lgsqr  24793  lgsdchr  24797  gausslemma2dlem1a  24807  gausslemma2dlem3  24810  gausslemma2dlem5a  24812  gausslemma2dlem6  24814  gausslemma2d  24816  lgseisenlem1  24817  lgseisenlem2  24818  lgseisenlem3  24819  lgseisenlem4  24820  lgsquadlem1  24822  lgsquadlem2  24823  lgsquadlem3  24824  lgsquad3  24829  2lgslem1a2  24832  2lgslem1  24836  2lgslem2  24837  2sqlem3  24862  2sqlem8  24868  2sqblem  24873  chebbnd1lem1  24875  chebbnd1lem2  24876  chebbnd1lem3  24877  dchrmusum2  24900  dchrvmasumlem1  24901  dchrvmasum2lem  24902  dchrvmasum2if  24903  dchrvmasumlem3  24905  dchrvmasumiflem2  24908  dchrisum0lem1  24922  dchrmusumlem  24928  mudivsum  24936  mulogsumlem  24937  mulogsum  24938  mulog2sumlem2  24941  mulog2sumlem3  24942  selberglem1  24951  selberglem2  24952  pntpbnd1  24992  pntlemg  25004  pntlemf  25011  qabvle  25031  padicabv  25036  padicabvcxp  25038  ostth2lem2  25040  axlowdimlem13  25552  axlowdimlem16  25555  clwwisshclwwlem1  26099  numclwwlk5  26405  nndiffz1  28742  fzsplit3  28746  bcm1n  28747  ltesubnnd  28761  2sqmod  28785  pnfinf  28874  dya2iocress  29469  dya2iocbrsiga  29470  dya2icobrsiga  29471  dya2icoseg  29472  dya2iocucvr  29479  sxbrsigalem2  29481  ballotlemfc0  29687  ballotlemfcc  29688  ballotlemodife  29692  ballotlemimin  29700  ballotlemsgt1  29705  ballotlemsel1i  29707  ballotlemsi  29709  ballotlemsima  29710  ballotlemrv2  29716  ballotlemfrceq  29723  ballotlemfrcn0  29724  ballotlemirc  29726  subfacval3  30231  erdszelem8  30240  erdszelem9  30241  supfz  30672  inffz  30673  inffzOLD  30674  dnizeq0  31441  dnizphlfeqhlf  31442  dnibndlem13  31456  knoppndvlem1  31479  knoppndvlem2  31480  knoppndvlem7  31485  knoppndvlem19  31497  knoppndvlem21  31499  ltflcei  32363  leceifl  32364  poimirlem1  32376  poimirlem2  32377  poimirlem6  32381  poimirlem7  32382  poimirlem8  32383  poimirlem15  32390  poimirlem16  32391  poimirlem17  32392  poimirlem19  32394  poimirlem20  32395  poimirlem23  32398  poimirlem24  32399  poimirlem27  32402  poimirlem29  32404  poimirlem31  32406  poimirlem32  32407  mblfinlem2  32413  itg2addnclem2  32428  mettrifi  32519  cntotbnd  32561  lzunuz  36145  lzenom  36147  diophin  36150  irrapxlem1  36200  irrapxlem2  36201  irrapxlem3  36202  irrapxlem4  36203  pellexlem5  36211  pellexlem6  36212  rmspecfund  36288  rmxypos  36328  ltrmynn0  36329  ltrmxnn0  36330  ltrmy  36333  rmyeq0  36334  rmyeq  36335  lermy  36336  rmyabs  36339  jm2.24nn  36340  jm2.17a  36341  jm2.17b  36342  jm2.17c  36343  jm2.24  36344  rmygeid  36345  acongrep  36361  fzmaxdif  36362  acongeq  36364  jm2.22  36376  jm2.23  36377  jm2.26lem3  36382  jm2.27a  36386  jm3.1lem1  36398  jm3.1lem3  36400  expdiophlem1  36402  prmunb2  37328  nzprmdif  37336  hashnzfzclim  37339  binomcxplemnn0  37366  uzwo4  38042  ssinc  38088  ssdec  38089  zltlesub  38234  monoords  38248  fzisoeu  38251  fperiodmul  38255  fzdifsuc2  38263  iuneqfzuzlem  38288  fmul01  38444  fmul01lt1lem1  38448  fmul01lt1lem2  38449  climsuselem1  38471  climsuse  38472  sumnnodd  38494  ltmod  38502  ioodvbdlimc1lem2  38619  ioodvbdlimc2lem  38621  dvnmul  38630  dvnprodlem1  38633  dvnprodlem2  38634  iblspltprt  38662  itgspltprt  38668  stoweidlem3  38693  stoweidlem11  38701  stoweidlem20  38710  stoweidlem26  38716  stoweidlem34  38724  stoweidlem59  38749  stirlinglem5  38768  dirkertrigeqlem3  38790  dirkeritg  38792  dirkercncflem1  38793  dirkercncflem2  38794  dirkercncflem4  38796  fourierdlem4  38801  fourierdlem6  38803  fourierdlem7  38804  fourierdlem11  38808  fourierdlem12  38809  fourierdlem15  38812  fourierdlem19  38816  fourierdlem20  38817  fourierdlem25  38822  fourierdlem26  38823  fourierdlem34  38831  fourierdlem35  38832  fourierdlem41  38838  fourierdlem48  38844  fourierdlem49  38845  fourierdlem50  38846  fourierdlem51  38847  fourierdlem54  38850  fourierdlem63  38859  fourierdlem64  38860  fourierdlem65  38861  fourierdlem71  38867  fourierdlem79  38875  fourierdlem89  38885  fourierdlem90  38886  fourierdlem91  38887  fourierdlem102  38898  fourierdlem103  38899  fourierdlem104  38900  fourierdlem114  38910  fouriersw  38921  elaa2lem  38923  etransclem3  38927  etransclem4  38928  etransclem7  38931  etransclem10  38934  etransclem15  38939  etransclem19  38943  etransclem23  38947  etransclem24  38948  etransclem25  38949  etransclem27  38951  etransclem31  38955  etransclem32  38956  etransclem35  38959  etransclem41  38965  etransclem44  38968  etransclem46  38970  etransclem48  38972  iundjiun  39150  caratheodorylem1  39213  fzopredsuc  39744  iccpartgt  39763  icceuelpartlem  39771  icceuelpart  39772  iccpartnel  39774  lighneallem2  39859  proththd  39867  dfodd4  39907  oexpnegALTV  39924  nnoALTV  39942  gbogt5  39982  gboage9  39984  stgoldbwt  39996  bgoldbst  39998  sgoldbalt  40001  bgoldbtbndlem1  40019  bgoldbtbndlem2  40020  bgoldbtbndlem3  40021  bgoldbtbnd  40023  bgoldbachlt  40025  tgblthelfgott  40027  tgoldbach  40030  bgoldbachltOLD  40032  tgblthelfgottOLD  40034  tgoldbachOLD  40037  2elfz2melfz  40175  elfzelfzlble  40178  fsummsndifre  40214  pthdlem1  40967  crctcsh1wlkn0  41019  crctcsh  41022  clwwisshclwwslemlem  41228  eucrctshift  41406  pw2m1lepw2m1  42099  m1modmmod  42105  difmodm1lt  42106  fllogbd  42147  logbpw2m1  42154  fllog2  42155  nnpw2blen  42167  nnolog2flm1  42177  dignn0flhalflem1  42202  dignn0flhalflem2  42203
  Copyright terms: Public domain W3C validator