Theorem zred 9375

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

Syntax hints:   -> wi 4   e. wcel 2148   RRcr 7810   ZZcz 9253

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 2740  df-un 3134  df-in 3136  df-ss 3143  df-sn 3599  df-pr 3600  df-op 3602  df-uni 3811  df-br 4005  df-iota 5179  df-fv 5225  df-ov 5878  df-neg 8131  df-z 9254

This theorem is referenced by:  zcnd  9376  btwnapz  9383  eluzelre  9538  eluzadd  9556  eluzsub  9557  uzm1  9558  z2ge  9826  zltaddlt1le  10007  fztri3or  10039  fznlem  10041  fzdisj  10052  fzpreddisj  10071  fznatpl1  10076  uzdisj  10093  fzm1  10100  fz0fzdiffz0  10130  elfzmlbm  10131  elfzmlbp  10132  difelfznle  10135  nn0disj  10138  elfzolt3  10157  fzonel  10160  fzouzdisj  10180  fzonmapblen  10187  fzoaddel  10192  elfzonelfzo  10230  qtri3or  10243  exbtwnzlemstep  10248  exbtwnzlemex  10250  exbtwnz  10251  rebtwn2zlemstep  10253  rebtwn2z  10255  qbtwnrelemcalc  10256  qbtwnre  10257  apbtwnz  10274  qfraclt1  10280  qfracge0  10281  flqge  10282  flid  10284  flqltnz  10287  flqwordi  10288  flqaddz  10297  flqmulnn0  10299  btwnzge0  10300  2tnp1ge0ge0  10301  flhalf  10302  flltdivnn0lt  10304  fldiv4p1lem1div2  10305  ceiqge  10309  ceiqm1l  10311  ceiqle  10313  flqleceil  10317  flqeqceilz  10318  intfracq  10320  modqval  10324  modqge0  10332  modqlt  10333  modqmulnn  10342  mulp1mod1  10365  modaddmodup  10387  modaddmodlo  10388  modsumfzodifsn  10396  addmodlteq  10398  frec2uzlt2d  10404  frec2uzf1od  10406  uzennn  10436  seq3split  10479  iseqf1olemkle  10484  iseqf1olemqcl  10486  iseqf1olemnab  10488  iseqf1olemab  10489  iseqf1olemqk  10494  seq3f1olemqsumkj  10498  seq3f1olemqsumk  10499  seq3f1olemqsum  10500  exp3val  10522  expcanlem  10695  expcan  10696  facavg  10726  bcval4  10732  bcp1nk  10742  bcval5  10743  zfz1isolemiso  10819  seq3coll  10822  seq3shft  10847  resqrexlemdecn  11021  fzomaxdiflem  11121  fsum3cvg3  11404  fsumm1  11424  fsum1p  11426  fsum0diaglem  11448  isumshft  11498  isumsplit  11499  divcnv  11505  geolim2  11520  cvgratnnlemabsle  11535  cvgratnnlemsumlt  11536  cvgratnnlemrate  11538  cvgratz  11540  mertenslemi1  11543  fprodntrivap  11592  prodsnf  11600  fprod1p  11607  fprodeq0  11625  zdvdsdc  11819  dvdslelemd  11849  oexpneg  11882  ltoddhalfle  11898  divalglemnqt  11925  divalglemex  11927  divalglemeuneg  11928  flodddiv4t2lthalf  11942  zsupcl  11948  zssinfcl  11949  infssuzex  11950  suprzubdc  11953  zsupssdc  11955  suprzcl2dc  11956  dvdsbnd  11957  dvdslegcd  11965  gcd0id  11980  gcdneg  11983  bezoutlemsup  12010  dfgcd2  12015  uzwodc  12038  nn0seqcvgd  12041  lcmgcdlem  12077  ncoprmgcdne1b  12089  nprm  12123  prmdc  12130  prmdvdsfz  12139  isprm5lem  12141  coprm  12144  prmexpb  12151  prmfac1  12152  znege1  12178  sqrt2irrap  12180  hashdvds  12221  eulerthlemrprm  12229  eulerthlema  12230  hashgcdlem  12238  pythagtriplem13  12276  pythagtriplem16  12279  pcxcl  12311  pcaddlem  12338  pcadd  12339  pcfac  12348  qexpz  12350  4sqlem7  12382  4sqlem10  12385  oddennn  12393  ennnfoneleminc  12412  nninfdclemp1  12451  nninfdclemlt  12452  mulgfng  12987  subgmulg  13048  ltexp2  14363  logblt  14383  lgsval2lem  14414  lgsvalmod  14423  lgsneg  14428  lgsdilem  14431  lgssq  14444  lgssq2  14445  lgseisenlem2  14454  2sqlem3  14467  2sqlem8  14473  supfz  14821  inffz  14822