Theorem zred 12355

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

Syntax hints:   → wi 4   ∈ wcel 2108  ℝcr 10801  ℤcz 12249

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 844  df-3or 1086  df-3an 1087  df-tru 1542  df-fal 1552  df-ex 1784  df-sb 2069  df-clab 2716  df-cleq 2730  df-clel 2817  df-rab 3072  df-v 3424  df-dif 3886  df-un 3888  df-in 3890  df-ss 3900  df-nul 4254  df-if 4457  df-sn 4559  df-pr 4561  df-op 4565  df-uni 4837  df-br 5071  df-iota 6376  df-fv 6426  df-ov 7258  df-neg 11138  df-z 12250

This theorem is referenced by:  zcnd  12356  suprfinzcl  12365  eluzmn  12518  eluzelre  12522  subeluzsub  12544  uzm1  12545  zsupss  12606  suprzcl2  12607  uzwo3  12612  rpnnen1lem3  12648  rpnnen1lem5  12650  zltaddlt1le  13166  fzsplit2  13210  fzdisj  13212  ssfzunsnext  13230  fzpreddisj  13234  fznatpl1  13239  fzp1disj  13244  uzdisj  13258  fzm1  13265  fz0fzdiffz0  13294  elfzmlbm  13295  elfzmlbp  13296  difelfznle  13299  nn0disj  13301  elfzolt3  13326  fzonel  13329  fzospliti  13347  fzodisj  13349  fzouzdisj  13351  fzodisjsn  13353  fzonmapblen  13361  fzoaddel  13368  elincfzoext  13373  reflcl  13444  flge  13453  flwordi  13460  fladdz  13473  2tnp1ge0ge0  13477  flhalf  13478  fldiv4p1lem1div2  13483  fldiv4lem1div2uz2  13484  fldiv4lem1div2  13485  flleceil  13501  fleqceilz  13502  quoremz  13503  uzsup  13511  modmul12d  13573  modaddmodup  13582  modaddmodlo  13583  modfzo0difsn  13591  modsumfzodifsn  13592  addmodlteq  13594  om2uzlti  13598  om2uzf1oi  13601  seqf1olem1  13690  seqf1olem2  13691  bcval4  13949  bcp1nk  13959  bcval5  13960  fzsdom2  14071  seqcoll  14106  seqcoll2  14107  ccatrn  14222  ccatalpha  14226  cshwidxmodr  14445  fzomaxdiflem  14982  fzomaxdif  14983  rexuzre  14992  limsupgre  15118  rlimclim1  15182  isercoll  15307  iseralt  15324  fsumm1  15391  fsum1p  15393  fsum0diaglem  15416  modfsummods  15433  isumsplit  15480  climcndslem1  15489  mertenslem1  15524  ntrivcvgmul  15542  fprodntriv  15580  fprod1p  15606  fprodeq0  15613  fallfacval4  15681  bpoly4  15697  fzo0dvdseq  15960  dvdsmod  15966  oexpneg  15982  mod2eq1n2dvds  15984  ltoddhalfle  15998  flodddiv4t2lthalf  16053  bitsp1  16066  bitsfzolem  16069  bitsfzo  16070  bitsmod  16071  bitscmp  16073  bitsinv1lem  16076  sadaddlem  16101  bitsres  16108  bitsuz  16109  smumul  16128  gcd0id  16154  gcdneg  16157  dfgcd2  16182  nn0seqcvgd  16203  lcmgcdlem  16239  nprm  16321  prmdvdsfz  16338  isprm5  16340  isprm7  16341  coprm  16344  prmexpb  16353  prmfac1  16354  hashdvds  16404  crth  16407  eulerthlem2  16411  fermltl  16413  prmdiv  16414  prmdiveq  16415  hashgcdlem  16417  odzdvds  16424  vfermltlALT  16431  modprm0  16434  modprmn0modprm0  16436  prm23ge5  16444  pythagtriplem13  16456  pcxcl  16490  pcaddlem  16517  pcadd  16518  pcfac  16528  qexpz  16530  prmunb  16543  1arithlem4  16555  4sqlem5  16571  4sqlem6  16572  4sqlem7  16573  4sqlem10  16576  4sqlem11  16584  4sqlem12  16585  4sqlem15  16588  4sqlem16  16589  4sqlem17  16590  vdwnnlem3  16626  prmgaplem7  16686  cshwshashlem3  16727  subgmulg  18684  mndodconglem  19064  odnncl  19068  odmod  19069  oddvds  19070  dfod2  19086  sylow1lem3  19120  efgsp1  19258  efgredleme  19264  telgsumfzs  19505  zringlpirlem1  20596  zringlpirlem3  20598  znf1o  20671  zcld  23882  ovoliunlem1  24571  ovoliunlem2  24572  dyadss  24663  dyaddisjlem  24664  dyadmaxlem  24666  dvfsumle  25090  dvfsumge  25091  dvfsumabs  25092  dvfsumlem1  25095  dvfsumlem3  25097  degltlem1  25142  plyco0  25258  plyeq0lem  25276  plydivex  25362  aannenlem1  25393  efif1olem2  25604  nnlogbexp  25836  logblt  25839  ang180lem1  25864  ang180lem3  25866  wilthlem2  26123  basellem3  26137  basellem4  26138  ppiprm  26205  chtdif  26212  ppidif  26217  chtub  26265  mersenne  26280  bcmono  26330  bcmax  26331  bposlem1  26337  bposlem3  26339  bposlem5  26341  bposlem6  26342  lgsval2lem  26360  lgsvalmod  26369  lgsneg  26374  lgsmod  26376  lgsdilem  26377  lgsdirprm  26384  lgsdilem2  26386  lgsne0  26388  lgssq  26390  lgssq2  26391  lgsqr  26404  lgsdchr  26408  gausslemma2dlem1a  26418  gausslemma2dlem3  26421  gausslemma2dlem5a  26423  gausslemma2dlem6  26425  gausslemma2d  26427  lgseisenlem1  26428  lgseisenlem2  26429  lgseisenlem3  26430  lgseisenlem4  26431  lgsquadlem1  26433  lgsquadlem2  26434  lgsquadlem3  26435  lgsquad3  26440  2lgslem1a2  26443  2lgslem1  26447  2lgslem2  26448  2sqlem3  26473  2sqlem8  26479  2sqblem  26484  2sqmod  26489  chebbnd1lem1  26522  chebbnd1lem2  26523  chebbnd1lem3  26524  dchrmusum2  26547  dchrvmasumlem1  26548  dchrvmasum2lem  26549  dchrvmasum2if  26550  dchrvmasumlem3  26552  dchrvmasumiflem2  26555  dchrisum0lem1  26569  dchrmusumlem  26575  mudivsum  26583  mulogsumlem  26584  mulogsum  26585  mulog2sumlem2  26588  mulog2sumlem3  26589  selberglem1  26598  selberglem2  26599  pntpbnd1  26639  pntlemg  26651  pntlemf  26658  qabvle  26678  padicabv  26683  padicabvcxp  26685  ostth2lem2  26687  axlowdimlem13  27225  axlowdimlem16  27228  pthdlem1  28035  crctcshwlkn0  28087  crctcsh  28090  clwwisshclwwslemlem  28278  eucrctshift  28508  nndiffz1  31009  fzsplit3  31017  bcm1n  31018  fzone1  31023  ltesubnnd  31038  wrdt2ind  31127  cshwrnid  31135  cycpmfv2  31283  cycpmco2lem6  31300  cycpmco2lem7  31301  cycpmrn  31312  cyc3conja  31326  pnfinf  31339  znfermltl  31464  dya2iocress  32141  dya2iocbrsiga  32142  dya2icobrsiga  32143  dya2icoseg  32144  dya2iocucvr  32151  sxbrsigalem2  32153  ballotlemfc0  32359  ballotlemfcc  32360  ballotlemodife  32364  ballotlemimin  32372  ballotlemsgt1  32377  ballotlemsel1i  32379  ballotlemsi  32381  ballotlemsima  32382  ballotlemrv2  32388  ballotlemfrceq  32395  ballotlemfrcn0  32396  ballotlemirc  32398  fsum2dsub  32487  reprlt  32499  reprgt  32501  breprexplemc  32512  tgoldbachgnn  32539  tgoldbachgt  32543  subfacval3  33051  erdszelem8  33060  erdszelem9  33061  supfz  33600  inffz  33601  dnizeq0  34582  dnizphlfeqhlf  34583  dnibndlem13  34597  knoppndvlem1  34619  knoppndvlem2  34620  knoppndvlem7  34625  knoppndvlem19  34637  knoppndvlem21  34639  ltflcei  35692  leceifl  35693  poimirlem1  35705  poimirlem2  35706  poimirlem6  35710  poimirlem7  35711  poimirlem8  35712  poimirlem15  35719  poimirlem16  35720  poimirlem17  35721  poimirlem19  35723  poimirlem20  35724  poimirlem23  35727  poimirlem24  35728  poimirlem27  35731  poimirlem29  35733  poimirlem31  35735  poimirlem32  35736  mblfinlem2  35742  itg2addnclem2  35756  mettrifi  35842  cntotbnd  35881  fzne2d  39917  aks4d1lem1  39998  aks4d1p1p3  40005  aks4d1p1p2  40006  aks4d1p1p4  40007  aks4d1p1  40012  aks4d1p2  40013  aks4d1p3  40014  aks4d1p5  40016  aks4d1p6  40017  aks4d1p7d1  40018  aks4d1p7  40019  aks4d1p8d3  40022  aks4d1p8  40023  aks4d1p9  40024  2ap1caineq  40029  sticksstones6  40035  sticksstones7  40036  sticksstones10  40039  sticksstones12a  40041  sticksstones12  40042  sticksstones22  40052  metakunt7  40059  metakunt12  40064  metakunt15  40067  metakunt16  40068  metakunt22  40074  metakunt28  40080  prodsplit  40089  frlmvscadiccat  40163  dffltz  40387  lzunuz  40506  lzenom  40508  diophin  40510  irrapxlem1  40560  irrapxlem2  40561  irrapxlem3  40562  irrapxlem4  40563  pellexlem5  40571  pellexlem6  40572  rmspecfund  40647  rmxypos  40685  ltrmynn0  40686  ltrmxnn0  40687  ltrmy  40690  rmyeq0  40691  rmyeq  40692  lermy  40693  rmyabs  40696  jm2.24nn  40697  jm2.17a  40698  jm2.17b  40699  jm2.17c  40700  jm2.24  40701  rmygeid  40702  acongrep  40718  fzmaxdif  40719  acongeq  40721  jm2.22  40733  jm2.23  40734  jm2.26lem3  40739  jm2.27a  40743  jm3.1lem1  40755  jm3.1lem3  40757  expdiophlem1  40759  prmunb2  41818  nzprmdif  41826  hashnzfzclim  41829  binomcxplemnn0  41856  uzwo4  42490  ssinc  42526  ssdec  42527  zltlesub  42713  monoords  42726  fzisoeu  42729  fperiodmul  42733  fzdifsuc2  42739  iuneqfzuzlem  42763  uzublem  42860  zxrd  42883  uzinico  42988  uzubioo  42995  fmul01  43011  fmul01lt1lem1  43015  fmul01lt1lem2  43016  climsuselem1  43038  climsuse  43039  sumnnodd  43061  ltmod  43069  limsupresuz  43134  limsupubuzlem  43143  limsupequzlem  43153  limsupmnfuzlem  43157  limsupequzmptlem  43159  limsupre3uzlem  43166  supcnvlimsup  43171  limsup10exlem  43203  liminfresuz  43215  liminfvaluz  43223  limsupvaluz3  43229  ioodvbdlimc1lem2  43363  ioodvbdlimc2lem  43365  dvnmul  43374  dvnprodlem1  43377  dvnprodlem2  43378  iblspltprt  43404  itgspltprt  43410  stoweidlem3  43434  stoweidlem11  43442  stoweidlem20  43451  stoweidlem26  43457  stoweidlem34  43465  stoweidlem59  43490  stirlinglem5  43509  dirkertrigeqlem3  43531  dirkeritg  43533  dirkercncflem1  43534  dirkercncflem2  43535  dirkercncflem4  43537  fourierdlem4  43542  fourierdlem6  43544  fourierdlem7  43545  fourierdlem11  43549  fourierdlem12  43550  fourierdlem15  43553  fourierdlem19  43557  fourierdlem20  43558  fourierdlem25  43563  fourierdlem26  43564  fourierdlem34  43572  fourierdlem35  43573  fourierdlem41  43579  fourierdlem48  43585  fourierdlem49  43586  fourierdlem50  43587  fourierdlem51  43588  fourierdlem54  43591  fourierdlem63  43600  fourierdlem64  43601  fourierdlem65  43602  fourierdlem71  43608  fourierdlem79  43616  fourierdlem89  43626  fourierdlem90  43627  fourierdlem91  43628  fourierdlem102  43639  fourierdlem103  43640  fourierdlem104  43641  fourierdlem114  43651  fouriersw  43662  elaa2lem  43664  etransclem3  43668  etransclem4  43669  etransclem7  43672  etransclem10  43675  etransclem15  43680  etransclem19  43684  etransclem23  43688  etransclem24  43689  etransclem25  43690  etransclem27  43692  etransclem31  43696  etransclem32  43697  etransclem35  43700  etransclem41  43706  etransclem44  43709  etransclem46  43711  etransclem48  43713  iundjiun  43888  caratheodorylem1  43954  smflimsuplem4  44243  smfliminflem  44250  2elfz2melfz  44698  elfzelfzlble  44701  fzopredsuc  44703  fsummsndifre  44712  iccpartgt  44767  icceuelpartlem  44775  icceuelpart  44776  iccpartnel  44778  lighneallem2  44946  proththd  44954  dfodd4  44999  oexpnegALTV  45017  nnoALTV  45035  evenltle  45057  fpprwppr  45079  gbowgt5  45102  gboge9  45104  stgoldbwt  45116  sbgoldbst  45118  sbgoldbalt  45121  sgoldbeven3prm  45123  mogoldbb  45125  bgoldbtbndlem1  45145  bgoldbtbndlem2  45146  bgoldbtbndlem3  45147  bgoldbtbnd  45149  bgoldbachlt  45153  tgblthelfgott  45155  tgoldbach  45157  pw2m1lepw2m1  45749  m1modmmod  45755  difmodm1lt  45756  fllogbd  45794  logbpw2m1  45801  fllog2  45802  nnpw2blen  45814  nnolog2flm1  45824  dignn0flhalflem1  45849  dignn0flhalflem2  45850