Theorem zred 12583

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

Syntax hints:   → wi 4   ∈ wcel 2113  ℝcr 11012  ℤcz 12475

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 2705

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 2712  df-cleq 2725  df-clel 2808  df-rab 3397  df-v 3439  df-dif 3901  df-un 3903  df-ss 3915  df-nul 4283  df-if 4475  df-sn 4576  df-pr 4578  df-op 4582  df-uni 4859  df-br 5094  df-iota 6442  df-fv 6494  df-ov 7355  df-neg 11354  df-z 12476

This theorem is referenced by:  zcnd  12584  suprfinzcl  12593  eluzmn  12745  eluzelre  12749  eluzadd  12767  subeluzsub  12771  uzm1  12772  zsupss  12837  suprzcl2  12838  uzwo3  12843  rpnnen1lem3  12879  rpnnen1lem5  12881  zltaddlt1le  13407  fzsplit2  13451  fzdisj  13453  ssfzunsnext  13471  fzpreddisj  13475  fznatpl1  13480  fzp1disj  13485  uzdisj  13499  fzdif1  13507  fzm1  13509  fz0fzdiffz0  13539  elfzmlbm  13540  elfzmlbp  13541  difelfznle  13544  nn0disj  13546  elfzolt3  13571  fzonel  13575  fzospliti  13593  fzodisj  13595  fzouzdisj  13597  fzodisjsn  13599  elfzo0subge1  13607  elfzo0suble  13608  fzonmapblen  13610  fzoaddel  13619  elincfzoext  13625  fzone1  13686  reflcl  13702  flge  13711  flwordi  13718  fladdz  13731  2tnp1ge0ge0  13735  flhalf  13736  fldiv4p1lem1div2  13741  fldiv4lem1div2uz2  13742  fldiv4lem1div2  13743  flleceil  13759  fleqceilz  13760  quoremz  13761  uzsup  13769  modaddid  13816  modmul12d  13834  modaddmodup  13843  modaddmodlo  13844  modfzo0difsn  13852  modsumfzodifsn  13853  addmodlteq  13855  om2uzlti  13859  om2uzf1oi  13862  seqf1olem1  13950  seqf1olem2  13951  bcval4  14216  bcp1nk  14226  bcval5  14227  fzsdom2  14337  seqcoll  14373  seqcoll2  14374  ccatrn  14499  ccatalpha  14503  cshwidxmodr  14713  fzomaxdiflem  15252  fzomaxdif  15253  rexuzre  15262  limsupgre  15390  rlimclim1  15454  isercoll  15577  iseralt  15594  fsumm1  15660  fsum1p  15662  fsum0diaglem  15685  modfsummods  15702  isumsplit  15749  climcndslem1  15758  mertenslem1  15793  ntrivcvgmul  15811  fprodntriv  15851  fprod1p  15877  fprodeq0  15884  fallfacval4  15952  bpoly4  15968  fzo0dvdseq  16236  dvdsmod  16242  oexpneg  16258  mod2eq1n2dvds  16260  ltoddhalfle  16274  flodddiv4t2lthalf  16331  bitsp1  16344  bitsfzolem  16347  bitsfzo  16348  bitsmod  16349  bitscmp  16351  bitsinv1lem  16354  sadaddlem  16379  bitsres  16386  bitsuz  16387  smumul  16406  gcd0id  16432  gcdneg  16435  dfgcd2  16459  nn0seqcvgd  16483  lcmgcdlem  16519  nprm  16601  prmdvdsfz  16618  isprm5  16620  isprm7  16621  coprm  16624  prmexpb  16632  prmfac1  16633  hashdvds  16688  crth  16691  eulerthlem2  16695  fermltl  16697  prmdiv  16698  prmdiveq  16699  hashgcdlem  16701  odzdvds  16709  vfermltlALT  16716  modprm0  16719  modprmn0modprm0  16721  prm23ge5  16729  pythagtriplem13  16741  pcxcl  16775  pcaddlem  16802  pcadd  16803  pcfac  16813  qexpz  16815  prmunb  16828  1arithlem4  16840  4sqlem5  16856  4sqlem6  16857  4sqlem7  16858  4sqlem10  16861  4sqlem11  16869  4sqlem12  16870  4sqlem15  16873  4sqlem16  16874  4sqlem17  16875  vdwnnlem3  16911  prmgaplem7  16971  cshwshashlem3  17011  chnub  18530  chnso  18532  chnccat  18534  chnpof1  18538  subgmulg  19055  mndodconglem  19455  odnncl  19459  odmod  19460  oddvds  19461  dfod2  19478  sylow1lem3  19514  efgsp1  19651  efgredleme  19657  telgsumfzs  19903  zringlpirlem1  21401  zringlpirlem3  21403  fermltlchr  21468  znf1o  21490  zcld  24730  ovoliunlem1  25431  ovoliunlem2  25432  dyadss  25523  dyaddisjlem  25524  dyadmaxlem  25526  dvfsumle  25954  dvfsumleOLD  25955  dvfsumge  25956  dvfsumabs  25957  dvfsumlem1  25960  dvfsumlem3  25963  degltlem1  26005  plyco0  26125  plyeq0lem  26143  plydivex  26233  aannenlem1  26264  efif1olem2  26480  nnlogbexp  26719  logblt  26722  ang180lem1  26747  ang180lem3  26749  wilthlem2  27007  basellem3  27021  basellem4  27022  ppiprm  27089  chtdif  27096  ppidif  27101  chtub  27151  mersenne  27166  bcmono  27216  bcmax  27217  bposlem1  27223  bposlem3  27225  bposlem5  27227  bposlem6  27228  lgsval2lem  27246  lgsvalmod  27255  lgsneg  27260  lgsmod  27262  lgsdilem  27263  lgsdirprm  27270  lgsdilem2  27272  lgsne0  27274  lgssq  27276  lgssq2  27277  lgsqr  27290  lgsdchr  27294  gausslemma2dlem1a  27304  gausslemma2dlem3  27307  gausslemma2dlem5a  27309  gausslemma2dlem6  27311  gausslemma2d  27313  lgseisenlem1  27314  lgseisenlem2  27315  lgseisenlem3  27316  lgseisenlem4  27317  lgsquadlem1  27319  lgsquadlem2  27320  lgsquadlem3  27321  lgsquad3  27326  2lgslem1a2  27329  2lgslem1  27333  2lgslem2  27334  2sqlem3  27359  2sqlem8  27365  2sqblem  27370  2sqmod  27375  chebbnd1lem1  27408  chebbnd1lem2  27409  chebbnd1lem3  27410  dchrmusum2  27433  dchrvmasumlem1  27434  dchrvmasum2lem  27435  dchrvmasum2if  27436  dchrvmasumlem3  27438  dchrvmasumiflem2  27441  dchrisum0lem1  27455  dchrmusumlem  27461  mudivsum  27469  mulogsumlem  27470  mulogsum  27471  mulog2sumlem2  27474  mulog2sumlem3  27475  selberglem1  27484  selberglem2  27485  pntpbnd1  27525  pntlemg  27537  pntlemf  27544  qabvle  27564  padicabv  27569  padicabvcxp  27571  ostth2lem2  27573  axlowdimlem13  28934  axlowdimlem16  28937  pthdlem1  29746  crctcshwlkn0  29801  crctcsh  29804  clwwisshclwwslemlem  29995  eucrctshift  30225  nndiffz1  32773  fzsplit3  32780  bcm1n  32782  suppssnn0  32792  ltesubnnd  32810  wrdt2ind  32941  cshwrnid  32949  cycpmfv2  33090  cycpmco2lem6  33107  cycpmco2lem7  33108  cycpmrn  33119  cyc3conja  33133  pnfinf  33159  znfermltl  33338  constrext2chnlem  33784  cos9thpiminplylem1  33816  cos9thpiminplylem2  33817  dya2iocress  34308  dya2iocbrsiga  34309  dya2icobrsiga  34310  dya2icoseg  34311  dya2iocucvr  34318  sxbrsigalem2  34320  ballotlemfc0  34527  ballotlemfcc  34528  ballotlemodife  34532  ballotlemimin  34540  ballotlemsgt1  34545  ballotlemsel1i  34547  ballotlemsi  34549  ballotlemsima  34550  ballotlemrv2  34556  ballotlemfrceq  34563  ballotlemfrcn0  34564  ballotlemirc  34566  fsum2dsub  34641  reprlt  34653  reprgt  34655  breprexplemc  34666  tgoldbachgnn  34693  tgoldbachgt  34697  subfacval3  35254  erdszelem8  35263  erdszelem9  35264  supfz  35794  inffz  35795  dnizeq0  36540  dnizphlfeqhlf  36541  dnibndlem13  36555  knoppndvlem1  36577  knoppndvlem2  36578  knoppndvlem7  36583  knoppndvlem19  36595  knoppndvlem21  36597  ltflcei  37669  leceifl  37670  poimirlem1  37682  poimirlem2  37683  poimirlem6  37687  poimirlem7  37688  poimirlem8  37689  poimirlem15  37696  poimirlem16  37697  poimirlem17  37698  poimirlem19  37700  poimirlem20  37701  poimirlem23  37704  poimirlem24  37705  poimirlem27  37708  poimirlem29  37710  poimirlem31  37712  poimirlem32  37713  mblfinlem2  37719  itg2addnclem2  37733  mettrifi  37818  cntotbnd  37857  fzne2d  42094  aks4d1lem1  42176  aks4d1p1p3  42183  aks4d1p1p2  42184  aks4d1p1p4  42185  aks4d1p1  42190  aks4d1p2  42191  aks4d1p3  42192  aks4d1p5  42194  aks4d1p6  42195  aks4d1p7d1  42196  aks4d1p7  42197  aks4d1p8d3  42200  aks4d1p8  42201  aks4d1p9  42202  posbezout  42214  aks6d1c1  42230  hashscontpow1  42235  hashscontpow  42236  aks6d1c2  42244  aks6d1c5lem1  42250  2ap1caineq  42259  sticksstones6  42265  sticksstones7  42266  sticksstones10  42269  sticksstones12a  42271  sticksstones12  42272  sticksstones22  42282  bcled  42292  bcle2d  42293  aks6d1c7lem1  42294  aks6d1c7lem2  42295  aks6d1c7  42298  aks5lem6  42306  unitscyglem2  42310  unitscyglem4  42312  aks5lem8  42315  sumcubes  42432  frlmvscadiccat  42625  dffltz  42753  lzunuz  42886  lzenom  42888  diophin  42890  irrapxlem1  42940  irrapxlem2  42941  irrapxlem3  42942  irrapxlem4  42943  pellexlem5  42951  pellexlem6  42952  rmspecfund  43027  rmxypos  43065  ltrmynn0  43066  ltrmxnn0  43067  ltrmy  43070  rmyeq0  43071  rmyeq  43072  lermy  43073  rmyabs  43076  jm2.24nn  43077  jm2.17a  43078  jm2.17b  43079  jm2.17c  43080  jm2.24  43081  rmygeid  43082  acongrep  43098  fzmaxdif  43099  acongeq  43101  jm2.22  43113  jm2.23  43114  jm2.26lem3  43119  jm2.27a  43123  jm3.1lem1  43135  jm3.1lem3  43137  expdiophlem1  43139  fzuntd  43574  fzunt1d  43575  fzuntgd  43576  prmunb2  44429  nzprmdif  44437  hashnzfzclim  44440  binomcxplemnn0  44467  uzwo4  45175  ssinc  45209  ssdec  45210  zltlesub  45411  monoords  45423  fzisoeu  45426  fperiodmul  45430  fzdifsuc2  45436  iuneqfzuzlem  45458  uzublem  45553  zxrd  45576  uzinico  45684  uzubioo  45690  fmul01  45705  fmul01lt1lem1  45709  fmul01lt1lem2  45710  climsuselem1  45732  climsuse  45733  sumnnodd  45755  ltmod  45761  limsupresuz  45826  limsupubuzlem  45835  limsupequzlem  45845  limsupmnfuzlem  45849  limsupequzmptlem  45851  limsupre3uzlem  45858  supcnvlimsup  45863  limsup10exlem  45895  liminfresuz  45907  liminfvaluz  45915  limsupvaluz3  45921  ioodvbdlimc1lem2  46055  ioodvbdlimc2lem  46057  dvnmul  46066  dvnprodlem1  46069  dvnprodlem2  46070  iblspltprt  46096  itgspltprt  46102  stoweidlem3  46126  stoweidlem11  46134  stoweidlem20  46143  stoweidlem26  46149  stoweidlem34  46157  stoweidlem59  46182  stirlinglem5  46201  dirkertrigeqlem3  46223  dirkeritg  46225  dirkercncflem1  46226  dirkercncflem2  46227  dirkercncflem4  46229  fourierdlem4  46234  fourierdlem6  46236  fourierdlem7  46237  fourierdlem11  46241  fourierdlem12  46242  fourierdlem15  46245  fourierdlem19  46249  fourierdlem20  46250  fourierdlem25  46255  fourierdlem26  46256  fourierdlem34  46264  fourierdlem35  46265  fourierdlem41  46271  fourierdlem48  46277  fourierdlem49  46278  fourierdlem50  46279  fourierdlem51  46280  fourierdlem54  46283  fourierdlem63  46292  fourierdlem64  46293  fourierdlem65  46294  fourierdlem71  46300  fourierdlem79  46308  fourierdlem89  46318  fourierdlem90  46319  fourierdlem91  46320  fourierdlem102  46331  fourierdlem103  46332  fourierdlem104  46333  fourierdlem114  46343  fouriersw  46354  elaa2lem  46356  etransclem3  46360  etransclem4  46361  etransclem7  46364  etransclem10  46367  etransclem15  46372  etransclem19  46376  etransclem23  46380  etransclem24  46381  etransclem25  46382  etransclem27  46384  etransclem31  46388  etransclem32  46389  etransclem35  46392  etransclem41  46398  etransclem44  46401  etransclem46  46403  etransclem48  46405  iundjiun  46583  caratheodorylem1  46649  smflimsuplem4  46946  smfliminflem  46953  ormklocald  46997  ormkglobd  46998  natglobalincr  47000  chnerlem3  47007  2elfz2melfz  47443  elfzelfzlble  47446  fzopredsuc  47448  2ltceilhalf  47453  ceilhalfgt1  47454  ceilhalfnn  47461  submodlt  47475  m1modmmod  47483  difmodm1lt  47484  modmknepk  47487  mod2addne  47489  fsummsndifre  47497  iccpartgt  47552  icceuelpartlem  47560  icceuelpart  47561  iccpartnel  47563  lighneallem2  47731  proththd  47739  dfodd4  47784  oexpnegALTV  47802  nnoALTV  47820  evenltle  47842  fpprwppr  47864  gbowgt5  47887  gboge9  47889  stgoldbwt  47901  sbgoldbst  47903  sbgoldbalt  47906  sgoldbeven3prm  47908  mogoldbb  47910  bgoldbtbndlem1  47930  bgoldbtbndlem2  47931  bgoldbtbndlem3  47932  bgoldbtbnd  47934  bgoldbachlt  47938  tgblthelfgott  47940  tgoldbach  47942  upgrimpthslem2  48033  gpgprismgrusgra  48183  gpgedgvtx1  48187  gpgvtxedg0  48188  gpgvtxedg1  48189  gpg5nbgrvtx13starlem2  48197  gpg3nbgrvtx0  48201  gpg3kgrtriexlem1  48208  gpg3kgrtriexlem4  48211  gpg3kgrtriexlem6  48213  pw2m1lepw2m1  48646  fllogbd  48686  logbpw2m1  48693  fllog2  48694  nnpw2blen  48706  nnolog2flm1  48716  dignn0flhalflem1  48741  dignn0flhalflem2  48742