Theorem zred 9703

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

Step	Hyp	Ref	Expression
1		zssre 9586	. 2 |- ZZ C_ RR
2		zred.1	. 2 |- ( ph -> A e. ZZ )
3	1, 2	sselid 3238	1 |- ( ph -> A e. RR )

Syntax hints:   -> wi 4   e. wcel 2205   RRcr 8128   ZZcz 9579

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-io 717  ax-5 1496  ax-7 1497  ax-gen 1498  ax-ie1 1542  ax-ie2 1543  ax-8 1553  ax-10 1554  ax-11 1555  ax-i12 1556  ax-bndl 1558  ax-4 1559  ax-17 1575  ax-i9 1579  ax-ial 1583  ax-i5r 1584  ax-ext 2216

This theorem depends on definitions:  df-bi 117  df-3or 1006  df-3an 1007  df-tru 1401  df-nf 1510  df-sb 1812  df-clab 2221  df-cleq 2227  df-clel 2230  df-nfc 2375  df-rex 2528  df-rab 2531  df-v 2817  df-un 3217  df-in 3219  df-ss 3226  df-sn 3697  df-pr 3698  df-op 3700  df-uni 3917  df-br 4112  df-iota 5314  df-fv 5362  df-ov 6055  df-neg 8449  df-z 9580

This theorem is referenced by:  zcnd  9704  btwnapz  9711  eluzmn  9863  eluzelre  9867  eluzadd  9886  eluzsub  9887  uzm1  9888  z2ge  10162  zltaddlt1le  10344  fztri3or  10376  fznlem  10378  fzdisj  10389  fzpreddisj  10409  fznatpl1  10414  uzdisj  10431  fzm1  10438  fz0fzdiffz0  10468  elfzmlbm  10469  elfzmlbp  10470  difelfznle  10473  nn0disj  10476  elfzolt3  10496  fzonel  10499  fzouzdisj  10520  fzodisjsn  10522  fzonmapblen  10530  fzoaddel  10536  elincfzoext  10542  elfzonelfzo  10579  zsupcl  10595  zssinfcl  10596  infssuzex  10597  suprzubdc  10600  zsupssdc  10602  suprzcl2dc  10603  qtri3or  10604  exbtwnzlemstep  10611  exbtwnzlemex  10613  exbtwnz  10614  rebtwn2zlemstep  10616  rebtwn2z  10618  qbtwnrelemcalc  10619  qbtwnre  10620  apbtwnz  10638  qfraclt1  10644  qfracge0  10645  flqge  10646  flid  10648  flqltnz  10651  flqwordi  10652  flqaddz  10661  flqmulnn0  10663  btwnzge0  10664  2tnp1ge0ge0  10665  flhalf  10666  flltdivnn0lt  10668  fldiv4p1lem1div2  10669  fldiv4lem1div2uz2  10670  ceiqge  10675  ceiqm1l  10677  ceiqle  10679  flqleceil  10683  flqeqceilz  10684  intfracq  10686  modqval  10690  modqge0  10698  modqlt  10699  modqmulnn  10708  mulp1mod1  10731  modaddmodup  10753  modaddmodlo  10754  modsumfzodifsn  10762  addmodlteq  10764  frec2uzlt2d  10770  frec2uzf1od  10772  uzennn  10802  seq3split  10854  iseqf1olemkle  10863  iseqf1olemqcl  10865  iseqf1olemnab  10867  iseqf1olemab  10868  iseqf1olemqk  10873  seq3f1olemqsumkj  10877  seq3f1olemqsumk  10878  seq3f1olemqsum  10879  seqf1oglem1  10885  seqf1oglem2  10886  seqfeq4g  10897  exp3val  10907  expcanlem  11081  expcan  11082  facavg  11112  bcval4  11118  bcp1nk  11128  bcval5  11129  bcm1n  11135  zfz1isolemiso  11215  seq3coll  11218  iswrdiz  11235  ccatrn  11301  ccatalpha  11305  seq3shft  11527  resqrexlemdecn  11701  fzomaxdiflem  11801  nn0maxcl  11914  fsum3cvg3  12086  fsumm1  12106  fsum1p  12108  fsum0diaglem  12130  isumshft  12180  isumsplit  12181  divcnv  12187  geolim2  12202  cvgratnnlemabsle  12217  cvgratnnlemsumlt  12218  cvgratnnlemrate  12220  cvgratz  12222  mertenslemi1  12225  fprodntrivap  12274  prodsnf  12282  fprod1p  12289  fprodeq0  12307  zdvdsdc  12502  dvdslelemd  12533  oexpneg  12567  ltoddhalfle  12583  divalglemnqt  12610  divalglemex  12612  divalglemeuneg  12613  flodddiv4t2lthalf  12629  bitsfzolem  12644  bitsfzo  12645  bitsmod  12646  bitscmp  12648  dvdsbnd  12656  dvdslegcd  12664  gcd0id  12679  gcdneg  12682  bezoutlemsup  12709  dfgcd2  12714  uzwodc  12737  nn0seqcvgd  12742  lcmgcdlem  12778  ncoprmgcdne1b  12790  nprm  12824  prmdc  12831  prmdvdsfz  12840  isprm5lem  12842  coprm  12845  prmexpb  12852  prmfac1  12853  znege1  12879  sqrt2irrap  12881  hashdvds  12922  eulerthlemrprm  12930  eulerthlema  12931  hashgcdlem  12939  pythagtriplem13  12978  pythagtriplem16  12981  pcxcl  13013  pcaddlem  13041  pcadd  13042  pcfac  13052  qexpz  13054  4sqlem7  13086  4sqlem10  13089  4sqexercise2  13101  4sqlemsdc  13102  4sqlem11  13103  4sqlem12  13104  4sqlem15  13107  4sqlem16  13108  4sqlem17  13109  ballotfilemfc0  13153  ballotfilemfcc  13154  oddennn  13160  ennnfoneleminc  13179  nninfdclemp1  13218  nninfdclemlt  13219  gsumfzval  13621  gsumfzz  13725  gsumfzcl  13729  mulgfng  13858  subgmulg  13922  gsumfzreidx  14071  gsumfzsubmcl  14072  gsumfzmptfidmadd  14073  gsumfzmhm  14077  gsumsplit0  14080  gsumfzfsumlemm  14752  gsumfzfsum  14753  ltexp2  15823  logblt  15844  mersenne  15882  lgsval2lem  15900  lgsvalmod  15909  lgsneg  15914  lgsdilem  15917  lgssq  15930  lgssq2  15931  gausslemma2dlem1a  15948  gausslemma2dlem3  15953  lgseisenlem2  15961  lgsquadlem1  15967  lgsquadlem2  15968  lgsquadlem3  15969  lgsquad3  15974  2lgslem1a2  15977  2sqlem3  16007  2sqlem8  16013  supfz  16874  inffz  16875  gsumgfsumlem  16882