Theorem zred 9770

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

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

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 8500  df-z 9647

This theorem is used by:  zcnd  9771  btwnapz  9778  eluzmn  9930  eluzelre  9934  eluzadd  9953  eluzsub  9954  uzm1  9955  ltesubnnd  10172  z2ge  10230  zltaddlt1le  10412  fztri3or  10445  fznlem  10447  fzdisj  10459  fzpreddisj  10480  fznatpl1  10485  uzdisj  10502  fzm1  10509  fz0fzdiffz0  10539  elfzmlbm  10540  elfzmlbp  10541  difelfznle  10544  nn0disj  10547  elfzolt3  10567  fzonel  10570  fzouzdisj  10591  fzodisjsn  10593  fzonmapblen  10601  fzoaddel  10607  elincfzoext  10613  elfzonelfzo  10650  zsupcl  10666  zssinfcl  10667  infssuzex  10668  suprzubdc  10673  zsupssdc  10675  suprzcl2dc  10676  qtri3or  10677  exbtwnzlemstep  10684  exbtwnzlemex  10686  exbtwnz  10687  rebtwn2zlemstep  10689  rebtwn2z  10691  qbtwnrelemcalc  10692  qbtwnre  10693  apbtwnz  10711  qfraclt1  10717  qfracge0  10718  flqge  10719  flid  10721  flqltnz  10724  flqwordi  10725  flqaddz  10734  flqmulnn0  10736  btwnzge0  10737  2tnp1ge0ge0  10738  flhalf  10739  flltdivnn0lt  10741  fldiv4p1lem1div2  10742  fldiv4lem1div2uz2  10743  ceiqge  10748  ceiqm1l  10750  ceiqle  10752  flqleceil  10756  flqeqceilz  10757  intfracq  10759  modqval  10763  modqge0  10771  modqlt  10772  modqmulnn  10781  mulp1mod1  10804  modaddmodup  10826  modaddmodlo  10827  modsumfzodifsn  10835  addmodlteq  10837  frec2uzlt2d  10843  frec2uzf1od  10845  uzennn  10875  seq3split  10927  iseqf1olemkle  10936  iseqf1olemqcl  10938  iseqf1olemnab  10940  iseqf1olemab  10941  iseqf1olemqk  10946  seq3f1olemqsumkj  10950  seq3f1olemqsumk  10951  seq3f1olemqsum  10952  seqf1oglem1  10958  seqf1oglem2  10959  seqfeq4g  10970  exp3val  10980  expcanlem  11155  expcan  11156  facavg  11186  bcval4  11192  bcp1nk  11202  bcval5  11203  bcm1n  11209  zfz1isolemiso  11293  seq3coll  11296  iswrdiz  11313  ccatrn  11379  ccatalpha  11383  seq3shft  11605  resqrexlemdecn  11780  fzomaxdiflem  11880  nn0maxcl  11993  fsum3cvg3  12165  fsumm1  12185  fsum1p  12187  fsum0diaglem  12209  isumshft  12259  isumsplit  12260  divcnv  12266  geolim2  12281  cvgratnnlemabsle  12296  cvgratnnlemsumlt  12297  cvgratnnlemrate  12299  cvgratz  12301  mertenslemi1  12304  fprodntrivap  12353  prodsnf  12361  fprod1p  12368  fprodeq0  12386  zdvdsdc  12581  dvdslelemd  12612  oexpneg  12646  ltoddhalfle  12662  divalglemnqt  12689  divalglemex  12691  divalglemeuneg  12692  flodddiv4t2lthalf  12708  bitsfzolem  12723  bitsfzo  12724  bitsmod  12725  bitscmp  12727  dvdsbnd  12735  dvdslegcd  12743  gcd0id  12758  gcdneg  12761  bezoutlemsup  12788  dfgcd2  12793  uzwodc  12816  nn0seqcvgd  12821  lcmgcdlem  12857  ncoprmgcdne1b  12869  nprm  12903  prmdc  12910  prmdvdsfz  12919  isprm5lem  12921  coprm  12924  prmexpb  12931  prmfac1  12932  znege1  12958  sqrt2irrap  12960  hashdvds  13001  eulerthlemrprm  13009  eulerthlema  13010  hashgcdlem  13018  pythagtriplem13  13057  pythagtriplem16  13060  pcxcl  13092  pcaddlem  13120  pcadd  13121  pcfac  13131  qexpz  13133  4sqlem7  13165  4sqlem10  13168  4sqexercise2  13180  4sqlemsdc  13181  4sqlem11  13182  4sqlem12  13183  4sqlem15  13186  4sqlem16  13187  4sqlem17  13188  ballotfilemfc0  13234  ballotfilemfcc  13235  ballotfilemimin  13251  ballotfilemsgt1  13256  ballotfilemsel1i  13258  ballotfilemsi  13260  ballotfilemsima  13261  ballotfilemgun  13270  ballotfilemfrceq  13274  ballotfilemfrcn0  13275  ballotfilemirc  13277  oddennn  13285  ennnfoneleminc  13304  nninfdclemp1  13343  nninfdclemlt  13344  gzsumfzval  13713  gzsumcl  13806  mulgfng  13929  subgmulg  13993  gzsumreidx  14143  gzsumsubmcl  14144  gzsummhm  14147  gzsumsplit0  14150  gzsumshift  14151  ltexp2  16049  logblt  16070  mersenne  16117  bcmono  16124  bcmax  16125  lgsval2lem  16141  lgsvalmod  16150  lgsneg  16155  lgsdilem  16158  lgssq  16171  lgssq2  16172  gausslemma2dlem1a  16189  gausslemma2dlem3  16194  lgseisenlem2  16202  lgsquadlem1  16208  lgsquadlem2  16209  lgsquadlem3  16210  lgsquad3  16215  2lgslem1a2  16218  2sqlem3  16248  2sqlem8  16254  supfz  17133  inffz  17134