Theorem zred 9663

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

Syntax hints:   -> wi 4   e. wcel 2202   RRcr 8091   ZZcz 9540

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 2213

This theorem depends on definitions:  df-bi 117  df-3or 1006  df-3an 1007  df-tru 1401  df-nf 1510  df-sb 1811  df-clab 2218  df-cleq 2224  df-clel 2227  df-nfc 2364  df-rex 2517  df-rab 2520  df-v 2805  df-un 3205  df-in 3207  df-ss 3214  df-sn 3679  df-pr 3680  df-op 3682  df-uni 3899  df-br 4094  df-iota 5293  df-fv 5341  df-ov 6031  df-neg 8412  df-z 9541

This theorem is referenced by:  zcnd  9664  btwnapz  9671  eluzmn  9823  eluzelre  9827  eluzadd  9846  eluzsub  9847  uzm1  9848  z2ge  10122  zltaddlt1le  10304  fztri3or  10336  fznlem  10338  fzdisj  10349  fzpreddisj  10368  fznatpl1  10373  uzdisj  10390  fzm1  10397  fz0fzdiffz0  10427  elfzmlbm  10428  elfzmlbp  10429  difelfznle  10432  nn0disj  10435  elfzolt3  10455  fzonel  10458  fzouzdisj  10479  fzodisjsn  10481  fzonmapblen  10489  fzoaddel  10495  elincfzoext  10501  elfzonelfzo  10538  zsupcl  10554  zssinfcl  10555  infssuzex  10556  suprzubdc  10559  zsupssdc  10561  suprzcl2dc  10562  qtri3or  10563  exbtwnzlemstep  10570  exbtwnzlemex  10572  exbtwnz  10573  rebtwn2zlemstep  10575  rebtwn2z  10577  qbtwnrelemcalc  10578  qbtwnre  10579  apbtwnz  10597  qfraclt1  10603  qfracge0  10604  flqge  10605  flid  10607  flqltnz  10610  flqwordi  10611  flqaddz  10620  flqmulnn0  10622  btwnzge0  10623  2tnp1ge0ge0  10624  flhalf  10625  flltdivnn0lt  10627  fldiv4p1lem1div2  10628  fldiv4lem1div2uz2  10629  ceiqge  10634  ceiqm1l  10636  ceiqle  10638  flqleceil  10642  flqeqceilz  10643  intfracq  10645  modqval  10649  modqge0  10657  modqlt  10658  modqmulnn  10667  mulp1mod1  10690  modaddmodup  10712  modaddmodlo  10713  modsumfzodifsn  10721  addmodlteq  10723  frec2uzlt2d  10729  frec2uzf1od  10731  uzennn  10761  seq3split  10813  iseqf1olemkle  10822  iseqf1olemqcl  10824  iseqf1olemnab  10826  iseqf1olemab  10827  iseqf1olemqk  10832  seq3f1olemqsumkj  10836  seq3f1olemqsumk  10837  seq3f1olemqsum  10838  seqf1oglem1  10844  seqf1oglem2  10845  seqfeq4g  10856  exp3val  10866  expcanlem  11040  expcan  11041  facavg  11071  bcval4  11077  bcp1nk  11087  bcval5  11088  zfz1isolemiso  11166  seq3coll  11169  iswrdiz  11186  ccatrn  11252  ccatalpha  11256  seq3shft  11478  resqrexlemdecn  11652  fzomaxdiflem  11752  nn0maxcl  11865  fsum3cvg3  12037  fsumm1  12057  fsum1p  12059  fsum0diaglem  12081  isumshft  12131  isumsplit  12132  divcnv  12138  geolim2  12153  cvgratnnlemabsle  12168  cvgratnnlemsumlt  12169  cvgratnnlemrate  12171  cvgratz  12173  mertenslemi1  12176  fprodntrivap  12225  prodsnf  12233  fprod1p  12240  fprodeq0  12258  zdvdsdc  12453  dvdslelemd  12484  oexpneg  12518  ltoddhalfle  12534  divalglemnqt  12561  divalglemex  12563  divalglemeuneg  12564  flodddiv4t2lthalf  12580  bitsfzolem  12595  bitsfzo  12596  bitsmod  12597  bitscmp  12599  dvdsbnd  12607  dvdslegcd  12615  gcd0id  12630  gcdneg  12633  bezoutlemsup  12660  dfgcd2  12665  uzwodc  12688  nn0seqcvgd  12693  lcmgcdlem  12729  ncoprmgcdne1b  12741  nprm  12775  prmdc  12782  prmdvdsfz  12791  isprm5lem  12793  coprm  12796  prmexpb  12803  prmfac1  12804  znege1  12830  sqrt2irrap  12832  hashdvds  12873  eulerthlemrprm  12881  eulerthlema  12882  hashgcdlem  12890  pythagtriplem13  12929  pythagtriplem16  12932  pcxcl  12964  pcaddlem  12992  pcadd  12993  pcfac  13003  qexpz  13005  4sqlem7  13037  4sqlem10  13040  4sqexercise2  13052  4sqlemsdc  13053  4sqlem11  13054  4sqlem12  13055  4sqlem15  13058  4sqlem16  13059  4sqlem17  13060  oddennn  13093  ennnfoneleminc  13112  nninfdclemp1  13151  nninfdclemlt  13152  gsumfzval  13554  gsumfzz  13658  gsumfzcl  13662  mulgfng  13791  subgmulg  13855  gsumfzreidx  14004  gsumfzsubmcl  14005  gsumfzmptfidmadd  14006  gsumfzmhm  14010  gsumsplit0  14013  gsumfzfsumlemm  14683  gsumfzfsum  14684  ltexp2  15752  logblt  15773  mersenne  15811  lgsval2lem  15829  lgsvalmod  15838  lgsneg  15843  lgsdilem  15846  lgssq  15859  lgssq2  15860  gausslemma2dlem1a  15877  gausslemma2dlem3  15882  lgseisenlem2  15890  lgsquadlem1  15896  lgsquadlem2  15897  lgsquadlem3  15898  lgsquad3  15903  2lgslem1a2  15906  2sqlem3  15936  2sqlem8  15942  supfz  16804  inffz  16805  gsumgfsumlem  16812