Theorem zred 9773

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

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2209  ℝcr 8179  ℤcz 9649

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-io 721  ax-5 1500  ax-7 1501  ax-gen 1502  ax-ie1 1546  ax-ie2 1547  ax-8 1557  ax-10 1558  ax-11 1559  ax-i12 1560  ax-bndl 1562  ax-4 1563  ax-17 1579  ax-i9 1583  ax-ial 1587  ax-i5r 1588  ax-ext 2220

This proof depends on definitions:  df-bi 117  df-3or 1010  df-3an 1011  df-tru 1405  df-nf 1514  df-sb 1816  df-clab 2225  df-cleq 2231  df-clel 2234  df-nfc 2381  df-rex 2534  df-rab 2537  df-v 2823  df-un 3224  df-in 3226  df-ss 3233  df-sn 3715  df-pr 3716  df-op 3718  df-uni 3936  df-br 4131  df-iota 5337  df-fv 5385  df-ov 6088  df-neg 8502  df-z 9650

This theorem is used by:  zcnd  9774  btwnapz  9781  eluzmn  9938  eluzelre  9942  eluzadd  9961  eluzsub  9962  uzm1  9963  ltesubnnd  10181  z2ge  10239  zltaddlt1le  10421  fztri3or  10454  fznlem  10456  fzdisj  10468  fzpreddisj  10489  fznatpl1  10494  uzdisj  10511  fzm1  10518  fz0fzdiffz0  10548  elfzmlbm  10549  elfzmlbp  10550  difelfznle  10553  nn0disj  10556  elfzolt3  10576  fzonel  10579  fzouzdisj  10600  fzodisjsn  10602  fzonmapblen  10610  fzoaddel  10616  elincfzoext  10622  elfzonelfzo  10659  zsupcl  10675  zssinfcl  10676  infssuzex  10677  suprzubdc  10682  zsupssdc  10684  suprzcl2dc  10685  qtri3or  10686  exbtwnzlemstep  10693  exbtwnzlemex  10695  exbtwnz  10696  rebtwn2zlemstep  10698  rebtwn2z  10700  qbtwnrelemcalc  10701  qbtwnre  10702  apbtwnz  10720  qfraclt1  10728  qfracge0  10729  flqge  10730  flapge  10731  flid  10733  flqltnz  10736  flqwordi  10737  flqaddz  10746  flqmulnn0  10748  btwnzge0  10749  2tnp1ge0ge0  10750  flhalf  10751  flltdivnn0lt  10753  fldiv4p1lem1div2  10754  fldiv4lem1div2uz2  10755  ceiqge  10760  ceiqm1l  10762  ceiqle  10764  flqleceil  10768  flqeqceilz  10769  intfracq  10771  modqval  10775  modqge0  10783  modqlt  10784  modqmulnn  10793  mulp1mod1  10816  modaddmodup  10838  modaddmodlo  10839  modsumfzodifsn  10847  addmodlteq  10849  frec2uzlt2d  10855  frec2uzf1od  10857  uzennn  10887  seq3split  10939  iseqf1olemkle  10948  iseqf1olemqcl  10950  iseqf1olemnab  10952  iseqf1olemab  10953  iseqf1olemqk  10958  seq3f1olemqsumkj  10962  seq3f1olemqsumk  10963  seq3f1olemqsum  10964  seqf1oglem1  10970  seqf1oglem2  10971  seqfeq4g  10982  exp3val  10992  expcanlem  11168  expcan  11169  facavg  11199  bcval4  11205  bcp1nk  11215  bcval5  11216  bcm1n  11222  zfz1isolemiso  11306  seq3coll  11309  iswrdiz  11326  ccatrn  11392  ccatalpha  11396  seq3shft  11618  resqrexlemdecn  11793  fzomaxdiflem  11894  nn0maxcl  12007  fiidxsupcl  12011  fsum3cvg3  12181  fsumm1  12201  fsum1p  12203  fsum0diaglem  12225  isumshft  12275  isumsplit  12276  divcnv  12282  geolim2  12297  cvgratnnlemabsle  12312  cvgratnnlemsumlt  12313  cvgratnnlemrate  12315  cvgratz  12317  mertenslemi1  12320  fprodntrivap  12369  prodsnf  12377  fprod1p  12384  fprodeq0  12402  zdvdsdc  12597  dvdslelemd  12628  oexpneg  12662  ltoddhalfle  12678  divalglemnqt  12705  divalglemex  12707  divalglemeuneg  12708  flodddiv4t2lthalf  12724  bitsfzolem  12739  bitsfzo  12740  bitsmod  12741  bitscmp  12743  dvdsbnd  12751  dvdslegcd  12759  gcd0id  12774  gcdneg  12777  bezoutlemsup  12804  dfgcd2  12809  uzwodc  12832  nn0seqcvgd  12837  lcmgcdlem  12873  ncoprmgcdne1b  12885  nprm  12919  prmdc  12926  prmdvdsfz  12936  isprm5lem  12938  coprm  12941  prmexpb  12948  prmfac1  12949  znege1  12976  sqrt2irrap  12978  hashdvds  13021  eulerthlemrprm  13029  eulerthlema  13030  hashgcdlem  13038  pythagtriplem13  13077  pythagtriplem16  13080  pcxcl  13112  pcaddlem  13140  pcadd  13141  pcfac  13151  qexpz  13153  4sqlem7  13185  4sqlem10  13188  4sqexercise2  13200  4sqlemsdc  13201  4sqlem11  13202  4sqlem12  13203  4sqlem15  13206  4sqlem16  13207  4sqlem17  13208  ballotfilemfc0  13283  ballotfilemfcc  13284  ballotfilemimin  13300  ballotfilemsgt1  13305  ballotfilemsel1i  13307  ballotfilemsi  13309  ballotfilemsima  13310  ballotfilemgun  13319  ballotfilemfrceq  13323  ballotfilemfrcn0  13324  ballotfilemirc  13326  oddennn  13334  ennnfoneleminc  13353  nninfdclemp1  13392  nninfdclemlt  13393  gzsumfzval  13762  gzsumcl  13855  mulgfng  13978  subgmulg  14042  gzsumreidx  14192  gzsumsubmcl  14193  gzsummhm  14196  gzsumsplit0  14199  gzsumshift  14200  psrbaglefifi  15114  ltexp2  16099  logblt  16120  ppiqfi  16164  chtdif  16186  ppidif  16191  ppiqub  16215  chtqub  16218  mersenne  16219  bcmono  16226  bcmax  16227  prmefexple  16230  bposlem1  16233  bposlem3  16235  bposlem4  16236  bposlem5  16237  lgsval2lem  16251  lgsvalmod  16260  lgsneg  16265  lgsdilem  16268  lgssq  16281  lgssq2  16282  gausslemma2dlem1a  16299  gausslemma2dlem3  16304  lgseisenlem2  16312  lgsquadlem1  16318  lgsquadlem2  16319  lgsquadlem3  16320  lgsquad3  16325  2lgslem1a2  16328  2sqlem3  16358  2sqlem8  16364  supfz  17243  inffz  17244