Theorem zred 9718

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

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

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 8463  df-z 9595

This theorem is referenced by:  zcnd  9719  btwnapz  9726  eluzmn  9878  eluzelre  9882  eluzadd  9901  eluzsub  9902  uzm1  9903  ltesubnnd  10120  z2ge  10178  zltaddlt1le  10360  fztri3or  10393  fznlem  10395  fzdisj  10406  fzpreddisj  10427  fznatpl1  10432  uzdisj  10449  fzm1  10456  fz0fzdiffz0  10486  elfzmlbm  10487  elfzmlbp  10488  difelfznle  10491  nn0disj  10494  elfzolt3  10514  fzonel  10517  fzouzdisj  10538  fzodisjsn  10540  fzonmapblen  10548  fzoaddel  10554  elincfzoext  10560  elfzonelfzo  10597  zsupcl  10613  zssinfcl  10614  infssuzex  10615  suprzubdc  10620  zsupssdc  10622  suprzcl2dc  10623  qtri3or  10624  exbtwnzlemstep  10631  exbtwnzlemex  10633  exbtwnz  10634  rebtwn2zlemstep  10636  rebtwn2z  10638  qbtwnrelemcalc  10639  qbtwnre  10640  apbtwnz  10658  qfraclt1  10664  qfracge0  10665  flqge  10666  flid  10668  flqltnz  10671  flqwordi  10672  flqaddz  10681  flqmulnn0  10683  btwnzge0  10684  2tnp1ge0ge0  10685  flhalf  10686  flltdivnn0lt  10688  fldiv4p1lem1div2  10689  fldiv4lem1div2uz2  10690  ceiqge  10695  ceiqm1l  10697  ceiqle  10699  flqleceil  10703  flqeqceilz  10704  intfracq  10706  modqval  10710  modqge0  10718  modqlt  10719  modqmulnn  10728  mulp1mod1  10751  modaddmodup  10773  modaddmodlo  10774  modsumfzodifsn  10782  addmodlteq  10784  frec2uzlt2d  10790  frec2uzf1od  10792  uzennn  10822  seq3split  10874  iseqf1olemkle  10883  iseqf1olemqcl  10885  iseqf1olemnab  10887  iseqf1olemab  10888  iseqf1olemqk  10893  seq3f1olemqsumkj  10897  seq3f1olemqsumk  10898  seq3f1olemqsum  10899  seqf1oglem1  10905  seqf1oglem2  10906  seqfeq4g  10917  exp3val  10927  expcanlem  11102  expcan  11103  facavg  11133  bcval4  11139  bcp1nk  11149  bcval5  11150  bcm1n  11156  zfz1isolemiso  11236  seq3coll  11239  iswrdiz  11256  ccatrn  11322  ccatalpha  11326  seq3shft  11548  resqrexlemdecn  11722  fzomaxdiflem  11822  nn0maxcl  11935  fsum3cvg3  12107  fsumm1  12127  fsum1p  12129  fsum0diaglem  12151  isumshft  12201  isumsplit  12202  divcnv  12208  geolim2  12223  cvgratnnlemabsle  12238  cvgratnnlemsumlt  12239  cvgratnnlemrate  12241  cvgratz  12243  mertenslemi1  12246  fprodntrivap  12295  prodsnf  12303  fprod1p  12310  fprodeq0  12328  zdvdsdc  12523  dvdslelemd  12554  oexpneg  12588  ltoddhalfle  12604  divalglemnqt  12631  divalglemex  12633  divalglemeuneg  12634  flodddiv4t2lthalf  12650  bitsfzolem  12665  bitsfzo  12666  bitsmod  12667  bitscmp  12669  dvdsbnd  12677  dvdslegcd  12685  gcd0id  12700  gcdneg  12703  bezoutlemsup  12730  dfgcd2  12735  uzwodc  12758  nn0seqcvgd  12763  lcmgcdlem  12799  ncoprmgcdne1b  12811  nprm  12845  prmdc  12852  prmdvdsfz  12861  isprm5lem  12863  coprm  12866  prmexpb  12873  prmfac1  12874  znege1  12900  sqrt2irrap  12902  hashdvds  12943  eulerthlemrprm  12951  eulerthlema  12952  hashgcdlem  12960  pythagtriplem13  12999  pythagtriplem16  13002  pcxcl  13034  pcaddlem  13062  pcadd  13063  pcfac  13073  qexpz  13075  4sqlem7  13107  4sqlem10  13110  4sqexercise2  13122  4sqlemsdc  13123  4sqlem11  13124  4sqlem12  13125  4sqlem15  13128  4sqlem16  13129  4sqlem17  13130  ballotfilemfc0  13176  ballotfilemfcc  13177  ballotfilemimin  13193  ballotfilemsgt1  13198  ballotfilemsel1i  13200  ballotfilemsi  13202  ballotfilemsima  13203  ballotfilemgun  13212  ballotfilemfrceq  13216  ballotfilemfrcn0  13217  ballotfilemirc  13219  oddennn  13227  ennnfoneleminc  13246  nninfdclemp1  13285  nninfdclemlt  13286  gsumfzval  13688  gsumfzz  13792  gsumfzcl  13796  mulgfng  13925  subgmulg  13989  gsumfzreidx  14138  gsumfzsubmcl  14139  gsumfzmptfidmadd  14140  gsumfzmhm  14144  gsumsplit0  14147  gsumfzfsumlemm  14847  gsumfzfsum  14848  ltexp2  15918  logblt  15939  mersenne  15977  lgsval2lem  15995  lgsvalmod  16004  lgsneg  16009  lgsdilem  16012  lgssq  16025  lgssq2  16026  gausslemma2dlem1a  16043  gausslemma2dlem3  16048  lgseisenlem2  16056  lgsquadlem1  16062  lgsquadlem2  16063  lgsquadlem3  16064  lgsquad3  16069  2lgslem1a2  16072  2sqlem3  16102  2sqlem8  16108  supfz  16969  inffz  16970  gsumgfsumlem  16977