Theorem zred 12088

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

Syntax hints:   → wi 4   ∈ wcel 2114  ℝcr 10536  ℤcz 11982

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 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2793

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3or 1084  df-3an 1085  df-tru 1540  df-ex 1781  df-nf 1785  df-sb 2070  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-rab 3147  df-v 3496  df-dif 3939  df-un 3941  df-in 3943  df-ss 3952  df-nul 4292  df-if 4468  df-sn 4568  df-pr 4570  df-op 4574  df-uni 4839  df-br 5067  df-iota 6314  df-fv 6363  df-ov 7159  df-neg 10873  df-z 11983

This theorem is referenced by:  zcnd  12089  suprfinzcl  12098  eluzmn  12251  eluzelre  12255  subeluzsub  12276  uzm1  12277  zsupss  12338  suprzcl2  12339  uzwo3  12344  rpnnen1lem3  12379  rpnnen1lem5  12381  zltaddlt1le  12891  fzsplit2  12933  fzdisj  12935  ssfzunsnext  12953  fzpreddisj  12957  fznatpl1  12962  fzp1disj  12967  uzdisj  12981  fzm1  12988  fz0fzdiffz0  13017  elfzmlbm  13018  elfzmlbp  13019  difelfznle  13022  nn0disj  13024  elfzolt3  13049  fzonel  13052  fzospliti  13070  fzodisj  13072  fzouzdisj  13074  fzodisjsn  13076  fzonmapblen  13084  fzoaddel  13091  elincfzoext  13096  reflcl  13167  flge  13176  flwordi  13183  fladdz  13196  2tnp1ge0ge0  13200  flhalf  13201  fldiv4p1lem1div2  13206  fldiv4lem1div2uz2  13207  fldiv4lem1div2  13208  flleceil  13222  fleqceilz  13223  quoremz  13224  uzsup  13232  modmul12d  13294  modaddmodup  13303  modaddmodlo  13304  modfzo0difsn  13312  modsumfzodifsn  13313  addmodlteq  13315  om2uzlti  13319  om2uzf1oi  13322  seqf1olem1  13410  seqf1olem2  13411  bcval4  13668  bcp1nk  13678  bcval5  13679  fzsdom2  13790  seqcoll  13823  seqcoll2  13824  ccatrn  13943  ccatalpha  13947  cshwidxmodr  14166  fzomaxdiflem  14702  fzomaxdif  14703  rexuzre  14712  limsupgre  14838  rlimclim1  14902  isercoll  15024  iseralt  15041  fsumm1  15106  fsum1p  15108  fsum0diaglem  15131  modfsummods  15148  isumsplit  15195  climcndslem1  15204  mertenslem1  15240  ntrivcvgmul  15258  fprodntriv  15296  fprod1p  15322  fprodeq0  15329  fallfacval4  15397  bpoly4  15413  fzo0dvdseq  15673  dvdsmod  15678  oexpneg  15694  mod2eq1n2dvds  15696  ltoddhalfle  15710  flodddiv4t2lthalf  15767  bitsp1  15780  bitsfzolem  15783  bitsfzo  15784  bitsmod  15785  bitscmp  15787  bitsinv1lem  15790  sadaddlem  15815  bitsres  15822  bitsuz  15823  smumul  15842  gcd0id  15867  gcdneg  15870  dfgcd2  15894  nn0seqcvgd  15914  lcmgcdlem  15950  nprm  16032  prmdvdsfz  16049  isprm5  16051  isprm7  16052  coprm  16055  prmexpb  16062  prmfac1  16063  hashdvds  16112  crth  16115  eulerthlem2  16119  fermltl  16121  prmdiv  16122  prmdiveq  16123  hashgcdlem  16125  odzdvds  16132  vfermltlALT  16139  modprm0  16142  modprmn0modprm0  16144  prm23ge5  16152  pythagtriplem13  16164  pcxcl  16197  pcaddlem  16224  pcadd  16225  pcfac  16235  qexpz  16237  prmunb  16250  1arithlem4  16262  4sqlem5  16278  4sqlem6  16279  4sqlem7  16280  4sqlem10  16283  4sqlem11  16291  4sqlem12  16292  4sqlem15  16295  4sqlem16  16296  4sqlem17  16297  vdwnnlem3  16333  prmgaplem7  16393  cshwshashlem3  16431  subgmulg  18293  mndodconglem  18669  odnncl  18673  odmod  18674  oddvds  18675  dfod2  18691  sylow1lem3  18725  efgsp1  18863  efgredleme  18869  telgsumfzs  19109  zringlpirlem1  20631  zringlpirlem3  20633  znf1o  20698  zcld  23421  ovoliunlem1  24103  ovoliunlem2  24104  dyadss  24195  dyaddisjlem  24196  dyadmaxlem  24198  dvfsumle  24618  dvfsumge  24619  dvfsumabs  24620  dvfsumlem1  24623  dvfsumlem3  24625  degltlem1  24666  plyco0  24782  plyeq0lem  24800  plydivex  24886  aannenlem1  24917  efif1olem2  25127  nnlogbexp  25359  logblt  25362  ang180lem1  25387  ang180lem3  25389  wilthlem2  25646  basellem3  25660  basellem4  25661  ppiprm  25728  chtdif  25735  ppidif  25740  chtub  25788  mersenne  25803  bcmono  25853  bcmax  25854  bposlem1  25860  bposlem3  25862  bposlem5  25864  bposlem6  25865  lgsval2lem  25883  lgsvalmod  25892  lgsneg  25897  lgsmod  25899  lgsdilem  25900  lgsdirprm  25907  lgsdilem2  25909  lgsne0  25911  lgssq  25913  lgssq2  25914  lgsqr  25927  lgsdchr  25931  gausslemma2dlem1a  25941  gausslemma2dlem3  25944  gausslemma2dlem5a  25946  gausslemma2dlem6  25948  gausslemma2d  25950  lgseisenlem1  25951  lgseisenlem2  25952  lgseisenlem3  25953  lgseisenlem4  25954  lgsquadlem1  25956  lgsquadlem2  25957  lgsquadlem3  25958  lgsquad3  25963  2lgslem1a2  25966  2lgslem1  25970  2lgslem2  25971  2sqlem3  25996  2sqlem8  26002  2sqblem  26007  2sqmod  26012  chebbnd1lem1  26045  chebbnd1lem2  26046  chebbnd1lem3  26047  dchrmusum2  26070  dchrvmasumlem1  26071  dchrvmasum2lem  26072  dchrvmasum2if  26073  dchrvmasumlem3  26075  dchrvmasumiflem2  26078  dchrisum0lem1  26092  dchrmusumlem  26098  mudivsum  26106  mulogsumlem  26107  mulogsum  26108  mulog2sumlem2  26111  mulog2sumlem3  26112  selberglem1  26121  selberglem2  26122  pntpbnd1  26162  pntlemg  26174  pntlemf  26181  qabvle  26201  padicabv  26206  padicabvcxp  26208  ostth2lem2  26210  axlowdimlem13  26740  axlowdimlem16  26743  pthdlem1  27547  crctcshwlkn0  27599  crctcsh  27602  clwwisshclwwslemlem  27791  eucrctshift  28022  nndiffz1  30509  fzsplit3  30517  bcm1n  30518  fzone1  30523  ltesubnnd  30538  wrdt2ind  30627  cshwrnid  30635  cycpmfv2  30756  cycpmco2lem6  30773  cycpmco2lem7  30774  cycpmrn  30785  cyc3conja  30799  pnfinf  30812  dya2iocress  31532  dya2iocbrsiga  31533  dya2icobrsiga  31534  dya2icoseg  31535  dya2iocucvr  31542  sxbrsigalem2  31544  ballotlemfc0  31750  ballotlemfcc  31751  ballotlemodife  31755  ballotlemimin  31763  ballotlemsgt1  31768  ballotlemsel1i  31770  ballotlemsi  31772  ballotlemsima  31773  ballotlemrv2  31779  ballotlemfrceq  31786  ballotlemfrcn0  31787  ballotlemirc  31789  fsum2dsub  31878  reprlt  31890  reprgt  31892  breprexplemc  31903  tgoldbachgnn  31930  tgoldbachgt  31934  subfacval3  32436  erdszelem8  32445  erdszelem9  32446  supfz  32960  inffz  32961  dnizeq0  33814  dnizphlfeqhlf  33815  dnibndlem13  33829  knoppndvlem1  33851  knoppndvlem2  33852  knoppndvlem7  33857  knoppndvlem19  33869  knoppndvlem21  33871  ltflcei  34895  leceifl  34896  poimirlem1  34908  poimirlem2  34909  poimirlem6  34913  poimirlem7  34914  poimirlem8  34915  poimirlem15  34922  poimirlem16  34923  poimirlem17  34924  poimirlem19  34926  poimirlem20  34927  poimirlem23  34930  poimirlem24  34931  poimirlem27  34934  poimirlem29  34936  poimirlem31  34938  poimirlem32  34939  mblfinlem2  34945  itg2addnclem2  34959  mettrifi  35047  cntotbnd  35089  prodsplit  39116  frlmvscadiccat  39165  exp11d  39209  dffltz  39291  lzunuz  39385  lzenom  39387  diophin  39389  irrapxlem1  39439  irrapxlem2  39440  irrapxlem3  39441  irrapxlem4  39442  pellexlem5  39450  pellexlem6  39451  rmspecfund  39526  rmxypos  39564  ltrmynn0  39565  ltrmxnn0  39566  ltrmy  39569  rmyeq0  39570  rmyeq  39571  lermy  39572  rmyabs  39575  jm2.24nn  39576  jm2.17a  39577  jm2.17b  39578  jm2.17c  39579  jm2.24  39580  rmygeid  39581  acongrep  39597  fzmaxdif  39598  acongeq  39600  jm2.22  39612  jm2.23  39613  jm2.26lem3  39618  jm2.27a  39622  jm3.1lem1  39634  jm3.1lem3  39636  expdiophlem1  39638  prmunb2  40663  nzprmdif  40671  hashnzfzclim  40674  binomcxplemnn0  40701  uzwo4  41335  ssinc  41373  ssdec  41374  zltlesub  41571  monoords  41584  fzisoeu  41587  fperiodmul  41591  fzdifsuc2  41597  iuneqfzuzlem  41622  uzublem  41724  zxrd  41749  uzinico  41856  uzubioo  41863  fmul01  41881  fmul01lt1lem1  41885  fmul01lt1lem2  41886  climsuselem1  41908  climsuse  41909  sumnnodd  41931  ltmod  41939  limsupresuz  42004  limsupubuzlem  42013  limsupequzlem  42023  limsupmnfuzlem  42027  limsupequzmptlem  42029  limsupre3uzlem  42036  supcnvlimsup  42041  limsup10exlem  42073  liminfresuz  42085  liminfvaluz  42093  limsupvaluz3  42099  ioodvbdlimc1lem2  42237  ioodvbdlimc2lem  42239  dvnmul  42248  dvnprodlem1  42251  dvnprodlem2  42252  iblspltprt  42278  itgspltprt  42284  stoweidlem3  42308  stoweidlem11  42316  stoweidlem20  42325  stoweidlem26  42331  stoweidlem34  42339  stoweidlem59  42364  stirlinglem5  42383  dirkertrigeqlem3  42405  dirkeritg  42407  dirkercncflem1  42408  dirkercncflem2  42409  dirkercncflem4  42411  fourierdlem4  42416  fourierdlem6  42418  fourierdlem7  42419  fourierdlem11  42423  fourierdlem12  42424  fourierdlem15  42427  fourierdlem19  42431  fourierdlem20  42432  fourierdlem25  42437  fourierdlem26  42438  fourierdlem34  42446  fourierdlem35  42447  fourierdlem41  42453  fourierdlem48  42459  fourierdlem49  42460  fourierdlem50  42461  fourierdlem51  42462  fourierdlem54  42465  fourierdlem63  42474  fourierdlem64  42475  fourierdlem65  42476  fourierdlem71  42482  fourierdlem79  42490  fourierdlem89  42500  fourierdlem90  42501  fourierdlem91  42502  fourierdlem102  42513  fourierdlem103  42514  fourierdlem104  42515  fourierdlem114  42525  fouriersw  42536  elaa2lem  42538  etransclem3  42542  etransclem4  42543  etransclem7  42546  etransclem10  42549  etransclem15  42554  etransclem19  42558  etransclem23  42562  etransclem24  42563  etransclem25  42564  etransclem27  42566  etransclem31  42570  etransclem32  42571  etransclem35  42574  etransclem41  42580  etransclem44  42583  etransclem46  42585  etransclem48  42587  iundjiun  42762  caratheodorylem1  42828  smflimsuplem4  43117  smfliminflem  43124  2elfz2melfz  43538  elfzelfzlble  43541  fzopredsuc  43543  fsummsndifre  43552  iccpartgt  43607  icceuelpartlem  43615  icceuelpart  43616  iccpartnel  43618  lighneallem2  43791  proththd  43799  dfodd4  43844  oexpnegALTV  43862  nnoALTV  43880  evenltle  43902  fpprwppr  43924  gbowgt5  43947  gboge9  43949  stgoldbwt  43961  sbgoldbst  43963  sbgoldbalt  43966  sgoldbeven3prm  43968  mogoldbb  43970  bgoldbtbndlem1  43990  bgoldbtbndlem2  43991  bgoldbtbndlem3  43992  bgoldbtbnd  43994  bgoldbachlt  43998  tgblthelfgott  44000  tgoldbach  44002  pw2m1lepw2m1  44595  m1modmmod  44601  difmodm1lt  44602  fllogbd  44640  logbpw2m1  44647  fllog2  44648  nnpw2blen  44660  nnolog2flm1  44670  dignn0flhalflem1  44695  dignn0flhalflem2  44696