Theorem zred 9780

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

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

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 4132  df-iota 5340  df-fv 5388  df-ov 6091  df-neg 8508  df-z 9657

This theorem is used by:  zcnd  9781  btwnapz  9788  eluzmn  9945  eluzelre  9949  eluzadd  9968  eluzsub  9969  uzm1  9970  ltesubnnd  10188  z2ge  10246  zltaddlt1le  10428  fztri3or  10461  fznlem  10463  fzdisj  10475  fzpreddisj  10496  fznatpl1  10501  uzdisj  10518  fzm1  10525  fz0fzdiffz0  10555  elfzmlbm  10556  elfzmlbp  10557  difelfznle  10560  nn0disj  10563  elfzolt3  10583  fzonel  10586  fzouzdisj  10607  fzodisjsn  10609  fzonmapblen  10617  fzoaddel  10623  elincfzoext  10629  elfzonelfzo  10666  zsupcl  10682  zssinfcl  10683  infssuzex  10684  suprzubdc  10689  zsupssdc  10691  suprzcl2dc  10692  qtri3or  10693  exbtwnzlemstep  10700  exbtwnzlemex  10702  exbtwnz  10703  rebtwn2zlemstep  10705  rebtwn2z  10707  qbtwnrelemcalc  10708  qbtwnre  10709  apbtwnz  10727  qfraclt1  10735  qfracge0  10736  flqge  10737  flapge  10738  flaplt  10740  flid  10741  flqltnz  10744  flqwordi  10745  flqaddz  10754  flqmulnn0  10756  btwnzge0  10757  2tnp1ge0ge0  10758  flhalf  10759  flltdivnn0lt  10761  fldiv4p1lem1div2  10762  fldiv4lem1div2uz2  10763  ceiqge  10768  ceiqm1l  10770  ceiqle  10772  flqleceil  10776  flqeqceilz  10777  intfracq  10779  modqval  10783  modqge0  10791  modqlt  10792  modqmulnn  10801  mulp1mod1  10824  modaddmodup  10846  modaddmodlo  10847  modsumfzodifsn  10855  addmodlteq  10857  frec2uzlt2d  10863  frec2uzf1od  10865  uzennn  10895  seq3split  10947  iseqf1olemkle  10956  iseqf1olemqcl  10958  iseqf1olemnab  10960  iseqf1olemab  10961  iseqf1olemqk  10966  seq3f1olemqsumkj  10970  seq3f1olemqsumk  10971  seq3f1olemqsum  10972  seqf1oglem1  10978  seqf1oglem2  10979  seqfeq4g  10990  exp3val  11000  expcanlem  11176  expcan  11177  facavg  11207  bcval4  11213  bcp1nk  11223  bcval5  11224  bcm1n  11230  zfz1isolemiso  11314  seq3coll  11317  iswrdiz  11334  ccatrn  11400  ccatalpha  11404  seq3shft  11626  resqrexlemdecn  11801  fzomaxdiflem  11902  nn0maxcl  12015  fiidxsupcl  12019  fsum3cvg3  12189  fsumm1  12209  fsum1p  12211  fsum0diaglem  12233  isumshft  12283  isumsplit  12284  divcnv  12290  geolim2  12305  cvgratnnlemabsle  12320  cvgratnnlemsumlt  12321  cvgratnnlemrate  12323  cvgratz  12325  mertenslemi1  12328  fprodntrivap  12377  prodsnf  12385  fprod1p  12392  fprodeq0  12410  zdvdsdc  12605  dvdslelemd  12636  oexpneg  12670  ltoddhalfle  12686  divalglemnqt  12713  divalglemex  12715  divalglemeuneg  12716  flodddiv4t2lthalf  12732  bitsfzolem  12747  bitsfzo  12748  bitsmod  12749  bitscmp  12751  dvdsbnd  12759  dvdslegcd  12767  gcd0id  12782  gcdneg  12785  bezoutlemsup  12812  dfgcd2  12817  uzwodc  12840  nn0seqcvgd  12845  lcmgcdlem  12881  ncoprmgcdne1b  12893  nprm  12927  prmdc  12934  prmdvdsfz  12944  isprm5lem  12946  coprm  12949  prmexpb  12956  prmfac1  12957  znege1  12984  sqrt2irrap  12986  hashdvds  13029  eulerthlemrprm  13037  eulerthlema  13038  hashgcdlem  13046  pythagtriplem13  13085  pythagtriplem16  13088  pcxcl  13120  pcaddlem  13148  pcadd  13149  pcfac  13159  qexpz  13161  4sqlem7  13193  4sqlem10  13196  4sqexercise2  13208  4sqlemsdc  13209  4sqlem11  13210  4sqlem12  13211  4sqlem15  13214  4sqlem16  13215  4sqlem17  13216  ballotfilemfc0  13291  ballotfilemfcc  13292  ballotfilemimin  13308  ballotfilemsgt1  13313  ballotfilemsel1i  13315  ballotfilemsi  13317  ballotfilemsima  13318  ballotfilemgun  13327  ballotfilemfrceq  13331  ballotfilemfrcn0  13332  ballotfilemirc  13334  oddennn  13342  ennnfoneleminc  13361  nninfdclemp1  13400  nninfdclemlt  13401  gzsumfzval  13771  gzsumcl  13864  mulgfng  13987  subgmulg  14051  gzsumreidx  14232  gzsumsubmcl  14233  gzsummhm  14236  gzsumsplit0  14239  gzsumshift  14240  psrbaglefifi  15177  ltexp2  16189  logblt  16210  ppiqfi  16254  chtdif  16276  ppidif  16281  ppiqub  16305  chtqub  16308  mersenne  16309  bcmono  16316  bcmax  16317  prmefexple  16320  bposlem1  16323  bposlem3  16325  bposlem4  16326  bposlem5  16327  bposlem6  16328  lgsval2lem  16346  lgsvalmod  16355  lgsneg  16360  lgsdilem  16363  lgssq  16376  lgssq2  16377  gausslemma2dlem1a  16394  gausslemma2dlem3  16399  lgseisenlem2  16407  lgsquadlem1  16413  lgsquadlem2  16414  lgsquadlem3  16415  lgsquad3  16420  2lgslem1a2  16423  2sqlem3  16453  2sqlem8  16459  supfz  17340  inffz  17341