Theorem eluzle 12891

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

Syntax hints:   → wi 4   ∈ wcel 2108   class class class wbr 5143  ‘cfv 6561   ≤ cle 11296  ℤcz 12613  ℤ_≥cuz 12878

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 2007  ax-8 2110  ax-9 2118  ax-10 2141  ax-11 2157  ax-12 2177  ax-ext 2708  ax-sep 5296  ax-nul 5306  ax-pr 5432  ax-cnex 11211  ax-resscn 11212

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3or 1088  df-3an 1089  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2065  df-mo 2540  df-eu 2569  df-clab 2715  df-cleq 2729  df-clel 2816  df-nfc 2892  df-ral 3062  df-rex 3071  df-rab 3437  df-v 3482  df-dif 3954  df-un 3956  df-in 3958  df-ss 3968  df-nul 4334  df-if 4526  df-pw 4602  df-sn 4627  df-pr 4629  df-op 4633  df-uni 4908  df-br 5144  df-opab 5206  df-mpt 5226  df-id 5578  df-xp 5691  df-rel 5692  df-cnv 5693  df-co 5694  df-dm 5695  df-rn 5696  df-res 5697  df-ima 5698  df-iota 6514  df-fun 6563  df-fn 6564  df-f 6565  df-fv 6569  df-ov 7434  df-neg 11495  df-z 12614  df-uz 12879

This theorem is referenced by:  uztrn  12896  uzneg  12898  uzss  12901  uz11  12903  eluzp1l  12905  eluzadd  12907  eluzsub  12908  subeluzsub  12915  uzm1  12916  uzin  12918  uzind4  12948  uzwo  12953  uzsupss  12982  ge2halflem1  13150  elfz5  13556  elfzle1  13567  elfzle2  13568  elfzle3  13570  elfz1uz  13634  uzsplit  13636  uzdisj  13637  uznfz  13650  elfz2nn0  13658  uzsubfz0  13676  nn0disj  13684  fzouzdisj  13735  fzoun  13736  fldiv4lem1div2uz2  13876  m1modge3gt1  13959  expmulnbnd  14274  seqcoll  14503  swrdlen2  14698  swrdfv2  14699  rexuzre  15391  rlimclim1  15581  isercoll  15704  iseralt  15721  o1fsum  15849  mertenslem1  15920  fprodeq0  16011  efcllem  16113  rpnnen2lem9  16258  smuval2  16519  smupvallem  16520  isprm7  16745  hashdvds  16812  pcmpt2  16931  pcfaclem  16936  pcfac  16937  vdwlem6  17024  ramtlecl  17038  prmlem1  17145  prmlem2  17157  znfld  21579  lmnn  25297  mbflimsup  25701  mbfi1fseqlem6  25755  dvfsumge  26062  plyco0  26231  coeeulem  26263  radcnvlem2  26457  log2tlbnd  26988  lgamgulmlem4  27075  lgamcvg2  27098  chtub  27256  chpval2  27262  chpchtsum  27263  bcmax  27322  bpos1lem  27326  bpos1  27327  bposlem3  27330  bposlem4  27331  bposlem5  27332  bposlem6  27333  lgslem1  27341  lgsdirprm  27375  lgseisen  27423  dchrisumlema  27532  dchrisumlem2  27534  dchrisum0lem1  27560  axlowdimlem3  28959  axlowdimlem6  28962  axlowdimlem7  28963  axlowdimlem16  28972  axlowdimlem17  28973  dlwwlknondlwlknonf1olem1  30383  minvecolem3  30895  minvecolem4  30899  breprexplemc  34647  subfacval3  35194  climuzcnv  35676  knoppndvlem6  36518  poimirlem29  37656  fdc  37752  aks4d1lem1  42063  aks4d1p1  42077  aks4d1p2  42078  aks4d1p3  42079  aks4d1p5  42081  aks4d1p6  42082  aks4d1p7d1  42083  aks4d1p7  42084  aks4d1p8  42088  aks4d1p9  42089  aks6d1c7lem1  42181  aks6d1c7lem2  42182  aks6d1c7  42185  aks5lem6  42193  aks5lem8  42202  jm2.24nn  42971  jm2.23  43008  expdiophlem1  43033  hashnzfz2  44340  bccbc  44364  binomcxplemnn0  44368  ssinc  45092  ssdec  45093  fzdifsuc2  45322  uzfissfz  45337  iuneqfzuzlem  45345  ssuzfz  45360  uzublem  45441  uzinico  45573  fmul01lt1lem1  45599  climsuselem1  45622  climsuse  45623  limsupubuzlem  45727  limsupequzlem  45737  limsupmnfuzlem  45741  limsupre3uzlem  45750  ioodvbdlimc1lem2  45947  ioodvbdlimc2lem  45949  iblspltprt  45988  itgspltprt  45994  stoweidlem11  46026  stirlinglem11  46099  fourierdlem79  46200  fourierdlem103  46224  fourierdlem104  46225  vonioolem1  46695  fmtnoprmfac1  47552  fmtnoprmfac2lem1  47553  lighneallem2  47593  lighneallem4a  47595  gboge9  47751  bgoldbnnsum3prm  47791  2ltceilhalf  48015  nnolog2flm1  48511