Theorem eluzelz 12828

Description: A member of an upper set of integers is an integer. (Contributed by NM, 6-Sep-2005.)

Assertion

Ref	Expression
eluzelz	⊢ (𝑁 ∈ (ℤ≥‘𝑀) → 𝑁 ∈ ℤ)

Proof of Theorem eluzelz

Step	Hyp	Ref	Expression
1		eluz2 12824	. 2 ⊢ (𝑁 ∈ (ℤ≥‘𝑀) ↔ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑀 ≤ 𝑁))
2	1	simp2bi 1146	1 ⊢ (𝑁 ∈ (ℤ≥‘𝑀) → 𝑁 ∈ ℤ)

Syntax hints:   → wi 4   ∈ wcel 2106   class class class wbr 5147  ‘cfv 6540   ≤ cle 11245  ℤcz 12554  ℤ_≥cuz 12818

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2703  ax-sep 5298  ax-nul 5305  ax-pr 5426  ax-cnex 11162  ax-resscn 11163

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3or 1088  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-nf 1786  df-sb 2068  df-mo 2534  df-eu 2563  df-clab 2710  df-cleq 2724  df-clel 2810  df-nfc 2885  df-ral 3062  df-rex 3071  df-rab 3433  df-v 3476  df-dif 3950  df-un 3952  df-in 3954  df-ss 3964  df-nul 4322  df-if 4528  df-pw 4603  df-sn 4628  df-pr 4630  df-op 4634  df-uni 4908  df-br 5148  df-opab 5210  df-mpt 5231  df-id 5573  df-xp 5681  df-rel 5682  df-cnv 5683  df-co 5684  df-dm 5685  df-rn 5686  df-res 5687  df-ima 5688  df-iota 6492  df-fun 6542  df-fn 6543  df-f 6544  df-fv 6548  df-ov 7408  df-neg 11443  df-z 12555  df-uz 12819

