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

Theorem zred 10739
Description: An integer is a real number. (Contributed by Mario Carneiro, 28-May-2016.)
Hypothesis
Ref Expression
zred.1  |-  ( ph  ->  A  e.  ZZ )
Assertion
Ref Expression
zred  |-  ( ph  ->  A  e.  RR )

Proof of Theorem zred
StepHypRef Expression
1 zssre 10645 . 2  |-  ZZ  C_  RR
2 zred.1 . 2  |-  ( ph  ->  A  e.  ZZ )
31, 2sseldi 3349 1  |-  ( ph  ->  A  e.  RR )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    e. wcel 1756   RRcr 9273   ZZcz 10638
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2419
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3or 966  df-3an 967  df-tru 1372  df-ex 1587  df-nf 1590  df-sb 1701  df-clab 2425  df-cleq 2431  df-clel 2434  df-nfc 2563  df-rex 2716  df-rab 2719  df-v 2969  df-dif 3326  df-un 3328  df-in 3330  df-ss 3337  df-nul 3633  df-if 3787  df-sn 3873  df-pr 3875  df-op 3879  df-uni 4087  df-br 4288  df-iota 5376  df-fv 5421  df-ov 6089  df-neg 9590  df-z 10639
This theorem is referenced by:  zcnd  10740  eluzelre  10863  uzm1  10883  zsupss  10936  suprzcl2  10937  uzwo3  10940  rpnnen1lem3  10973  rpnnen1lem5  10975  fzsplit2  11466  fzdisj  11468  fz0fzdiffz0  11481  elfzmlbp  11483  fzpreddisj  11496  fznatpl1  11502  fzp1disj  11507  uzdisj  11523  elfzolt3  11554  fzonel  11557  fzospliti  11573  fzodisj  11575  fzouzdisj  11577  fzonmapblen  11584  fzoaddel  11589  reflcl  11638  flge  11647  flwordi  11652  fladdz  11662  flhalf  11666  flleceil  11684  fleqceilz  11685  quoremz  11686  uzsup  11694  modmul12d  11745  modaddmodup  11754  modaddmodlo  11755  om2uzlti  11765  om2uzf1oi  11768  seqf1olem1  11837  seqf1olem2  11838  bcval4  12075  bcp1nk  12085  bcval5  12086  fzsdom2  12181  seqcoll  12208  seqcoll2  12209  fzomaxdiflem  12822  fzomaxdif  12823  rexuzre  12832  limsupgre  12951  rlimclim1  13015  isercoll  13137  iseralt  13154  fsumm1  13212  fsum1p  13214  fsum0diaglem  13235  isumsplit  13295  climcndslem1  13304  mertenslem1  13336  fzo0dvdseq  13578  dvdsmod  13582  oexpneg  13587  bitsp1  13619  bitsfzolem  13622  bitsfzo  13623  bitsmod  13624  bitscmp  13626  bitsinv1lem  13629  sadaddlem  13654  bitsres  13661  bitsuz  13662  smumul  13681  gcd0id  13699  gcdneg  13702  nn0seqcvgd  13737  nprm  13769  coprm  13778  isprm5  13790  prmexpb  13795  prmfac1  13796  hashdvds  13842  crt  13845  eulerthlem2  13849  fermltl  13851  prmdiv  13852  prmdiveq  13853  odzdvds  13859  modprm0  13865  modprmn0modprm0  13867  pythagtriplem13  13886  pcxcl  13919  pcaddlem  13942  pcadd  13943  pcfac  13953  qexpz  13955  prmunb  13967  1arithlem4  13979  4sqlem5  13995  4sqlem6  13996  4sqlem7  13997  4sqlem10  14000  4sqlem11  14008  4sqlem12  14009  4sqlem15  14012  4sqlem16  14013  4sqlem17  14014  vdwnnlem3  14050  cshwshashlem3  14116  subgmulg  15686  mndodconglem  16035  odnncl  16039  odmod  16040  oddvds  16041  dfod2  16056  sylow1lem3  16090  efgsp1  16225  efgredleme  16231  zringlpirlem1  17878  zringlpirlem3  17880  zlpirlem1  17883  zlpirlem3  17885  znf1o  17959  zcld  20365  ovoliunlem1  20960  ovoliunlem2  20961  dyadss  21049  dyaddisjlem  21050  dyadmaxlem  21052  dvfsumle  21468  dvfsumge  21469  dvfsumabs  21470  dvfsumlem1  21473  dvfsumlem3  21475  degltlem1  21518  plyco0  21635  plyeq0lem  21653  plydivex  21738  aannenlem1  21769  efif1olem2  21974  ang180lem1  22180  ang180lem3  22182  wilthlem2  22382  basellem3  22395  basellem4  22396  ppiprm  22464  chtdif  22471  ppidif  22476  chtub  22526  mersenne  22541  bcmono  22591  bcmax  22592  bposlem1  22598  bposlem3  22600  bposlem5  22602  bposlem6  22603  lgslem4  22613  lgsval2lem  22620  lgsvalmod  22629  lgsneg  22633  lgsmod  22635  lgsdilem  22636  lgsdirprm  22643  lgsdilem2  22645  lgsne0  22647  lgssq  22649  lgssq2  22650  lgsqr  22660  lgsdchr  22662  lgseisenlem1  22663  lgseisenlem2  22664  lgseisenlem3  22665  lgseisenlem4  22666  lgsquadlem1  22668  lgsquadlem2  22669  lgsquadlem3  22670  lgsquad3  22675  2sqlem3  22680  2sqlem8  22686  2sqblem  22691  chebbnd1lem1  22693  chebbnd1lem2  22694  chebbnd1lem3  22695  dchrmusum2  22718  dchrvmasumlem1  22719  dchrvmasum2lem  22720  dchrvmasum2if  22721  dchrvmasumlem3  22723  dchrvmasumiflem2  22726  dchrisum0lem1  22740  dchrmusumlem  22746  mudivsum  22754  mulogsumlem  22755  mulogsum  22756  mulog2sumlem2  22759  mulog2sumlem3  22760  selberglem1  22769  selberglem2  22770  pntpbnd1  22810  pntlemg  22822  pntlemf  22829  qabvle  22849  padicabv  22854  padicabvcxp  22856  ostth2lem2  22858  axlowdimlem13  23151  axlowdimlem16  23154  nndiffz1  26026  fzsplit3  26029  bcm1n  26030  ltesubnnd  26042  pnfinf  26151  nnlogbexp  26415  logblt  26417  dya2iocress  26641  dya2iocbrsiga  26642  dya2icobrsiga  26643  dya2icoseg  26644  dya2iocucvr  26651  sxbrsigalem2  26653  ballotlemfc0  26827  ballotlemfcc  26828  ballotlemodife  26832  ballotlemimin  26840  ballotlemsgt1  26845  ballotlemsel1i  26847  ballotlemsi  26849  ballotlemsima  26850  ballotlemrv2  26856  ballotlemfrceq  26863  ballotlemfrcn0  26864  ballotlemirc  26866  eluzmn  26887  subfacval3  27029  erdszelem8  27038  erdszelem9  27039  supfz  27337  inffz  27338  ntrivcvgmul  27368  fprodntriv  27406  fprod1p  27429  fprodeq0  27437  fallfacval4  27497  bpoly4  28153  ltflcei  28372  leceifl  28373  mblfinlem2  28382  dvtanlem  28394  itg2addnclem2  28397  mettrifi  28606  cntotbnd  28648  lzunuz  29059  lzenom  29061  diophin  29064  irrapxlem1  29116  irrapxlem2  29117  irrapxlem3  29118  irrapxlem4  29119  pellexlem5  29127  pellexlem6  29128  rmspecfund  29203  rmxypos  29243  ltrmynn0  29244  ltrmxnn0  29245  ltrmy  29248  rmyeq0  29249  rmyeq  29250  lermy  29251  rmyabs  29254  jm2.24nn  29255  jm2.17a  29256  jm2.17b  29257  jm2.17c  29258  jm2.24  29259  rmygeid  29260  acongrep  29276  fzmaxdif  29277  acongeq  29279  jm2.22  29297  jm2.23  29298  jm2.26lem3  29303  jm2.27a  29307  jm3.1lem1  29319  jm3.1lem3  29321  expdiophlem1  29323  hashgcdlem  29518  fmul01  29714  fmul01lt1lem1  29718  fmul01lt1lem2  29719  climsuselem1  29733  climsuse  29734  stoweidlem3  29751  stoweidlem11  29759  stoweidlem20  29768  stoweidlem26  29774  stoweidlem34  29782  stoweidlem59  29807  stirlinglem5  29826  2elfz2melfz  30155  elfzelfzlble  30162  fsummsndifre  30190  modfsummods  30197  clwwisshclwwlem1  30422  difelfznle  30441  numclwwlk5  30658  suprfinzcl  30696
  Copyright terms: Public domain W3C validator