Theorem zred 9374

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

Syntax hints:   -> wi 4   e. wcel 2148   RRcr 7809   ZZcz 9252

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 709  ax-5 1447  ax-7 1448  ax-gen 1449  ax-ie1 1493  ax-ie2 1494  ax-8 1504  ax-10 1505  ax-11 1506  ax-i12 1507  ax-bndl 1509  ax-4 1510  ax-17 1526  ax-i9 1530  ax-ial 1534  ax-i5r 1535  ax-ext 2159

This theorem depends on definitions:  df-bi 117  df-3or 979  df-3an 980  df-tru 1356  df-nf 1461  df-sb 1763  df-clab 2164  df-cleq 2170  df-clel 2173  df-nfc 2308  df-rex 2461  df-rab 2464  df-v 2739  df-un 3133  df-in 3135  df-ss 3142  df-sn 3598  df-pr 3599  df-op 3601  df-uni 3810  df-br 4004  df-iota 5178  df-fv 5224  df-ov 5877  df-neg 8130  df-z 9253

This theorem is referenced by:  zcnd  9375  btwnapz  9382  eluzelre  9537  eluzadd  9555  eluzsub  9556  uzm1  9557  z2ge  9825  zltaddlt1le  10006  fztri3or  10038  fznlem  10040  fzdisj  10051  fzpreddisj  10070  fznatpl1  10075  uzdisj  10092  fzm1  10099  fz0fzdiffz0  10129  elfzmlbm  10130  elfzmlbp  10131  difelfznle  10134  nn0disj  10137  elfzolt3  10156  fzonel  10159  fzouzdisj  10179  fzonmapblen  10186  fzoaddel  10191  elfzonelfzo  10229  qtri3or  10242  exbtwnzlemstep  10247  exbtwnzlemex  10249  exbtwnz  10250  rebtwn2zlemstep  10252  rebtwn2z  10254  qbtwnrelemcalc  10255  qbtwnre  10256  apbtwnz  10273  qfraclt1  10279  qfracge0  10280  flqge  10281  flid  10283  flqltnz  10286  flqwordi  10287  flqaddz  10296  flqmulnn0  10298  btwnzge0  10299  2tnp1ge0ge0  10300  flhalf  10301  flltdivnn0lt  10303  fldiv4p1lem1div2  10304  ceiqge  10308  ceiqm1l  10310  ceiqle  10312  flqleceil  10316  flqeqceilz  10317  intfracq  10319  modqval  10323  modqge0  10331  modqlt  10332  modqmulnn  10341  mulp1mod1  10364  modaddmodup  10386  modaddmodlo  10387  modsumfzodifsn  10395  addmodlteq  10397  frec2uzlt2d  10403  frec2uzf1od  10405  uzennn  10435  seq3split  10478  iseqf1olemkle  10483  iseqf1olemqcl  10485  iseqf1olemnab  10487  iseqf1olemab  10488  iseqf1olemqk  10493  seq3f1olemqsumkj  10497  seq3f1olemqsumk  10498  seq3f1olemqsum  10499  exp3val  10521  expcanlem  10694  expcan  10695  facavg  10725  bcval4  10731  bcp1nk  10741  bcval5  10742  zfz1isolemiso  10818  seq3coll  10821  seq3shft  10846  resqrexlemdecn  11020  fzomaxdiflem  11120  fsum3cvg3  11403  fsumm1  11423  fsum1p  11425  fsum0diaglem  11447  isumshft  11497  isumsplit  11498  divcnv  11504  geolim2  11519  cvgratnnlemabsle  11534  cvgratnnlemsumlt  11535  cvgratnnlemrate  11537  cvgratz  11539  mertenslemi1  11542  fprodntrivap  11591  prodsnf  11599  fprod1p  11606  fprodeq0  11624  zdvdsdc  11818  dvdslelemd  11848  oexpneg  11881  ltoddhalfle  11897  divalglemnqt  11924  divalglemex  11926  divalglemeuneg  11927  flodddiv4t2lthalf  11941  zsupcl  11947  zssinfcl  11948  infssuzex  11949  suprzubdc  11952  zsupssdc  11954  suprzcl2dc  11955  dvdsbnd  11956  dvdslegcd  11964  gcd0id  11979  gcdneg  11982  bezoutlemsup  12009  dfgcd2  12014  uzwodc  12037  nn0seqcvgd  12040  lcmgcdlem  12076  ncoprmgcdne1b  12088  nprm  12122  prmdc  12129  prmdvdsfz  12138  isprm5lem  12140  coprm  12143  prmexpb  12150  prmfac1  12151  znege1  12177  sqrt2irrap  12179  hashdvds  12220  eulerthlemrprm  12228  eulerthlema  12229  hashgcdlem  12237  pythagtriplem13  12275  pythagtriplem16  12278  pcxcl  12310  pcaddlem  12337  pcadd  12338  pcfac  12347  qexpz  12349  4sqlem7  12381  4sqlem10  12384  oddennn  12392  ennnfoneleminc  12411  nninfdclemp1  12450  nninfdclemlt  12451  mulgfng  12986  subgmulg  13046  ltexp2  14330  logblt  14350  lgsval2lem  14381  lgsvalmod  14390  lgsneg  14395  lgsdilem  14398  lgssq  14411  lgssq2  14412  lgseisenlem2  14421  2sqlem3  14434  2sqlem8  14440  supfz  14788  inffz  14789