Theorem zred 9699

Description: An integer is a real number. (Contributed by Mario Carneiro, 28-May-2016.)

Hypothesis

Ref	Expression
zred.1	⊢ (𝜑 → 𝐴 ∈ ℤ)

Assertion

Ref	Expression
zred	⊢ (𝜑 → 𝐴 ∈ ℝ)

Proof of Theorem zred

Step	Hyp	Ref	Expression
1		zssre 9583	. 2 ⊢ ℤ ⊆ ℝ
2		zred.1	. 2 ⊢ (𝜑 → 𝐴 ∈ ℤ)
3	1, 2	sselid 3235	1 ⊢ (𝜑 → 𝐴 ∈ ℝ)

Syntax hints:   → wi 4   ∈ wcel 2203  ℝcr 8125  ℤcz 9576

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 2214

This theorem depends on definitions:  df-bi 117  df-3or 1006  df-3an 1007  df-tru 1401  df-nf 1510  df-sb 1812  df-clab 2219  df-cleq 2225  df-clel 2228  df-nfc 2373  df-rex 2526  df-rab 2529  df-v 2814  df-un 3214  df-in 3216  df-ss 3223  df-sn 3694  df-pr 3695  df-op 3697  df-uni 3914  df-br 4109  df-iota 5311  df-fv 5359  df-ov 6052  df-neg 8446  df-z 9577

This theorem is referenced by:  zcnd  9700  btwnapz  9707  eluzmn  9859  eluzelre  9863  eluzadd  9882  eluzsub  9883  uzm1  9884  z2ge  10158  zltaddlt1le  10340  fztri3or  10372  fznlem  10374  fzdisj  10385  fzpreddisj  10404  fznatpl1  10409  uzdisj  10426  fzm1  10433  fz0fzdiffz0  10463  elfzmlbm  10464  elfzmlbp  10465  difelfznle  10468  nn0disj  10471  elfzolt3  10491  fzonel  10494  fzouzdisj  10515  fzodisjsn  10517  fzonmapblen  10525  fzoaddel  10531  elincfzoext  10537  elfzonelfzo  10574  zsupcl  10590  zssinfcl  10591  infssuzex  10592  suprzubdc  10595  zsupssdc  10597  suprzcl2dc  10598  qtri3or  10599  exbtwnzlemstep  10606  exbtwnzlemex  10608  exbtwnz  10609  rebtwn2zlemstep  10611  rebtwn2z  10613  qbtwnrelemcalc  10614  qbtwnre  10615  apbtwnz  10633  qfraclt1  10639  qfracge0  10640  flqge  10641  flid  10643  flqltnz  10646  flqwordi  10647  flqaddz  10656  flqmulnn0  10658  btwnzge0  10659  2tnp1ge0ge0  10660  flhalf  10661  flltdivnn0lt  10663  fldiv4p1lem1div2  10664  fldiv4lem1div2uz2  10665  ceiqge  10670  ceiqm1l  10672  ceiqle  10674  flqleceil  10678  flqeqceilz  10679  intfracq  10681  modqval  10685  modqge0  10693  modqlt  10694  modqmulnn  10703  mulp1mod1  10726  modaddmodup  10748  modaddmodlo  10749  modsumfzodifsn  10757  addmodlteq  10759  frec2uzlt2d  10765  frec2uzf1od  10767  uzennn  10797  seq3split  10849  iseqf1olemkle  10858  iseqf1olemqcl  10860  iseqf1olemnab  10862  iseqf1olemab  10863  iseqf1olemqk  10868  seq3f1olemqsumkj  10872  seq3f1olemqsumk  10873  seq3f1olemqsum  10874  seqf1oglem1  10880  seqf1oglem2  10881  seqfeq4g  10892  exp3val  10902  expcanlem  11076  expcan  11077  facavg  11107  bcval4  11113  bcp1nk  11123  bcval5  11124  zfz1isolemiso  11207  seq3coll  11210  iswrdiz  11227  ccatrn  11293  ccatalpha  11297  seq3shft  11519  resqrexlemdecn  11693  fzomaxdiflem  11793  nn0maxcl  11906  fsum3cvg3  12078  fsumm1  12098  fsum1p  12100  fsum0diaglem  12122  isumshft  12172  isumsplit  12173  divcnv  12179  geolim2  12194  cvgratnnlemabsle  12209  cvgratnnlemsumlt  12210  cvgratnnlemrate  12212  cvgratz  12214  mertenslemi1  12217  fprodntrivap  12266  prodsnf  12274  fprod1p  12281  fprodeq0  12299  zdvdsdc  12494  dvdslelemd  12525  oexpneg  12559  ltoddhalfle  12575  divalglemnqt  12602  divalglemex  12604  divalglemeuneg  12605  flodddiv4t2lthalf  12621  bitsfzolem  12636  bitsfzo  12637  bitsmod  12638  bitscmp  12640  dvdsbnd  12648  dvdslegcd  12656  gcd0id  12671  gcdneg  12674  bezoutlemsup  12701  dfgcd2  12706  uzwodc  12729  nn0seqcvgd  12734  lcmgcdlem  12770  ncoprmgcdne1b  12782  nprm  12816  prmdc  12823  prmdvdsfz  12832  isprm5lem  12834  coprm  12837  prmexpb  12844  prmfac1  12845  znege1  12871  sqrt2irrap  12873  hashdvds  12914  eulerthlemrprm  12922  eulerthlema  12923  hashgcdlem  12931  pythagtriplem13  12970  pythagtriplem16  12973  pcxcl  13005  pcaddlem  13033  pcadd  13034  pcfac  13044  qexpz  13046  4sqlem7  13078  4sqlem10  13081  4sqexercise2  13093  4sqlemsdc  13094  4sqlem11  13095  4sqlem12  13096  4sqlem15  13099  4sqlem16  13100  4sqlem17  13101  oddennn  13135  ennnfoneleminc  13154  nninfdclemp1  13193  nninfdclemlt  13194  gsumfzval  13596  gsumfzz  13700  gsumfzcl  13704  mulgfng  13833  subgmulg  13897  gsumfzreidx  14046  gsumfzsubmcl  14047  gsumfzmptfidmadd  14048  gsumfzmhm  14052  gsumsplit0  14055  gsumfzfsumlemm  14727  gsumfzfsum  14728  ltexp2  15798  logblt  15819  mersenne  15857  lgsval2lem  15875  lgsvalmod  15884  lgsneg  15889  lgsdilem  15892  lgssq  15905  lgssq2  15906  gausslemma2dlem1a  15923  gausslemma2dlem3  15928  lgseisenlem2  15936  lgsquadlem1  15942  lgsquadlem2  15943  lgsquadlem3  15944  lgsquad3  15949  2lgslem1a2  15952  2sqlem3  15982  2sqlem8  15988  supfz  16848  inffz  16849  gsumgfsumlem  16856