Theorem zred 12090

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

Syntax hints:   → wi 4   ∈ wcel 2113  ℝcr 10539  ℤcz 11984

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1969  ax-7 2014  ax-8 2115  ax-9 2123  ax-10 2144  ax-11 2160  ax-12 2176  ax-ext 2796

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3or 1084  df-3an 1085  df-tru 1539  df-ex 1780  df-nf 1784  df-sb 2069  df-clab 2803  df-cleq 2817  df-clel 2896  df-nfc 2966  df-rab 3150  df-v 3499  df-dif 3942  df-un 3944  df-in 3946  df-ss 3955  df-nul 4295  df-if 4471  df-sn 4571  df-pr 4573  df-op 4577  df-uni 4842  df-br 5070  df-iota 6317  df-fv 6366  df-ov 7162  df-neg 10876  df-z 11985

This theorem is referenced by:  zcnd  12091  suprfinzcl  12100  eluzmn  12253  eluzelre  12257  subeluzsub  12278  uzm1  12279  zsupss  12340  suprzcl2  12341  uzwo3  12346  rpnnen1lem3  12381  rpnnen1lem5  12383  zltaddlt1le  12893  fzsplit2  12935  fzdisj  12937  ssfzunsnext  12955  fzpreddisj  12959  fznatpl1  12964  fzp1disj  12969  uzdisj  12983  fzm1  12990  fz0fzdiffz0  13019  elfzmlbm  13020  elfzmlbp  13021  difelfznle  13024  nn0disj  13026  elfzolt3  13051  fzonel  13054  fzospliti  13072  fzodisj  13074  fzouzdisj  13076  fzodisjsn  13078  fzonmapblen  13086  fzoaddel  13093  elincfzoext  13098  reflcl  13169  flge  13178  flwordi  13185  fladdz  13198  2tnp1ge0ge0  13202  flhalf  13203  fldiv4p1lem1div2  13208  fldiv4lem1div2uz2  13209  fldiv4lem1div2  13210  flleceil  13224  fleqceilz  13225  quoremz  13226  uzsup  13234  modmul12d  13296  modaddmodup  13305  modaddmodlo  13306  modfzo0difsn  13314  modsumfzodifsn  13315  addmodlteq  13317  om2uzlti  13321  om2uzf1oi  13324  seqf1olem1  13412  seqf1olem2  13413  bcval4  13670  bcp1nk  13680  bcval5  13681  fzsdom2  13792  seqcoll  13825  seqcoll2  13826  ccatrn  13946  ccatalpha  13950  cshwidxmodr  14169  fzomaxdiflem  14705  fzomaxdif  14706  rexuzre  14715  limsupgre  14841  rlimclim1  14905  isercoll  15027  iseralt  15044  fsumm1  15109  fsum1p  15111  fsum0diaglem  15134  modfsummods  15151  isumsplit  15198  climcndslem1  15207  mertenslem1  15243  ntrivcvgmul  15261  fprodntriv  15299  fprod1p  15325  fprodeq0  15332  fallfacval4  15400  bpoly4  15416  fzo0dvdseq  15676  dvdsmod  15681  oexpneg  15697  mod2eq1n2dvds  15699  ltoddhalfle  15713  flodddiv4t2lthalf  15770  bitsp1  15783  bitsfzolem  15786  bitsfzo  15787  bitsmod  15788  bitscmp  15790  bitsinv1lem  15793  sadaddlem  15818  bitsres  15825  bitsuz  15826  smumul  15845  gcd0id  15870  gcdneg  15873  dfgcd2  15897  nn0seqcvgd  15917  lcmgcdlem  15953  nprm  16035  prmdvdsfz  16052  isprm5  16054  isprm7  16055  coprm  16058  prmexpb  16065  prmfac1  16066  hashdvds  16115  crth  16118  eulerthlem2  16122  fermltl  16124  prmdiv  16125  prmdiveq  16126  hashgcdlem  16128  odzdvds  16135  vfermltlALT  16142  modprm0  16145  modprmn0modprm0  16147  prm23ge5  16155  pythagtriplem13  16167  pcxcl  16200  pcaddlem  16227  pcadd  16228  pcfac  16238  qexpz  16240  prmunb  16253  1arithlem4  16265  4sqlem5  16281  4sqlem6  16282  4sqlem7  16283  4sqlem10  16286  4sqlem11  16294  4sqlem12  16295  4sqlem15  16298  4sqlem16  16299  4sqlem17  16300  vdwnnlem3  16336  prmgaplem7  16396  cshwshashlem3  16434  subgmulg  18296  mndodconglem  18672  odnncl  18676  odmod  18677  oddvds  18678  dfod2  18694  sylow1lem3  18728  efgsp1  18866  efgredleme  18872  telgsumfzs  19112  zringlpirlem1  20634  zringlpirlem3  20636  znf1o  20701  zcld  23424  ovoliunlem1  24106  ovoliunlem2  24107  dyadss  24198  dyaddisjlem  24199  dyadmaxlem  24201  dvfsumle  24621  dvfsumge  24622  dvfsumabs  24623  dvfsumlem1  24626  dvfsumlem3  24628  degltlem1  24669  plyco0  24785  plyeq0lem  24803  plydivex  24889  aannenlem1  24920  efif1olem2  25130  nnlogbexp  25362  logblt  25365  ang180lem1  25390  ang180lem3  25392  wilthlem2  25649  basellem3  25663  basellem4  25664  ppiprm  25731  chtdif  25738  ppidif  25743  chtub  25791  mersenne  25806  bcmono  25856  bcmax  25857  bposlem1  25863  bposlem3  25865  bposlem5  25867  bposlem6  25868  lgsval2lem  25886  lgsvalmod  25895  lgsneg  25900  lgsmod  25902  lgsdilem  25903  lgsdirprm  25910  lgsdilem2  25912  lgsne0  25914  lgssq  25916  lgssq2  25917  lgsqr  25930  lgsdchr  25934  gausslemma2dlem1a  25944  gausslemma2dlem3  25947  gausslemma2dlem5a  25949  gausslemma2dlem6  25951  gausslemma2d  25953  lgseisenlem1  25954  lgseisenlem2  25955  lgseisenlem3  25956  lgseisenlem4  25957  lgsquadlem1  25959  lgsquadlem2  25960  lgsquadlem3  25961  lgsquad3  25966  2lgslem1a2  25969  2lgslem1  25973  2lgslem2  25974  2sqlem3  25999  2sqlem8  26005  2sqblem  26010  2sqmod  26015  chebbnd1lem1  26048  chebbnd1lem2  26049  chebbnd1lem3  26050  dchrmusum2  26073  dchrvmasumlem1  26074  dchrvmasum2lem  26075  dchrvmasum2if  26076  dchrvmasumlem3  26078  dchrvmasumiflem2  26081  dchrisum0lem1  26095  dchrmusumlem  26101  mudivsum  26109  mulogsumlem  26110  mulogsum  26111  mulog2sumlem2  26114  mulog2sumlem3  26115  selberglem1  26124  selberglem2  26125  pntpbnd1  26165  pntlemg  26177  pntlemf  26184  qabvle  26204  padicabv  26209  padicabvcxp  26211  ostth2lem2  26213  axlowdimlem13  26743  axlowdimlem16  26746  pthdlem1  27550  crctcshwlkn0  27602  crctcsh  27605  clwwisshclwwslemlem  27794  eucrctshift  28025  nndiffz1  30512  fzsplit3  30520  bcm1n  30521  fzone1  30526  ltesubnnd  30542  wrdt2ind  30631  cshwrnid  30639  cycpmfv2  30760  cycpmco2lem6  30777  cycpmco2lem7  30778  cycpmrn  30789  cyc3conja  30803  pnfinf  30816  dya2iocress  31536  dya2iocbrsiga  31537  dya2icobrsiga  31538  dya2icoseg  31539  dya2iocucvr  31546  sxbrsigalem2  31548  ballotlemfc0  31754  ballotlemfcc  31755  ballotlemodife  31759  ballotlemimin  31767  ballotlemsgt1  31772  ballotlemsel1i  31774  ballotlemsi  31776  ballotlemsima  31777  ballotlemrv2  31783  ballotlemfrceq  31790  ballotlemfrcn0  31791  ballotlemirc  31793  fsum2dsub  31882  reprlt  31894  reprgt  31896  breprexplemc  31907  tgoldbachgnn  31934  tgoldbachgt  31938  subfacval3  32440  erdszelem8  32449  erdszelem9  32450  supfz  32964  inffz  32965  dnizeq0  33818  dnizphlfeqhlf  33819  dnibndlem13  33833  knoppndvlem1  33855  knoppndvlem2  33856  knoppndvlem7  33861  knoppndvlem19  33873  knoppndvlem21  33875  ltflcei  34884  leceifl  34885  poimirlem1  34897  poimirlem2  34898  poimirlem6  34902  poimirlem7  34903  poimirlem8  34904  poimirlem15  34911  poimirlem16  34912  poimirlem17  34913  poimirlem19  34915  poimirlem20  34916  poimirlem23  34919  poimirlem24  34920  poimirlem27  34923  poimirlem29  34925  poimirlem31  34927  poimirlem32  34928  mblfinlem2  34934  itg2addnclem2  34948  mettrifi  35036  cntotbnd  35078  frlmvscadiccat  39151  exp11d  39195  dffltz  39277  lzunuz  39371  lzenom  39373  diophin  39375  irrapxlem1  39425  irrapxlem2  39426  irrapxlem3  39427  irrapxlem4  39428  pellexlem5  39436  pellexlem6  39437  rmspecfund  39512  rmxypos  39550  ltrmynn0  39551  ltrmxnn0  39552  ltrmy  39555  rmyeq0  39556  rmyeq  39557  lermy  39558  rmyabs  39561  jm2.24nn  39562  jm2.17a  39563  jm2.17b  39564  jm2.17c  39565  jm2.24  39566  rmygeid  39567  acongrep  39583  fzmaxdif  39584  acongeq  39586  jm2.22  39598  jm2.23  39599  jm2.26lem3  39604  jm2.27a  39608  jm3.1lem1  39620  jm3.1lem3  39622  expdiophlem1  39624  prmunb2  40649  nzprmdif  40657  hashnzfzclim  40660  binomcxplemnn0  40687  uzwo4  41321  ssinc  41359  ssdec  41360  zltlesub  41557  monoords  41570  fzisoeu  41573  fperiodmul  41577  fzdifsuc2  41583  iuneqfzuzlem  41608  uzublem  41710  zxrd  41735  uzinico  41842  uzubioo  41849  fmul01  41867  fmul01lt1lem1  41871  fmul01lt1lem2  41872  climsuselem1  41894  climsuse  41895  sumnnodd  41917  ltmod  41925  limsupresuz  41990  limsupubuzlem  41999  limsupequzlem  42009  limsupmnfuzlem  42013  limsupequzmptlem  42015  limsupre3uzlem  42022  supcnvlimsup  42027  limsup10exlem  42059  liminfresuz  42071  liminfvaluz  42079  limsupvaluz3  42085  ioodvbdlimc1lem2  42223  ioodvbdlimc2lem  42225  dvnmul  42234  dvnprodlem1  42237  dvnprodlem2  42238  iblspltprt  42264  itgspltprt  42270  stoweidlem3  42295  stoweidlem11  42303  stoweidlem20  42312  stoweidlem26  42318  stoweidlem34  42326  stoweidlem59  42351  stirlinglem5  42370  dirkertrigeqlem3  42392  dirkeritg  42394  dirkercncflem1  42395  dirkercncflem2  42396  dirkercncflem4  42398  fourierdlem4  42403  fourierdlem6  42405  fourierdlem7  42406  fourierdlem11  42410  fourierdlem12  42411  fourierdlem15  42414  fourierdlem19  42418  fourierdlem20  42419  fourierdlem25  42424  fourierdlem26  42425  fourierdlem34  42433  fourierdlem35  42434  fourierdlem41  42440  fourierdlem48  42446  fourierdlem49  42447  fourierdlem50  42448  fourierdlem51  42449  fourierdlem54  42452  fourierdlem63  42461  fourierdlem64  42462  fourierdlem65  42463  fourierdlem71  42469  fourierdlem79  42477  fourierdlem89  42487  fourierdlem90  42488  fourierdlem91  42489  fourierdlem102  42500  fourierdlem103  42501  fourierdlem104  42502  fourierdlem114  42512  fouriersw  42523  elaa2lem  42525  etransclem3  42529  etransclem4  42530  etransclem7  42533  etransclem10  42536  etransclem15  42541  etransclem19  42545  etransclem23  42549  etransclem24  42550  etransclem25  42551  etransclem27  42553  etransclem31  42557  etransclem32  42558  etransclem35  42561  etransclem41  42567  etransclem44  42570  etransclem46  42572  etransclem48  42574  iundjiun  42749  caratheodorylem1  42815  smflimsuplem4  43104  smfliminflem  43111  2elfz2melfz  43525  elfzelfzlble  43528  fzopredsuc  43530  fsummsndifre  43539  iccpartgt  43594  icceuelpartlem  43602  icceuelpart  43603  iccpartnel  43605  lighneallem2  43778  proththd  43786  dfodd4  43831  oexpnegALTV  43849  nnoALTV  43867  evenltle  43889  fpprwppr  43911  gbowgt5  43934  gboge9  43936  stgoldbwt  43948  sbgoldbst  43950  sbgoldbalt  43953  sgoldbeven3prm  43955  mogoldbb  43957  bgoldbtbndlem1  43977  bgoldbtbndlem2  43978  bgoldbtbndlem3  43979  bgoldbtbnd  43981  bgoldbachlt  43985  tgblthelfgott  43987  tgoldbach  43989  pw2m1lepw2m1  44582  m1modmmod  44588  difmodm1lt  44589  fllogbd  44627  logbpw2m1  44634  fllog2  44635  nnpw2blen  44647  nnolog2flm1  44657  dignn0flhalflem1  44682  dignn0flhalflem2  44683