Theorem zred 12161

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

Syntax hints:   → wi 4   ∈ wcel 2113  ℝcr 10607  ℤcz 12055

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1916  ax-6 1974  ax-7 2019  ax-8 2115  ax-9 2123  ax-10 2144  ax-11 2161  ax-12 2178  ax-ext 2710

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 847  df-3or 1089  df-3an 1090  df-tru 1545  df-ex 1787  df-nf 1791  df-sb 2074  df-clab 2717  df-cleq 2730  df-clel 2811  df-nfc 2881  df-rab 3062  df-v 3399  df-un 3846  df-in 3848  df-ss 3858  df-sn 4514  df-pr 4516  df-op 4520  df-uni 4794  df-br 5028  df-iota 6291  df-fv 6341  df-ov 7167  df-neg 10944  df-z 12056

This theorem is referenced by:  zcnd  12162  suprfinzcl  12171  eluzmn  12324  eluzelre  12328  subeluzsub  12350  uzm1  12351  zsupss  12412  suprzcl2  12413  uzwo3  12418  rpnnen1lem3  12454  rpnnen1lem5  12456  zltaddlt1le  12972  fzsplit2  13016  fzdisj  13018  ssfzunsnext  13036  fzpreddisj  13040  fznatpl1  13045  fzp1disj  13050  uzdisj  13064  fzm1  13071  fz0fzdiffz0  13100  elfzmlbm  13101  elfzmlbp  13102  difelfznle  13105  nn0disj  13107  elfzolt3  13132  fzonel  13135  fzospliti  13153  fzodisj  13155  fzouzdisj  13157  fzodisjsn  13159  fzonmapblen  13167  fzoaddel  13174  elincfzoext  13179  reflcl  13250  flge  13259  flwordi  13266  fladdz  13279  2tnp1ge0ge0  13283  flhalf  13284  fldiv4p1lem1div2  13289  fldiv4lem1div2uz2  13290  fldiv4lem1div2  13291  flleceil  13305  fleqceilz  13306  quoremz  13307  uzsup  13315  modmul12d  13377  modaddmodup  13386  modaddmodlo  13387  modfzo0difsn  13395  modsumfzodifsn  13396  addmodlteq  13398  om2uzlti  13402  om2uzf1oi  13405  seqf1olem1  13494  seqf1olem2  13495  bcval4  13752  bcp1nk  13762  bcval5  13763  fzsdom2  13874  seqcoll  13909  seqcoll2  13910  ccatrn  14025  ccatalpha  14029  cshwidxmodr  14248  fzomaxdiflem  14785  fzomaxdif  14786  rexuzre  14795  limsupgre  14921  rlimclim1  14985  isercoll  15110  iseralt  15127  fsumm1  15192  fsum1p  15194  fsum0diaglem  15217  modfsummods  15234  isumsplit  15281  climcndslem1  15290  mertenslem1  15325  ntrivcvgmul  15343  fprodntriv  15381  fprod1p  15407  fprodeq0  15414  fallfacval4  15482  bpoly4  15498  fzo0dvdseq  15761  dvdsmod  15767  oexpneg  15783  mod2eq1n2dvds  15785  ltoddhalfle  15799  flodddiv4t2lthalf  15854  bitsp1  15867  bitsfzolem  15870  bitsfzo  15871  bitsmod  15872  bitscmp  15874  bitsinv1lem  15877  sadaddlem  15902  bitsres  15909  bitsuz  15910  smumul  15929  gcd0id  15955  gcdneg  15958  dfgcd2  15983  nn0seqcvgd  16004  lcmgcdlem  16040  nprm  16122  prmdvdsfz  16139  isprm5  16141  isprm7  16142  coprm  16145  prmexpb  16154  prmfac1  16155  hashdvds  16205  crth  16208  eulerthlem2  16212  fermltl  16214  prmdiv  16215  prmdiveq  16216  hashgcdlem  16218  odzdvds  16225  vfermltlALT  16232  modprm0  16235  modprmn0modprm0  16237  prm23ge5  16245  pythagtriplem13  16257  pcxcl  16290  pcaddlem  16317  pcadd  16318  pcfac  16328  qexpz  16330  prmunb  16343  1arithlem4  16355  4sqlem5  16371  4sqlem6  16372  4sqlem7  16373  4sqlem10  16376  4sqlem11  16384  4sqlem12  16385  4sqlem15  16388  4sqlem16  16389  4sqlem17  16390  vdwnnlem3  16426  prmgaplem7  16486  cshwshashlem3  16527  subgmulg  18404  mndodconglem  18780  odnncl  18784  odmod  18785  oddvds  18786  dfod2  18802  sylow1lem3  18836  efgsp1  18974  efgredleme  18980  telgsumfzs  19221  zringlpirlem1  20296  zringlpirlem3  20298  znf1o  20363  zcld  23558  ovoliunlem1  24247  ovoliunlem2  24248  dyadss  24339  dyaddisjlem  24340  dyadmaxlem  24342  dvfsumle  24765  dvfsumge  24766  dvfsumabs  24767  dvfsumlem1  24770  dvfsumlem3  24772  degltlem1  24817  plyco0  24933  plyeq0lem  24951  plydivex  25037  aannenlem1  25068  efif1olem2  25279  nnlogbexp  25511  logblt  25514  ang180lem1  25539  ang180lem3  25541  wilthlem2  25798  basellem3  25812  basellem4  25813  ppiprm  25880  chtdif  25887  ppidif  25892  chtub  25940  mersenne  25955  bcmono  26005  bcmax  26006  bposlem1  26012  bposlem3  26014  bposlem5  26016  bposlem6  26017  lgsval2lem  26035  lgsvalmod  26044  lgsneg  26049  lgsmod  26051  lgsdilem  26052  lgsdirprm  26059  lgsdilem2  26061  lgsne0  26063  lgssq  26065  lgssq2  26066  lgsqr  26079  lgsdchr  26083  gausslemma2dlem1a  26093  gausslemma2dlem3  26096  gausslemma2dlem5a  26098  gausslemma2dlem6  26100  gausslemma2d  26102  lgseisenlem1  26103  lgseisenlem2  26104  lgseisenlem3  26105  lgseisenlem4  26106  lgsquadlem1  26108  lgsquadlem2  26109  lgsquadlem3  26110  lgsquad3  26115  2lgslem1a2  26118  2lgslem1  26122  2lgslem2  26123  2sqlem3  26148  2sqlem8  26154  2sqblem  26159  2sqmod  26164  chebbnd1lem1  26197  chebbnd1lem2  26198  chebbnd1lem3  26199  dchrmusum2  26222  dchrvmasumlem1  26223  dchrvmasum2lem  26224  dchrvmasum2if  26225  dchrvmasumlem3  26227  dchrvmasumiflem2  26230  dchrisum0lem1  26244  dchrmusumlem  26250  mudivsum  26258  mulogsumlem  26259  mulogsum  26260  mulog2sumlem2  26263  mulog2sumlem3  26264  selberglem1  26273  selberglem2  26274  pntpbnd1  26314  pntlemg  26326  pntlemf  26333  qabvle  26353  padicabv  26358  padicabvcxp  26360  ostth2lem2  26362  axlowdimlem13  26892  axlowdimlem16  26895  pthdlem1  27699  crctcshwlkn0  27751  crctcsh  27754  clwwisshclwwslemlem  27942  eucrctshift  28172  nndiffz1  30674  fzsplit3  30682  bcm1n  30683  fzone1  30688  ltesubnnd  30703  wrdt2ind  30792  cshwrnid  30800  cycpmfv2  30950  cycpmco2lem6  30967  cycpmco2lem7  30968  cycpmrn  30979  cyc3conja  30993  pnfinf  31006  znfermltl  31126  dya2iocress  31803  dya2iocbrsiga  31804  dya2icobrsiga  31805  dya2icoseg  31806  dya2iocucvr  31813  sxbrsigalem2  31815  ballotlemfc0  32021  ballotlemfcc  32022  ballotlemodife  32026  ballotlemimin  32034  ballotlemsgt1  32039  ballotlemsel1i  32041  ballotlemsi  32043  ballotlemsima  32044  ballotlemrv2  32050  ballotlemfrceq  32057  ballotlemfrcn0  32058  ballotlemirc  32060  fsum2dsub  32149  reprlt  32161  reprgt  32163  breprexplemc  32174  tgoldbachgnn  32201  tgoldbachgt  32205  subfacval3  32714  erdszelem8  32723  erdszelem9  32724  supfz  33257  inffz  33258  dnizeq0  34285  dnizphlfeqhlf  34286  dnibndlem13  34300  knoppndvlem1  34322  knoppndvlem2  34323  knoppndvlem7  34328  knoppndvlem19  34340  knoppndvlem21  34342  ltflcei  35377  leceifl  35378  poimirlem1  35390  poimirlem2  35391  poimirlem6  35395  poimirlem7  35396  poimirlem8  35397  poimirlem15  35404  poimirlem16  35405  poimirlem17  35406  poimirlem19  35408  poimirlem20  35409  poimirlem23  35412  poimirlem24  35413  poimirlem27  35416  poimirlem29  35418  poimirlem31  35420  poimirlem32  35421  mblfinlem2  35427  itg2addnclem2  35441  mettrifi  35527  cntotbnd  35566  fzne2d  39598  aks4d1p1p3  39685  aks4d1p1p2  39686  aks4d1p1p4  39687  aks4d1p1  39692  2ap1caineq  39696  sticksstones6  39702  sticksstones7  39703  metakunt7  39711  metakunt12  39716  metakunt15  39719  metakunt16  39720  metakunt22  39726  metakunt28  39732  prodsplit  39741  frlmvscadiccat  39803  dffltz  40027  lzunuz  40146  lzenom  40148  diophin  40150  irrapxlem1  40200  irrapxlem2  40201  irrapxlem3  40202  irrapxlem4  40203  pellexlem5  40211  pellexlem6  40212  rmspecfund  40287  rmxypos  40325  ltrmynn0  40326  ltrmxnn0  40327  ltrmy  40330  rmyeq0  40331  rmyeq  40332  lermy  40333  rmyabs  40336  jm2.24nn  40337  jm2.17a  40338  jm2.17b  40339  jm2.17c  40340  jm2.24  40341  rmygeid  40342  acongrep  40358  fzmaxdif  40359  acongeq  40361  jm2.22  40373  jm2.23  40374  jm2.26lem3  40379  jm2.27a  40383  jm3.1lem1  40395  jm3.1lem3  40397  expdiophlem1  40399  prmunb2  41451  nzprmdif  41459  hashnzfzclim  41462  binomcxplemnn0  41489  uzwo4  42123  ssinc  42159  ssdec  42160  zltlesub  42345  monoords  42358  fzisoeu  42361  fperiodmul  42365  fzdifsuc2  42371  iuneqfzuzlem  42395  uzublem  42492  zxrd  42517  uzinico  42622  uzubioo  42629  fmul01  42647  fmul01lt1lem1  42651  fmul01lt1lem2  42652  climsuselem1  42674  climsuse  42675  sumnnodd  42697  ltmod  42705  limsupresuz  42770  limsupubuzlem  42779  limsupequzlem  42789  limsupmnfuzlem  42793  limsupequzmptlem  42795  limsupre3uzlem  42802  supcnvlimsup  42807  limsup10exlem  42839  liminfresuz  42851  liminfvaluz  42859  limsupvaluz3  42865  ioodvbdlimc1lem2  42999  ioodvbdlimc2lem  43001  dvnmul  43010  dvnprodlem1  43013  dvnprodlem2  43014  iblspltprt  43040  itgspltprt  43046  stoweidlem3  43070  stoweidlem11  43078  stoweidlem20  43087  stoweidlem26  43093  stoweidlem34  43101  stoweidlem59  43126  stirlinglem5  43145  dirkertrigeqlem3  43167  dirkeritg  43169  dirkercncflem1  43170  dirkercncflem2  43171  dirkercncflem4  43173  fourierdlem4  43178  fourierdlem6  43180  fourierdlem7  43181  fourierdlem11  43185  fourierdlem12  43186  fourierdlem15  43189  fourierdlem19  43193  fourierdlem20  43194  fourierdlem25  43199  fourierdlem26  43200  fourierdlem34  43208  fourierdlem35  43209  fourierdlem41  43215  fourierdlem48  43221  fourierdlem49  43222  fourierdlem50  43223  fourierdlem51  43224  fourierdlem54  43227  fourierdlem63  43236  fourierdlem64  43237  fourierdlem65  43238  fourierdlem71  43244  fourierdlem79  43252  fourierdlem89  43262  fourierdlem90  43263  fourierdlem91  43264  fourierdlem102  43275  fourierdlem103  43276  fourierdlem104  43277  fourierdlem114  43287  fouriersw  43298  elaa2lem  43300  etransclem3  43304  etransclem4  43305  etransclem7  43308  etransclem10  43311  etransclem15  43316  etransclem19  43320  etransclem23  43324  etransclem24  43325  etransclem25  43326  etransclem27  43328  etransclem31  43332  etransclem32  43333  etransclem35  43336  etransclem41  43342  etransclem44  43345  etransclem46  43347  etransclem48  43349  iundjiun  43524  caratheodorylem1  43590  smflimsuplem4  43879  smfliminflem  43886  2elfz2melfz  44328  elfzelfzlble  44331  fzopredsuc  44333  fsummsndifre  44342  iccpartgt  44397  icceuelpartlem  44405  icceuelpart  44406  iccpartnel  44408  lighneallem2  44576  proththd  44584  dfodd4  44629  oexpnegALTV  44647  nnoALTV  44665  evenltle  44687  fpprwppr  44709  gbowgt5  44732  gboge9  44734  stgoldbwt  44746  sbgoldbst  44748  sbgoldbalt  44751  sgoldbeven3prm  44753  mogoldbb  44755  bgoldbtbndlem1  44775  bgoldbtbndlem2  44776  bgoldbtbndlem3  44777  bgoldbtbnd  44779  bgoldbachlt  44783  tgblthelfgott  44785  tgoldbach  44787  pw2m1lepw2m1  45379  m1modmmod  45385  difmodm1lt  45386  fllogbd  45424  logbpw2m1  45431  fllog2  45432  nnpw2blen  45444  nnolog2flm1  45454  dignn0flhalflem1  45479  dignn0flhalflem2  45480