Theorem zred 12662

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

Syntax hints:   → wi 4   ∈ wcel 2107  ℝcr 11105  ℤcz 12554

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2704

This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3or 1089  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-rab 3434  df-v 3477  df-dif 3950  df-un 3952  df-in 3954  df-ss 3964  df-nul 4322  df-if 4528  df-sn 4628  df-pr 4630  df-op 4634  df-uni 4908  df-br 5148  df-iota 6492  df-fv 6548  df-ov 7407  df-neg 11443  df-z 12555

This theorem is referenced by:  zcnd  12663  suprfinzcl  12672  eluzmn  12825  eluzelre  12829  eluzadd  12847  subeluzsub  12855  uzm1  12856  zsupss  12917  suprzcl2  12918  uzwo3  12923  rpnnen1lem3  12959  rpnnen1lem5  12961  zltaddlt1le  13478  fzsplit2  13522  fzdisj  13524  ssfzunsnext  13542  fzpreddisj  13546  fznatpl1  13551  fzp1disj  13556  uzdisj  13570  fzm1  13577  fz0fzdiffz0  13606  elfzmlbm  13607  elfzmlbp  13608  difelfznle  13611  nn0disj  13613  elfzolt3  13638  fzonel  13642  fzospliti  13660  fzodisj  13662  fzouzdisj  13664  fzodisjsn  13666  fzonmapblen  13674  fzoaddel  13681  elincfzoext  13686  reflcl  13757  flge  13766  flwordi  13773  fladdz  13786  2tnp1ge0ge0  13790  flhalf  13791  fldiv4p1lem1div2  13796  fldiv4lem1div2uz2  13797  fldiv4lem1div2  13798  flleceil  13814  fleqceilz  13815  quoremz  13816  uzsup  13824  modmul12d  13886  modaddmodup  13895  modaddmodlo  13896  modfzo0difsn  13904  modsumfzodifsn  13905  addmodlteq  13907  om2uzlti  13911  om2uzf1oi  13914  seqf1olem1  14003  seqf1olem2  14004  bcval4  14263  bcp1nk  14273  bcval5  14274  fzsdom2  14384  seqcoll  14421  seqcoll2  14422  ccatrn  14535  ccatalpha  14539  cshwidxmodr  14750  fzomaxdiflem  15285  fzomaxdif  15286  rexuzre  15295  limsupgre  15421  rlimclim1  15485  isercoll  15610  iseralt  15627  fsumm1  15693  fsum1p  15695  fsum0diaglem  15718  modfsummods  15735  isumsplit  15782  climcndslem1  15791  mertenslem1  15826  ntrivcvgmul  15844  fprodntriv  15882  fprod1p  15908  fprodeq0  15915  fallfacval4  15983  bpoly4  15999  fzo0dvdseq  16262  dvdsmod  16268  oexpneg  16284  mod2eq1n2dvds  16286  ltoddhalfle  16300  flodddiv4t2lthalf  16355  bitsp1  16368  bitsfzolem  16371  bitsfzo  16372  bitsmod  16373  bitscmp  16375  bitsinv1lem  16378  sadaddlem  16403  bitsres  16410  bitsuz  16411  smumul  16430  gcd0id  16456  gcdneg  16459  dfgcd2  16484  nn0seqcvgd  16503  lcmgcdlem  16539  nprm  16621  prmdvdsfz  16638  isprm5  16640  isprm7  16641  coprm  16644  prmexpb  16653  prmfac1  16654  hashdvds  16704  crth  16707  eulerthlem2  16711  fermltl  16713  prmdiv  16714  prmdiveq  16715  hashgcdlem  16717  odzdvds  16724  vfermltlALT  16731  modprm0  16734  modprmn0modprm0  16736  prm23ge5  16744  pythagtriplem13  16756  pcxcl  16790  pcaddlem  16817  pcadd  16818  pcfac  16828  qexpz  16830  prmunb  16843  1arithlem4  16855  4sqlem5  16871  4sqlem6  16872  4sqlem7  16873  4sqlem10  16876  4sqlem11  16884  4sqlem12  16885  4sqlem15  16888  4sqlem16  16889  4sqlem17  16890  vdwnnlem3  16926  prmgaplem7  16986  cshwshashlem3  17027  subgmulg  19014  mndodconglem  19402  odnncl  19406  odmod  19407  oddvds  19408  dfod2  19425  sylow1lem3  19461  efgsp1  19598  efgredleme  19604  telgsumfzs  19849  zringlpirlem1  21016  zringlpirlem3  21018  znf1o  21091  zcld  24311  ovoliunlem1  25001  ovoliunlem2  25002  dyadss  25093  dyaddisjlem  25094  dyadmaxlem  25096  dvfsumle  25520  dvfsumge  25521  dvfsumabs  25522  dvfsumlem1  25525  dvfsumlem3  25527  degltlem1  25572  plyco0  25688  plyeq0lem  25706  plydivex  25792  aannenlem1  25823  efif1olem2  26034  nnlogbexp  26266  logblt  26269  ang180lem1  26294  ang180lem3  26296  wilthlem2  26553  basellem3  26567  basellem4  26568  ppiprm  26635  chtdif  26642  ppidif  26647  chtub  26695  mersenne  26710  bcmono  26760  bcmax  26761  bposlem1  26767  bposlem3  26769  bposlem5  26771  bposlem6  26772  lgsval2lem  26790  lgsvalmod  26799  lgsneg  26804  lgsmod  26806  lgsdilem  26807  lgsdirprm  26814  lgsdilem2  26816  lgsne0  26818  lgssq  26820  lgssq2  26821  lgsqr  26834  lgsdchr  26838  gausslemma2dlem1a  26848  gausslemma2dlem3  26851  gausslemma2dlem5a  26853  gausslemma2dlem6  26855  gausslemma2d  26857  lgseisenlem1  26858  lgseisenlem2  26859  lgseisenlem3  26860  lgseisenlem4  26861  lgsquadlem1  26863  lgsquadlem2  26864  lgsquadlem3  26865  lgsquad3  26870  2lgslem1a2  26873  2lgslem1  26877  2lgslem2  26878  2sqlem3  26903  2sqlem8  26909  2sqblem  26914  2sqmod  26919  chebbnd1lem1  26952  chebbnd1lem2  26953  chebbnd1lem3  26954  dchrmusum2  26977  dchrvmasumlem1  26978  dchrvmasum2lem  26979  dchrvmasum2if  26980  dchrvmasumlem3  26982  dchrvmasumiflem2  26985  dchrisum0lem1  26999  dchrmusumlem  27005  mudivsum  27013  mulogsumlem  27014  mulogsum  27015  mulog2sumlem2  27018  mulog2sumlem3  27019  selberglem1  27028  selberglem2  27029  pntpbnd1  27069  pntlemg  27081  pntlemf  27088  qabvle  27108  padicabv  27113  padicabvcxp  27115  ostth2lem2  27117  axlowdimlem13  28192  axlowdimlem16  28195  pthdlem1  29003  crctcshwlkn0  29055  crctcsh  29058  clwwisshclwwslemlem  29246  eucrctshift  29476  nndiffz1  31975  fzsplit3  31983  bcm1n  31984  fzone1  31989  suppssnn0  31995  ltesubnnd  32006  wrdt2ind  32095  cshwrnid  32103  cycpmfv2  32251  cycpmco2lem6  32268  cycpmco2lem7  32269  cycpmrn  32280  cyc3conja  32294  pnfinf  32307  fermltlchr  32447  znfermltl  32448  dya2iocress  33211  dya2iocbrsiga  33212  dya2icobrsiga  33213  dya2icoseg  33214  dya2iocucvr  33221  sxbrsigalem2  33223  ballotlemfc0  33429  ballotlemfcc  33430  ballotlemodife  33434  ballotlemimin  33442  ballotlemsgt1  33447  ballotlemsel1i  33449  ballotlemsi  33451  ballotlemsima  33452  ballotlemrv2  33458  ballotlemfrceq  33465  ballotlemfrcn0  33466  ballotlemirc  33468  fsum2dsub  33557  reprlt  33569  reprgt  33571  breprexplemc  33582  tgoldbachgnn  33609  tgoldbachgt  33613  subfacval3  34118  erdszelem8  34127  erdszelem9  34128  supfz  34636  inffz  34637  gg-dvfsumle  35120  dnizeq0  35289  dnizphlfeqhlf  35290  dnibndlem13  35304  knoppndvlem1  35326  knoppndvlem2  35327  knoppndvlem7  35332  knoppndvlem19  35344  knoppndvlem21  35346  ltflcei  36414  leceifl  36415  poimirlem1  36427  poimirlem2  36428  poimirlem6  36432  poimirlem7  36433  poimirlem8  36434  poimirlem15  36441  poimirlem16  36442  poimirlem17  36443  poimirlem19  36445  poimirlem20  36446  poimirlem23  36449  poimirlem24  36450  poimirlem27  36453  poimirlem29  36455  poimirlem31  36457  poimirlem32  36458  mblfinlem2  36464  itg2addnclem2  36478  mettrifi  36563  cntotbnd  36602  fzne2d  40784  aks4d1lem1  40865  aks4d1p1p3  40872  aks4d1p1p2  40873  aks4d1p1p4  40874  aks4d1p1  40879  aks4d1p2  40880  aks4d1p3  40881  aks4d1p5  40883  aks4d1p6  40884  aks4d1p7d1  40885  aks4d1p7  40886  aks4d1p8d3  40889  aks4d1p8  40890  aks4d1p9  40891  2ap1caineq  40899  sticksstones6  40905  sticksstones7  40906  sticksstones10  40909  sticksstones12a  40911  sticksstones12  40912  sticksstones22  40922  metakunt7  40929  metakunt12  40934  metakunt15  40937  metakunt16  40938  metakunt22  40944  metakunt28  40950  prodsplit  40959  frlmvscadiccat  41029  dffltz  41320  lzunuz  41439  lzenom  41441  diophin  41443  irrapxlem1  41493  irrapxlem2  41494  irrapxlem3  41495  irrapxlem4  41496  pellexlem5  41504  pellexlem6  41505  rmspecfund  41580  rmxypos  41619  ltrmynn0  41620  ltrmxnn0  41621  ltrmy  41624  rmyeq0  41625  rmyeq  41626  lermy  41627  rmyabs  41630  jm2.24nn  41631  jm2.17a  41632  jm2.17b  41633  jm2.17c  41634  jm2.24  41635  rmygeid  41636  acongrep  41652  fzmaxdif  41653  acongeq  41655  jm2.22  41667  jm2.23  41668  jm2.26lem3  41673  jm2.27a  41677  jm3.1lem1  41689  jm3.1lem3  41691  expdiophlem1  41693  fzuntd  42140  fzunt1d  42141  fzuntgd  42142  prmunb2  43003  nzprmdif  43011  hashnzfzclim  43014  binomcxplemnn0  43041  uzwo4  43673  ssinc  43709  ssdec  43710  zltlesub  43930  monoords  43942  fzisoeu  43945  fperiodmul  43949  fzdifsuc2  43955  iuneqfzuzlem  43979  uzublem  44075  zxrd  44098  uzinico  44208  uzubioo  44215  fmul01  44231  fmul01lt1lem1  44235  fmul01lt1lem2  44236  climsuselem1  44258  climsuse  44259  sumnnodd  44281  ltmod  44289  limsupresuz  44354  limsupubuzlem  44363  limsupequzlem  44373  limsupmnfuzlem  44377  limsupequzmptlem  44379  limsupre3uzlem  44386  supcnvlimsup  44391  limsup10exlem  44423  liminfresuz  44435  liminfvaluz  44443  limsupvaluz3  44449  ioodvbdlimc1lem2  44583  ioodvbdlimc2lem  44585  dvnmul  44594  dvnprodlem1  44597  dvnprodlem2  44598  iblspltprt  44624  itgspltprt  44630  stoweidlem3  44654  stoweidlem11  44662  stoweidlem20  44671  stoweidlem26  44677  stoweidlem34  44685  stoweidlem59  44710  stirlinglem5  44729  dirkertrigeqlem3  44751  dirkeritg  44753  dirkercncflem1  44754  dirkercncflem2  44755  dirkercncflem4  44757  fourierdlem4  44762  fourierdlem6  44764  fourierdlem7  44765  fourierdlem11  44769  fourierdlem12  44770  fourierdlem15  44773  fourierdlem19  44777  fourierdlem20  44778  fourierdlem25  44783  fourierdlem26  44784  fourierdlem34  44792  fourierdlem35  44793  fourierdlem41  44799  fourierdlem48  44805  fourierdlem49  44806  fourierdlem50  44807  fourierdlem51  44808  fourierdlem54  44811  fourierdlem63  44820  fourierdlem64  44821  fourierdlem65  44822  fourierdlem71  44828  fourierdlem79  44836  fourierdlem89  44846  fourierdlem90  44847  fourierdlem91  44848  fourierdlem102  44859  fourierdlem103  44860  fourierdlem104  44861  fourierdlem114  44871  fouriersw  44882  elaa2lem  44884  etransclem3  44888  etransclem4  44889  etransclem7  44892  etransclem10  44895  etransclem15  44900  etransclem19  44904  etransclem23  44908  etransclem24  44909  etransclem25  44910  etransclem27  44912  etransclem31  44916  etransclem32  44917  etransclem35  44920  etransclem41  44926  etransclem44  44929  etransclem46  44931  etransclem48  44933  iundjiun  45111  caratheodorylem1  45177  smflimsuplem4  45474  smfliminflem  45481  natglobalincr  45526  2elfz2melfz  45961  elfzelfzlble  45964  fzopredsuc  45966  fsummsndifre  45975  iccpartgt  46030  icceuelpartlem  46038  icceuelpart  46039  iccpartnel  46041  lighneallem2  46209  proththd  46217  dfodd4  46262  oexpnegALTV  46280  nnoALTV  46298  evenltle  46320  fpprwppr  46342  gbowgt5  46365  gboge9  46367  stgoldbwt  46379  sbgoldbst  46381  sbgoldbalt  46384  sgoldbeven3prm  46386  mogoldbb  46388  bgoldbtbndlem1  46408  bgoldbtbndlem2  46409  bgoldbtbndlem3  46410  bgoldbtbnd  46412  bgoldbachlt  46416  tgblthelfgott  46418  tgoldbach  46420  pw2m1lepw2m1  47103  m1modmmod  47109  difmodm1lt  47110  fllogbd  47148  logbpw2m1  47155  fllog2  47156  nnpw2blen  47168  nnolog2flm1  47178  dignn0flhalflem1  47203  dignn0flhalflem2  47204