Theorem zred 12624

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

Syntax hints:   → wi 4   ∈ wcel 2114  ℝcr 11028  ℤcz 12515

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3or 1088  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-rab 3391  df-v 3432  df-dif 3893  df-un 3895  df-ss 3907  df-nul 4275  df-if 4468  df-sn 4569  df-pr 4571  df-op 4575  df-uni 4852  df-br 5087  df-iota 6448  df-fv 6500  df-ov 7363  df-neg 11371  df-z 12516

This theorem is referenced by:  zcnd  12625  suprfinzcl  12634  eluzmn  12786  eluzelre  12790  eluzadd  12808  subeluzsub  12812  uzm1  12813  zsupss  12878  suprzcl2  12879  uzwo3  12884  rpnnen1lem3  12920  rpnnen1lem5  12922  zltaddlt1le  13449  fzsplit2  13494  fzdisj  13496  ssfzunsnext  13514  fzpreddisj  13518  fznatpl1  13523  fzp1disj  13528  uzdisj  13542  fzdif1  13550  fzm1  13552  fz0fzdiffz0  13582  elfzmlbm  13583  elfzmlbp  13584  difelfznle  13587  nn0disj  13589  elfzolt3  13615  fzonel  13619  fzospliti  13637  fzodisj  13639  fzouzdisj  13641  fzodisjsn  13643  elfzo0subge1  13651  elfzo0suble  13652  fzonmapblen  13654  fzoaddel  13663  elincfzoext  13669  fzone1  13730  reflcl  13746  flge  13755  flwordi  13762  fladdz  13775  2tnp1ge0ge0  13779  flhalf  13780  fldiv4p1lem1div2  13785  fldiv4lem1div2uz2  13786  fldiv4lem1div2  13787  flleceil  13803  fleqceilz  13804  quoremz  13805  uzsup  13813  modaddid  13860  modmul12d  13878  modaddmodup  13887  modaddmodlo  13888  modfzo0difsn  13896  modsumfzodifsn  13897  addmodlteq  13899  om2uzlti  13903  om2uzf1oi  13906  seqf1olem1  13994  seqf1olem2  13995  bcval4  14260  bcp1nk  14270  bcval5  14271  fzsdom2  14381  seqcoll  14417  seqcoll2  14418  ccatrn  14543  ccatalpha  14547  cshwidxmodr  14757  fzomaxdiflem  15296  fzomaxdif  15297  rexuzre  15306  limsupgre  15434  rlimclim1  15498  isercoll  15621  iseralt  15638  fsumm1  15704  fsum1p  15706  fsum0diaglem  15729  modfsummods  15747  isumsplit  15796  climcndslem1  15805  mertenslem1  15840  ntrivcvgmul  15858  fprodntriv  15898  fprod1p  15924  fprodeq0  15931  fallfacval4  15999  bpoly4  16015  fzo0dvdseq  16283  dvdsmod  16289  oexpneg  16305  mod2eq1n2dvds  16307  ltoddhalfle  16321  flodddiv4t2lthalf  16378  bitsp1  16391  bitsfzolem  16394  bitsfzo  16395  bitsmod  16396  bitscmp  16398  bitsinv1lem  16401  sadaddlem  16426  bitsres  16433  bitsuz  16434  smumul  16453  gcd0id  16479  gcdneg  16482  dfgcd2  16506  nn0seqcvgd  16530  lcmgcdlem  16566  nprm  16648  prmdvdsfz  16666  isprm5  16668  isprm7  16669  coprm  16672  prmexpb  16680  prmfac1  16681  hashdvds  16736  crth  16739  eulerthlem2  16743  fermltl  16745  prmdiv  16746  prmdiveq  16747  hashgcdlem  16749  odzdvds  16757  vfermltlALT  16764  modprm0  16767  modprmn0modprm0  16769  prm23ge5  16777  pythagtriplem13  16789  pcxcl  16823  pcaddlem  16850  pcadd  16851  pcfac  16861  qexpz  16863  prmunb  16876  1arithlem4  16888  4sqlem5  16904  4sqlem6  16905  4sqlem7  16906  4sqlem10  16909  4sqlem11  16917  4sqlem12  16918  4sqlem15  16921  4sqlem16  16922  4sqlem17  16923  vdwnnlem3  16959  prmgaplem7  17019  cshwshashlem3  17059  chnub  18579  chnso  18581  chnccat  18583  chnpof1  18587  subgmulg  19107  mndodconglem  19507  odnncl  19511  odmod  19512  oddvds  19513  dfod2  19530  sylow1lem3  19566  efgsp1  19703  efgredleme  19709  telgsumfzs  19955  zringlpirlem1  21452  zringlpirlem3  21454  fermltlchr  21519  znf1o  21541  zcld  24789  ovoliunlem1  25479  ovoliunlem2  25480  dyadss  25571  dyaddisjlem  25572  dyadmaxlem  25574  dvfsumle  25998  dvfsumge  25999  dvfsumabs  26000  dvfsumlem1  26003  dvfsumlem3  26005  degltlem1  26047  plyco0  26167  plyeq0lem  26185  plydivex  26274  aannenlem1  26305  efif1olem2  26520  nnlogbexp  26758  logblt  26761  ang180lem1  26786  ang180lem3  26788  wilthlem2  27046  basellem3  27060  basellem4  27061  ppiprm  27128  chtdif  27135  ppidif  27140  chtub  27189  mersenne  27204  bcmono  27254  bcmax  27255  bposlem1  27261  bposlem3  27263  bposlem5  27265  bposlem6  27266  lgsval2lem  27284  lgsvalmod  27293  lgsneg  27298  lgsmod  27300  lgsdilem  27301  lgsdirprm  27308  lgsdilem2  27310  lgsne0  27312  lgssq  27314  lgssq2  27315  lgsqr  27328  lgsdchr  27332  gausslemma2dlem1a  27342  gausslemma2dlem3  27345  gausslemma2dlem5a  27347  gausslemma2dlem6  27349  gausslemma2d  27351  lgseisenlem1  27352  lgseisenlem2  27353  lgseisenlem3  27354  lgseisenlem4  27355  lgsquadlem1  27357  lgsquadlem2  27358  lgsquadlem3  27359  lgsquad3  27364  2lgslem1a2  27367  2lgslem1  27371  2lgslem2  27372  2sqlem3  27397  2sqlem8  27403  2sqblem  27408  2sqmod  27413  chebbnd1lem1  27446  chebbnd1lem2  27447  chebbnd1lem3  27448  dchrmusum2  27471  dchrvmasumlem1  27472  dchrvmasum2lem  27473  dchrvmasum2if  27474  dchrvmasumlem3  27476  dchrvmasumiflem2  27479  dchrisum0lem1  27493  dchrmusumlem  27499  mudivsum  27507  mulogsumlem  27508  mulogsum  27509  mulog2sumlem2  27512  mulog2sumlem3  27513  selberglem1  27522  selberglem2  27523  pntpbnd1  27563  pntlemg  27575  pntlemf  27582  qabvle  27602  padicabv  27607  padicabvcxp  27609  ostth2lem2  27611  axlowdimlem13  29037  axlowdimlem16  29040  pthdlem1  29849  crctcshwlkn0  29904  crctcsh  29907  clwwisshclwwslemlem  30098  eucrctshift  30328  nndiffz1  32874  fzsplit3  32881  bcm1n  32883  suppssnn0  32893  ltesubnnd  32911  wrdt2ind  33028  cshwrnid  33036  cycpmfv2  33190  cycpmco2lem6  33207  cycpmco2lem7  33208  cycpmrn  33219  cyc3conja  33233  pnfinf  33259  znfermltl  33441  constrext2chnlem  33910  cos9thpiminplylem1  33942  cos9thpiminplylem2  33943  dya2iocress  34434  dya2iocbrsiga  34435  dya2icobrsiga  34436  dya2icoseg  34437  dya2iocucvr  34444  sxbrsigalem2  34446  ballotlemfc0  34653  ballotlemfcc  34654  ballotlemodife  34658  ballotlemimin  34666  ballotlemsgt1  34671  ballotlemsel1i  34673  ballotlemsi  34675  ballotlemsima  34676  ballotlemrv2  34682  ballotlemfrceq  34689  ballotlemfrcn0  34690  ballotlemirc  34692  fsum2dsub  34767  reprlt  34779  reprgt  34781  breprexplemc  34792  tgoldbachgnn  34819  tgoldbachgt  34823  subfacval3  35387  erdszelem8  35396  erdszelem9  35397  supfz  35927  inffz  35928  dnizeq0  36751  dnizphlfeqhlf  36752  dnibndlem13  36766  knoppndvlem1  36788  knoppndvlem2  36789  knoppndvlem7  36794  knoppndvlem19  36806  knoppndvlem21  36808  ltflcei  37943  leceifl  37944  poimirlem1  37956  poimirlem2  37957  poimirlem6  37961  poimirlem7  37962  poimirlem8  37963  poimirlem15  37970  poimirlem16  37971  poimirlem17  37972  poimirlem19  37974  poimirlem20  37975  poimirlem23  37978  poimirlem24  37979  poimirlem27  37982  poimirlem29  37984  poimirlem31  37986  poimirlem32  37987  mblfinlem2  37993  itg2addnclem2  38007  mettrifi  38092  cntotbnd  38131  fzne2d  42433  aks4d1lem1  42515  aks4d1p1p3  42522  aks4d1p1p2  42523  aks4d1p1p4  42524  aks4d1p1  42529  aks4d1p2  42530  aks4d1p3  42531  aks4d1p5  42533  aks4d1p6  42534  aks4d1p7d1  42535  aks4d1p7  42536  aks4d1p8d3  42539  aks4d1p8  42540  aks4d1p9  42541  posbezout  42553  aks6d1c1  42569  hashscontpow1  42574  hashscontpow  42575  aks6d1c2  42583  aks6d1c5lem1  42589  2ap1caineq  42598  sticksstones6  42604  sticksstones7  42605  sticksstones10  42608  sticksstones12a  42610  sticksstones12  42611  sticksstones22  42621  bcled  42631  bcle2d  42632  aks6d1c7lem1  42633  aks6d1c7lem2  42634  aks6d1c7  42637  aks5lem6  42645  unitscyglem2  42649  unitscyglem4  42651  aks5lem8  42654  sumcubes  42759  frlmvscadiccat  42965  dffltz  43081  lzunuz  43214  lzenom  43216  diophin  43218  irrapxlem1  43268  irrapxlem2  43269  irrapxlem3  43270  irrapxlem4  43271  pellexlem5  43279  pellexlem6  43280  rmspecfund  43355  rmxypos  43393  ltrmynn0  43394  ltrmxnn0  43395  ltrmy  43398  rmyeq0  43399  rmyeq  43400  lermy  43401  rmyabs  43404  jm2.24nn  43405  jm2.17a  43406  jm2.17b  43407  jm2.17c  43408  jm2.24  43409  rmygeid  43410  acongrep  43426  fzmaxdif  43427  acongeq  43429  jm2.22  43441  jm2.23  43442  jm2.26lem3  43447  jm2.27a  43451  jm3.1lem1  43463  jm3.1lem3  43465  expdiophlem1  43467  fzuntd  43901  fzunt1d  43902  fzuntgd  43903  prmunb2  44756  nzprmdif  44764  hashnzfzclim  44767  binomcxplemnn0  44794  uzwo4  45502  ssinc  45535  ssdec  45536  zltlesub  45736  monoords  45748  fzisoeu  45751  fperiodmul  45755  fzdifsuc2  45761  iuneqfzuzlem  45782  uzublem  45876  zxrd  45899  uzinico  46007  uzubioo  46013  fmul01  46028  fmul01lt1lem1  46032  fmul01lt1lem2  46033  climsuselem1  46055  climsuse  46056  sumnnodd  46078  ltmod  46084  limsupresuz  46149  limsupubuzlem  46158  limsupequzlem  46168  limsupmnfuzlem  46172  limsupequzmptlem  46174  limsupre3uzlem  46181  supcnvlimsup  46186  limsup10exlem  46218  liminfresuz  46230  liminfvaluz  46238  limsupvaluz3  46244  ioodvbdlimc1lem2  46378  ioodvbdlimc2lem  46380  dvnmul  46389  dvnprodlem1  46392  dvnprodlem2  46393  iblspltprt  46419  itgspltprt  46425  stoweidlem3  46449  stoweidlem11  46457  stoweidlem20  46466  stoweidlem26  46472  stoweidlem34  46480  stoweidlem59  46505  stirlinglem5  46524  dirkertrigeqlem3  46546  dirkeritg  46548  dirkercncflem1  46549  dirkercncflem2  46550  dirkercncflem4  46552  fourierdlem4  46557  fourierdlem6  46559  fourierdlem7  46560  fourierdlem11  46564  fourierdlem12  46565  fourierdlem15  46568  fourierdlem19  46572  fourierdlem20  46573  fourierdlem25  46578  fourierdlem26  46579  fourierdlem34  46587  fourierdlem35  46588  fourierdlem41  46594  fourierdlem48  46600  fourierdlem49  46601  fourierdlem50  46602  fourierdlem51  46603  fourierdlem54  46606  fourierdlem63  46615  fourierdlem64  46616  fourierdlem65  46617  fourierdlem71  46623  fourierdlem79  46631  fourierdlem89  46641  fourierdlem90  46642  fourierdlem91  46643  fourierdlem102  46654  fourierdlem103  46655  fourierdlem104  46656  fourierdlem114  46666  fouriersw  46677  elaa2lem  46679  etransclem3  46683  etransclem4  46684  etransclem7  46687  etransclem10  46690  etransclem15  46695  etransclem19  46699  etransclem23  46703  etransclem24  46704  etransclem25  46705  etransclem27  46707  etransclem31  46711  etransclem32  46712  etransclem35  46715  etransclem41  46721  etransclem44  46724  etransclem46  46726  etransclem48  46728  iundjiun  46906  caratheodorylem1  46972  hoicvr  46994  smflimsuplem4  47269  smfliminflem  47276  ormklocald  47320  ormkglobd  47321  natglobalincr  47323  chnerlem3  47330  2elfz2melfz  47778  elfzelfzlble  47781  fzopredsuc  47784  nnmul2  47790  2ltceilhalf  47792  ceilhalfgt1  47793  ceilhalfnn  47800  submodlt  47816  m1modmmod  47824  difmodm1lt  47825  modmknepk  47828  mod2addne  47830  2timesltsq  47838  2timesltsqm1  47839  fsummsndifre  47840  iccpartgt  47899  icceuelpartlem  47907  icceuelpart  47908  iccpartnel  47910  nprmmul2  48000  nprmmul3  48001  lighneallem2  48081  proththd  48089  nprmdvdsfacm1lem4  48098  dfodd4  48147  oexpnegALTV  48165  nnoALTV  48183  evenltle  48205  fpprwppr  48227  gbowgt5  48250  gboge9  48252  stgoldbwt  48264  sbgoldbst  48266  sbgoldbalt  48269  sgoldbeven3prm  48271  mogoldbb  48273  bgoldbtbndlem1  48293  bgoldbtbndlem2  48294  bgoldbtbndlem3  48295  bgoldbtbnd  48297  bgoldbachlt  48301  tgblthelfgott  48303  tgoldbach  48305  upgrimpthslem2  48396  gpgprismgrusgra  48546  gpgedgvtx1  48550  gpgvtxedg0  48551  gpgvtxedg1  48552  gpg5nbgrvtx13starlem2  48560  gpg3nbgrvtx0  48564  gpg3kgrtriexlem1  48571  gpg3kgrtriexlem4  48574  gpg3kgrtriexlem6  48576  pw2m1lepw2m1  49008  fllogbd  49048  logbpw2m1  49055  fllog2  49056  nnpw2blen  49068  nnolog2flm1  49078  dignn0flhalflem1  49103  dignn0flhalflem2  49104