Theorem eluzelz 12742

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 12738	. 2 ⊢ (𝑁 ∈ (ℤ≥‘𝑀) ↔ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑀 ≤ 𝑁))
2	1	simp2bi 1146	1 ⊢ (𝑁 ∈ (ℤ≥‘𝑀) → 𝑁 ∈ ℤ)

Syntax hints:   → wi 4   ∈ wcel 2111   class class class wbr 5089  ‘cfv 6481   ≤ cle 11147  ℤcz 12468  ℤ_≥cuz 12732

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 2113  ax-9 2121  ax-10 2144  ax-11 2160  ax-12 2180  ax-ext 2703  ax-sep 5232  ax-nul 5242  ax-pr 5368  ax-cnex 11062  ax-resscn 11063

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-nf 1785  df-sb 2068  df-mo 2535  df-eu 2564  df-clab 2710  df-cleq 2723  df-clel 2806  df-nfc 2881  df-ne 2929  df-ral 3048  df-rex 3057  df-rab 3396  df-v 3438  df-dif 3900  df-un 3902  df-in 3904  df-ss 3914  df-nul 4281  df-if 4473  df-pw 4549  df-sn 4574  df-pr 4576  df-op 4580  df-uni 4857  df-br 5090  df-opab 5152  df-mpt 5171  df-id 5509  df-xp 5620  df-rel 5621  df-cnv 5622  df-co 5623  df-dm 5624  df-rn 5625  df-res 5626  df-ima 5627  df-iota 6437  df-fun 6483  df-fn 6484  df-f 6485  df-fv 6489  df-ov 7349  df-neg 11347  df-z 12469  df-uz 12733

