Theorem zred 11482

Description: An integer is a real number. (Contributed by Mario Carneiro, 28-May-2016.)

Hypothesis

Ref	Expression
zred.1	|- ( ph -> A e. ZZ )

Assertion

Ref	Expression
zred	|- ( ph -> A e. RR )

Proof of Theorem zred

Step	Hyp	Ref	Expression
1		zssre 11384	. 2 |- ZZ C_ RR
2		zred.1	. 2 |- ( ph -> A e. ZZ )
3	1, 2	sseldi 3601	1 |- ( ph -> A e. RR )

Syntax hints:   -> wi 4   e. wcel 1990   RRcr 9935   ZZcz 11377

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3or 1038  df-3an 1039  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-rex 2918  df-rab 2921  df-v 3202  df-dif 3577  df-un 3579  df-in 3581  df-ss 3588  df-nul 3916  df-if 4087  df-sn 4178  df-pr 4180  df-op 4184  df-uni 4437  df-br 4654  df-iota 5851  df-fv 5896  df-ov 6653  df-neg 10269  df-z 11378

This theorem is referenced by:  zcnd  11483  suprfinzcl  11492  eluzmn  11694  eluzelre  11698  uzm1  11718  zsupss  11777  suprzcl2  11778  uzwo3  11783  rpnnen1lem3  11816  rpnnen1lem5  11818  rpnnen1lem3OLD  11822  rpnnen1lem5OLD  11824  zltaddlt1le  12324  fzsplit2  12366  fzdisj  12368  ssfzunsnext  12386  fzpreddisj  12390  fznatpl1  12395  fzp1disj  12399  uzdisj  12413  fzm1  12420  fz0fzdiffz0  12448  elfzmlbm  12449  elfzmlbp  12450  difelfznle  12453  nn0disj  12455  elfzolt3  12480  fzonel  12483  fzospliti  12500  fzodisj  12502  fzouzdisj  12504  fzodisjsn  12505  fzonmapblen  12513  fzoaddel  12520  elincfzoext  12525  reflcl  12597  flge  12606  flwordi  12613  fladdz  12626  2tnp1ge0ge0  12630  flhalf  12631  fldiv4p1lem1div2  12636  fldiv4lem1div2uz2  12637  fldiv4lem1div2  12638  flleceil  12652  fleqceilz  12653  quoremz  12654  uzsup  12662  modmul12d  12724  modaddmodup  12733  modaddmodlo  12734  modfzo0difsn  12742  modsumfzodifsn  12743  addmodlteq  12745  om2uzlti  12749  om2uzf1oi  12752  seqf1olem1  12840  seqf1olem2  12841  bcval4  13094  bcp1nk  13104  bcval5  13105  fzsdom2  13215  seqcoll  13248  seqcoll2  13249  ccatrn  13372  ccatalpha  13375  cshwidxmodr  13550  fzomaxdiflem  14082  fzomaxdif  14083  rexuzre  14092  limsupgre  14212  rlimclim1  14276  isercoll  14398  iseralt  14415  fsumm1  14480  fsum1p  14482  fsum0diaglem  14508  modfsummods  14525  isumsplit  14572  climcndslem1  14581  mertenslem1  14616  ntrivcvgmul  14634  fprodntriv  14672  fprod1p  14698  fprodeq0  14705  fallfacval4  14774  bpoly4  14790  fzo0dvdseq  15045  dvdsmod  15050  oexpneg  15069  mod2eq1n2dvds  15071  ltoddhalfle  15085  flodddiv4t2lthalf  15140  bitsp1  15153  bitsfzolem  15156  bitsfzo  15157  bitsmod  15158  bitscmp  15160  bitsinv1lem  15163  sadaddlem  15188  bitsres  15195  bitsuz  15196  smumul  15215  gcd0id  15240  gcdneg  15243  dfgcd2  15263  nn0seqcvgd  15283  lcmgcdlem  15319  nprm  15401  prmdvdsfz  15417  isprm5  15419  isprm7  15420  coprm  15423  prmexpb  15430  prmfac1  15431  hashdvds  15480  crth  15483  eulerthlem2  15487  fermltl  15489  prmdiv  15490  prmdiveq  15491  hashgcdlem  15493  odzdvds  15500  vfermltlALT  15507  modprm0  15510  modprmn0modprm0  15512  prm23ge5  15520  pythagtriplem13  15532  pcxcl  15565  pcaddlem  15592  pcadd  15593  pcfac  15603  qexpz  15605  prmunb  15618  1arithlem4  15630  4sqlem5  15646  4sqlem6  15647  4sqlem7  15648  4sqlem10  15651  4sqlem11  15659  4sqlem12  15660  4sqlem15  15663  4sqlem16  15664  4sqlem17  15665  vdwnnlem3  15701  prmgaplem7  15761  cshwshashlem3  15804  subgmulg  17608  mndodconglem  17960  odnncl  17964  odmod  17965  oddvds  17966  dfod2  17981  sylow1lem3  18015  efgsp1  18150  efgredleme  18156  telgsumfzs  18386  zringlpirlem1  19832  zringlpirlem3  19834  znf1o  19900  zcld  22616  ovoliunlem1  23270  ovoliunlem2  23271  dyadss  23362  dyaddisjlem  23363  dyadmaxlem  23365  dvfsumle  23784  dvfsumge  23785  dvfsumabs  23786  dvfsumlem1  23789  dvfsumlem3  23791  degltlem1  23832  plyco0  23948  plyeq0lem  23966  plydivex  24052  aannenlem1  24083  efif1olem2  24289  nnlogbexp  24519  logblt  24522  ang180lem1  24539  ang180lem3  24541  wilthlem2  24795  basellem3  24809  basellem4  24810  ppiprm  24877  chtdif  24884  ppidif  24889  chtub  24937  mersenne  24952  bcmono  25002  bcmax  25003  bposlem1  25009  bposlem3  25011  bposlem5  25013  bposlem6  25014  lgslem4  25025  lgsval2lem  25032  lgsvalmod  25041  lgsneg  25046  lgsmod  25048  lgsdilem  25049  lgsdirprm  25056  lgsdilem2  25058  lgsne0  25060  lgssq  25062  lgssq2  25063  lgsqr  25076  lgsdchr  25080  gausslemma2dlem1a  25090  gausslemma2dlem3  25093  gausslemma2dlem5a  25095  gausslemma2dlem6  25097  gausslemma2d  25099  lgseisenlem1  25100  lgseisenlem2  25101  lgseisenlem3  25102  lgseisenlem4  25103  lgsquadlem1  25105  lgsquadlem2  25106  lgsquadlem3  25107  lgsquad3  25112  2lgslem1a2  25115  2lgslem1  25119  2lgslem2  25120  2sqlem3  25145  2sqlem8  25151  2sqblem  25156  chebbnd1lem1  25158  chebbnd1lem2  25159  chebbnd1lem3  25160  dchrmusum2  25183  dchrvmasumlem1  25184  dchrvmasum2lem  25185  dchrvmasum2if  25186  dchrvmasumlem3  25188  dchrvmasumiflem2  25191  dchrisum0lem1  25205  dchrmusumlem  25211  mudivsum  25219  mulogsumlem  25220  mulogsum  25221  mulog2sumlem2  25224  mulog2sumlem3  25225  selberglem1  25234  selberglem2  25235  pntpbnd1  25275  pntlemg  25287  pntlemf  25294  qabvle  25314  padicabv  25319  padicabvcxp  25321  ostth2lem2  25323  axlowdimlem13  25834  axlowdimlem16  25837  pthdlem1  26662  crctcshwlkn0  26713  crctcsh  26716  clwwisshclwwslemlem  26926  eucrctshift  27103  nndiffz1  29548  fzsplit3  29553  bcm1n  29554  ltesubnnd  29568  2sqmod  29648  pnfinf  29737  dya2iocress  30336  dya2iocbrsiga  30337  dya2icobrsiga  30338  dya2icoseg  30339  dya2iocucvr  30346  sxbrsigalem2  30348  ballotlemfc0  30554  ballotlemfcc  30555  ballotlemodife  30559  ballotlemimin  30567  ballotlemsgt1  30572  ballotlemsel1i  30574  ballotlemsi  30576  ballotlemsima  30577  ballotlemrv2  30583  ballotlemfrceq  30590  ballotlemfrcn0  30591  ballotlemirc  30593  fsum2dsub  30685  reprlt  30697  reprgt  30699  breprexplemc  30710  tgoldbachgnn  30737  tgoldbachgt  30741  subfacval3  31171  erdszelem8  31180  erdszelem9  31181  supfz  31613  inffz  31614  inffzOLD  31615  dnizeq0  32465  dnizphlfeqhlf  32466  dnibndlem13  32480  knoppndvlem1  32503  knoppndvlem2  32504  knoppndvlem7  32509  knoppndvlem19  32521  knoppndvlem21  32523  ltflcei  33397  leceifl  33398  poimirlem1  33410  poimirlem2  33411  poimirlem6  33415  poimirlem7  33416  poimirlem8  33417  poimirlem15  33424  poimirlem16  33425  poimirlem17  33426  poimirlem19  33428  poimirlem20  33429  poimirlem23  33432  poimirlem24  33433  poimirlem27  33436  poimirlem29  33438  poimirlem31  33440  poimirlem32  33441  mblfinlem2  33447  itg2addnclem2  33462  mettrifi  33553  cntotbnd  33595  lzunuz  37331  lzenom  37333  diophin  37336  irrapxlem1  37386  irrapxlem2  37387  irrapxlem3  37388  irrapxlem4  37389  pellexlem5  37397  pellexlem6  37398  rmspecfund  37474  rmxypos  37514  ltrmynn0  37515  ltrmxnn0  37516  ltrmy  37519  rmyeq0  37520  rmyeq  37521  lermy  37522  rmyabs  37525  jm2.24nn  37526  jm2.17a  37527  jm2.17b  37528  jm2.17c  37529  jm2.24  37530  rmygeid  37531  acongrep  37547  fzmaxdif  37548  acongeq  37550  jm2.22  37562  jm2.23  37563  jm2.26lem3  37568  jm2.27a  37572  jm3.1lem1  37584  jm3.1lem3  37586  expdiophlem1  37588  prmunb2  38510  nzprmdif  38518  hashnzfzclim  38521  binomcxplemnn0  38548  uzwo4  39221  ssinc  39264  ssdec  39265  zltlesub  39497  monoords  39511  fzisoeu  39514  fperiodmul  39518  fzdifsuc2  39525  iuneqfzuzlem  39550  uzublem  39657  zxrd  39682  uzinico  39787  uzubioo  39794  fmul01  39812  fmul01lt1lem1  39816  fmul01lt1lem2  39817  climsuselem1  39839  climsuse  39840  sumnnodd  39862  ltmod  39870  limsupresuz  39935  limsupubuzlem  39944  limsupequzlem  39954  limsupmnfuzlem  39958  limsupequzmptlem  39960  limsupre3uzlem  39967  supcnvlimsup  39972  limsup10exlem  40004  liminfresuz  40016  liminfvaluz  40024  limsupvaluz3  40030  ioodvbdlimc1lem2  40147  ioodvbdlimc2lem  40149  dvnmul  40158  dvnprodlem1  40161  dvnprodlem2  40162  iblspltprt  40189  itgspltprt  40195  stoweidlem3  40220  stoweidlem11  40228  stoweidlem20  40237  stoweidlem26  40243  stoweidlem34  40251  stoweidlem59  40276  stirlinglem5  40295  dirkertrigeqlem3  40317  dirkeritg  40319  dirkercncflem1  40320  dirkercncflem2  40321  dirkercncflem4  40323  fourierdlem4  40328  fourierdlem6  40330  fourierdlem7  40331  fourierdlem11  40335  fourierdlem12  40336  fourierdlem15  40339  fourierdlem19  40343  fourierdlem20  40344  fourierdlem25  40349  fourierdlem26  40350  fourierdlem34  40358  fourierdlem35  40359  fourierdlem41  40365  fourierdlem48  40371  fourierdlem49  40372  fourierdlem50  40373  fourierdlem51  40374  fourierdlem54  40377  fourierdlem63  40386  fourierdlem64  40387  fourierdlem65  40388  fourierdlem71  40394  fourierdlem79  40402  fourierdlem89  40412  fourierdlem90  40413  fourierdlem91  40414  fourierdlem102  40425  fourierdlem103  40426  fourierdlem104  40427  fourierdlem114  40437  fouriersw  40448  elaa2lem  40450  etransclem3  40454  etransclem4  40455  etransclem7  40458  etransclem10  40461  etransclem15  40466  etransclem19  40470  etransclem23  40474  etransclem24  40475  etransclem25  40476  etransclem27  40478  etransclem31  40482  etransclem32  40483  etransclem35  40486  etransclem41  40492  etransclem44  40495  etransclem46  40497  etransclem48  40499  iundjiun  40677  caratheodorylem1  40740  smflimsuplem4  41029  smfliminflem  41036  2elfz2melfz  41328  elfzelfzlble  41331  fzopredsuc  41333  fsummsndifre  41342  iccpartgt  41363  icceuelpartlem  41371  icceuelpart  41372  iccpartnel  41374  lighneallem2  41523  proththd  41531  dfodd4  41571  oexpnegALTV  41588  nnoALTV  41606  evenltle  41626  gbowgt5  41650  gboge9  41652  stgoldbwt  41664  sbgoldbst  41666  sbgoldbalt  41669  sgoldbeven3prm  41671  mogoldbb  41673  bgoldbtbndlem1  41693  bgoldbtbndlem2  41694  bgoldbtbndlem3  41695  bgoldbtbnd  41697  bgoldbachlt  41701  tgblthelfgott  41703  tgoldbach  41705  bgoldbachltOLD  41707  tgblthelfgottOLD  41709  tgoldbachOLD  41712  pw2m1lepw2m1  42310  m1modmmod  42316  difmodm1lt  42317  fllogbd  42354  logbpw2m1  42361  fllog2  42362  nnpw2blen  42374  nnolog2flm1  42384  dignn0flhalflem1  42409  dignn0flhalflem2  42410