Theorem zred 12598

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

Syntax hints:   → wi 4   ∈ wcel 2109  ℝcr 11027  ℤcz 12489

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 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-rab 3397  df-v 3440  df-dif 3908  df-un 3910  df-ss 3922  df-nul 4287  df-if 4479  df-sn 4580  df-pr 4582  df-op 4586  df-uni 4862  df-br 5096  df-iota 6442  df-fv 6494  df-ov 7356  df-neg 11368  df-z 12490

This theorem is referenced by:  zcnd  12599  suprfinzcl  12608  eluzmn  12760  eluzelre  12764  eluzadd  12782  subeluzsub  12790  uzm1  12791  zsupss  12856  suprzcl2  12857  uzwo3  12862  rpnnen1lem3  12898  rpnnen1lem5  12900  zltaddlt1le  13426  fzsplit2  13470  fzdisj  13472  ssfzunsnext  13490  fzpreddisj  13494  fznatpl1  13499  fzp1disj  13504  uzdisj  13518  fzdif1  13526  fzm1  13528  fz0fzdiffz0  13558  elfzmlbm  13559  elfzmlbp  13560  difelfznle  13563  nn0disj  13565  elfzolt3  13590  fzonel  13594  fzospliti  13612  fzodisj  13614  fzouzdisj  13616  fzodisjsn  13618  elfzo0subge1  13626  elfzo0suble  13627  fzonmapblen  13629  fzoaddel  13638  elincfzoext  13644  reflcl  13718  flge  13727  flwordi  13734  fladdz  13747  2tnp1ge0ge0  13751  flhalf  13752  fldiv4p1lem1div2  13757  fldiv4lem1div2uz2  13758  fldiv4lem1div2  13759  flleceil  13775  fleqceilz  13776  quoremz  13777  uzsup  13785  modaddid  13832  modmul12d  13850  modaddmodup  13859  modaddmodlo  13860  modfzo0difsn  13868  modsumfzodifsn  13869  addmodlteq  13871  om2uzlti  13875  om2uzf1oi  13878  seqf1olem1  13966  seqf1olem2  13967  bcval4  14232  bcp1nk  14242  bcval5  14243  fzsdom2  14353  seqcoll  14389  seqcoll2  14390  ccatrn  14514  ccatalpha  14518  cshwidxmodr  14728  fzomaxdiflem  15268  fzomaxdif  15269  rexuzre  15278  limsupgre  15406  rlimclim1  15470  isercoll  15593  iseralt  15610  fsumm1  15676  fsum1p  15678  fsum0diaglem  15701  modfsummods  15718  isumsplit  15765  climcndslem1  15774  mertenslem1  15809  ntrivcvgmul  15827  fprodntriv  15867  fprod1p  15893  fprodeq0  15900  fallfacval4  15968  bpoly4  15984  fzo0dvdseq  16252  dvdsmod  16258  oexpneg  16274  mod2eq1n2dvds  16276  ltoddhalfle  16290  flodddiv4t2lthalf  16347  bitsp1  16360  bitsfzolem  16363  bitsfzo  16364  bitsmod  16365  bitscmp  16367  bitsinv1lem  16370  sadaddlem  16395  bitsres  16402  bitsuz  16403  smumul  16422  gcd0id  16448  gcdneg  16451  dfgcd2  16475  nn0seqcvgd  16499  lcmgcdlem  16535  nprm  16617  prmdvdsfz  16634  isprm5  16636  isprm7  16637  coprm  16640  prmexpb  16648  prmfac1  16649  hashdvds  16704  crth  16707  eulerthlem2  16711  fermltl  16713  prmdiv  16714  prmdiveq  16715  hashgcdlem  16717  odzdvds  16725  vfermltlALT  16732  modprm0  16735  modprmn0modprm0  16737  prm23ge5  16745  pythagtriplem13  16757  pcxcl  16791  pcaddlem  16818  pcadd  16819  pcfac  16829  qexpz  16831  prmunb  16844  1arithlem4  16856  4sqlem5  16872  4sqlem6  16873  4sqlem7  16874  4sqlem10  16877  4sqlem11  16885  4sqlem12  16886  4sqlem15  16889  4sqlem16  16890  4sqlem17  16891  vdwnnlem3  16927  prmgaplem7  16987  cshwshashlem3  17027  subgmulg  19037  mndodconglem  19438  odnncl  19442  odmod  19443  oddvds  19444  dfod2  19461  sylow1lem3  19497  efgsp1  19634  efgredleme  19640  telgsumfzs  19886  zringlpirlem1  21387  zringlpirlem3  21389  fermltlchr  21454  znf1o  21476  zcld  24718  ovoliunlem1  25419  ovoliunlem2  25420  dyadss  25511  dyaddisjlem  25512  dyadmaxlem  25514  dvfsumle  25942  dvfsumleOLD  25943  dvfsumge  25944  dvfsumabs  25945  dvfsumlem1  25948  dvfsumlem3  25951  degltlem1  25993  plyco0  26113  plyeq0lem  26131  plydivex  26221  aannenlem1  26252  efif1olem2  26468  nnlogbexp  26707  logblt  26710  ang180lem1  26735  ang180lem3  26737  wilthlem2  26995  basellem3  27009  basellem4  27010  ppiprm  27077  chtdif  27084  ppidif  27089  chtub  27139  mersenne  27154  bcmono  27204  bcmax  27205  bposlem1  27211  bposlem3  27213  bposlem5  27215  bposlem6  27216  lgsval2lem  27234  lgsvalmod  27243  lgsneg  27248  lgsmod  27250  lgsdilem  27251  lgsdirprm  27258  lgsdilem2  27260  lgsne0  27262  lgssq  27264  lgssq2  27265  lgsqr  27278  lgsdchr  27282  gausslemma2dlem1a  27292  gausslemma2dlem3  27295  gausslemma2dlem5a  27297  gausslemma2dlem6  27299  gausslemma2d  27301  lgseisenlem1  27302  lgseisenlem2  27303  lgseisenlem3  27304  lgseisenlem4  27305  lgsquadlem1  27307  lgsquadlem2  27308  lgsquadlem3  27309  lgsquad3  27314  2lgslem1a2  27317  2lgslem1  27321  2lgslem2  27322  2sqlem3  27347  2sqlem8  27353  2sqblem  27358  2sqmod  27363  chebbnd1lem1  27396  chebbnd1lem2  27397  chebbnd1lem3  27398  dchrmusum2  27421  dchrvmasumlem1  27422  dchrvmasum2lem  27423  dchrvmasum2if  27424  dchrvmasumlem3  27426  dchrvmasumiflem2  27429  dchrisum0lem1  27443  dchrmusumlem  27449  mudivsum  27457  mulogsumlem  27458  mulogsum  27459  mulog2sumlem2  27462  mulog2sumlem3  27463  selberglem1  27472  selberglem2  27473  pntpbnd1  27513  pntlemg  27525  pntlemf  27532  qabvle  27552  padicabv  27557  padicabvcxp  27559  ostth2lem2  27561  axlowdimlem13  28917  axlowdimlem16  28920  pthdlem1  29729  crctcshwlkn0  29784  crctcsh  29787  clwwisshclwwslemlem  29975  eucrctshift  30205  nndiffz1  32742  fzsplit3  32749  bcm1n  32751  fzone1  32756  suppssnn0  32763  ltesubnnd  32780  wrdt2ind  32908  cshwrnid  32916  chnub  32967  chnso  32969  cycpmfv2  33069  cycpmco2lem6  33086  cycpmco2lem7  33087  cycpmrn  33098  cyc3conja  33112  pnfinf  33135  znfermltl  33313  constrext2chnlem  33716  cos9thpiminplylem1  33748  cos9thpiminplylem2  33749  dya2iocress  34241  dya2iocbrsiga  34242  dya2icobrsiga  34243  dya2icoseg  34244  dya2iocucvr  34251  sxbrsigalem2  34253  ballotlemfc0  34460  ballotlemfcc  34461  ballotlemodife  34465  ballotlemimin  34473  ballotlemsgt1  34478  ballotlemsel1i  34480  ballotlemsi  34482  ballotlemsima  34483  ballotlemrv2  34489  ballotlemfrceq  34496  ballotlemfrcn0  34497  ballotlemirc  34499  fsum2dsub  34574  reprlt  34586  reprgt  34588  breprexplemc  34599  tgoldbachgnn  34626  tgoldbachgt  34630  subfacval3  35161  erdszelem8  35170  erdszelem9  35171  supfz  35701  inffz  35702  dnizeq0  36448  dnizphlfeqhlf  36449  dnibndlem13  36463  knoppndvlem1  36485  knoppndvlem2  36486  knoppndvlem7  36491  knoppndvlem19  36503  knoppndvlem21  36505  ltflcei  37587  leceifl  37588  poimirlem1  37600  poimirlem2  37601  poimirlem6  37605  poimirlem7  37606  poimirlem8  37607  poimirlem15  37614  poimirlem16  37615  poimirlem17  37616  poimirlem19  37618  poimirlem20  37619  poimirlem23  37622  poimirlem24  37623  poimirlem27  37626  poimirlem29  37628  poimirlem31  37630  poimirlem32  37631  mblfinlem2  37637  itg2addnclem2  37651  mettrifi  37736  cntotbnd  37775  fzne2d  41953  aks4d1lem1  42035  aks4d1p1p3  42042  aks4d1p1p2  42043  aks4d1p1p4  42044  aks4d1p1  42049  aks4d1p2  42050  aks4d1p3  42051  aks4d1p5  42053  aks4d1p6  42054  aks4d1p7d1  42055  aks4d1p7  42056  aks4d1p8d3  42059  aks4d1p8  42060  aks4d1p9  42061  posbezout  42073  aks6d1c1  42089  hashscontpow1  42094  hashscontpow  42095  aks6d1c2  42103  aks6d1c5lem1  42109  2ap1caineq  42118  sticksstones6  42124  sticksstones7  42125  sticksstones10  42128  sticksstones12a  42130  sticksstones12  42131  sticksstones22  42141  bcled  42151  bcle2d  42152  aks6d1c7lem1  42153  aks6d1c7lem2  42154  aks6d1c7  42157  aks5lem6  42165  unitscyglem2  42169  unitscyglem4  42171  aks5lem8  42174  sumcubes  42286  frlmvscadiccat  42479  dffltz  42607  lzunuz  42741  lzenom  42743  diophin  42745  irrapxlem1  42795  irrapxlem2  42796  irrapxlem3  42797  irrapxlem4  42798  pellexlem5  42806  pellexlem6  42807  rmspecfund  42882  rmxypos  42920  ltrmynn0  42921  ltrmxnn0  42922  ltrmy  42925  rmyeq0  42926  rmyeq  42927  lermy  42928  rmyabs  42931  jm2.24nn  42932  jm2.17a  42933  jm2.17b  42934  jm2.17c  42935  jm2.24  42936  rmygeid  42937  acongrep  42953  fzmaxdif  42954  acongeq  42956  jm2.22  42968  jm2.23  42969  jm2.26lem3  42974  jm2.27a  42978  jm3.1lem1  42990  jm3.1lem3  42992  expdiophlem1  42994  fzuntd  43429  fzunt1d  43430  fzuntgd  43431  prmunb2  44284  nzprmdif  44292  hashnzfzclim  44295  binomcxplemnn0  44322  uzwo4  45031  ssinc  45065  ssdec  45066  zltlesub  45267  monoords  45279  fzisoeu  45282  fperiodmul  45286  fzdifsuc2  45292  iuneqfzuzlem  45314  uzublem  45410  zxrd  45433  uzinico  45541  uzubioo  45547  fmul01  45562  fmul01lt1lem1  45566  fmul01lt1lem2  45567  climsuselem1  45589  climsuse  45590  sumnnodd  45612  ltmod  45620  limsupresuz  45685  limsupubuzlem  45694  limsupequzlem  45704  limsupmnfuzlem  45708  limsupequzmptlem  45710  limsupre3uzlem  45717  supcnvlimsup  45722  limsup10exlem  45754  liminfresuz  45766  liminfvaluz  45774  limsupvaluz3  45780  ioodvbdlimc1lem2  45914  ioodvbdlimc2lem  45916  dvnmul  45925  dvnprodlem1  45928  dvnprodlem2  45929  iblspltprt  45955  itgspltprt  45961  stoweidlem3  45985  stoweidlem11  45993  stoweidlem20  46002  stoweidlem26  46008  stoweidlem34  46016  stoweidlem59  46041  stirlinglem5  46060  dirkertrigeqlem3  46082  dirkeritg  46084  dirkercncflem1  46085  dirkercncflem2  46086  dirkercncflem4  46088  fourierdlem4  46093  fourierdlem6  46095  fourierdlem7  46096  fourierdlem11  46100  fourierdlem12  46101  fourierdlem15  46104  fourierdlem19  46108  fourierdlem20  46109  fourierdlem25  46114  fourierdlem26  46115  fourierdlem34  46123  fourierdlem35  46124  fourierdlem41  46130  fourierdlem48  46136  fourierdlem49  46137  fourierdlem50  46138  fourierdlem51  46139  fourierdlem54  46142  fourierdlem63  46151  fourierdlem64  46152  fourierdlem65  46153  fourierdlem71  46159  fourierdlem79  46167  fourierdlem89  46177  fourierdlem90  46178  fourierdlem91  46179  fourierdlem102  46190  fourierdlem103  46191  fourierdlem104  46192  fourierdlem114  46202  fouriersw  46213  elaa2lem  46215  etransclem3  46219  etransclem4  46220  etransclem7  46223  etransclem10  46226  etransclem15  46231  etransclem19  46235  etransclem23  46239  etransclem24  46240  etransclem25  46241  etransclem27  46243  etransclem31  46247  etransclem32  46248  etransclem35  46251  etransclem41  46257  etransclem44  46260  etransclem46  46262  etransclem48  46264  iundjiun  46442  caratheodorylem1  46508  smflimsuplem4  46805  smfliminflem  46812  ormklocald  46856  ormkglobd  46857  natglobalincr  46859  2elfz2melfz  47303  elfzelfzlble  47306  fzopredsuc  47308  2ltceilhalf  47313  ceilhalfgt1  47314  ceilhalfnn  47321  submodlt  47335  m1modmmod  47343  difmodm1lt  47344  modmknepk  47347  mod2addne  47349  fsummsndifre  47357  iccpartgt  47412  icceuelpartlem  47420  icceuelpart  47421  iccpartnel  47423  lighneallem2  47591  proththd  47599  dfodd4  47644  oexpnegALTV  47662  nnoALTV  47680  evenltle  47702  fpprwppr  47724  gbowgt5  47747  gboge9  47749  stgoldbwt  47761  sbgoldbst  47763  sbgoldbalt  47766  sgoldbeven3prm  47768  mogoldbb  47770  bgoldbtbndlem1  47790  bgoldbtbndlem2  47791  bgoldbtbndlem3  47792  bgoldbtbnd  47794  bgoldbachlt  47798  tgblthelfgott  47800  tgoldbach  47802  upgrimpthslem2  47893  gpgprismgrusgra  48043  gpgedgvtx1  48047  gpgvtxedg0  48048  gpgvtxedg1  48049  gpg5nbgrvtx13starlem2  48057  gpg3nbgrvtx0  48061  gpg3kgrtriexlem1  48068  gpg3kgrtriexlem4  48071  gpg3kgrtriexlem6  48073  pw2m1lepw2m1  48506  fllogbd  48546  logbpw2m1  48553  fllog2  48554  nnpw2blen  48566  nnolog2flm1  48576  dignn0flhalflem1  48601  dignn0flhalflem2  48602