Theorem zred 12718

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

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2146  ℝcr 11117  ℤcz 12609

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2148  ax-9 2156  ax-ext 2738

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3or 1104  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-sb 2100  df-clab 2745  df-cleq 2758  df-clel 2841  df-rab 3420  df-v 3460  df-dif 3911  df-un 3913  df-ss 3925  df-nul 4290  df-if 4493  df-sn 4595  df-pr 4597  df-op 4601  df-uni 4878  df-br 5115  df-iota 6499  df-fv 6551  df-ov 7426  df-neg 11462  df-z 12610

This theorem is used by:  zcnd  12719  suprfinzcl  12728  eluzmn  12887  eluzelre  12891  eluzadd  12909  subeluzsub  12913  uzm1  12914  zsupss  12979  suprzcl2  12980  uzwo3  12985  rpnnen1lem3  13021  rpnnen1lem5  13023  zltaddlt1le  13550  fzsplit2  13596  fzdisj  13598  ssfzunsnext  13616  fzpreddisj  13620  fznatpl1  13625  fzp1disj  13630  uzdisj  13644  fzdif1  13652  fzm1  13654  fz0fzdiffz0  13684  elfzmlbm  13685  elfzmlbp  13686  difelfznle  13689  nn0disj  13691  elfzolt3  13717  fzonel  13721  fzospliti  13739  fzodisj  13741  fzouzdisj  13743  fzodisjsn  13745  elfzo0subge1  13753  elfzo0suble  13754  fzonmapblen  13756  fzoaddel  13765  elincfzoext  13771  fzone1  13832  reflcl  13849  flge  13858  flwordi  13865  fladdz  13878  2tnp1ge0ge0  13882  flhalf  13883  fldiv4p1lem1div2  13888  fldiv4lem1div2uz2  13889  fldiv4lem1div2  13890  flleceil  13906  fleqceilz  13907  quoremz  13908  uzsup  13916  modaddid  13963  modmul12d  13981  modaddmodup  13990  modaddmodlo  13991  modfzo0difsn  13999  modsumfzodifsn  14000  addmodlteq  14002  om2uzlti  14006  om2uzf1oi  14009  seqf1olem1  14097  seqf1olem2  14098  bcval4  14363  bcp1nk  14373  bcval5  14374  fzsdom2  14485  seqcoll  14521  seqcoll2  14522  ccatrn  14647  ccatalpha  14652  cshwidxmodr  14867  fzomaxdiflem  15420  fzomaxdif  15421  rexuzre  15430  limsupgre  15558  rlimclim1  15622  isercoll  15745  iseralt  15762  fsumm1  15828  fsum1p  15830  fsum0diaglem  15853  modfsummods  15871  isumsplit  15920  climcndslem1  15929  mertenslem1  15964  ntrivcvgmul  15982  fprodntriv  16022  fprod1p  16048  fprodeq0  16055  fallfacval4  16122  bpoly4  16138  fzo0dvdseq  16406  dvdsmod  16412  oexpneg  16428  mod2eq1n2dvds  16430  ltoddhalfle  16444  flodddiv4t2lthalf  16501  bitsp1  16514  bitsfzolem  16517  bitsfzo  16518  bitsmod  16519  bitscmp  16521  bitsinv1lem  16524  sadaddlem  16549  bitsres  16556  bitsuz  16557  smumul  16576  gcd0id  16602  gcdneg  16605  dfgcd2  16629  nn0seqcvgd  16653  lcmgcdlem  16689  nprm  16771  prmdvdsfz  16789  isprm5  16791  isprm7  16792  coprm  16795  prmexpb  16803  prmfac1  16804  hashdvds  16859  crth  16862  eulerthlem2  16866  fermltl  16868  prmdiv  16869  prmdiveq  16870  hashgcdlem  16872  odzdvds  16880  vfermltlALT  16887  modprm0  16890  modprmn0modprm0  16892  prm23ge5  16900  pythagtriplem13  16912  pcxcl  16946  pcaddlem  16973  pcadd  16974  pcfac  16984  qexpz  16986  prmunb  16999  1arithlem4  17011  4sqlem5  17027  4sqlem6  17028  4sqlem7  17029  4sqlem10  17032  4sqlem11  17040  4sqlem12  17041  4sqlem15  17044  4sqlem16  17045  4sqlem17  17046  vdwnnlem3  17082  prmgaplem7  17142  cshwshashlem3  17182  chnub  18703  chnso  18705  chnccat  18707  chnpof1  18711  subgmulg  19238  mndodconglem  19642  odnncl  19646  odmod  19647  oddvds  19648  dfod2  19665  sylow1lem3  19701  efgsp1  19838  efgredleme  19844  telgsumfzs  20090  zringlpirlem1  21649  zringlpirlem3  21651  fermltlchr  21716  znf1o  21738  zcld  25008  ovoliunlem1  25698  ovoliunlem2  25699  dyadss  25790  dyaddisjlem  25791  dyadmaxlem  25793  dvfsumle  26217  dvfsumge  26218  dvfsumabs  26219  dvfsumlem1  26222  dvfsumlem3  26224  degltlem1  26266  plyco0  26386  plyeq0lem  26404  plydivex  26495  aannenlem1  26528  efif1olem2  26745  nnlogbexp  26983  logblt  26986  ang180lem1  27011  ang180lem3  27013  wilthlem2  27270  basellem3  27284  basellem4  27285  ppiprm  27352  chtdif  27359  ppidif  27364  chtub  27413  mersenne  27428  bcmono  27478  bcmax  27479  bposlem1  27485  bposlem3  27487  bposlem5  27489  bposlem6  27490  lgsval2lem  27508  lgsvalmod  27517  lgsneg  27522  lgsmod  27524  lgsdilem  27525  lgsdirprm  27532  lgsdilem2  27534  lgsne0  27536  lgssq  27538  lgssq2  27539  lgsqr  27552  lgsdchr  27556  gausslemma2dlem1a  27566  gausslemma2dlem3  27569  gausslemma2dlem5a  27571  gausslemma2dlem6  27573  gausslemma2d  27575  lgseisenlem1  27576  lgseisenlem2  27577  lgseisenlem3  27578  lgseisenlem4  27579  lgsquadlem1  27581  lgsquadlem2  27582  lgsquadlem3  27583  lgsquad3  27588  2lgslem1a2  27591  2lgslem1  27595  2lgslem2  27596  2sqlem3  27621  2sqlem8  27627  2sqblem  27632  2sqmod  27637  chebbnd1lem1  27670  chebbnd1lem2  27671  chebbnd1lem3  27672  dchrmusum2  27695  dchrvmasumlem1  27696  dchrvmasum2lem  27697  dchrvmasum2if  27698  dchrvmasumlem3  27700  dchrvmasumiflem2  27703  dchrisum0lem1  27717  dchrmusumlem  27723  mudivsum  27731  mulogsumlem  27732  mulogsum  27733  mulog2sumlem2  27736  mulog2sumlem3  27737  selberglem1  27746  selberglem2  27747  pntpbnd1  27787  pntlemg  27799  pntlemf  27806  qabvle  27826  padicabv  27831  padicabvcxp  27833  ostth2lem2  27835  axlowdimlem13  29341  axlowdimlem16  29344  pthdlem1  30152  crctcshwlkn0  30207  crctcsh  30210  clwwisshclwwslemlem  30401  eucrctshift  30631  nndiffz1  33168  fzsplit3  33175  bcm1n  33177  suppssnn0  33187  ltesubnnd  33204  wrdt2ind  33306  cshwrnid  33312  cycpmfv2  33465  cycpmco2lem6  33482  cycpmco2lem7  33483  cycpmrn  33494  cyc3conja  33508  pnfinf  33534  znfermltl  33712  constrext2chnlem  34171  cos9thpiminplylem1  34203  cos9thpiminplylem2  34204  dya2iocress  34696  dya2iocbrsiga  34697  dya2icobrsiga  34698  dya2icoseg  34699  dya2iocucvr  34706  sxbrsigalem2  34708  ballotlemfc0  34915  ballotlemfcc  34916  ballotlemodife  34920  ballotlemimin  34928  ballotlemsgt1  34933  ballotlemsel1i  34935  ballotlemsi  34937  ballotlemsima  34938  ballotlemrv2  34944  ballotlemfrceq  34951  ballotlemfrcn0  34952  ballotlemirc  34954  fsum2dsub  35026  reprlt  35038  reprgt  35040  breprexplemc  35051  tgoldbachgnn  35078  tgoldbachgt  35082  subfacval3  35702  erdszelem8  35711  erdszelem9  35712  supfz  36242  inffz  36243  dnizeq0  37105  dnizphlfeqhlf  37106  dnibndlem13  37120  knoppndvlem1  37142  knoppndvlem2  37143  knoppndvlem7  37148  knoppndvlem19  37160  knoppndvlem21  37162  ltflcei  38300  leceifl  38301  poimirlem1  38313  poimirlem2  38314  poimirlem6  38318  poimirlem7  38319  poimirlem8  38320  poimirlem15  38327  poimirlem16  38328  poimirlem17  38329  poimirlem19  38331  poimirlem20  38332  poimirlem23  38335  poimirlem24  38336  poimirlem27  38339  poimirlem29  38341  poimirlem31  38343  poimirlem32  38344  mblfinlem2  38350  itg2addnclem2  38364  mettrifi  38449  cntotbnd  38488  fzne2d  42788  aks4d1lem1  42870  aks4d1p1p3  42877  aks4d1p1p2  42878  aks4d1p1p4  42879  aks4d1p1  42884  aks4d1p2  42885  aks4d1p3  42886  aks4d1p5  42888  aks4d1p6  42889  aks4d1p7d1  42890  aks4d1p7  42891  aks4d1p8d3  42894  aks4d1p8  42895  aks4d1p9  42896  posbezout  42908  aks6d1c1  42924  hashscontpow1  42929  hashscontpow  42930  aks6d1c2  42938  aks6d1c5lem1  42944  2ap1caineq  42953  sticksstones6  42959  sticksstones7  42960  sticksstones10  42963  sticksstones12a  42965  sticksstones12  42966  sticksstones22  42976  bcled  42986  bcle2d  42987  aks6d1c7lem1  42988  aks6d1c7lem2  42989  aks6d1c7  42992  aks5lem6  43000  unitscyglem2  43004  unitscyglem4  43006  aks5lem8  43009  sumcubes  43115  frlmvscadiccat  43321  dffltz  43407  lzunuz  43540  lzenom  43542  diophin  43544  irrapxlem1  43590  irrapxlem2  43591  irrapxlem3  43592  irrapxlem4  43593  pellexlem5  43601  pellexlem6  43602  rmspecfund  43677  rmxypos  43715  ltrmynn0  43716  ltrmxnn0  43717  ltrmy  43720  rmyeq0  43721  rmyeq  43722  lermy  43723  rmyabs  43726  jm2.24nn  43727  jm2.17a  43728  jm2.17b  43729  jm2.17c  43730  jm2.24  43731  rmygeid  43732  acongrep  43748  fzmaxdif  43749  acongeq  43751  jm2.22  43763  jm2.23  43764  jm2.26lem3  43769  jm2.27a  43773  jm3.1lem1  43785  jm3.1lem3  43787  expdiophlem1  43789  fzuntd  44223  fzunt1d  44224  fzuntgd  44225  prmunb2  45062  nzprmdif  45070  hashnzfzclim  45073  binomcxplemnn0  45100  uzwo4  45814  ssinc  45846  ssdec  45847  zltlesub  46045  monoords  46057  fzisoeu  46060  fperiodmul  46064  fzdifsuc2  46070  iuneqfzuzlem  46091  uzublem  46185  zxrd  46208  uzinico  46316  uzubioo  46322  fmul01  46337  fmul01lt1lem1  46341  fmul01lt1lem2  46342  climsuselem1  46364  climsuse  46365  sumnnodd  46387  ltmod  46393  limsupresuz  46458  limsupubuzlem  46467  limsupequzlem  46477  limsupmnfuzlem  46481  limsupequzmptlem  46483  limsupre3uzlem  46490  supcnvlimsup  46495  limsup10exlem  46527  liminfresuz  46539  liminfvaluz  46547  limsupvaluz3  46553  ioodvbdlimc1lem2  46687  ioodvbdlimc2lem  46689  dvnmul  46698  dvnprodlem1  46701  dvnprodlem2  46702  iblspltprt  46728  itgspltprt  46734  stoweidlem3  46758  stoweidlem11  46766  stoweidlem20  46775  stoweidlem26  46781  stoweidlem34  46789  stoweidlem59  46814  stirlinglem5  46833  dirkertrigeqlem3  46855  dirkeritg  46857  dirkercncflem1  46858  dirkercncflem2  46859  dirkercncflem4  46861  fourierdlem4  46866  fourierdlem6  46868  fourierdlem7  46869  fourierdlem11  46873  fourierdlem12  46874  fourierdlem15  46877  fourierdlem19  46881  fourierdlem20  46882  fourierdlem25  46887  fourierdlem26  46888  fourierdlem34  46896  fourierdlem35  46897  fourierdlem41  46903  fourierdlem48  46909  fourierdlem49  46910  fourierdlem50  46911  fourierdlem51  46912  fourierdlem54  46915  fourierdlem63  46924  fourierdlem64  46925  fourierdlem65  46926  fourierdlem71  46932  fourierdlem79  46940  fourierdlem89  46950  fourierdlem90  46951  fourierdlem91  46952  fourierdlem102  46963  fourierdlem103  46964  fourierdlem104  46965  fourierdlem114  46975  fouriersw  46986  elaa2lem  46988  etransclem3  46992  etransclem4  46993  etransclem7  46996  etransclem10  46999  etransclem15  47004  etransclem19  47008  etransclem23  47012  etransclem24  47013  etransclem25  47014  etransclem27  47016  etransclem31  47020  etransclem32  47021  etransclem35  47024  etransclem41  47030  etransclem44  47033  etransclem46  47035  etransclem48  47037  iundjiun  47215  caratheodorylem1  47281  hoicvr  47303  smflimsuplem4  47578  smfliminflem  47585  ormklocald  47631  ormkglobd  47632  natglobalincr  47634  chnerlem3  47641  2elfz2melfz  48096  elfzelfzlble  48099  fzopredsuc  48102  nnmul2  48108  2ltceilhalf  48110  ceilhalfgt1  48111  ceilhalfnn  48118  submodlt  48134  m1modmmod  48142  difmodm1lt  48143  modmknepk  48146  mod2addne  48148  2timesltsq  48156  2timesltsqm1  48157  fsummsndifre  48158  iccpartgt  48217  icceuelpartlem  48225  icceuelpart  48226  iccpartnel  48228  nprmmul2  48318  nprmmul3  48319  lighneallem2  48399  proththd  48407  nprmdvdsfacm1lem4  48416  dfodd4  48465  oexpnegALTV  48483  nnoALTV  48501  evenltle  48523  fpprwppr  48545  gbowgt5  48568  gboge9  48570  stgoldbwt  48582  sbgoldbst  48584  sbgoldbalt  48587  sgoldbeven3prm  48589  mogoldbb  48591  bgoldbtbndlem1  48611  bgoldbtbndlem2  48612  bgoldbtbndlem3  48613  bgoldbtbnd  48615  bgoldbachlt  48619  tgblthelfgott  48621  tgoldbach  48623  upgrimpthslem2  48714  gpgprismgrusgra  48864  gpgedgvtx1  48868  gpgvtxedg0  48869  gpgvtxedg1  48870  gpg5nbgrvtx13starlem2  48878  gpg3nbgrvtx0  48882  gpg3kgrtriexlem1  48889  gpg3kgrtriexlem4  48892  gpg3kgrtriexlem6  48894  pw2m1lepw2m1  49341  fllogbd  49381  logbpw2m1  49388  fllog2  49389  nnpw2blen  49401  nnolog2flm1  49411  dignn0flhalflem1  49436  dignn0flhalflem2  49437