Theorem zred 12596

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

Syntax hints:   → wi 4   ∈ wcel 2113  ℝcr 11025  ℤcz 12488

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-sb 2068  df-clab 2715  df-cleq 2728  df-clel 2811  df-rab 3400  df-v 3442  df-dif 3904  df-un 3906  df-ss 3918  df-nul 4286  df-if 4480  df-sn 4581  df-pr 4583  df-op 4587  df-uni 4864  df-br 5099  df-iota 6448  df-fv 6500  df-ov 7361  df-neg 11367  df-z 12489

This theorem is referenced by:  zcnd  12597  suprfinzcl  12606  eluzmn  12758  eluzelre  12762  eluzadd  12780  subeluzsub  12784  uzm1  12785  zsupss  12850  suprzcl2  12851  uzwo3  12856  rpnnen1lem3  12892  rpnnen1lem5  12894  zltaddlt1le  13421  fzsplit2  13465  fzdisj  13467  ssfzunsnext  13485  fzpreddisj  13489  fznatpl1  13494  fzp1disj  13499  uzdisj  13513  fzdif1  13521  fzm1  13523  fz0fzdiffz0  13553  elfzmlbm  13554  elfzmlbp  13555  difelfznle  13558  nn0disj  13560  elfzolt3  13585  fzonel  13589  fzospliti  13607  fzodisj  13609  fzouzdisj  13611  fzodisjsn  13613  elfzo0subge1  13621  elfzo0suble  13622  fzonmapblen  13624  fzoaddel  13633  elincfzoext  13639  fzone1  13700  reflcl  13716  flge  13725  flwordi  13732  fladdz  13745  2tnp1ge0ge0  13749  flhalf  13750  fldiv4p1lem1div2  13755  fldiv4lem1div2uz2  13756  fldiv4lem1div2  13757  flleceil  13773  fleqceilz  13774  quoremz  13775  uzsup  13783  modaddid  13830  modmul12d  13848  modaddmodup  13857  modaddmodlo  13858  modfzo0difsn  13866  modsumfzodifsn  13867  addmodlteq  13869  om2uzlti  13873  om2uzf1oi  13876  seqf1olem1  13964  seqf1olem2  13965  bcval4  14230  bcp1nk  14240  bcval5  14241  fzsdom2  14351  seqcoll  14387  seqcoll2  14388  ccatrn  14513  ccatalpha  14517  cshwidxmodr  14727  fzomaxdiflem  15266  fzomaxdif  15267  rexuzre  15276  limsupgre  15404  rlimclim1  15468  isercoll  15591  iseralt  15608  fsumm1  15674  fsum1p  15676  fsum0diaglem  15699  modfsummods  15716  isumsplit  15763  climcndslem1  15772  mertenslem1  15807  ntrivcvgmul  15825  fprodntriv  15865  fprod1p  15891  fprodeq0  15898  fallfacval4  15966  bpoly4  15982  fzo0dvdseq  16250  dvdsmod  16256  oexpneg  16272  mod2eq1n2dvds  16274  ltoddhalfle  16288  flodddiv4t2lthalf  16345  bitsp1  16358  bitsfzolem  16361  bitsfzo  16362  bitsmod  16363  bitscmp  16365  bitsinv1lem  16368  sadaddlem  16393  bitsres  16400  bitsuz  16401  smumul  16420  gcd0id  16446  gcdneg  16449  dfgcd2  16473  nn0seqcvgd  16497  lcmgcdlem  16533  nprm  16615  prmdvdsfz  16632  isprm5  16634  isprm7  16635  coprm  16638  prmexpb  16646  prmfac1  16647  hashdvds  16702  crth  16705  eulerthlem2  16709  fermltl  16711  prmdiv  16712  prmdiveq  16713  hashgcdlem  16715  odzdvds  16723  vfermltlALT  16730  modprm0  16733  modprmn0modprm0  16735  prm23ge5  16743  pythagtriplem13  16755  pcxcl  16789  pcaddlem  16816  pcadd  16817  pcfac  16827  qexpz  16829  prmunb  16842  1arithlem4  16854  4sqlem5  16870  4sqlem6  16871  4sqlem7  16872  4sqlem10  16875  4sqlem11  16883  4sqlem12  16884  4sqlem15  16887  4sqlem16  16888  4sqlem17  16889  vdwnnlem3  16925  prmgaplem7  16985  cshwshashlem3  17025  chnub  18545  chnso  18547  chnccat  18549  chnpof1  18553  subgmulg  19070  mndodconglem  19470  odnncl  19474  odmod  19475  oddvds  19476  dfod2  19493  sylow1lem3  19529  efgsp1  19666  efgredleme  19672  telgsumfzs  19918  zringlpirlem1  21417  zringlpirlem3  21419  fermltlchr  21484  znf1o  21506  zcld  24758  ovoliunlem1  25459  ovoliunlem2  25460  dyadss  25551  dyaddisjlem  25552  dyadmaxlem  25554  dvfsumle  25982  dvfsumleOLD  25983  dvfsumge  25984  dvfsumabs  25985  dvfsumlem1  25988  dvfsumlem3  25991  degltlem1  26033  plyco0  26153  plyeq0lem  26171  plydivex  26261  aannenlem1  26292  efif1olem2  26508  nnlogbexp  26747  logblt  26750  ang180lem1  26775  ang180lem3  26777  wilthlem2  27035  basellem3  27049  basellem4  27050  ppiprm  27117  chtdif  27124  ppidif  27129  chtub  27179  mersenne  27194  bcmono  27244  bcmax  27245  bposlem1  27251  bposlem3  27253  bposlem5  27255  bposlem6  27256  lgsval2lem  27274  lgsvalmod  27283  lgsneg  27288  lgsmod  27290  lgsdilem  27291  lgsdirprm  27298  lgsdilem2  27300  lgsne0  27302  lgssq  27304  lgssq2  27305  lgsqr  27318  lgsdchr  27322  gausslemma2dlem1a  27332  gausslemma2dlem3  27335  gausslemma2dlem5a  27337  gausslemma2dlem6  27339  gausslemma2d  27341  lgseisenlem1  27342  lgseisenlem2  27343  lgseisenlem3  27344  lgseisenlem4  27345  lgsquadlem1  27347  lgsquadlem2  27348  lgsquadlem3  27349  lgsquad3  27354  2lgslem1a2  27357  2lgslem1  27361  2lgslem2  27362  2sqlem3  27387  2sqlem8  27393  2sqblem  27398  2sqmod  27403  chebbnd1lem1  27436  chebbnd1lem2  27437  chebbnd1lem3  27438  dchrmusum2  27461  dchrvmasumlem1  27462  dchrvmasum2lem  27463  dchrvmasum2if  27464  dchrvmasumlem3  27466  dchrvmasumiflem2  27469  dchrisum0lem1  27483  dchrmusumlem  27489  mudivsum  27497  mulogsumlem  27498  mulogsum  27499  mulog2sumlem2  27502  mulog2sumlem3  27503  selberglem1  27512  selberglem2  27513  pntpbnd1  27553  pntlemg  27565  pntlemf  27572  qabvle  27592  padicabv  27597  padicabvcxp  27599  ostth2lem2  27601  axlowdimlem13  29027  axlowdimlem16  29030  pthdlem1  29839  crctcshwlkn0  29894  crctcsh  29897  clwwisshclwwslemlem  30088  eucrctshift  30318  nndiffz1  32866  fzsplit3  32873  bcm1n  32875  suppssnn0  32885  ltesubnnd  32903  wrdt2ind  33035  cshwrnid  33043  cycpmfv2  33196  cycpmco2lem6  33213  cycpmco2lem7  33214  cycpmrn  33225  cyc3conja  33239  pnfinf  33265  znfermltl  33447  constrext2chnlem  33907  cos9thpiminplylem1  33939  cos9thpiminplylem2  33940  dya2iocress  34431  dya2iocbrsiga  34432  dya2icobrsiga  34433  dya2icoseg  34434  dya2iocucvr  34441  sxbrsigalem2  34443  ballotlemfc0  34650  ballotlemfcc  34651  ballotlemodife  34655  ballotlemimin  34663  ballotlemsgt1  34668  ballotlemsel1i  34670  ballotlemsi  34672  ballotlemsima  34673  ballotlemrv2  34679  ballotlemfrceq  34686  ballotlemfrcn0  34687  ballotlemirc  34689  fsum2dsub  34764  reprlt  34776  reprgt  34778  breprexplemc  34789  tgoldbachgnn  34816  tgoldbachgt  34820  subfacval3  35383  erdszelem8  35392  erdszelem9  35393  supfz  35923  inffz  35924  dnizeq0  36675  dnizphlfeqhlf  36676  dnibndlem13  36690  knoppndvlem1  36712  knoppndvlem2  36713  knoppndvlem7  36718  knoppndvlem19  36730  knoppndvlem21  36732  ltflcei  37809  leceifl  37810  poimirlem1  37822  poimirlem2  37823  poimirlem6  37827  poimirlem7  37828  poimirlem8  37829  poimirlem15  37836  poimirlem16  37837  poimirlem17  37838  poimirlem19  37840  poimirlem20  37841  poimirlem23  37844  poimirlem24  37845  poimirlem27  37848  poimirlem29  37850  poimirlem31  37852  poimirlem32  37853  mblfinlem2  37859  itg2addnclem2  37873  mettrifi  37958  cntotbnd  37997  fzne2d  42234  aks4d1lem1  42316  aks4d1p1p3  42323  aks4d1p1p2  42324  aks4d1p1p4  42325  aks4d1p1  42330  aks4d1p2  42331  aks4d1p3  42332  aks4d1p5  42334  aks4d1p6  42335  aks4d1p7d1  42336  aks4d1p7  42337  aks4d1p8d3  42340  aks4d1p8  42341  aks4d1p9  42342  posbezout  42354  aks6d1c1  42370  hashscontpow1  42375  hashscontpow  42376  aks6d1c2  42384  aks6d1c5lem1  42390  2ap1caineq  42399  sticksstones6  42405  sticksstones7  42406  sticksstones10  42409  sticksstones12a  42411  sticksstones12  42412  sticksstones22  42422  bcled  42432  bcle2d  42433  aks6d1c7lem1  42434  aks6d1c7lem2  42435  aks6d1c7  42438  aks5lem6  42446  unitscyglem2  42450  unitscyglem4  42452  aks5lem8  42455  sumcubes  42568  frlmvscadiccat  42761  dffltz  42877  lzunuz  43010  lzenom  43012  diophin  43014  irrapxlem1  43064  irrapxlem2  43065  irrapxlem3  43066  irrapxlem4  43067  pellexlem5  43075  pellexlem6  43076  rmspecfund  43151  rmxypos  43189  ltrmynn0  43190  ltrmxnn0  43191  ltrmy  43194  rmyeq0  43195  rmyeq  43196  lermy  43197  rmyabs  43200  jm2.24nn  43201  jm2.17a  43202  jm2.17b  43203  jm2.17c  43204  jm2.24  43205  rmygeid  43206  acongrep  43222  fzmaxdif  43223  acongeq  43225  jm2.22  43237  jm2.23  43238  jm2.26lem3  43243  jm2.27a  43247  jm3.1lem1  43259  jm3.1lem3  43261  expdiophlem1  43263  fzuntd  43697  fzunt1d  43698  fzuntgd  43699  prmunb2  44552  nzprmdif  44560  hashnzfzclim  44563  binomcxplemnn0  44590  uzwo4  45298  ssinc  45331  ssdec  45332  zltlesub  45533  monoords  45545  fzisoeu  45548  fperiodmul  45552  fzdifsuc2  45558  iuneqfzuzlem  45579  uzublem  45674  zxrd  45697  uzinico  45805  uzubioo  45811  fmul01  45826  fmul01lt1lem1  45830  fmul01lt1lem2  45831  climsuselem1  45853  climsuse  45854  sumnnodd  45876  ltmod  45882  limsupresuz  45947  limsupubuzlem  45956  limsupequzlem  45966  limsupmnfuzlem  45970  limsupequzmptlem  45972  limsupre3uzlem  45979  supcnvlimsup  45984  limsup10exlem  46016  liminfresuz  46028  liminfvaluz  46036  limsupvaluz3  46042  ioodvbdlimc1lem2  46176  ioodvbdlimc2lem  46178  dvnmul  46187  dvnprodlem1  46190  dvnprodlem2  46191  iblspltprt  46217  itgspltprt  46223  stoweidlem3  46247  stoweidlem11  46255  stoweidlem20  46264  stoweidlem26  46270  stoweidlem34  46278  stoweidlem59  46303  stirlinglem5  46322  dirkertrigeqlem3  46344  dirkeritg  46346  dirkercncflem1  46347  dirkercncflem2  46348  dirkercncflem4  46350  fourierdlem4  46355  fourierdlem6  46357  fourierdlem7  46358  fourierdlem11  46362  fourierdlem12  46363  fourierdlem15  46366  fourierdlem19  46370  fourierdlem20  46371  fourierdlem25  46376  fourierdlem26  46377  fourierdlem34  46385  fourierdlem35  46386  fourierdlem41  46392  fourierdlem48  46398  fourierdlem49  46399  fourierdlem50  46400  fourierdlem51  46401  fourierdlem54  46404  fourierdlem63  46413  fourierdlem64  46414  fourierdlem65  46415  fourierdlem71  46421  fourierdlem79  46429  fourierdlem89  46439  fourierdlem90  46440  fourierdlem91  46441  fourierdlem102  46452  fourierdlem103  46453  fourierdlem104  46454  fourierdlem114  46464  fouriersw  46475  elaa2lem  46477  etransclem3  46481  etransclem4  46482  etransclem7  46485  etransclem10  46488  etransclem15  46493  etransclem19  46497  etransclem23  46501  etransclem24  46502  etransclem25  46503  etransclem27  46505  etransclem31  46509  etransclem32  46510  etransclem35  46513  etransclem41  46519  etransclem44  46522  etransclem46  46524  etransclem48  46526  iundjiun  46704  caratheodorylem1  46770  smflimsuplem4  47067  smfliminflem  47074  ormklocald  47118  ormkglobd  47119  natglobalincr  47121  chnerlem3  47128  2elfz2melfz  47564  elfzelfzlble  47567  fzopredsuc  47569  2ltceilhalf  47574  ceilhalfgt1  47575  ceilhalfnn  47582  submodlt  47596  m1modmmod  47604  difmodm1lt  47605  modmknepk  47608  mod2addne  47610  fsummsndifre  47618  iccpartgt  47673  icceuelpartlem  47681  icceuelpart  47682  iccpartnel  47684  lighneallem2  47852  proththd  47860  dfodd4  47905  oexpnegALTV  47923  nnoALTV  47941  evenltle  47963  fpprwppr  47985  gbowgt5  48008  gboge9  48010  stgoldbwt  48022  sbgoldbst  48024  sbgoldbalt  48027  sgoldbeven3prm  48029  mogoldbb  48031  bgoldbtbndlem1  48051  bgoldbtbndlem2  48052  bgoldbtbndlem3  48053  bgoldbtbnd  48055  bgoldbachlt  48059  tgblthelfgott  48061  tgoldbach  48063  upgrimpthslem2  48154  gpgprismgrusgra  48304  gpgedgvtx1  48308  gpgvtxedg0  48309  gpgvtxedg1  48310  gpg5nbgrvtx13starlem2  48318  gpg3nbgrvtx0  48322  gpg3kgrtriexlem1  48329  gpg3kgrtriexlem4  48332  gpg3kgrtriexlem6  48334  pw2m1lepw2m1  48766  fllogbd  48806  logbpw2m1  48813  fllog2  48814  nnpw2blen  48826  nnolog2flm1  48836  dignn0flhalflem1  48861  dignn0flhalflem2  48862