Theorem zred 8469

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 8358	. 2 |- ZZ C_ RR
2		zred.1	. 2 |- ( ph -> A e. ZZ )
3	1, 2	sseldi 2997	1 |- ( ph -> A e. RR )

Syntax hints:   -> wi 4   e. wcel 1433   RRcr 6980   ZZcz 8351

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-io 662  ax-5 1376  ax-7 1377  ax-gen 1378  ax-ie1 1422  ax-ie2 1423  ax-8 1435  ax-10 1436  ax-11 1437  ax-i12 1438  ax-bndl 1439  ax-4 1440  ax-17 1459  ax-i9 1463  ax-ial 1467  ax-i5r 1468  ax-ext 2063

This theorem depends on definitions:  df-bi 115  df-3or 920  df-3an 921  df-tru 1287  df-nf 1390  df-sb 1686  df-clab 2068  df-cleq 2074  df-clel 2077  df-nfc 2208  df-rex 2354  df-rab 2357  df-v 2603  df-un 2977  df-in 2979  df-ss 2986  df-sn 3404  df-pr 3405  df-op 3407  df-uni 3602  df-br 3786  df-iota 4887  df-fv 4930  df-ov 5535  df-neg 7282  df-z 8352

This theorem is referenced by:  zcnd  8470  eluzelre  8629  eluzadd  8647  eluzsub  8648  uzm1  8649  z2ge  8893  zltaddlt1le  9028  fztri3or  9058  fznlem  9060  fzdisj  9071  fzpreddisj  9088  fznatpl1  9093  uzdisj  9110  fzm1  9117  fz0fzdiffz0  9141  elfzmlbm  9142  elfzmlbp  9143  difelfznle  9146  nn0disj  9148  elfzolt3  9166  fzonel  9169  fzouzdisj  9189  fzonmapblen  9196  fzoaddel  9201  elfzonelfzo  9239  qtri3or  9252  qbtwnzlemstep  9257  qbtwnzlemex  9259  qbtwnz  9260  rebtwn2zlemstep  9261  rebtwn2z  9263  qbtwnrelemcalc  9264  qbtwnre  9265  qfraclt1  9282  qfracge0  9283  flqge  9284  flid  9286  flqltnz  9289  flqwordi  9290  flqaddz  9299  flqmulnn0  9301  btwnzge0  9302  2tnp1ge0ge0  9303  flhalf  9304  flltdivnn0lt  9306  fldiv4p1lem1div2  9307  ceiqge  9311  ceiqm1l  9313  ceiqle  9315  flqleceil  9319  flqeqceilz  9320  intfracq  9322  modqval  9326  modqge0  9334  modqlt  9335  modqmulnn  9344  mulp1mod1  9367  modaddmodup  9389  modaddmodlo  9390  modsumfzodifsn  9398  addmodlteq  9400  frec2uzlt2d  9406  frec2uzf1od  9408  expival  9478  expcanlem  9643  expcan  9644  facavg  9673  bcval4  9679  bcp1nk  9689  ibcval5  9690  resqrexlemdecn  9898  fzomaxdiflem  9998  zdvdsdc  10216  dvdslelemd  10243  oexpneg  10276  ltoddhalfle  10293  divalglemnqt  10320  divalglemex  10322  divalglemeuneg  10323  flodddiv4t2lthalf  10337  zsupcl  10343  zssinfcl  10344  infssuzex  10345  dvdsbnd  10348  dvdslegcd  10356  gcd0id  10370  gcdneg  10373  bezoutlemsup  10398  dfgcd2  10403  nn0seqcvgd  10423  lcmgcdlem  10459  ncoprmgcdne1b  10471  nprm  10505  prmdvdsfz  10520  coprm  10523  prmexpb  10530  prmfac1  10531  znege1  10556  sqrt2irrap  10558