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

Theorem zred 10994
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 10896 . 2
2 zred.1 . 2
31, 2sseldi 3501 1
Colors of variables: wff setvar class
Syntax hints:  ->wi 4  e.wcel 1818   cr 9512   cz 10889
This theorem is referenced by:  zcnd  10995  suprfinzcl  11003  eluzelre  11120  uzm1  11140  zsupss  11200  suprzcl2  11201  uzwo3  11206  rpnnen1lem3  11239  rpnnen1lem5  11241  fzsplit2  11739  fzdisj  11741  fzpreddisj  11758  fznatpl1  11763  fzp1disj  11767  uzdisj  11780  fzm1  11787  fz0fzdiffz0  11812  elfzmlbm  11813  elfzmlbp  11815  difelfznle  11818  nn0disj  11820  elfzolt3  11838  fzonel  11841  fzospliti  11857  fzodisj  11859  fzouzdisj  11861  fzonmapblen  11868  fzoaddel  11873  reflcl  11933  flge  11942  flwordi  11948  fladdz  11958  flhalf  11962  flleceil  11980  fleqceilz  11981  quoremz  11982  uzsup  11990  modmul12d  12041  modaddmodup  12050  modaddmodlo  12051  om2uzlti  12061  om2uzf1oi  12064  seqf1olem1  12146  seqf1olem2  12147  bcval4  12385  bcp1nk  12395  bcval5  12396  fzsdom2  12486  seqcoll  12512  seqcoll2  12513  ccatrn  12606  fzomaxdiflem  13175  fzomaxdif  13176  rexuzre  13185  limsupgre  13304  rlimclim1  13368  isercoll  13490  iseralt  13507  fsumm1  13566  fsum1p  13568  fsum0diaglem  13591  modfsummods  13607  isumsplit  13652  climcndslem1  13661  mertenslem1  13693  ntrivcvgmul  13711  fprodntriv  13749  fprod1p  13772  fprodeq0  13779  fzo0dvdseq  14039  dvdsmod  14043  oexpneg  14049  bitsp1  14081  bitsfzolem  14084  bitsfzo  14085  bitsmod  14086  bitscmp  14088  bitsinv1lem  14091  sadaddlem  14116  bitsres  14123  bitsuz  14124  smumul  14143  gcd0id  14161  gcdneg  14164  nn0seqcvgd  14199  nprm  14231  coprm  14241  isprm5  14253  prmexpb  14258  prmfac1  14259  hashdvds  14305  crt  14308  eulerthlem2  14312  fermltl  14314  prmdiv  14315  prmdiveq  14316  odzdvds  14322  modprm0  14330  modprmn0modprm0  14332  pythagtriplem13  14351  pcxcl  14384  pcaddlem  14407  pcadd  14408  pcfac  14418  qexpz  14420  prmunb  14432  1arithlem4  14444  4sqlem5  14460  4sqlem6  14461  4sqlem7  14462  4sqlem10  14465  4sqlem11  14473  4sqlem12  14474  4sqlem15  14477  4sqlem16  14478  4sqlem17  14479  vdwnnlem3  14515  cshwshashlem3  14582  subgmulg  16215  mndodconglem  16565  odnncl  16569  odmod  16570  oddvds  16571  dfod2  16586  sylow1lem3  16620  efgsp1  16755  efgredleme  16761  telgsumfzs  17018  zringlpirlem1  18509  zringlpirlem3  18511  zlpirlem1  18514  zlpirlem3  18516  znf1o  18590  zcld  21318  ovoliunlem1  21913  ovoliunlem2  21914  dyadss  22003  dyaddisjlem  22004  dyadmaxlem  22006  dvfsumle  22422  dvfsumge  22423  dvfsumabs  22424  dvfsumlem1  22427  dvfsumlem3  22429  degltlem1  22472  plyco0  22589  plyeq0lem  22607  plydivex  22693  aannenlem1  22724  efif1olem2  22930  ang180lem1  23141  ang180lem3  23143  wilthlem2  23343  basellem3  23356  basellem4  23357  ppiprm  23425  chtdif  23432  ppidif  23437  chtub  23487  mersenne  23502  bcmono  23552  bcmax  23553  bposlem1  23559  bposlem3  23561  bposlem5  23563  bposlem6  23564  lgslem4  23574  lgsval2lem  23581  lgsvalmod  23590  lgsneg  23594  lgsmod  23596  lgsdilem  23597  lgsdirprm  23604  lgsdilem2  23606  lgsne0  23608  lgssq  23610  lgssq2  23611  lgsqr  23621  lgsdchr  23623  lgseisenlem1  23624  lgseisenlem2  23625  lgseisenlem3  23626  lgseisenlem4  23627  lgsquadlem1  23629  lgsquadlem2  23630  lgsquadlem3  23631  lgsquad3  23636  2sqlem3  23641  2sqlem8  23647  2sqblem  23652  chebbnd1lem1  23654  chebbnd1lem2  23655  chebbnd1lem3  23656  dchrmusum2  23679  dchrvmasumlem1  23680  dchrvmasum2lem  23681  dchrvmasum2if  23682  dchrvmasumlem3  23684  dchrvmasumiflem2  23687  dchrisum0lem1  23701  dchrmusumlem  23707  mudivsum  23715  mulogsumlem  23716  mulogsum  23717  mulog2sumlem2  23720  mulog2sumlem3  23721  selberglem1  23730  selberglem2  23731  pntpbnd1  23771  pntlemg  23783  pntlemf  23790  qabvle  23810  padicabv  23815  padicabvcxp  23817  ostth2lem2  23819  axlowdimlem13  24257  axlowdimlem16  24260  clwwisshclwwlem1  24805  numclwwlk5  25112  nndiffz1  27596  fzsplit3  27599  bcm1n  27600  ltesubnnd  27612  2sqmod  27636  pnfinf  27727  nnlogbexp  28020  logblt  28022  dya2iocress  28245  dya2iocbrsiga  28246  dya2icobrsiga  28247  dya2icoseg  28248  dya2iocucvr  28255  sxbrsigalem2  28257  ballotlemfc0  28431  ballotlemfcc  28432  ballotlemodife  28436  ballotlemimin  28444  ballotlemsgt1  28449  ballotlemsel1i  28451  ballotlemsi  28453  ballotlemsima  28454  ballotlemrv2  28460  ballotlemfrceq  28467  ballotlemfrcn0  28468  ballotlemirc  28470  eluzmn  28491  subfacval3  28633  erdszelem8  28642  erdszelem9  28643  supfz  29107  inffz  29108  fallfacval4  29165  bpoly4  29821  ltflcei  30043  leceifl  30044  mblfinlem2  30052  dvtanlem  30064  itg2addnclem2  30067  mettrifi  30250  cntotbnd  30292  lzunuz  30701  lzenom  30703  diophin  30706  irrapxlem1  30758  irrapxlem2  30759  irrapxlem3  30760  irrapxlem4  30761  pellexlem5  30769  pellexlem6  30770  rmspecfund  30845  rmxypos  30885  ltrmynn0  30886  ltrmxnn0  30887  ltrmy  30890  rmyeq0  30891  rmyeq  30892  lermy  30893  rmyabs  30896  jm2.24nn  30897  jm2.17a  30898  jm2.17b  30899  jm2.17c  30900  jm2.24  30901  rmygeid  30902  acongrep  30918  fzmaxdif  30919  acongeq  30921  jm2.22  30937  jm2.23  30938  jm2.26lem3  30943  jm2.27a  30947  jm3.1lem1  30959  jm3.1lem3  30961  expdiophlem1  30963  hashgcdlem  31157  prmunb2  31191  isprm7  31192  lcmgcdlem  31212  nzprmdif  31224  hashnzfzclim  31227  binomcxplemnn0  31254  zltlesub  31468  monoords  31496  fzisoeu  31500  fperiodmul  31504  fzdifsuc2  31512  fmul01  31574  fmul01lt1lem1  31578  fmul01lt1lem2  31579  climsuselem1  31613  climsuse  31614  sumnnodd  31636  ltmod  31644  ioodvbdlimc1lem2  31729  ioodvbdlimc2lem  31731  dvnmul  31740  dvnprodlem1  31743  dvnprodlem2  31744  iblspltprt  31772  itgspltprt  31778  stoweidlem3  31785  stoweidlem11  31793  stoweidlem20  31802  stoweidlem26  31808  stoweidlem34  31816  stoweidlem59  31841  stirlinglem5  31860  dirkertrigeqlem3  31882  dirkeritg  31884  dirkercncflem1  31885  dirkercncflem2  31886  dirkercncflem4  31888  fourierdlem4  31893  fourierdlem6  31895  fourierdlem7  31896  fourierdlem11  31900  fourierdlem12  31901  fourierdlem15  31904  fourierdlem19  31908  fourierdlem20  31909  fourierdlem25  31914  fourierdlem26  31915  fourierdlem34  31923  fourierdlem35  31924  fourierdlem41  31930  fourierdlem48  31937  fourierdlem49  31938  fourierdlem50  31939  fourierdlem51  31940  fourierdlem54  31943  fourierdlem63  31952  fourierdlem64  31953  fourierdlem65  31954  fourierdlem71  31960  fourierdlem79  31968  fourierdlem89  31978  fourierdlem90  31979  fourierdlem91  31980  fourierdlem102  31991  fourierdlem103  31992  fourierdlem104  31993  fourierdlem114  32003  fouriersw  32014  elaa2lem  32016  etransclem3  32020  etransclem4  32021  etransclem7  32024  etransclem10  32027  etransclem15  32032  etransclem19  32036  etransclem23  32040  etransclem24  32041  etransclem25  32042  etransclem27  32044  etransclem31  32048  etransclem32  32049  etransclem35  32052  etransclem41  32058  etransclem44  32061  etransclem46  32063  etransclem48  32065  2elfz2melfz  32334  elfzelfzlble  32337  fsummsndifre  32345
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1618  ax-4 1631  ax-5 1704  ax-6 1747  ax-7 1790  ax-10 1837  ax-11 1842  ax-12 1854  ax-13 1999  ax-ext 2435
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3or 974  df-3an 975  df-tru 1398  df-ex 1613  df-nf 1617  df-sb 1740  df-clab 2443  df-cleq 2449  df-clel 2452  df-nfc 2607  df-rex 2813  df-rab 2816  df-v 3111  df-dif 3478  df-un 3480  df-in 3482  df-ss 3489  df-nul 3785  df-if 3942  df-sn 4030  df-pr 4032  df-op 4036  df-uni 4250  df-br 4453  df-iota 5556  df-fv 5601  df-ov 6299  df-neg 9831  df-z 10890
  Copyright terms: Public domain W3C validator