This theorem is referenced by:  eluzelre  12743  uztrn  12750  uzneg  12752  uzss  12755  eluzp1l  12759  eluzadd  12761  eluzsub  12762  eluzaddiOLD  12764  eluzsubiOLD  12766  subeluzsub  12769  uzm1  12770  uzin  12772  uzind4  12804  uzwo  12809  uz2mulcl  12824  uzsupss  12838  elfz5  13416  elfzel2  13422  elfzelz  13424  eluzfz2  13432  peano2fzr  13437  fzsplit2  13449  fzopth  13461  ssfzunsn  13470  fzsuc  13471  elfz1uz  13494  uzsplit  13496  uzdisj  13497  fzm1  13507  uznfz  13510  nn0disj  13544  preduz  13550  elfzo3  13576  fzoss2  13587  fzouzsplit  13594  fzoun  13596  eluzgtdifelfzo  13627  fzosplitsnm1  13640  fzofzp1b  13665  elfzonelfzo  13669  fzosplitsn  13676  fzisfzounsn  13680  fldiv4lem1div2uz2  13740  m1modge3gt1  13825  modaddmodup  13841  om2uzlti  13857  om2uzf1oi  13860  uzrdgxfr  13874  fzen2  13876  seqfveq2  13931  seqfeq2  13932  seqshft2  13935  monoord  13939  monoord2  13940  sermono  13941  seqsplit  13942  seqf1olem1  13948  seqf1olem2  13949  seqid  13954  leexp2a  14079  expnlbnd2  14141  expmulnbnd  14142  hashfz  14334  fzsdom2  14335  hashfzo  14336  hashfzp1  14338  seqcoll  14371  swrdfv2  14569  pfxccatin12  14640  rexuz3  15256  r19.2uz  15259  rexuzre  15260  cau4  15264  caubnd2  15265  clim  15401  climrlim2  15454  climshft2  15489  climaddc1  15542  climmulc2  15544  climsubc1  15545  climsubc2  15546  clim2ser  15562  clim2ser2  15563  iserex  15564  climlec2  15566  climub  15569  isercolllem2  15573  isercoll  15575  isercoll2  15576  climcau  15578  caurcvg2  15585  caucvgb  15587  serf0  15588  iseraltlem1  15589  iseraltlem2  15590  iseralt  15592  sumrblem  15618  fsumcvg  15619  summolem2a  15622  fsumcvg2  15634  fsumm1  15658  fzosump1  15659  fsump1  15663  fsumrev2  15689  telfsumo  15709  fsumparts  15713  isumsplit  15747  isumrpcl  15750  isumsup2  15753  cvgrat  15790  mertenslem1  15791  clim2div  15796  prodeq2ii  15818  fprodcvg  15837  prodmolem2a  15841  zprod  15844  fprodntriv  15849  fprodser  15856  fprodm1  15874  fprodp1  15876  fprodeq0  15882  isprm3  16594  nprm  16599  dvdsprm  16614  exprmfct  16615  isprm5  16618  maxprmfct  16620  prmdvdsncoprmbd  16638  ncoprmlnprm  16639  phibndlem  16681  dfphi2  16685  hashdvds  16686  pcaddlem  16800  pcfac  16811  expnprm  16814  prmreclem4  16831  vdwlem8  16900  gsumval2a  18593  efgs1b  19648  telgsumfzs  19901  iscau4  25206  caucfil  25210  iscmet3lem3  25217  iscmet3lem1  25218  iscmet3lem2  25219  lmle  25228  uniioombllem3  25513  mbflimsup  25594  mbfi1fseqlem6  25648  dvfsumle  25953  dvfsumleOLD  25954  dvfsumge  25955  dvfsumabs  25956  aaliou3lem1  26277  aaliou3lem2  26278  ulmres  26324  ulmshftlem  26325  ulmshft  26326  ulmcaulem  26330  ulmcau  26331  ulmdvlem1  26336  radcnvlem1  26349  logblt  26721  logbgcd1irr  26731  muval1  27070  chtdif  27095  ppidif  27100  chtub  27150  bcmono  27215  bpos1lem  27220  lgsquad2lem2  27323  2sqlem6  27361  2sqlem8a  27363  2sqlem8  27364  chebbnd1lem1  27407  dchrisumlem2  27428  dchrisum0lem1  27454  ostthlem2  27566  ostth2  27575  axlowdimlem3  28922  axlowdimlem6  28925  axlowdimlem7  28926  axlowdimlem16  28935  axlowdimlem17  28936  axlowdim  28939  clwwnrepclwwn  30324  fzspl  32772  fzdif2  32773  supfz  35773  divcnvlin  35777  nn0prpwlem  36366  fdc  37795  mettrifi  37807  caushft  37811  aks4d1lem1  42165  aks4d1p1  42179  aks4d1p2  42180  aks4d1p3  42181  aks4d1p5  42183  aks4d1p6  42184  aks4d1p7d1  42185  aks4d1p7  42186  aks4d1p8  42190  aks4d1p9  42191  aks6d1c7lem1  42283  aks6d1c7lem2  42284  aks6d1c7  42287  aks5lem6  42295  aks5lem8  42304  aks5  42307  fzosumm1  42353  dffltz  42737  rmspecnonsq  43010  rmspecfund  43012  rmxyadd  43024  rmxy1  43025  jm2.18  43091  jm2.22  43098  jm2.15nn0  43106  jm2.16nn0  43107  jm2.27a  43108  jm2.27c  43110  jm3.1lem2  43121  jm3.1lem3  43122  jm3.1  43123  expdiophlem1  43124  dvgrat  44415  cvgdvgrat  44416  hashnzfz  44423  uzwo4  45160  ssinc  45194  ssdec  45195  rexanuz3  45203  monoords  45408  fzdifsuc2  45421  iuneqfzuzlem  45443  eluzelzd  45483  allbutfi  45501  eluzelz2  45511  uzid2  45513  monoordxrv  45589  monoord2xrv  45591  fmul01  45690  fmul01lt1lem1  45694  fmul01lt1lem2  45695  climsuselem1  45717  climsuse  45718  climf  45732  climresmpt  45767  climf2  45774  limsupequzlem  45830  limsupmnfuzlem  45834  limsupre3uzlem  45843  itgsinexp  46063  iblspltprt  46081  itgspltprt  46087  iundjiun  46568  smflimsuplem2  46929  smflimsuplem4  46931  smflimsuplem5  46932  fzopredsuc  47433  m1modmmod  47468  smonoord  47481  iccpartiltu  47532  fmtnoprmfac2lem1  47676  fmtnofac2lem  47678  lighneallem2  47716  lighneallem4a  47718  lighneallem4b  47719  fppr2odd  47841  fpprwpprb  47850  gboge9  47874  nnsum3primesle9  47904  nnsum4primesevenALTV  47911  wtgoldbnnsum4prm  47912  bgoldbnnsum3prm  47914  bgoldbtbndlem2  47916  gpgusgralem  48166  gpgprismgr4cycllem9  48213  fllogbd  48671  fllog2  48679  dignn0ldlem  48713  dignnld  48714  digexp  48718  dignn0flhalf  48729  nn0sumshdiglemB  48731