Theorem zred 12806

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

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2144  ℝcr 11202  ℤcz 12696

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3or 1104  df-3an 1105  df-tru 1572  df-fal 1582  df-ex 1812  df-sb 2099  df-clab 2739  df-cleq 2752  df-clel 2835  df-rab 3413  df-v 3452  df-ss 3896  df-dif 4047  df-un 4151  df-nul 4279  df-if 4482  df-sn 4585  df-pr 4587  df-op 4835  df-uni 4867  df-br 5103  df-iota 6494  df-fv 6546  df-ov 7423  df-neg 11547  df-z 12697

This theorem is used by:  zcnd  12807  suprfinzcl  12816  eluzmn  12975  eluzelre  12979  eluzadd  12997  subeluzsub  13001  uzm1  13002  zsupss  13067  suprzcl2  13068  uzwo3  13073  rpnnen1lem3  13110  rpnnen1lem5  13112  zltaddlt1le  13639  fzsplit2  13686  fzdisj  13688  ssfzunsnext  13706  fzpreddisj  13710  fznatpl1  13715  fzp1disj  13720  uzdisj  13734  fzdif1  13742  fzm1  13744  fz0fzdiffz0  13774  elfzmlbm  13775  elfzmlbp  13776  difelfznle  13779  nn0disj  13781  elfzolt3  13807  fzonel  13811  fzospliti  13829  fzodisj  13831  fzouzdisj  13833  fzodisjsn  13835  elfzo0subge1  13843  elfzo0suble  13844  fzonmapblen  13846  fzoaddel  13855  elincfzoext  13861  fzone1  13922  reflcl  13939  flge  13948  flwordi  13955  fladdz  13968  2tnp1ge0ge0  13972  flhalf  13973  fldiv4p1lem1div2  13978  fldiv4lem1div2uz2  13979  fldiv4lem1div2  13980  flleceil  13996  fleqceilz  13997  quoremz  13998  uzsup  14006  modaddid  14053  modmul12d  14071  modaddmodup  14080  modaddmodlo  14081  modfzo0difsn  14089  modsumfzodifsn  14090  addmodlteq  14092  om2uzlti  14096  om2uzf1oi  14099  seqf1olem1  14187  seqf1olem2  14188  bcval4  14454  bcp1nk  14464  bcval5  14465  fzsdom2  14576  seqcoll  14612  seqcoll2  14613  ccatrn  14738  ccatalpha  14743  cshwidxmodr  14959  fzomaxdiflem  15515  fzomaxdif  15516  rexuzre  15525  limsupgre  15653  rlimclim1  15717  isercoll  15840  iseralt  15857  fsumm1  15922  fsum1p  15924  fsum0diaglem  15947  modfsummods  15965  isumsplit  16014  climcndslem1  16023  mertenslem1  16058  ntrivcvgmul  16076  fprodntriv  16114  fprod1p  16140  fprodeq0  16147  fallfacval4  16214  bpoly4  16230  fzo0dvdseq  16498  dvdsmod  16504  oexpneg  16520  mod2eq1n2dvds  16522  ltoddhalfle  16536  flodddiv4t2lthalf  16593  bitsp1  16606  bitsfzolem  16609  bitsfzo  16610  bitsmod  16611  bitscmp  16613  bitsinv1lem  16616  sadaddlem  16641  bitsres  16648  bitsuz  16649  smumul  16668  gcd0id  16696  gcdneg  16699  dfgcd2  16724  nn0seqcvgd  16750  lcmgcdlem  16786  nprm  16868  prmdvdsfz  16886  isprm5  16888  isprm7  16889  coprm  16892  prmexpb  16900  prmfac1  16901  hashdvds  16957  crth  16960  eulerthlem2  16964  fermltl  16966  prmdiv  16967  prmdiveq  16968  hashgcdlem  16970  odzdvds  16978  vfermltlALT  16985  modprm0  16988  modprmn0modprm0  16990  prm23ge5  16998  pythagtriplem13  17010  pcxcl  17044  pcaddlem  17071  pcadd  17072  pcfac  17082  qexpz  17084  prmunb  17097  1arithlem4  17109  4sqlem5  17125  4sqlem6  17126  4sqlem7  17127  4sqlem10  17130  4sqlem11  17138  4sqlem12  17139  4sqlem15  17142  4sqlem16  17143  4sqlem17  17144  vdwnnlem3  17180  prmgaplem7  17240  cshwshashlem3  17280  chnub  18801  chnso  18803  chnccat  18805  chnpof1  18809  subgmulg  19356  mndodconglem  19760  odnncl  19764  odmod  19765  oddvds  19766  dfod2  19783  sylow1lem3  19819  efgsp1  19956  efgredleme  19962  telgsumfzs  20208  zringlpirlem1  21773  zringlpirlem3  21775  fermltlchr  21840  znf1o  21862  zcld  25138  ovoliunlem1  25828  ovoliunlem2  25829  dyadss  25920  dyaddisjlem  25921  dyadmaxlem  25923  dvfsumle  26346  dvfsumge  26347  dvfsumabs  26348  dvfsumlem1  26351  dvfsumlem3  26353  degltlem1  26395  plyco0  26515  plyeq0lem  26534  plydivex  26623  aannenlem1  26660  efif1olem2  26876  nnlogbexp  27114  logblt  27117  ang180lem1  27142  ang180lem3  27144  wilthlem2  27401  basellem3  27415  basellem4  27416  ppiprm  27483  chtdif  27490  ppidif  27495  chtub  27544  mersenne  27559  bcmono  27609  bcmax  27610  bposlem1  27616  bposlem3  27618  bposlem5  27620  bposlem6  27621  lgsval2lem  27639  lgsvalmod  27648  lgsneg  27653  lgsmod  27655  lgsdilem  27656  lgsdirprm  27663  lgsdilem2  27665  lgsne0  27667  lgssq  27669  lgssq2  27670  lgsqr  27683  lgsdchr  27687  gausslemma2dlem1a  27697  gausslemma2dlem3  27700  gausslemma2dlem5a  27702  gausslemma2dlem6  27704  gausslemma2d  27706  lgseisenlem1  27707  lgseisenlem2  27708  lgseisenlem3  27709  lgseisenlem4  27710  lgsquadlem1  27712  lgsquadlem2  27713  lgsquadlem3  27714  lgsquad3  27719  2lgslem1a2  27722  2lgslem1  27726  2lgslem2  27727  2sqlem3  27752  2sqlem8  27758  2sqblem  27763  2sqmod  27768  chebbnd1lem1  27801  chebbnd1lem2  27802  chebbnd1lem3  27803  dchrmusum2  27826  dchrvmasumlem1  27827  dchrvmasum2lem  27828  dchrvmasum2if  27829  dchrvmasumlem3  27831  dchrvmasumiflem2  27834  dchrisum0lem1  27848  dchrmusumlem  27854  mudivsum  27862  mulogsumlem  27863  mulogsum  27864  mulog2sumlem2  27867  mulog2sumlem3  27868  selberglem1  27877  selberglem2  27878  pntpbnd1  27918  pntlemg  27930  pntlemf  27937  qabvle  27957  padicabv  27962  padicabvcxp  27964  ostth2lem2  27966  axlowdimlem13  29537  axlowdimlem16  29540  pthdlem1  30357  crctcshwlkn0  30415  crctcsh  30418  clwwisshclwwslemlem  30609  eucrctshift  30849  nndiffz1  33424  fzsplit3  33431  bcm1n  33433  suppssnn0  33443  ltesubnnd  33460  wrdt2ind  33562  cshwrnid  33568  cycpmfv2  33721  cycpmco2lem6  33738  cycpmco2lem7  33739  cycpmrn  33750  cyc3conja  33764  pnfinf  33790  znfermltl  33968  constrext2chnlem  34428  cos9thpiminplylem1  34460  cos9thpiminplylem2  34461  dya2iocress  34952  dya2iocbrsiga  34953  dya2icobrsiga  34954  dya2icoseg  34955  dya2iocucvr  34962  sxbrsigalem2  34964  ballotlemfc0  35171  ballotlemfcc  35172  ballotlemodife  35176  ballotlemimin  35184  ballotlemsgt1  35189  ballotlemsel1i  35191  ballotlemsi  35193  ballotlemsima  35194  ballotlemrv2  35200  ballotlemfrceq  35207  ballotlemfrcn0  35208  ballotlemirc  35210  fsum2dsub  35282  reprlt  35294  reprgt  35296  breprexplemc  35307  tgoldbachgnn  35334  tgoldbachgt  35338  subfacval3  36040  erdszelem8  36049  erdszelem9  36050  supfz  36586  inffz  36587  dnizeq0  37433  dnizphlfeqhlf  37434  dnibndlem13  37448  knoppndvlem1  37470  knoppndvlem2  37471  knoppndvlem7  37476  knoppndvlem19  37488  knoppndvlem21  37490  ltflcei  38624  leceifl  38625  poimirlem1  38632  poimirlem2  38633  poimirlem6  38637  poimirlem7  38638  poimirlem8  38639  poimirlem15  38646  poimirlem16  38647  poimirlem17  38648  poimirlem19  38650  poimirlem20  38651  poimirlem23  38654  poimirlem24  38655  poimirlem27  38658  poimirlem29  38660  poimirlem31  38662  poimirlem32  38663  mblfinlem2  38669  itg2addnclem2  38683  mettrifi  38784  cntotbnd  38823  fzne2d  43123  aks4d1lem1  43205  aks4d1p1p3  43212  aks4d1p1p2  43213  aks4d1p1p4  43214  aks4d1p1  43219  aks4d1p2  43220  aks4d1p3  43221  aks4d1p5  43223  aks4d1p6  43224  aks4d1p7d1  43225  aks4d1p7  43226  aks4d1p8d3  43229  aks4d1p8  43230  aks4d1p9  43231  posbezout  43243  aks6d1c1  43259  hashscontpow1  43264  hashscontpow  43265  aks6d1c2  43273  aks6d1c5lem1  43279  2ap1caineq  43288  sticksstones6  43294  sticksstones7  43295  sticksstones10  43298  sticksstones12a  43300  sticksstones12  43301  sticksstones22  43311  bcled  43321  bcle2d  43322  aks6d1c7lem1  43323  aks6d1c7lem2  43324  aks6d1c7  43327  aks5lem6  43335  unitscyglem2  43339  unitscyglem4  43341  aks5lem8  43344  sumcubes  43463  frlmvscadiccat  43666  dffltz  43763  lzunuz  43872  lzenom  43874  diophin  43876  irrapxlem1  43922  irrapxlem2  43923  irrapxlem3  43924  irrapxlem4  43925  pellexlem5  43933  pellexlem6  43934  rmspecfund  44009  rmxypos  44047  ltrmynn0  44048  ltrmxnn0  44049  ltrmy  44052  rmyeq0  44053  rmyeq  44054  lermy  44055  rmyabs  44058  jm2.24nn  44059  jm2.17a  44060  jm2.17b  44061  jm2.17c  44062  jm2.24  44063  rmygeid  44064  acongrep  44080  fzmaxdif  44081  acongeq  44083  jm2.22  44095  jm2.23  44096  jm2.26lem3  44101  jm2.27a  44105  jm3.1lem1  44117  jm3.1lem3  44119  expdiophlem1  44121  fzuntd  44550  fzunt1d  44551  fzuntgd  44552  prmunb2  45388  nzprmdif  45396  hashnzfzclim  45399  binomcxplemnn0  45426  uzwo4  46163  ssinc  46195  ssdec  46196  zltlesub  46394  monoords  46406  fzisoeu  46409  fperiodmul  46413  fzdifsuc2  46419  iuneqfzuzlem  46439  uzublem  46533  zxrd  46556  uzinico  46664  uzubioo  46670  fmul01  46685  fmul01lt1lem1  46689  fmul01lt1lem2  46690  climsuselem1  46712  climsuse  46713  sumnnodd  46735  ltmod  46741  limsupresuz  46806  limsupubuzlem  46815  limsupequzlem  46825  limsupmnfuzlem  46829  limsupequzmptlem  46831  limsupre3uzlem  46838  supcnvlimsup  46843  limsup10exlem  46875  liminfresuz  46887  liminfvaluz  46895  limsupvaluz3  46901  ioodvbdlimc1lem2  47035  ioodvbdlimc2lem  47037  dvnmul  47046  dvnprodlem1  47049  dvnprodlem2  47050  iblspltprt  47076  itgspltprt  47082  stoweidlem3  47106  stoweidlem11  47114  stoweidlem20  47123  stoweidlem26  47129  stoweidlem34  47137  stoweidlem59  47162  stirlinglem5  47181  dirkertrigeqlem3  47203  dirkeritg  47205  dirkercncflem1  47206  dirkercncflem2  47207  dirkercncflem4  47209  fourierdlem4  47214  fourierdlem6  47216  fourierdlem7  47217  fourierdlem11  47221  fourierdlem12  47222  fourierdlem15  47225  fourierdlem19  47229  fourierdlem20  47230  fourierdlem25  47235  fourierdlem26  47236  fourierdlem34  47244  fourierdlem35  47245  fourierdlem41  47251  fourierdlem48  47257  fourierdlem49  47258  fourierdlem50  47259  fourierdlem51  47260  fourierdlem54  47263  fourierdlem63  47272  fourierdlem64  47273  fourierdlem65  47274  fourierdlem71  47280  fourierdlem79  47288  fourierdlem89  47298  fourierdlem90  47299  fourierdlem91  47300  fourierdlem102  47311  fourierdlem103  47312  fourierdlem104  47313  fourierdlem114  47323  fouriersw  47334  elaa2lem  47336  etransclem3  47340  etransclem4  47341  etransclem7  47344  etransclem10  47347  etransclem15  47352  etransclem19  47356  etransclem23  47360  etransclem24  47361  etransclem25  47362  etransclem27  47364  etransclem31  47368  etransclem32  47369  etransclem35  47372  etransclem41  47378  etransclem44  47381  etransclem46  47383  etransclem48  47385  iundjiun  47563  caratheodorylem1  47629  hoicvr  47651  smflimsuplem4  47926  smfliminflem  47933  ormklocald  47979  ormkglobd  47980  chnerlem3  47987  2elfz2melfz  48481  elfzelfzlble  48484  fzopredsuc  48487  nnmul2  48493  2ltceilhalf  48495  ceilhalfgt1  48496  ceilhalfnn  48503  submodlt  48519  m1modmmod  48527  difmodm1lt  48528  modmknepk  48531  mod2addne  48533  2timesltsq  48541  2timesltsqm1  48542  fsummsndifre  48543  iccpartgt  48602  icceuelpartlem  48610  icceuelpart  48611  iccpartnel  48613  nprmmul2  48703  nprmmul3  48704  lighneallem2  48784  proththd  48792  nprmdvdsfacm1lem4  48801  dfodd4  48850  oexpnegALTV  48868  nnoALTV  48886  evenltle  48908  fpprwppr  48930  gbowgt5  48953  gboge9  48955  stgoldbwt  48967  sbgoldbst  48969  sbgoldbalt  48972  sgoldbeven3prm  48974  mogoldbb  48976  bgoldbtbndlem1  48996  bgoldbtbndlem2  48997  bgoldbtbndlem3  48998  bgoldbtbnd  49000  bgoldbachlt  49004  tgblthelfgott  49006  tgoldbach  49008  upgrimpthslem2  49099  gpgprismgrusgra  49249  gpgedgvtx1  49253  gpgvtxedg0  49254  gpgvtxedg1  49255  gpg5nbgrvtx13starlem2  49263  gpg3nbgrvtx0  49267  gpg3kgrtriexlem1  49274  gpg3kgrtriexlem4  49277  gpg3kgrtriexlem6  49279  pw2m1lepw2m1  49725  fllogbd  49765  logbpw2m1  49772  fllog2  49773  nnpw2blen  49785  nnolog2flm1  49795  dignn0flhalflem1  49820  dignn0flhalflem2  49821