Theorem zred 12784

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

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2145  ℝcr 11180  ℤcz 12674

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 2147  ax-9 2155  ax-ext 2733

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 2740  df-cleq 2753  df-clel 2836  df-rab 3414  df-v 3453  df-dif 3902  df-un 3904  df-ss 3916  df-nul 4280  df-if 4483  df-sn 4585  df-pr 4587  df-op 4591  df-uni 4868  df-br 5104  df-iota 6487  df-fv 6539  df-ov 7415  df-neg 11525  df-z 12675

This theorem is used by:  zcnd  12785  suprfinzcl  12794  eluzmn  12953  eluzelre  12957  eluzadd  12975  subeluzsub  12979  uzm1  12980  zsupss  13045  suprzcl2  13046  uzwo3  13051  rpnnen1lem3  13088  rpnnen1lem5  13090  zltaddlt1le  13617  fzsplit2  13663  fzdisj  13665  ssfzunsnext  13683  fzpreddisj  13687  fznatpl1  13692  fzp1disj  13697  uzdisj  13711  fzdif1  13719  fzm1  13721  fz0fzdiffz0  13751  elfzmlbm  13752  elfzmlbp  13753  difelfznle  13756  nn0disj  13758  elfzolt3  13784  fzonel  13788  fzospliti  13806  fzodisj  13808  fzouzdisj  13810  fzodisjsn  13812  elfzo0subge1  13820  elfzo0suble  13821  fzonmapblen  13823  fzoaddel  13832  elincfzoext  13838  fzone1  13899  reflcl  13916  flge  13925  flwordi  13932  fladdz  13945  2tnp1ge0ge0  13949  flhalf  13950  fldiv4p1lem1div2  13955  fldiv4lem1div2uz2  13956  fldiv4lem1div2  13957  flleceil  13973  fleqceilz  13974  quoremz  13975  uzsup  13983  modaddid  14030  modmul12d  14048  modaddmodup  14057  modaddmodlo  14058  modfzo0difsn  14066  modsumfzodifsn  14067  addmodlteq  14069  om2uzlti  14073  om2uzf1oi  14076  seqf1olem1  14164  seqf1olem2  14165  bcval4  14431  bcp1nk  14441  bcval5  14442  fzsdom2  14553  seqcoll  14589  seqcoll2  14590  ccatrn  14715  ccatalpha  14720  cshwidxmodr  14935  fzomaxdiflem  15490  fzomaxdif  15491  rexuzre  15500  limsupgre  15628  rlimclim1  15692  isercoll  15815  iseralt  15832  fsumm1  15897  fsum1p  15899  fsum0diaglem  15922  modfsummods  15940  isumsplit  15989  climcndslem1  15998  mertenslem1  16033  ntrivcvgmul  16051  fprodntriv  16089  fprod1p  16115  fprodeq0  16122  fallfacval4  16189  bpoly4  16205  fzo0dvdseq  16473  dvdsmod  16479  oexpneg  16495  mod2eq1n2dvds  16497  ltoddhalfle  16511  flodddiv4t2lthalf  16568  bitsp1  16581  bitsfzolem  16584  bitsfzo  16585  bitsmod  16586  bitscmp  16588  bitsinv1lem  16591  sadaddlem  16616  bitsres  16623  bitsuz  16624  smumul  16643  gcd0id  16671  gcdneg  16674  dfgcd2  16699  nn0seqcvgd  16725  lcmgcdlem  16761  nprm  16843  prmdvdsfz  16861  isprm5  16863  isprm7  16864  coprm  16867  prmexpb  16875  prmfac1  16876  hashdvds  16932  crth  16935  eulerthlem2  16939  fermltl  16941  prmdiv  16942  prmdiveq  16943  hashgcdlem  16945  odzdvds  16953  vfermltlALT  16960  modprm0  16963  modprmn0modprm0  16965  prm23ge5  16973  pythagtriplem13  16985  pcxcl  17019  pcaddlem  17046  pcadd  17047  pcfac  17057  qexpz  17059  prmunb  17072  1arithlem4  17084  4sqlem5  17100  4sqlem6  17101  4sqlem7  17102  4sqlem10  17105  4sqlem11  17113  4sqlem12  17114  4sqlem15  17117  4sqlem16  17118  4sqlem17  17119  vdwnnlem3  17155  prmgaplem7  17215  cshwshashlem3  17255  chnub  18776  chnso  18778  chnccat  18780  chnpof1  18784  subgmulg  19331  mndodconglem  19735  odnncl  19739  odmod  19740  oddvds  19741  dfod2  19758  sylow1lem3  19794  efgsp1  19931  efgredleme  19937  telgsumfzs  20183  zringlpirlem1  21748  zringlpirlem3  21750  fermltlchr  21815  znf1o  21837  zcld  25113  ovoliunlem1  25803  ovoliunlem2  25804  dyadss  25895  dyaddisjlem  25896  dyadmaxlem  25898  dvfsumle  26321  dvfsumge  26322  dvfsumabs  26323  dvfsumlem1  26326  dvfsumlem3  26328  degltlem1  26370  plyco0  26490  plyeq0lem  26509  plydivex  26600  aannenlem1  26637  efif1olem2  26853  nnlogbexp  27091  logblt  27094  ang180lem1  27119  ang180lem3  27121  wilthlem2  27378  basellem3  27392  basellem4  27393  ppiprm  27460  chtdif  27467  ppidif  27472  chtub  27521  mersenne  27536  bcmono  27586  bcmax  27587  bposlem1  27593  bposlem3  27595  bposlem5  27597  bposlem6  27598  lgsval2lem  27616  lgsvalmod  27625  lgsneg  27630  lgsmod  27632  lgsdilem  27633  lgsdirprm  27640  lgsdilem2  27642  lgsne0  27644  lgssq  27646  lgssq2  27647  lgsqr  27660  lgsdchr  27664  gausslemma2dlem1a  27674  gausslemma2dlem3  27677  gausslemma2dlem5a  27679  gausslemma2dlem6  27681  gausslemma2d  27683  lgseisenlem1  27684  lgseisenlem2  27685  lgseisenlem3  27686  lgseisenlem4  27687  lgsquadlem1  27689  lgsquadlem2  27690  lgsquadlem3  27691  lgsquad3  27696  2lgslem1a2  27699  2lgslem1  27703  2lgslem2  27704  2sqlem3  27729  2sqlem8  27735  2sqblem  27740  2sqmod  27745  chebbnd1lem1  27778  chebbnd1lem2  27779  chebbnd1lem3  27780  dchrmusum2  27803  dchrvmasumlem1  27804  dchrvmasum2lem  27805  dchrvmasum2if  27806  dchrvmasumlem3  27808  dchrvmasumiflem2  27811  dchrisum0lem1  27825  dchrmusumlem  27831  mudivsum  27839  mulogsumlem  27840  mulogsum  27841  mulog2sumlem2  27844  mulog2sumlem3  27845  selberglem1  27854  selberglem2  27855  pntpbnd1  27895  pntlemg  27907  pntlemf  27914  qabvle  27934  padicabv  27939  padicabvcxp  27941  ostth2lem2  27943  axlowdimlem13  29514  axlowdimlem16  29517  pthdlem1  30334  crctcshwlkn0  30392  crctcsh  30395  clwwisshclwwslemlem  30586  eucrctshift  30826  nndiffz1  33360  fzsplit3  33367  bcm1n  33369  suppssnn0  33379  ltesubnnd  33396  wrdt2ind  33498  cshwrnid  33504  cycpmfv2  33657  cycpmco2lem6  33674  cycpmco2lem7  33675  cycpmrn  33686  cyc3conja  33700  pnfinf  33726  znfermltl  33904  constrext2chnlem  34364  cos9thpiminplylem1  34396  cos9thpiminplylem2  34397  dya2iocress  34889  dya2iocbrsiga  34890  dya2icobrsiga  34891  dya2icoseg  34892  dya2iocucvr  34899  sxbrsigalem2  34901  ballotlemfc0  35108  ballotlemfcc  35109  ballotlemodife  35113  ballotlemimin  35121  ballotlemsgt1  35126  ballotlemsel1i  35128  ballotlemsi  35130  ballotlemsima  35131  ballotlemrv2  35137  ballotlemfrceq  35144  ballotlemfrcn0  35145  ballotlemirc  35147  fsum2dsub  35219  reprlt  35231  reprgt  35233  breprexplemc  35244  tgoldbachgnn  35271  tgoldbachgt  35275  subfacval3  35923  erdszelem8  35932  erdszelem9  35933  supfz  36463  inffz  36464  dnizeq0  37311  dnizphlfeqhlf  37312  dnibndlem13  37326  knoppndvlem1  37348  knoppndvlem2  37349  knoppndvlem7  37354  knoppndvlem19  37366  knoppndvlem21  37368  ltflcei  38499  leceifl  38500  poimirlem1  38507  poimirlem2  38508  poimirlem6  38512  poimirlem7  38513  poimirlem8  38514  poimirlem15  38521  poimirlem16  38522  poimirlem17  38523  poimirlem19  38525  poimirlem20  38526  poimirlem23  38529  poimirlem24  38530  poimirlem27  38533  poimirlem29  38535  poimirlem31  38537  poimirlem32  38538  mblfinlem2  38544  itg2addnclem2  38558  mettrifi  38659  cntotbnd  38698  fzne2d  42998  aks4d1lem1  43080  aks4d1p1p3  43087  aks4d1p1p2  43088  aks4d1p1p4  43089  aks4d1p1  43094  aks4d1p2  43095  aks4d1p3  43096  aks4d1p5  43098  aks4d1p6  43099  aks4d1p7d1  43100  aks4d1p7  43101  aks4d1p8d3  43104  aks4d1p8  43105  aks4d1p9  43106  posbezout  43118  aks6d1c1  43134  hashscontpow1  43139  hashscontpow  43140  aks6d1c2  43148  aks6d1c5lem1  43154  2ap1caineq  43163  sticksstones6  43169  sticksstones7  43170  sticksstones10  43173  sticksstones12a  43175  sticksstones12  43176  sticksstones22  43186  bcled  43196  bcle2d  43197  aks6d1c7lem1  43198  aks6d1c7lem2  43199  aks6d1c7  43202  aks5lem6  43210  unitscyglem2  43214  unitscyglem4  43216  aks5lem8  43219  sumcubes  43338  frlmvscadiccat  43538  dffltz  43624  lzunuz  43732  lzenom  43734  diophin  43736  irrapxlem1  43782  irrapxlem2  43783  irrapxlem3  43784  irrapxlem4  43785  pellexlem5  43793  pellexlem6  43794  rmspecfund  43869  rmxypos  43907  ltrmynn0  43908  ltrmxnn0  43909  ltrmy  43912  rmyeq0  43913  rmyeq  43914  lermy  43915  rmyabs  43918  jm2.24nn  43919  jm2.17a  43920  jm2.17b  43921  jm2.17c  43922  jm2.24  43923  rmygeid  43924  acongrep  43940  fzmaxdif  43941  acongeq  43943  jm2.22  43955  jm2.23  43956  jm2.26lem3  43961  jm2.27a  43965  jm3.1lem1  43977  jm3.1lem3  43979  expdiophlem1  43981  fzuntd  44415  fzunt1d  44416  fzuntgd  44417  prmunb2  45254  nzprmdif  45262  hashnzfzclim  45265  binomcxplemnn0  45292  uzwo4  46013  ssinc  46045  ssdec  46046  zltlesub  46244  monoords  46256  fzisoeu  46259  fperiodmul  46263  fzdifsuc2  46269  iuneqfzuzlem  46290  uzublem  46384  zxrd  46407  uzinico  46515  uzubioo  46521  fmul01  46536  fmul01lt1lem1  46540  fmul01lt1lem2  46541  climsuselem1  46563  climsuse  46564  sumnnodd  46586  ltmod  46592  limsupresuz  46657  limsupubuzlem  46666  limsupequzlem  46676  limsupmnfuzlem  46680  limsupequzmptlem  46682  limsupre3uzlem  46689  supcnvlimsup  46694  limsup10exlem  46726  liminfresuz  46738  liminfvaluz  46746  limsupvaluz3  46752  ioodvbdlimc1lem2  46886  ioodvbdlimc2lem  46888  dvnmul  46897  dvnprodlem1  46900  dvnprodlem2  46901  iblspltprt  46927  itgspltprt  46933  stoweidlem3  46957  stoweidlem11  46965  stoweidlem20  46974  stoweidlem26  46980  stoweidlem34  46988  stoweidlem59  47013  stirlinglem5  47032  dirkertrigeqlem3  47054  dirkeritg  47056  dirkercncflem1  47057  dirkercncflem2  47058  dirkercncflem4  47060  fourierdlem4  47065  fourierdlem6  47067  fourierdlem7  47068  fourierdlem11  47072  fourierdlem12  47073  fourierdlem15  47076  fourierdlem19  47080  fourierdlem20  47081  fourierdlem25  47086  fourierdlem26  47087  fourierdlem34  47095  fourierdlem35  47096  fourierdlem41  47102  fourierdlem48  47108  fourierdlem49  47109  fourierdlem50  47110  fourierdlem51  47111  fourierdlem54  47114  fourierdlem63  47123  fourierdlem64  47124  fourierdlem65  47125  fourierdlem71  47131  fourierdlem79  47139  fourierdlem89  47149  fourierdlem90  47150  fourierdlem91  47151  fourierdlem102  47162  fourierdlem103  47163  fourierdlem104  47164  fourierdlem114  47174  fouriersw  47185  elaa2lem  47187  etransclem3  47191  etransclem4  47192  etransclem7  47195  etransclem10  47198  etransclem15  47203  etransclem19  47207  etransclem23  47211  etransclem24  47212  etransclem25  47213  etransclem27  47215  etransclem31  47219  etransclem32  47220  etransclem35  47223  etransclem41  47229  etransclem44  47232  etransclem46  47234  etransclem48  47236  iundjiun  47414  caratheodorylem1  47480  hoicvr  47502  smflimsuplem4  47777  smfliminflem  47784  ormklocald  47830  ormkglobd  47831  chnerlem3  47838  2elfz2melfz  48332  elfzelfzlble  48335  fzopredsuc  48338  nnmul2  48344  2ltceilhalf  48346  ceilhalfgt1  48347  ceilhalfnn  48354  submodlt  48370  m1modmmod  48378  difmodm1lt  48379  modmknepk  48382  mod2addne  48384  2timesltsq  48392  2timesltsqm1  48393  fsummsndifre  48394  iccpartgt  48453  icceuelpartlem  48461  icceuelpart  48462  iccpartnel  48464  nprmmul2  48554  nprmmul3  48555  lighneallem2  48635  proththd  48643  nprmdvdsfacm1lem4  48652  dfodd4  48701  oexpnegALTV  48719  nnoALTV  48737  evenltle  48759  fpprwppr  48781  gbowgt5  48804  gboge9  48806  stgoldbwt  48818  sbgoldbst  48820  sbgoldbalt  48823  sgoldbeven3prm  48825  mogoldbb  48827  bgoldbtbndlem1  48847  bgoldbtbndlem2  48848  bgoldbtbndlem3  48849  bgoldbtbnd  48851  bgoldbachlt  48855  tgblthelfgott  48857  tgoldbach  48859  upgrimpthslem2  48950  gpgprismgrusgra  49100  gpgedgvtx1  49104  gpgvtxedg0  49105  gpgvtxedg1  49106  gpg5nbgrvtx13starlem2  49114  gpg3nbgrvtx0  49118  gpg3kgrtriexlem1  49125  gpg3kgrtriexlem4  49128  gpg3kgrtriexlem6  49130  pw2m1lepw2m1  49576  fllogbd  49616  logbpw2m1  49623  fllog2  49624  nnpw2blen  49636  nnolog2flm1  49646  dignn0flhalflem1  49671  dignn0flhalflem2  49672