Theorem zred 9721

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 9604	. 2 ⊢ ℤ ⊆ ℝ
2		zred.1	. 2 ⊢ (𝜑 → 𝐴 ∈ ℤ)
3	1, 2	sselid 3240	1 ⊢ (𝜑 → 𝐴 ∈ ℝ)

Syntax hints:   → wi 4   ∈ wcel 2205  ℝcr 8142  ℤcz 9597

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 2216

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 2221  df-cleq 2227  df-clel 2230  df-nfc 2375  df-rex 2528  df-rab 2531  df-v 2817  df-un 3218  df-in 3220  df-ss 3227  df-sn 3700  df-pr 3701  df-op 3703  df-uni 3920  df-br 4115  df-iota 5317  df-fv 5365  df-ov 6061  df-neg 8464  df-z 9598

This theorem is referenced by:  zcnd  9722  btwnapz  9729  eluzmn  9881  eluzelre  9885  eluzadd  9904  eluzsub  9905  uzm1  9906  ltesubnnd  10123  z2ge  10181  zltaddlt1le  10363  fztri3or  10396  fznlem  10398  fzdisj  10409  fzpreddisj  10430  fznatpl1  10435  uzdisj  10452  fzm1  10459  fz0fzdiffz0  10489  elfzmlbm  10490  elfzmlbp  10491  difelfznle  10494  nn0disj  10497  elfzolt3  10517  fzonel  10520  fzouzdisj  10541  fzodisjsn  10543  fzonmapblen  10551  fzoaddel  10557  elincfzoext  10563  elfzonelfzo  10600  zsupcl  10616  zssinfcl  10617  infssuzex  10618  suprzubdc  10623  zsupssdc  10625  suprzcl2dc  10626  qtri3or  10627  exbtwnzlemstep  10634  exbtwnzlemex  10636  exbtwnz  10637  rebtwn2zlemstep  10639  rebtwn2z  10641  qbtwnrelemcalc  10642  qbtwnre  10643  apbtwnz  10661  qfraclt1  10667  qfracge0  10668  flqge  10669  flid  10671  flqltnz  10674  flqwordi  10675  flqaddz  10684  flqmulnn0  10686  btwnzge0  10687  2tnp1ge0ge0  10688  flhalf  10689  flltdivnn0lt  10691  fldiv4p1lem1div2  10692  fldiv4lem1div2uz2  10693  ceiqge  10698  ceiqm1l  10700  ceiqle  10702  flqleceil  10706  flqeqceilz  10707  intfracq  10709  modqval  10713  modqge0  10721  modqlt  10722  modqmulnn  10731  mulp1mod1  10754  modaddmodup  10776  modaddmodlo  10777  modsumfzodifsn  10785  addmodlteq  10787  frec2uzlt2d  10793  frec2uzf1od  10795  uzennn  10825  seq3split  10877  iseqf1olemkle  10886  iseqf1olemqcl  10888  iseqf1olemnab  10890  iseqf1olemab  10891  iseqf1olemqk  10896  seq3f1olemqsumkj  10900  seq3f1olemqsumk  10901  seq3f1olemqsum  10902  seqf1oglem1  10908  seqf1oglem2  10909  seqfeq4g  10920  exp3val  10930  expcanlem  11105  expcan  11106  facavg  11136  bcval4  11142  bcp1nk  11152  bcval5  11153  bcm1n  11159  zfz1isolemiso  11239  seq3coll  11242  iswrdiz  11259  ccatrn  11325  ccatalpha  11329  seq3shft  11551  resqrexlemdecn  11726  fzomaxdiflem  11826  nn0maxcl  11939  fsum3cvg3  12111  fsumm1  12131  fsum1p  12133  fsum0diaglem  12155  isumshft  12205  isumsplit  12206  divcnv  12212  geolim2  12227  cvgratnnlemabsle  12242  cvgratnnlemsumlt  12243  cvgratnnlemrate  12245  cvgratz  12247  mertenslemi1  12250  fprodntrivap  12299  prodsnf  12307  fprod1p  12314  fprodeq0  12332  zdvdsdc  12527  dvdslelemd  12558  oexpneg  12592  ltoddhalfle  12608  divalglemnqt  12635  divalglemex  12637  divalglemeuneg  12638  flodddiv4t2lthalf  12654  bitsfzolem  12669  bitsfzo  12670  bitsmod  12671  bitscmp  12673  dvdsbnd  12681  dvdslegcd  12689  gcd0id  12704  gcdneg  12707  bezoutlemsup  12734  dfgcd2  12739  uzwodc  12762  nn0seqcvgd  12767  lcmgcdlem  12803  ncoprmgcdne1b  12815  nprm  12849  prmdc  12856  prmdvdsfz  12865  isprm5lem  12867  coprm  12870  prmexpb  12877  prmfac1  12878  znege1  12904  sqrt2irrap  12906  hashdvds  12947  eulerthlemrprm  12955  eulerthlema  12956  hashgcdlem  12964  pythagtriplem13  13003  pythagtriplem16  13006  pcxcl  13038  pcaddlem  13066  pcadd  13067  pcfac  13077  qexpz  13079  4sqlem7  13111  4sqlem10  13114  4sqexercise2  13126  4sqlemsdc  13127  4sqlem11  13128  4sqlem12  13129  4sqlem15  13132  4sqlem16  13133  4sqlem17  13134  ballotfilemfc0  13180  ballotfilemfcc  13181  ballotfilemimin  13197  ballotfilemsgt1  13202  ballotfilemsel1i  13204  ballotfilemsi  13206  ballotfilemsima  13207  ballotfilemgun  13216  ballotfilemfrceq  13220  ballotfilemfrcn0  13221  ballotfilemirc  13223  oddennn  13231  ennnfoneleminc  13250  nninfdclemp1  13289  nninfdclemlt  13290  gsumfzval  13658  gsumfzz  13754  gsumfzcl  13758  mulgfng  13881  subgmulg  13945  gsumfzreidx  14094  gsumfzsubmcl  14095  gsumfzmptfidmadd  14096  gsumfzmhm  14100  gsumsplit0  14103  gsumshift  14109  gsumfzfsumlemm  14865  gsumfzfsum  14866  ltexp2  15936  logblt  15957  mersenne  15995  lgsval2lem  16013  lgsvalmod  16022  lgsneg  16027  lgsdilem  16030  lgssq  16043  lgssq2  16044  gausslemma2dlem1a  16061  gausslemma2dlem3  16066  lgseisenlem2  16074  lgsquadlem1  16080  lgsquadlem2  16081  lgsquadlem3  16082  lgsquad3  16087  2lgslem1a2  16090  2sqlem3  16120  2sqlem8  16126  supfz  16996  inffz  16997