Theorem zred 9439

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

Syntax hints:   → wi 4   ∈ wcel 2164  ℝcr 7871  ℤcz 9317

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 710  ax-5 1458  ax-7 1459  ax-gen 1460  ax-ie1 1504  ax-ie2 1505  ax-8 1515  ax-10 1516  ax-11 1517  ax-i12 1518  ax-bndl 1520  ax-4 1521  ax-17 1537  ax-i9 1541  ax-ial 1545  ax-i5r 1546  ax-ext 2175

This theorem depends on definitions:  df-bi 117  df-3or 981  df-3an 982  df-tru 1367  df-nf 1472  df-sb 1774  df-clab 2180  df-cleq 2186  df-clel 2189  df-nfc 2325  df-rex 2478  df-rab 2481  df-v 2762  df-un 3157  df-in 3159  df-ss 3166  df-sn 3624  df-pr 3625  df-op 3627  df-uni 3836  df-br 4030  df-iota 5215  df-fv 5262  df-ov 5921  df-neg 8193  df-z 9318

This theorem is referenced by:  zcnd  9440  btwnapz  9447  eluzelre  9602  eluzadd  9621  eluzsub  9622  uzm1  9623  z2ge  9892  zltaddlt1le  10073  fztri3or  10105  fznlem  10107  fzdisj  10118  fzpreddisj  10137  fznatpl1  10142  uzdisj  10159  fzm1  10166  fz0fzdiffz0  10196  elfzmlbm  10197  elfzmlbp  10198  difelfznle  10201  nn0disj  10204  elfzolt3  10224  fzonel  10227  fzouzdisj  10247  fzonmapblen  10254  fzoaddel  10259  elfzonelfzo  10297  qtri3or  10310  exbtwnzlemstep  10316  exbtwnzlemex  10318  exbtwnz  10319  rebtwn2zlemstep  10321  rebtwn2z  10323  qbtwnrelemcalc  10324  qbtwnre  10325  apbtwnz  10343  qfraclt1  10349  qfracge0  10350  flqge  10351  flid  10353  flqltnz  10356  flqwordi  10357  flqaddz  10366  flqmulnn0  10368  btwnzge0  10369  2tnp1ge0ge0  10370  flhalf  10371  flltdivnn0lt  10373  fldiv4p1lem1div2  10374  fldiv4lem1div2uz2  10375  ceiqge  10380  ceiqm1l  10382  ceiqle  10384  flqleceil  10388  flqeqceilz  10389  intfracq  10391  modqval  10395  modqge0  10403  modqlt  10404  modqmulnn  10413  mulp1mod1  10436  modaddmodup  10458  modaddmodlo  10459  modsumfzodifsn  10467  addmodlteq  10469  frec2uzlt2d  10475  frec2uzf1od  10477  uzennn  10507  seq3split  10559  iseqf1olemkle  10568  iseqf1olemqcl  10570  iseqf1olemnab  10572  iseqf1olemab  10573  iseqf1olemqk  10578  seq3f1olemqsumkj  10582  seq3f1olemqsumk  10583  seq3f1olemqsum  10584  seqf1oglem1  10590  seqf1oglem2  10591  seqfeq4g  10602  exp3val  10612  expcanlem  10786  expcan  10787  facavg  10817  bcval4  10823  bcp1nk  10833  bcval5  10834  zfz1isolemiso  10910  seq3coll  10913  iswrdiz  10921  seq3shft  10982  resqrexlemdecn  11156  fzomaxdiflem  11256  fsum3cvg3  11539  fsumm1  11559  fsum1p  11561  fsum0diaglem  11583  isumshft  11633  isumsplit  11634  divcnv  11640  geolim2  11655  cvgratnnlemabsle  11670  cvgratnnlemsumlt  11671  cvgratnnlemrate  11673  cvgratz  11675  mertenslemi1  11678  fprodntrivap  11727  prodsnf  11735  fprod1p  11742  fprodeq0  11760  zdvdsdc  11955  dvdslelemd  11985  oexpneg  12018  ltoddhalfle  12034  divalglemnqt  12061  divalglemex  12063  divalglemeuneg  12064  flodddiv4t2lthalf  12078  zsupcl  12084  zssinfcl  12085  infssuzex  12086  suprzubdc  12089  zsupssdc  12091  suprzcl2dc  12092  dvdsbnd  12093  dvdslegcd  12101  gcd0id  12116  gcdneg  12119  bezoutlemsup  12146  dfgcd2  12151  uzwodc  12174  nn0seqcvgd  12179  lcmgcdlem  12215  ncoprmgcdne1b  12227  nprm  12261  prmdc  12268  prmdvdsfz  12277  isprm5lem  12279  coprm  12282  prmexpb  12289  prmfac1  12290  znege1  12316  sqrt2irrap  12318  hashdvds  12359  eulerthlemrprm  12367  eulerthlema  12368  hashgcdlem  12376  pythagtriplem13  12414  pythagtriplem16  12417  pcxcl  12449  pcaddlem  12477  pcadd  12478  pcfac  12488  qexpz  12490  4sqlem7  12522  4sqlem10  12525  4sqexercise2  12537  4sqlemsdc  12538  4sqlem11  12539  4sqlem12  12540  4sqlem15  12543  4sqlem16  12544  4sqlem17  12545  oddennn  12549  ennnfoneleminc  12568  nninfdclemp1  12607  nninfdclemlt  12608  gsumfzval  12974  gsumfzz  13067  gsumfzcl  13071  mulgfng  13194  subgmulg  13258  gsumfzreidx  13407  gsumfzsubmcl  13408  gsumfzmptfidmadd  13409  gsumfzmhm  13413  gsumfzfsumlemm  14075  gsumfzfsum  14076  ltexp2  15074  logblt  15094  lgsval2lem  15126  lgsvalmod  15135  lgsneg  15140  lgsdilem  15143  lgssq  15156  lgssq2  15157  gausslemma2dlem1a  15174  gausslemma2dlem3  15179  lgseisenlem2  15187  lgsquadlem1  15191  2sqlem3  15204  2sqlem8  15210  supfz  15561  inffz  15562