Theorem zred 9778

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 9660	. 2 |- ZZ C_ RR
2		zred.1	. 2 |- ( ph -> A e. ZZ )
3	1, 2	sselid 3246	1 |- ( ph -> A e. RR )

This proof depends on syntax axioms:   -> wi 4   e. wcel 2209   RRcr 8184   ZZcz 9653

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-io 721  ax-5 1500  ax-7 1501  ax-gen 1502  ax-ie1 1546  ax-ie2 1547  ax-8 1557  ax-10 1558  ax-11 1559  ax-i12 1560  ax-bndl 1562  ax-4 1563  ax-17 1579  ax-i9 1583  ax-ial 1587  ax-i5r 1588  ax-ext 2220

This proof depends on definitions:  df-bi 117  df-3or 1010  df-3an 1011  df-tru 1405  df-nf 1514  df-sb 1816  df-clab 2225  df-cleq 2231  df-clel 2234  df-nfc 2381  df-rex 2534  df-rab 2537  df-v 2823  df-un 3224  df-in 3226  df-ss 3233  df-sn 3715  df-pr 3716  df-op 3718  df-uni 3936  df-br 4132  df-iota 5340  df-fv 5388  df-ov 6091  df-neg 8507  df-z 9654

This theorem is used by:  zcnd  9779  btwnapz  9786  eluzmn  9943  eluzelre  9947  eluzadd  9966  eluzsub  9967  uzm1  9968  ltesubnnd  10186  z2ge  10244  zltaddlt1le  10426  fztri3or  10459  fznlem  10461  fzdisj  10473  fzpreddisj  10494  fznatpl1  10499  uzdisj  10516  fzm1  10523  fz0fzdiffz0  10553  elfzmlbm  10554  elfzmlbp  10555  difelfznle  10558  nn0disj  10561  elfzolt3  10581  fzonel  10584  fzouzdisj  10605  fzodisjsn  10607  fzonmapblen  10615  fzoaddel  10621  elincfzoext  10627  elfzonelfzo  10664  zsupcl  10680  zssinfcl  10681  infssuzex  10682  suprzubdc  10687  zsupssdc  10689  suprzcl2dc  10690  qtri3or  10691  exbtwnzlemstep  10698  exbtwnzlemex  10700  exbtwnz  10701  rebtwn2zlemstep  10703  rebtwn2z  10705  qbtwnrelemcalc  10706  qbtwnre  10707  apbtwnz  10725  qfraclt1  10733  qfracge0  10734  flqge  10735  flapge  10736  flaplt  10738  flid  10739  flqltnz  10742  flqwordi  10743  flqaddz  10752  flqmulnn0  10754  btwnzge0  10755  2tnp1ge0ge0  10756  flhalf  10757  flltdivnn0lt  10759  fldiv4p1lem1div2  10760  fldiv4lem1div2uz2  10761  ceiqge  10766  ceiqm1l  10768  ceiqle  10770  flqleceil  10774  flqeqceilz  10775  intfracq  10777  modqval  10781  modqge0  10789  modqlt  10790  modqmulnn  10799  mulp1mod1  10822  modaddmodup  10844  modaddmodlo  10845  modsumfzodifsn  10853  addmodlteq  10855  frec2uzlt2d  10861  frec2uzf1od  10863  uzennn  10893  seq3split  10945  iseqf1olemkle  10954  iseqf1olemqcl  10956  iseqf1olemnab  10958  iseqf1olemab  10959  iseqf1olemqk  10964  seq3f1olemqsumkj  10968  seq3f1olemqsumk  10969  seq3f1olemqsum  10970  seqf1oglem1  10976  seqf1oglem2  10977  seqfeq4g  10988  exp3val  10998  expcanlem  11174  expcan  11175  facavg  11205  bcval4  11211  bcp1nk  11221  bcval5  11222  bcm1n  11228  zfz1isolemiso  11312  seq3coll  11315  iswrdiz  11332  ccatrn  11398  ccatalpha  11402  seq3shft  11624  resqrexlemdecn  11799  fzomaxdiflem  11900  nn0maxcl  12013  fiidxsupcl  12017  fsum3cvg3  12187  fsumm1  12207  fsum1p  12209  fsum0diaglem  12231  isumshft  12281  isumsplit  12282  divcnv  12288  geolim2  12303  cvgratnnlemabsle  12318  cvgratnnlemsumlt  12319  cvgratnnlemrate  12321  cvgratz  12323  mertenslemi1  12326  fprodntrivap  12375  prodsnf  12383  fprod1p  12390  fprodeq0  12408  zdvdsdc  12603  dvdslelemd  12634  oexpneg  12668  ltoddhalfle  12684  divalglemnqt  12711  divalglemex  12713  divalglemeuneg  12714  flodddiv4t2lthalf  12730  bitsfzolem  12745  bitsfzo  12746  bitsmod  12747  bitscmp  12749  dvdsbnd  12757  dvdslegcd  12765  gcd0id  12780  gcdneg  12783  bezoutlemsup  12810  dfgcd2  12815  uzwodc  12838  nn0seqcvgd  12843  lcmgcdlem  12879  ncoprmgcdne1b  12891  nprm  12925  prmdc  12932  prmdvdsfz  12942  isprm5lem  12944  coprm  12947  prmexpb  12954  prmfac1  12955  znege1  12982  sqrt2irrap  12984  hashdvds  13027  eulerthlemrprm  13035  eulerthlema  13036  hashgcdlem  13044  pythagtriplem13  13083  pythagtriplem16  13086  pcxcl  13118  pcaddlem  13146  pcadd  13147  pcfac  13157  qexpz  13159  4sqlem7  13191  4sqlem10  13194  4sqexercise2  13206  4sqlemsdc  13207  4sqlem11  13208  4sqlem12  13209  4sqlem15  13212  4sqlem16  13213  4sqlem17  13214  ballotfilemfc0  13289  ballotfilemfcc  13290  ballotfilemimin  13306  ballotfilemsgt1  13311  ballotfilemsel1i  13313  ballotfilemsi  13315  ballotfilemsima  13316  ballotfilemgun  13325  ballotfilemfrceq  13329  ballotfilemfrcn0  13330  ballotfilemirc  13332  oddennn  13340  ennnfoneleminc  13359  nninfdclemp1  13398  nninfdclemlt  13399  gzsumfzval  13769  gzsumcl  13862  mulgfng  13985  subgmulg  14049  gzsumreidx  14230  gzsumsubmcl  14231  gzsummhm  14234  gzsumsplit0  14237  gzsumshift  14238  psrbaglefifi  15175  ltexp2  16194  logblt  16215  ppiqfi  16259  chtdif  16281  ppidif  16286  ppiqub  16310  chtqub  16313  mersenne  16314  bcmono  16321  bcmax  16322  prmefexple  16325  bposlem1  16328  bposlem3  16330  bposlem4  16331  bposlem5  16332  bposlem6  16333  lgsval2lem  16351  lgsvalmod  16360  lgsneg  16365  lgsdilem  16368  lgssq  16381  lgssq2  16382  gausslemma2dlem1a  16399  gausslemma2dlem3  16404  lgseisenlem2  16412  lgsquadlem1  16418  lgsquadlem2  16419  lgsquadlem3  16420  lgsquad3  16425  2lgslem1a2  16428  2sqlem3  16458  2sqlem8  16464  supfz  17345  inffz  17346