Theorem zred 12075

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

Syntax hints:   → wi 4   ∈ wcel 2111  ℝcr 10525  ℤcz 11969

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-10 2142  ax-11 2158  ax-12 2175  ax-ext 2770

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3or 1085  df-3an 1086  df-tru 1541  df-ex 1782  df-nf 1786  df-sb 2070  df-clab 2777  df-cleq 2791  df-clel 2870  df-nfc 2938  df-rab 3115  df-v 3443  df-un 3886  df-in 3888  df-ss 3898  df-sn 4526  df-pr 4528  df-op 4532  df-uni 4801  df-br 5031  df-iota 6283  df-fv 6332  df-ov 7138  df-neg 10862  df-z 11970

This theorem is referenced by:  zcnd  12076  suprfinzcl  12085  eluzmn  12238  eluzelre  12242  subeluzsub  12263  uzm1  12264  zsupss  12325  suprzcl2  12326  uzwo3  12331  rpnnen1lem3  12366  rpnnen1lem5  12368  zltaddlt1le  12883  fzsplit2  12927  fzdisj  12929  ssfzunsnext  12947  fzpreddisj  12951  fznatpl1  12956  fzp1disj  12961  uzdisj  12975  fzm1  12982  fz0fzdiffz0  13011  elfzmlbm  13012  elfzmlbp  13013  difelfznle  13016  nn0disj  13018  elfzolt3  13043  fzonel  13046  fzospliti  13064  fzodisj  13066  fzouzdisj  13068  fzodisjsn  13070  fzonmapblen  13078  fzoaddel  13085  elincfzoext  13090  reflcl  13161  flge  13170  flwordi  13177  fladdz  13190  2tnp1ge0ge0  13194  flhalf  13195  fldiv4p1lem1div2  13200  fldiv4lem1div2uz2  13201  fldiv4lem1div2  13202  flleceil  13216  fleqceilz  13217  quoremz  13218  uzsup  13226  modmul12d  13288  modaddmodup  13297  modaddmodlo  13298  modfzo0difsn  13306  modsumfzodifsn  13307  addmodlteq  13309  om2uzlti  13313  om2uzf1oi  13316  seqf1olem1  13405  seqf1olem2  13406  bcval4  13663  bcp1nk  13673  bcval5  13674  fzsdom2  13785  seqcoll  13818  seqcoll2  13819  ccatrn  13934  ccatalpha  13938  cshwidxmodr  14157  fzomaxdiflem  14694  fzomaxdif  14695  rexuzre  14704  limsupgre  14830  rlimclim1  14894  isercoll  15016  iseralt  15033  fsumm1  15098  fsum1p  15100  fsum0diaglem  15123  modfsummods  15140  isumsplit  15187  climcndslem1  15196  mertenslem1  15232  ntrivcvgmul  15250  fprodntriv  15288  fprod1p  15314  fprodeq0  15321  fallfacval4  15389  bpoly4  15405  fzo0dvdseq  15665  dvdsmod  15670  oexpneg  15686  mod2eq1n2dvds  15688  ltoddhalfle  15702  flodddiv4t2lthalf  15757  bitsp1  15770  bitsfzolem  15773  bitsfzo  15774  bitsmod  15775  bitscmp  15777  bitsinv1lem  15780  sadaddlem  15805  bitsres  15812  bitsuz  15813  smumul  15832  gcd0id  15857  gcdneg  15860  dfgcd2  15884  nn0seqcvgd  15904  lcmgcdlem  15940  nprm  16022  prmdvdsfz  16039  isprm5  16041  isprm7  16042  coprm  16045  prmexpb  16052  prmfac1  16053  hashdvds  16102  crth  16105  eulerthlem2  16109  fermltl  16111  prmdiv  16112  prmdiveq  16113  hashgcdlem  16115  odzdvds  16122  vfermltlALT  16129  modprm0  16132  modprmn0modprm0  16134  prm23ge5  16142  pythagtriplem13  16154  pcxcl  16187  pcaddlem  16214  pcadd  16215  pcfac  16225  qexpz  16227  prmunb  16240  1arithlem4  16252  4sqlem5  16268  4sqlem6  16269  4sqlem7  16270  4sqlem10  16273  4sqlem11  16281  4sqlem12  16282  4sqlem15  16285  4sqlem16  16286  4sqlem17  16287  vdwnnlem3  16323  prmgaplem7  16383  cshwshashlem3  16423  subgmulg  18285  mndodconglem  18661  odnncl  18665  odmod  18666  oddvds  18667  dfod2  18683  sylow1lem3  18717  efgsp1  18855  efgredleme  18861  telgsumfzs  19102  zringlpirlem1  20177  zringlpirlem3  20179  znf1o  20243  zcld  23418  ovoliunlem1  24106  ovoliunlem2  24107  dyadss  24198  dyaddisjlem  24199  dyadmaxlem  24201  dvfsumle  24624  dvfsumge  24625  dvfsumabs  24626  dvfsumlem1  24629  dvfsumlem3  24631  degltlem1  24673  plyco0  24789  plyeq0lem  24807  plydivex  24893  aannenlem1  24924  efif1olem2  25135  nnlogbexp  25367  logblt  25370  ang180lem1  25395  ang180lem3  25397  wilthlem2  25654  basellem3  25668  basellem4  25669  ppiprm  25736  chtdif  25743  ppidif  25748  chtub  25796  mersenne  25811  bcmono  25861  bcmax  25862  bposlem1  25868  bposlem3  25870  bposlem5  25872  bposlem6  25873  lgsval2lem  25891  lgsvalmod  25900  lgsneg  25905  lgsmod  25907  lgsdilem  25908  lgsdirprm  25915  lgsdilem2  25917  lgsne0  25919  lgssq  25921  lgssq2  25922  lgsqr  25935  lgsdchr  25939  gausslemma2dlem1a  25949  gausslemma2dlem3  25952  gausslemma2dlem5a  25954  gausslemma2dlem6  25956  gausslemma2d  25958  lgseisenlem1  25959  lgseisenlem2  25960  lgseisenlem3  25961  lgseisenlem4  25962  lgsquadlem1  25964  lgsquadlem2  25965  lgsquadlem3  25966  lgsquad3  25971  2lgslem1a2  25974  2lgslem1  25978  2lgslem2  25979  2sqlem3  26004  2sqlem8  26010  2sqblem  26015  2sqmod  26020  chebbnd1lem1  26053  chebbnd1lem2  26054  chebbnd1lem3  26055  dchrmusum2  26078  dchrvmasumlem1  26079  dchrvmasum2lem  26080  dchrvmasum2if  26081  dchrvmasumlem3  26083  dchrvmasumiflem2  26086  dchrisum0lem1  26100  dchrmusumlem  26106  mudivsum  26114  mulogsumlem  26115  mulogsum  26116  mulog2sumlem2  26119  mulog2sumlem3  26120  selberglem1  26129  selberglem2  26130  pntpbnd1  26170  pntlemg  26182  pntlemf  26189  qabvle  26209  padicabv  26214  padicabvcxp  26216  ostth2lem2  26218  axlowdimlem13  26748  axlowdimlem16  26751  pthdlem1  27555  crctcshwlkn0  27607  crctcsh  27610  clwwisshclwwslemlem  27798  eucrctshift  28028  nndiffz1  30535  fzsplit3  30543  bcm1n  30544  fzone1  30549  ltesubnnd  30564  wrdt2ind  30653  cshwrnid  30661  cycpmfv2  30806  cycpmco2lem6  30823  cycpmco2lem7  30824  cycpmrn  30835  cyc3conja  30849  pnfinf  30862  dya2iocress  31642  dya2iocbrsiga  31643  dya2icobrsiga  31644  dya2icoseg  31645  dya2iocucvr  31652  sxbrsigalem2  31654  ballotlemfc0  31860  ballotlemfcc  31861  ballotlemodife  31865  ballotlemimin  31873  ballotlemsgt1  31878  ballotlemsel1i  31880  ballotlemsi  31882  ballotlemsima  31883  ballotlemrv2  31889  ballotlemfrceq  31896  ballotlemfrcn0  31897  ballotlemirc  31899  fsum2dsub  31988  reprlt  32000  reprgt  32002  breprexplemc  32013  tgoldbachgnn  32040  tgoldbachgt  32044  subfacval3  32549  erdszelem8  32558  erdszelem9  32559  supfz  33073  inffz  33074  dnizeq0  33927  dnizphlfeqhlf  33928  dnibndlem13  33942  knoppndvlem1  33964  knoppndvlem2  33965  knoppndvlem7  33970  knoppndvlem19  33982  knoppndvlem21  33984  ltflcei  35045  leceifl  35046  poimirlem1  35058  poimirlem2  35059  poimirlem6  35063  poimirlem7  35064  poimirlem8  35065  poimirlem15  35072  poimirlem16  35073  poimirlem17  35074  poimirlem19  35076  poimirlem20  35077  poimirlem23  35080  poimirlem24  35081  poimirlem27  35084  poimirlem29  35086  poimirlem31  35088  poimirlem32  35089  mblfinlem2  35095  itg2addnclem2  35109  mettrifi  35195  cntotbnd  35234  fzne2d  39268  2ap1caineq  39349  metakunt7  39356  metakunt12  39361  metakunt15  39364  metakunt16  39365  metakunt22  39371  metakunt28  39377  prodsplit  39386  frlmvscadiccat  39440  exp11d  39497  dffltz  39615  lzunuz  39709  lzenom  39711  diophin  39713  irrapxlem1  39763  irrapxlem2  39764  irrapxlem3  39765  irrapxlem4  39766  pellexlem5  39774  pellexlem6  39775  rmspecfund  39850  rmxypos  39888  ltrmynn0  39889  ltrmxnn0  39890  ltrmy  39893  rmyeq0  39894  rmyeq  39895  lermy  39896  rmyabs  39899  jm2.24nn  39900  jm2.17a  39901  jm2.17b  39902  jm2.17c  39903  jm2.24  39904  rmygeid  39905  acongrep  39921  fzmaxdif  39922  acongeq  39924  jm2.22  39936  jm2.23  39937  jm2.26lem3  39942  jm2.27a  39946  jm3.1lem1  39958  jm3.1lem3  39960  expdiophlem1  39962  prmunb2  41015  nzprmdif  41023  hashnzfzclim  41026  binomcxplemnn0  41053  uzwo4  41687  ssinc  41723  ssdec  41724  zltlesub  41916  monoords  41929  fzisoeu  41932  fperiodmul  41936  fzdifsuc2  41942  iuneqfzuzlem  41966  uzublem  42067  zxrd  42092  uzinico  42197  uzubioo  42204  fmul01  42222  fmul01lt1lem1  42226  fmul01lt1lem2  42227  climsuselem1  42249  climsuse  42250  sumnnodd  42272  ltmod  42280  limsupresuz  42345  limsupubuzlem  42354  limsupequzlem  42364  limsupmnfuzlem  42368  limsupequzmptlem  42370  limsupre3uzlem  42377  supcnvlimsup  42382  limsup10exlem  42414  liminfresuz  42426  liminfvaluz  42434  limsupvaluz3  42440  ioodvbdlimc1lem2  42574  ioodvbdlimc2lem  42576  dvnmul  42585  dvnprodlem1  42588  dvnprodlem2  42589  iblspltprt  42615  itgspltprt  42621  stoweidlem3  42645  stoweidlem11  42653  stoweidlem20  42662  stoweidlem26  42668  stoweidlem34  42676  stoweidlem59  42701  stirlinglem5  42720  dirkertrigeqlem3  42742  dirkeritg  42744  dirkercncflem1  42745  dirkercncflem2  42746  dirkercncflem4  42748  fourierdlem4  42753  fourierdlem6  42755  fourierdlem7  42756  fourierdlem11  42760  fourierdlem12  42761  fourierdlem15  42764  fourierdlem19  42768  fourierdlem20  42769  fourierdlem25  42774  fourierdlem26  42775  fourierdlem34  42783  fourierdlem35  42784  fourierdlem41  42790  fourierdlem48  42796  fourierdlem49  42797  fourierdlem50  42798  fourierdlem51  42799  fourierdlem54  42802  fourierdlem63  42811  fourierdlem64  42812  fourierdlem65  42813  fourierdlem71  42819  fourierdlem79  42827  fourierdlem89  42837  fourierdlem90  42838  fourierdlem91  42839  fourierdlem102  42850  fourierdlem103  42851  fourierdlem104  42852  fourierdlem114  42862  fouriersw  42873  elaa2lem  42875  etransclem3  42879  etransclem4  42880  etransclem7  42883  etransclem10  42886  etransclem15  42891  etransclem19  42895  etransclem23  42899  etransclem24  42900  etransclem25  42901  etransclem27  42903  etransclem31  42907  etransclem32  42908  etransclem35  42911  etransclem41  42917  etransclem44  42920  etransclem46  42922  etransclem48  42924  iundjiun  43099  caratheodorylem1  43165  smflimsuplem4  43454  smfliminflem  43461  2elfz2melfz  43875  elfzelfzlble  43878  fzopredsuc  43880  fsummsndifre  43889  iccpartgt  43944  icceuelpartlem  43952  icceuelpart  43953  iccpartnel  43955  lighneallem2  44124  proththd  44132  dfodd4  44177  oexpnegALTV  44195  nnoALTV  44213  evenltle  44235  fpprwppr  44257  gbowgt5  44280  gboge9  44282  stgoldbwt  44294  sbgoldbst  44296  sbgoldbalt  44299  sgoldbeven3prm  44301  mogoldbb  44303  bgoldbtbndlem1  44323  bgoldbtbndlem2  44324  bgoldbtbndlem3  44325  bgoldbtbnd  44327  bgoldbachlt  44331  tgblthelfgott  44333  tgoldbach  44335  pw2m1lepw2m1  44929  m1modmmod  44935  difmodm1lt  44936  fllogbd  44974  logbpw2m1  44981  fllog2  44982  nnpw2blen  44994  nnolog2flm1  45004  dignn0flhalflem1  45029  dignn0flhalflem2  45030