This theorem is referenced by:  eluzelre  12829  uztrn  12836  uzneg  12838  uzss  12841  eluzp1l  12845  eluzadd  12847  eluzsub  12848  eluzaddiOLD  12850  eluzsubiOLD  12852  subeluzsub  12855  uzm1  12856  uzin  12858  uzind4  12886  uzwo  12891  uz2mulcl  12906  uzsupss  12920  elfz5  13489  elfzel2  13495  elfzelz  13497  eluzfz2  13505  peano2fzr  13510  fzsplit2  13522  fzopth  13534  ssfzunsn  13543  fzsuc  13544  elfz1uz  13567  uzsplit  13569  uzdisj  13570  fzm1  13577  uznfz  13580  nn0disj  13613  preduz  13619  elfzo3  13645  fzoss2  13656  fzouzsplit  13663  fzoun  13665  eluzgtdifelfzo  13690  fzosplitsnm1  13703  fzofzp1b  13726  elfzonelfzo  13730  fzosplitsn  13736  fzisfzounsn  13740  fldiv4lem1div2uz2  13797  m1modge3gt1  13879  modaddmodup  13895  om2uzlti  13911  om2uzf1oi  13914  uzrdgxfr  13928  fzen2  13930  seqfveq2  13986  seqfeq2  13987  seqshft2  13990  monoord  13994  monoord2  13995  sermono  13996  seqsplit  13997  seqf1olem1  14003  seqf1olem2  14004  seqid  14009  leexp2a  14133  expnlbnd2  14193  expmulnbnd  14194  hashfz  14383  fzsdom2  14384  hashfzo  14385  hashfzp1  14387  seqcoll  14421  swrdfv2  14607  pfxccatin12  14679  rexuz3  15291  r19.2uz  15294  rexuzre  15295  cau4  15299  caubnd2  15300  clim  15434  climrlim2  15487  climshft2  15522  climaddc1  15575  climmulc2  15577  climsubc1  15578  climsubc2  15579  clim2ser  15597  clim2ser2  15598  iserex  15599  climlec2  15601  climub  15604  isercolllem2  15608  isercoll  15610  isercoll2  15611  climcau  15613  caurcvg2  15620  caucvgb  15622  serf0  15623  iseraltlem1  15624  iseraltlem2  15625  iseralt  15627  sumrblem  15653  fsumcvg  15654  summolem2a  15657  fsumcvg2  15669  fsumm1  15693  fzosump1  15694  fsump1  15698  fsumrev2  15724  telfsumo  15744  fsumparts  15748  isumsplit  15782  isumrpcl  15785  isumsup2  15788  cvgrat  15825  mertenslem1  15826  clim2div  15831  prodeq2ii  15853  fprodcvg  15870  prodmolem2a  15874  zprod  15877  fprodntriv  15882  fprodser  15889  fprodm1  15907  fprodp1  15909  fprodeq0  15915  isprm3  16616  nprm  16621  dvdsprm  16636  exprmfct  16637  isprm5  16640  maxprmfct  16642  prmdvdsncoprmbd  16659  ncoprmlnprm  16660  phibndlem  16699  dfphi2  16703  hashdvds  16704  pcaddlem  16817  pcfac  16828  expnprm  16831  prmreclem4  16848  vdwlem8  16917  gsumval2a  18600  efgs1b  19598  telgsumfzs  19851  iscau4  24787  caucfil  24791  iscmet3lem3  24798  iscmet3lem1  24799  iscmet3lem2  24800  lmle  24809  uniioombllem3  25093  mbflimsup  25174  mbfi1fseqlem6  25229  dvfsumle  25529  dvfsumge  25530  dvfsumabs  25531  aaliou3lem1  25846  aaliou3lem2  25847  ulmres  25891  ulmshftlem  25892  ulmshft  25893  ulmcaulem  25897  ulmcau  25898  ulmdvlem1  25903  radcnvlem1  25916  logblt  26278  logbgcd1irr  26288  muval1  26626  chtdif  26651  ppidif  26656  chtub  26704  bcmono  26769  bpos1lem  26774  lgsquad2lem2  26877  2sqlem6  26915  2sqlem8a  26917  2sqlem8  26918  chebbnd1lem1  26961  dchrisumlem2  26982  dchrisum0lem1  27008  ostthlem2  27120  ostth2  27129  axlowdimlem3  28191  axlowdimlem6  28194  axlowdimlem7  28195  axlowdimlem16  28204  axlowdimlem17  28205  axlowdim  28208  clwwnrepclwwn  29586  fzspl  31988  fzdif2  31989  supfz  34686  divcnvlin  34690  gg-dvfsumle  35170  nn0prpwlem  35195  fdc  36601  mettrifi  36613  caushft  36617  aks4d1lem1  40915  aks4d1p1  40929  aks4d1p2  40930  aks4d1p3  40931  aks4d1p5  40933  aks4d1p6  40934  aks4d1p7d1  40935  aks4d1p7  40936  aks4d1p8  40940  aks4d1p9  40941  fzosumm1  41065  dffltz  41372  rmspecnonsq  41630  rmspecfund  41632  rmxyadd  41645  rmxy1  41646  jm2.18  41712  jm2.22  41719  jm2.15nn0  41727  jm2.16nn0  41728  jm2.27a  41729  jm2.27c  41731  jm3.1lem2  41742  jm3.1lem3  41743  jm3.1  41744  expdiophlem1  41745  dvgrat  43056  cvgdvgrat  43057  hashnzfz  43064  uzwo4  43725  ssinc  43761  ssdec  43762  rexanuz3  43770  monoords  43993  fzdifsuc2  44006  iuneqfzuzlem  44030  eluzelzd  44071  allbutfi  44089  eluzelz2  44099  uzid2  44101  monoordxrv  44178  monoord2xrv  44180  fmul01  44282  fmul01lt1lem1  44286  fmul01lt1lem2  44287  climsuselem1  44309  climsuse  44310  climf  44324  climresmpt  44361  climf2  44368  limsupequzlem  44424  limsupmnfuzlem  44428  limsupre3uzlem  44437  itgsinexp  44657  iblspltprt  44675  itgspltprt  44681  iundjiun  45162  smflimsuplem2  45523  smflimsuplem4  45525  smflimsuplem5  45526  fzopredsuc  46017  smonoord  46025  iccpartiltu  46076  fmtnoprmfac2lem1  46220  fmtnofac2lem  46222  lighneallem2  46260  lighneallem4a  46262  lighneallem4b  46263  fppr2odd  46385  fpprwpprb  46394  gboge9  46418  nnsum3primesle9  46448  nnsum4primesevenALTV  46455  wtgoldbnnsum4prm  46456  bgoldbnnsum3prm  46458  bgoldbtbndlem2  46460  m1modmmod  47160  fllogbd  47199  fllog2  47207  dignn0ldlem  47241  dignnld  47242  digexp  47246  dignn0flhalf  47257  nn0sumshdiglemB  47259