Theorem zred 9779

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 9662	. 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 9655

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 9656

This theorem is used by:  zcnd  9780  btwnapz  9787  eluzmn  9944  eluzelre  9948  eluzadd  9967  eluzsub  9968  uzm1  9969  ltesubnnd  10187  z2ge  10245  zltaddlt1le  10427  fztri3or  10460  fznlem  10462  fzdisj  10474  fzpreddisj  10495  fznatpl1  10500  uzdisj  10517  fzm1  10524  fz0fzdiffz0  10554  elfzmlbm  10555  elfzmlbp  10556  difelfznle  10559  nn0disj  10562  elfzolt3  10582  fzonel  10585  fzouzdisj  10606  fzodisjsn  10608  fzonmapblen  10616  fzoaddel  10622  elincfzoext  10628  elfzonelfzo  10665  zsupcl  10681  zssinfcl  10682  infssuzex  10683  suprzubdc  10688  zsupssdc  10690  suprzcl2dc  10691  qtri3or  10692  exbtwnzlemstep  10699  exbtwnzlemex  10701  exbtwnz  10702  rebtwn2zlemstep  10704  rebtwn2z  10706  qbtwnrelemcalc  10707  qbtwnre  10708  apbtwnz  10726  qfraclt1  10734  qfracge0  10735  flqge  10736  flapge  10737  flaplt  10739  flid  10740  flqltnz  10743  flqwordi  10744  flqaddz  10753  flqmulnn0  10755  btwnzge0  10756  2tnp1ge0ge0  10757  flhalf  10758  flltdivnn0lt  10760  fldiv4p1lem1div2  10761  fldiv4lem1div2uz2  10762  ceiqge  10767  ceiqm1l  10769  ceiqle  10771  flqleceil  10775  flqeqceilz  10776  intfracq  10778  modqval  10782  modqge0  10790  modqlt  10791  modqmulnn  10800  mulp1mod1  10823  modaddmodup  10845  modaddmodlo  10846  modsumfzodifsn  10854  addmodlteq  10856  frec2uzlt2d  10862  frec2uzf1od  10864  uzennn  10894  seq3split  10946  iseqf1olemkle  10955  iseqf1olemqcl  10957  iseqf1olemnab  10959  iseqf1olemab  10960  iseqf1olemqk  10965  seq3f1olemqsumkj  10969  seq3f1olemqsumk  10970  seq3f1olemqsum  10971  seqf1oglem1  10977  seqf1oglem2  10978  seqfeq4g  10989  exp3val  10999  expcanlem  11175  expcan  11176  facavg  11206  bcval4  11212  bcp1nk  11222  bcval5  11223  bcm1n  11229  zfz1isolemiso  11313  seq3coll  11316  iswrdiz  11333  ccatrn  11399  ccatalpha  11403  seq3shft  11625  resqrexlemdecn  11800  fzomaxdiflem  11901  nn0maxcl  12014  fiidxsupcl  12018  fsum3cvg3  12188  fsumm1  12208  fsum1p  12210  fsum0diaglem  12232  isumshft  12282  isumsplit  12283  divcnv  12289  geolim2  12304  cvgratnnlemabsle  12319  cvgratnnlemsumlt  12320  cvgratnnlemrate  12322  cvgratz  12324  mertenslemi1  12327  fprodntrivap  12376  prodsnf  12384  fprod1p  12391  fprodeq0  12409  zdvdsdc  12604  dvdslelemd  12635  oexpneg  12669  ltoddhalfle  12685  divalglemnqt  12712  divalglemex  12714  divalglemeuneg  12715  flodddiv4t2lthalf  12731  bitsfzolem  12746  bitsfzo  12747  bitsmod  12748  bitscmp  12750  dvdsbnd  12758  dvdslegcd  12766  gcd0id  12781  gcdneg  12784  bezoutlemsup  12811  dfgcd2  12816  uzwodc  12839  nn0seqcvgd  12844  lcmgcdlem  12880  ncoprmgcdne1b  12892  nprm  12926  prmdc  12933  prmdvdsfz  12943  isprm5lem  12945  coprm  12948  prmexpb  12955  prmfac1  12956  znege1  12983  sqrt2irrap  12985  hashdvds  13028  eulerthlemrprm  13036  eulerthlema  13037  hashgcdlem  13045  pythagtriplem13  13084  pythagtriplem16  13087  pcxcl  13119  pcaddlem  13147  pcadd  13148  pcfac  13158  qexpz  13160  4sqlem7  13192  4sqlem10  13195  4sqexercise2  13207  4sqlemsdc  13208  4sqlem11  13209  4sqlem12  13210  4sqlem15  13213  4sqlem16  13214  4sqlem17  13215  ballotfilemfc0  13290  ballotfilemfcc  13291  ballotfilemimin  13307  ballotfilemsgt1  13312  ballotfilemsel1i  13314  ballotfilemsi  13316  ballotfilemsima  13317  ballotfilemgun  13326  ballotfilemfrceq  13330  ballotfilemfrcn0  13331  ballotfilemirc  13333  oddennn  13341  ennnfoneleminc  13360  nninfdclemp1  13399  nninfdclemlt  13400  gzsumfzval  13770  gzsumcl  13863  mulgfng  13986  subgmulg  14050  gzsumreidx  14231  gzsumsubmcl  14232  gzsummhm  14235  gzsumsplit0  14238  gzsumshift  14239  psrbaglefifi  15172  ltexp2  16177  logblt  16198  ppiqfi  16242  chtdif  16264  ppidif  16269  ppiqub  16293  chtqub  16296  mersenne  16297  bcmono  16304  bcmax  16305  prmefexple  16308  bposlem1  16311  bposlem3  16313  bposlem4  16314  bposlem5  16315  bposlem6  16316  lgsval2lem  16334  lgsvalmod  16343  lgsneg  16348  lgsdilem  16351  lgssq  16364  lgssq2  16365  gausslemma2dlem1a  16382  gausslemma2dlem3  16387  lgseisenlem2  16395  lgsquadlem1  16401  lgsquadlem2  16402  lgsquadlem3  16403  lgsquad3  16408  2lgslem1a2  16411  2sqlem3  16441  2sqlem8  16447  supfz  17328  inffz  17329