Theorem zred 12596

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

Syntax hints:   → wi 4   ∈ wcel 2113  ℝcr 11025  ℤcz 12488

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-sb 2068  df-clab 2715  df-cleq 2728  df-clel 2811  df-rab 3400  df-v 3442  df-dif 3904  df-un 3906  df-ss 3918  df-nul 4286  df-if 4480  df-sn 4581  df-pr 4583  df-op 4587  df-uni 4864  df-br 5099  df-iota 6448  df-fv 6500  df-ov 7361  df-neg 11367  df-z 12489

This theorem is referenced by:  zcnd  12597  suprfinzcl  12606  eluzmn  12758  eluzelre  12762  eluzadd  12780  subeluzsub  12784  uzm1  12785  zsupss  12850  suprzcl2  12851  uzwo3  12856  rpnnen1lem3  12892  rpnnen1lem5  12894  zltaddlt1le  13421  fzsplit2  13465  fzdisj  13467  ssfzunsnext  13485  fzpreddisj  13489  fznatpl1  13494  fzp1disj  13499  uzdisj  13513  fzdif1  13521  fzm1  13523  fz0fzdiffz0  13553  elfzmlbm  13554  elfzmlbp  13555  difelfznle  13558  nn0disj  13560  elfzolt3  13585  fzonel  13589  fzospliti  13607  fzodisj  13609  fzouzdisj  13611  fzodisjsn  13613  elfzo0subge1  13621  elfzo0suble  13622  fzonmapblen  13624  fzoaddel  13633  elincfzoext  13639  fzone1  13700  reflcl  13716  flge  13725  flwordi  13732  fladdz  13745  2tnp1ge0ge0  13749  flhalf  13750  fldiv4p1lem1div2  13755  fldiv4lem1div2uz2  13756  fldiv4lem1div2  13757  flleceil  13773  fleqceilz  13774  quoremz  13775  uzsup  13783  modaddid  13830  modmul12d  13848  modaddmodup  13857  modaddmodlo  13858  modfzo0difsn  13866  modsumfzodifsn  13867  addmodlteq  13869  om2uzlti  13873  om2uzf1oi  13876  seqf1olem1  13964  seqf1olem2  13965  bcval4  14230  bcp1nk  14240  bcval5  14241  fzsdom2  14351  seqcoll  14387  seqcoll2  14388  ccatrn  14513  ccatalpha  14517  cshwidxmodr  14727  fzomaxdiflem  15266  fzomaxdif  15267  rexuzre  15276  limsupgre  15404  rlimclim1  15468  isercoll  15591  iseralt  15608  fsumm1  15674  fsum1p  15676  fsum0diaglem  15699  modfsummods  15716  isumsplit  15763  climcndslem1  15772  mertenslem1  15807  ntrivcvgmul  15825  fprodntriv  15865  fprod1p  15891  fprodeq0  15898  fallfacval4  15966  bpoly4  15982  fzo0dvdseq  16250  dvdsmod  16256  oexpneg  16272  mod2eq1n2dvds  16274  ltoddhalfle  16288  flodddiv4t2lthalf  16345  bitsp1  16358  bitsfzolem  16361  bitsfzo  16362  bitsmod  16363  bitscmp  16365  bitsinv1lem  16368  sadaddlem  16393  bitsres  16400  bitsuz  16401  smumul  16420  gcd0id  16446  gcdneg  16449  dfgcd2  16473  nn0seqcvgd  16497  lcmgcdlem  16533  nprm  16615  prmdvdsfz  16632  isprm5  16634  isprm7  16635  coprm  16638  prmexpb  16646  prmfac1  16647  hashdvds  16702  crth  16705  eulerthlem2  16709  fermltl  16711  prmdiv  16712  prmdiveq  16713  hashgcdlem  16715  odzdvds  16723  vfermltlALT  16730  modprm0  16733  modprmn0modprm0  16735  prm23ge5  16743  pythagtriplem13  16755  pcxcl  16789  pcaddlem  16816  pcadd  16817  pcfac  16827  qexpz  16829  prmunb  16842  1arithlem4  16854  4sqlem5  16870  4sqlem6  16871  4sqlem7  16872  4sqlem10  16875  4sqlem11  16883  4sqlem12  16884  4sqlem15  16887  4sqlem16  16888  4sqlem17  16889  vdwnnlem3  16925  prmgaplem7  16985  cshwshashlem3  17025  chnub  18545  chnso  18547  chnccat  18549  chnpof1  18553  subgmulg  19070  mndodconglem  19470  odnncl  19474  odmod  19475  oddvds  19476  dfod2  19493  sylow1lem3  19529  efgsp1  19666  efgredleme  19672  telgsumfzs  19918  zringlpirlem1  21417  zringlpirlem3  21419  fermltlchr  21484  znf1o  21506  zcld  24758  ovoliunlem1  25459  ovoliunlem2  25460  dyadss  25551  dyaddisjlem  25552  dyadmaxlem  25554  dvfsumle  25982  dvfsumleOLD  25983  dvfsumge  25984  dvfsumabs  25985  dvfsumlem1  25988  dvfsumlem3  25991  degltlem1  26033  plyco0  26153  plyeq0lem  26171  plydivex  26261  aannenlem1  26292  efif1olem2  26508  nnlogbexp  26747  logblt  26750  ang180lem1  26775  ang180lem3  26777  wilthlem2  27035  basellem3  27049  basellem4  27050  ppiprm  27117  chtdif  27124  ppidif  27129  chtub  27179  mersenne  27194  bcmono  27244  bcmax  27245  bposlem1  27251  bposlem3  27253  bposlem5  27255  bposlem6  27256  lgsval2lem  27274  lgsvalmod  27283  lgsneg  27288  lgsmod  27290  lgsdilem  27291  lgsdirprm  27298  lgsdilem2  27300  lgsne0  27302  lgssq  27304  lgssq2  27305  lgsqr  27318  lgsdchr  27322  gausslemma2dlem1a  27332  gausslemma2dlem3  27335  gausslemma2dlem5a  27337  gausslemma2dlem6  27339  gausslemma2d  27341  lgseisenlem1  27342  lgseisenlem2  27343  lgseisenlem3  27344  lgseisenlem4  27345  lgsquadlem1  27347  lgsquadlem2  27348  lgsquadlem3  27349  lgsquad3  27354  2lgslem1a2  27357  2lgslem1  27361  2lgslem2  27362  2sqlem3  27387  2sqlem8  27393  2sqblem  27398  2sqmod  27403  chebbnd1lem1  27436  chebbnd1lem2  27437  chebbnd1lem3  27438  dchrmusum2  27461  dchrvmasumlem1  27462  dchrvmasum2lem  27463  dchrvmasum2if  27464  dchrvmasumlem3  27466  dchrvmasumiflem2  27469  dchrisum0lem1  27483  dchrmusumlem  27489  mudivsum  27497  mulogsumlem  27498  mulogsum  27499  mulog2sumlem2  27502  mulog2sumlem3  27503  selberglem1  27512  selberglem2  27513  pntpbnd1  27553  pntlemg  27565  pntlemf  27572  qabvle  27592  padicabv  27597  padicabvcxp  27599  ostth2lem2  27601  axlowdimlem13  29027  axlowdimlem16  29030  pthdlem1  29839  crctcshwlkn0  29894  crctcsh  29897  clwwisshclwwslemlem  30088  eucrctshift  30318  nndiffz1  32866  fzsplit3  32873  bcm1n  32875  suppssnn0  32885  ltesubnnd  32903  wrdt2ind  33035  cshwrnid  33043  cycpmfv2  33196  cycpmco2lem6  33213  cycpmco2lem7  33214  cycpmrn  33225  cyc3conja  33239  pnfinf  33265  znfermltl  33447  constrext2chnlem  33907  cos9thpiminplylem1  33939  cos9thpiminplylem2  33940  dya2iocress  34431  dya2iocbrsiga  34432  dya2icobrsiga  34433  dya2icoseg  34434  dya2iocucvr  34441  sxbrsigalem2  34443  ballotlemfc0  34650  ballotlemfcc  34651  ballotlemodife  34655  ballotlemimin  34663  ballotlemsgt1  34668  ballotlemsel1i  34670  ballotlemsi  34672  ballotlemsima  34673  ballotlemrv2  34679  ballotlemfrceq  34686  ballotlemfrcn0  34687  ballotlemirc  34689  fsum2dsub  34764  reprlt  34776  reprgt  34778  breprexplemc  34789  tgoldbachgnn  34816  tgoldbachgt  34820  subfacval3  35383  erdszelem8  35392  erdszelem9  35393  supfz  35923  inffz  35924  dnizeq0  36675  dnizphlfeqhlf  36676  dnibndlem13  36690  knoppndvlem1  36712  knoppndvlem2  36713  knoppndvlem7  36718  knoppndvlem19  36730  knoppndvlem21  36732  ltflcei  37805  leceifl  37806  poimirlem1  37818  poimirlem2  37819  poimirlem6  37823  poimirlem7  37824  poimirlem8  37825  poimirlem15  37832  poimirlem16  37833  poimirlem17  37834  poimirlem19  37836  poimirlem20  37837  poimirlem23  37840  poimirlem24  37841  poimirlem27  37844  poimirlem29  37846  poimirlem31  37848  poimirlem32  37849  mblfinlem2  37855  itg2addnclem2  37869  mettrifi  37954  cntotbnd  37993  fzne2d  42230  aks4d1lem1  42312  aks4d1p1p3  42319  aks4d1p1p2  42320  aks4d1p1p4  42321  aks4d1p1  42326  aks4d1p2  42327  aks4d1p3  42328  aks4d1p5  42330  aks4d1p6  42331  aks4d1p7d1  42332  aks4d1p7  42333  aks4d1p8d3  42336  aks4d1p8  42337  aks4d1p9  42338  posbezout  42350  aks6d1c1  42366  hashscontpow1  42371  hashscontpow  42372  aks6d1c2  42380  aks6d1c5lem1  42386  2ap1caineq  42395  sticksstones6  42401  sticksstones7  42402  sticksstones10  42405  sticksstones12a  42407  sticksstones12  42408  sticksstones22  42418  bcled  42428  bcle2d  42429  aks6d1c7lem1  42430  aks6d1c7lem2  42431  aks6d1c7  42434  aks5lem6  42442  unitscyglem2  42446  unitscyglem4  42448  aks5lem8  42451  sumcubes  42564  frlmvscadiccat  42757  dffltz  42873  lzunuz  43006  lzenom  43008  diophin  43010  irrapxlem1  43060  irrapxlem2  43061  irrapxlem3  43062  irrapxlem4  43063  pellexlem5  43071  pellexlem6  43072  rmspecfund  43147  rmxypos  43185  ltrmynn0  43186  ltrmxnn0  43187  ltrmy  43190  rmyeq0  43191  rmyeq  43192  lermy  43193  rmyabs  43196  jm2.24nn  43197  jm2.17a  43198  jm2.17b  43199  jm2.17c  43200  jm2.24  43201  rmygeid  43202  acongrep  43218  fzmaxdif  43219  acongeq  43221  jm2.22  43233  jm2.23  43234  jm2.26lem3  43239  jm2.27a  43243  jm3.1lem1  43255  jm3.1lem3  43257  expdiophlem1  43259  fzuntd  43693  fzunt1d  43694  fzuntgd  43695  prmunb2  44548  nzprmdif  44556  hashnzfzclim  44559  binomcxplemnn0  44586  uzwo4  45294  ssinc  45327  ssdec  45328  zltlesub  45529  monoords  45541  fzisoeu  45544  fperiodmul  45548  fzdifsuc2  45554  iuneqfzuzlem  45575  uzublem  45670  zxrd  45693  uzinico  45801  uzubioo  45807  fmul01  45822  fmul01lt1lem1  45826  fmul01lt1lem2  45827  climsuselem1  45849  climsuse  45850  sumnnodd  45872  ltmod  45878  limsupresuz  45943  limsupubuzlem  45952  limsupequzlem  45962  limsupmnfuzlem  45966  limsupequzmptlem  45968  limsupre3uzlem  45975  supcnvlimsup  45980  limsup10exlem  46012  liminfresuz  46024  liminfvaluz  46032  limsupvaluz3  46038  ioodvbdlimc1lem2  46172  ioodvbdlimc2lem  46174  dvnmul  46183  dvnprodlem1  46186  dvnprodlem2  46187  iblspltprt  46213  itgspltprt  46219  stoweidlem3  46243  stoweidlem11  46251  stoweidlem20  46260  stoweidlem26  46266  stoweidlem34  46274  stoweidlem59  46299  stirlinglem5  46318  dirkertrigeqlem3  46340  dirkeritg  46342  dirkercncflem1  46343  dirkercncflem2  46344  dirkercncflem4  46346  fourierdlem4  46351  fourierdlem6  46353  fourierdlem7  46354  fourierdlem11  46358  fourierdlem12  46359  fourierdlem15  46362  fourierdlem19  46366  fourierdlem20  46367  fourierdlem25  46372  fourierdlem26  46373  fourierdlem34  46381  fourierdlem35  46382  fourierdlem41  46388  fourierdlem48  46394  fourierdlem49  46395  fourierdlem50  46396  fourierdlem51  46397  fourierdlem54  46400  fourierdlem63  46409  fourierdlem64  46410  fourierdlem65  46411  fourierdlem71  46417  fourierdlem79  46425  fourierdlem89  46435  fourierdlem90  46436  fourierdlem91  46437  fourierdlem102  46448  fourierdlem103  46449  fourierdlem104  46450  fourierdlem114  46460  fouriersw  46471  elaa2lem  46473  etransclem3  46477  etransclem4  46478  etransclem7  46481  etransclem10  46484  etransclem15  46489  etransclem19  46493  etransclem23  46497  etransclem24  46498  etransclem25  46499  etransclem27  46501  etransclem31  46505  etransclem32  46506  etransclem35  46509  etransclem41  46515  etransclem44  46518  etransclem46  46520  etransclem48  46522  iundjiun  46700  caratheodorylem1  46766  smflimsuplem4  47063  smfliminflem  47070  ormklocald  47114  ormkglobd  47115  natglobalincr  47117  chnerlem3  47124  2elfz2melfz  47560  elfzelfzlble  47563  fzopredsuc  47565  2ltceilhalf  47570  ceilhalfgt1  47571  ceilhalfnn  47578  submodlt  47592  m1modmmod  47600  difmodm1lt  47601  modmknepk  47604  mod2addne  47606  fsummsndifre  47614  iccpartgt  47669  icceuelpartlem  47677  icceuelpart  47678  iccpartnel  47680  lighneallem2  47848  proththd  47856  dfodd4  47901  oexpnegALTV  47919  nnoALTV  47937  evenltle  47959  fpprwppr  47981  gbowgt5  48004  gboge9  48006  stgoldbwt  48018  sbgoldbst  48020  sbgoldbalt  48023  sgoldbeven3prm  48025  mogoldbb  48027  bgoldbtbndlem1  48047  bgoldbtbndlem2  48048  bgoldbtbndlem3  48049  bgoldbtbnd  48051  bgoldbachlt  48055  tgblthelfgott  48057  tgoldbach  48059  upgrimpthslem2  48150  gpgprismgrusgra  48300  gpgedgvtx1  48304  gpgvtxedg0  48305  gpgvtxedg1  48306  gpg5nbgrvtx13starlem2  48314  gpg3nbgrvtx0  48318  gpg3kgrtriexlem1  48325  gpg3kgrtriexlem4  48328  gpg3kgrtriexlem6  48330  pw2m1lepw2m1  48762  fllogbd  48802  logbpw2m1  48809  fllog2  48810  nnpw2blen  48822  nnolog2flm1  48832  dignn0flhalflem1  48857  dignn0flhalflem2  48858