Theorem eluzle 12748

Description: Implication of membership in an upper set of integers. (Contributed by NM, 6-Sep-2005.)

Assertion

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

Proof of Theorem eluzle

Step	Hyp	Ref	Expression
1		eluz2 12741	. 2 ⊢ (𝑁 ∈ (ℤ≥‘𝑀) ↔ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑀 ≤ 𝑁))
2	1	simp3bi 1147	1 ⊢ (𝑁 ∈ (ℤ≥‘𝑀) → 𝑀 ≤ 𝑁)

Syntax hints:   → wi 4   ∈ wcel 2109   class class class wbr 5092  ‘cfv 6482   ≤ cle 11150  ℤcz 12471  ℤ_≥cuz 12735

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-10 2142  ax-11 2158  ax-12 2178  ax-ext 2701  ax-sep 5235  ax-nul 5245  ax-pr 5371  ax-cnex 11065  ax-resscn 11066

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2533  df-eu 2562  df-clab 2708  df-cleq 2721  df-clel 2803  df-nfc 2878  df-ral 3045  df-rex 3054  df-rab 3395  df-v 3438  df-dif 3906  df-un 3908  df-in 3910  df-ss 3920  df-nul 4285  df-if 4477  df-pw 4553  df-sn 4578  df-pr 4580  df-op 4584  df-uni 4859  df-br 5093  df-opab 5155  df-mpt 5174  df-id 5514  df-xp 5625  df-rel 5626  df-cnv 5627  df-co 5628  df-dm 5629  df-rn 5630  df-res 5631  df-ima 5632  df-iota 6438  df-fun 6484  df-fn 6485  df-f 6486  df-fv 6490  df-ov 7352  df-neg 11350  df-z 12472  df-uz 12736

This theorem is referenced by:  uztrn  12753  uzneg  12755  uzss  12758  uz11  12760  eluzp1l  12762  eluzadd  12764  eluzsub  12765  subeluzsub  12772  uzm1  12773  uzin  12775  uzind4  12807  uzwo  12812  uzsupss  12841  ge2halflem1  13010  elfz5  13419  elfzle1  13430  elfzle2  13431  elfzle3  13433  elfz1uz  13497  uzsplit  13499  uzdisj  13500  uznfz  13513  elfz2nn0  13521  uzsubfz0  13539  nn0disj  13547  fzouzdisj  13598  fzoun  13599  fldiv4lem1div2uz2  13740  m1modge3gt1  13825  expmulnbnd  14142  seqcoll  14371  swrdlen2  14567  swrdfv2  14568  rexuzre  15260  rlimclim1  15452  isercoll  15575  iseralt  15592  o1fsum  15720  mertenslem1  15791  fprodeq0  15882  efcllem  15984  rpnnen2lem9  16131  smuval2  16393  smupvallem  16394  isprm7  16619  hashdvds  16686  pcmpt2  16805  pcfaclem  16810  pcfac  16811  vdwlem6  16898  ramtlecl  16912  prmlem1  17019  prmlem2  17031  znfld  21467  lmnn  25161  mbflimsup  25565  mbfi1fseqlem6  25619  dvfsumge  25926  plyco0  26095  coeeulem  26127  radcnvlem2  26321  log2tlbnd  26853  lgamgulmlem4  26940  lgamcvg2  26963  chtub  27121  chpval2  27127  chpchtsum  27128  bcmax  27187  bpos1lem  27191  bpos1  27192  bposlem3  27195  bposlem4  27196  bposlem5  27197  bposlem6  27198  lgslem1  27206  lgsdirprm  27240  lgseisen  27288  dchrisumlema  27397  dchrisumlem2  27399  dchrisum0lem1  27425  axlowdimlem3  28889  axlowdimlem6  28892  axlowdimlem7  28893  axlowdimlem16  28902  axlowdimlem17  28903  dlwwlknondlwlknonf1olem1  30308  minvecolem3  30820  minvecolem4  30824  breprexplemc  34600  subfacval3  35166  climuzcnv  35648  knoppndvlem6  36495  poimirlem29  37633  fdc  37729  aks4d1lem1  42039  aks4d1p1  42053  aks4d1p2  42054  aks4d1p3  42055  aks4d1p5  42057  aks4d1p6  42058  aks4d1p7d1  42059  aks4d1p7  42060  aks4d1p8  42064  aks4d1p9  42065  aks6d1c7lem1  42157  aks6d1c7lem2  42158  aks6d1c7  42161  aks5lem6  42169  aks5lem8  42178  jm2.24nn  42936  jm2.23  42973  expdiophlem1  42998  hashnzfz2  44298  bccbc  44322  binomcxplemnn0  44326  ssinc  45069  ssdec  45070  fzdifsuc2  45296  uzfissfz  45310  iuneqfzuzlem  45318  ssuzfz  45333  uzublem  45413  uzinico  45544  fmul01lt1lem1  45569  climsuselem1  45592  climsuse  45593  limsupubuzlem  45697  limsupequzlem  45707  limsupmnfuzlem  45711  limsupre3uzlem  45720  ioodvbdlimc1lem2  45917  ioodvbdlimc2lem  45919  iblspltprt  45958  itgspltprt  45964  stoweidlem11  45996  stirlinglem11  46069  fourierdlem79  46170  fourierdlem103  46194  fourierdlem104  46195  vonioolem1  46665  2ltceilhalf  47316  ceilhalfnn  47324  fmtnoprmfac1  47553  fmtnoprmfac2lem1  47554  lighneallem2  47594  lighneallem4a  47596  gboge9  47752  bgoldbnnsum3prm  47792  nnolog2flm1  48579