Theorem zred 9768

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 9651	. 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 8178   ZZcz 9644

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 4131  df-iota 5337  df-fv 5385  df-ov 6088  df-neg 8500  df-z 9645

This theorem is used by:  zcnd  9769  btwnapz  9776  eluzmn  9928  eluzelre  9932  eluzadd  9951  eluzsub  9952  uzm1  9953  ltesubnnd  10170  z2ge  10228  zltaddlt1le  10410  fztri3or  10443  fznlem  10445  fzdisj  10457  fzpreddisj  10478  fznatpl1  10483  uzdisj  10500  fzm1  10507  fz0fzdiffz0  10537  elfzmlbm  10538  elfzmlbp  10539  difelfznle  10542  nn0disj  10545  elfzolt3  10565  fzonel  10568  fzouzdisj  10589  fzodisjsn  10591  fzonmapblen  10599  fzoaddel  10605  elincfzoext  10611  elfzonelfzo  10648  zsupcl  10664  zssinfcl  10665  infssuzex  10666  suprzubdc  10671  zsupssdc  10673  suprzcl2dc  10674  qtri3or  10675  exbtwnzlemstep  10682  exbtwnzlemex  10684  exbtwnz  10685  rebtwn2zlemstep  10687  rebtwn2z  10689  qbtwnrelemcalc  10690  qbtwnre  10691  apbtwnz  10709  qfraclt1  10715  qfracge0  10716  flqge  10717  flid  10719  flqltnz  10722  flqwordi  10723  flqaddz  10732  flqmulnn0  10734  btwnzge0  10735  2tnp1ge0ge0  10736  flhalf  10737  flltdivnn0lt  10739  fldiv4p1lem1div2  10740  fldiv4lem1div2uz2  10741  ceiqge  10746  ceiqm1l  10748  ceiqle  10750  flqleceil  10754  flqeqceilz  10755  intfracq  10757  modqval  10761  modqge0  10769  modqlt  10770  modqmulnn  10779  mulp1mod1  10802  modaddmodup  10824  modaddmodlo  10825  modsumfzodifsn  10833  addmodlteq  10835  frec2uzlt2d  10841  frec2uzf1od  10843  uzennn  10873  seq3split  10925  iseqf1olemkle  10934  iseqf1olemqcl  10936  iseqf1olemnab  10938  iseqf1olemab  10939  iseqf1olemqk  10944  seq3f1olemqsumkj  10948  seq3f1olemqsumk  10949  seq3f1olemqsum  10950  seqf1oglem1  10956  seqf1oglem2  10957  seqfeq4g  10968  exp3val  10978  expcanlem  11153  expcan  11154  facavg  11184  bcval4  11190  bcp1nk  11200  bcval5  11201  bcm1n  11207  zfz1isolemiso  11291  seq3coll  11294  iswrdiz  11311  ccatrn  11377  ccatalpha  11381  seq3shft  11603  resqrexlemdecn  11778  fzomaxdiflem  11878  nn0maxcl  11991  fsum3cvg3  12163  fsumm1  12183  fsum1p  12185  fsum0diaglem  12207  isumshft  12257  isumsplit  12258  divcnv  12264  geolim2  12279  cvgratnnlemabsle  12294  cvgratnnlemsumlt  12295  cvgratnnlemrate  12297  cvgratz  12299  mertenslemi1  12302  fprodntrivap  12351  prodsnf  12359  fprod1p  12366  fprodeq0  12384  zdvdsdc  12579  dvdslelemd  12610  oexpneg  12644  ltoddhalfle  12660  divalglemnqt  12687  divalglemex  12689  divalglemeuneg  12690  flodddiv4t2lthalf  12706  bitsfzolem  12721  bitsfzo  12722  bitsmod  12723  bitscmp  12725  dvdsbnd  12733  dvdslegcd  12741  gcd0id  12756  gcdneg  12759  bezoutlemsup  12786  dfgcd2  12791  uzwodc  12814  nn0seqcvgd  12819  lcmgcdlem  12855  ncoprmgcdne1b  12867  nprm  12901  prmdc  12908  prmdvdsfz  12917  isprm5lem  12919  coprm  12922  prmexpb  12929  prmfac1  12930  znege1  12956  sqrt2irrap  12958  hashdvds  12999  eulerthlemrprm  13007  eulerthlema  13008  hashgcdlem  13016  pythagtriplem13  13055  pythagtriplem16  13058  pcxcl  13090  pcaddlem  13118  pcadd  13119  pcfac  13129  qexpz  13131  4sqlem7  13163  4sqlem10  13166  4sqexercise2  13178  4sqlemsdc  13179  4sqlem11  13180  4sqlem12  13181  4sqlem15  13184  4sqlem16  13185  4sqlem17  13186  ballotfilemfc0  13232  ballotfilemfcc  13233  ballotfilemimin  13249  ballotfilemsgt1  13254  ballotfilemsel1i  13256  ballotfilemsi  13258  ballotfilemsima  13259  ballotfilemgun  13268  ballotfilemfrceq  13272  ballotfilemfrcn0  13273  ballotfilemirc  13275  oddennn  13283  ennnfoneleminc  13302  nninfdclemp1  13341  nninfdclemlt  13342  gzsumfzval  13711  gzsumcl  13804  mulgfng  13927  subgmulg  13991  gzsumreidx  14141  gzsumsubmcl  14142  gzsummhm  14145  gzsumsplit0  14148  gzsumshift  14149  ltexp2  16043  logblt  16064  mersenne  16111  lgsval2lem  16129  lgsvalmod  16138  lgsneg  16143  lgsdilem  16146  lgssq  16159  lgssq2  16160  gausslemma2dlem1a  16177  gausslemma2dlem3  16182  lgseisenlem2  16190  lgsquadlem1  16196  lgsquadlem2  16197  lgsquadlem3  16198  lgsquad3  16203  2lgslem1a2  16206  2sqlem3  16236  2sqlem8  16242  supfz  17121  inffz  17122