Theorem eluzle 12870

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

Syntax hints:   → wi 4   ∈ wcel 2109   class class class wbr 5124  ‘cfv 6536   ≤ cle 11275  ℤcz 12593  ℤ_≥cuz 12857

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 2708  ax-sep 5271  ax-nul 5281  ax-pr 5407  ax-cnex 11190  ax-resscn 11191

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 2540  df-eu 2569  df-clab 2715  df-cleq 2728  df-clel 2810  df-nfc 2886  df-ral 3053  df-rex 3062  df-rab 3421  df-v 3466  df-dif 3934  df-un 3936  df-in 3938  df-ss 3948  df-nul 4314  df-if 4506  df-pw 4582  df-sn 4607  df-pr 4609  df-op 4613  df-uni 4889  df-br 5125  df-opab 5187  df-mpt 5207  df-id 5553  df-xp 5665  df-rel 5666  df-cnv 5667  df-co 5668  df-dm 5669  df-rn 5670  df-res 5671  df-ima 5672  df-iota 6489  df-fun 6538  df-fn 6539  df-f 6540  df-fv 6544  df-ov 7413  df-neg 11474  df-z 12594  df-uz 12858

This theorem is referenced by:  uztrn  12875  uzneg  12877  uzss  12880  uz11  12882  eluzp1l  12884  eluzadd  12886  eluzsub  12887  subeluzsub  12894  uzm1  12895  uzin  12897  uzind4  12927  uzwo  12932  uzsupss  12961  ge2halflem1  13129  elfz5  13538  elfzle1  13549  elfzle2  13550  elfzle3  13552  elfz1uz  13616  uzsplit  13618  uzdisj  13619  uznfz  13632  elfz2nn0  13640  uzsubfz0  13658  nn0disj  13666  fzouzdisj  13717  fzoun  13718  fldiv4lem1div2uz2  13858  m1modge3gt1  13941  expmulnbnd  14258  seqcoll  14487  swrdlen2  14683  swrdfv2  14684  rexuzre  15376  rlimclim1  15566  isercoll  15689  iseralt  15706  o1fsum  15834  mertenslem1  15905  fprodeq0  15996  efcllem  16098  rpnnen2lem9  16245  smuval2  16506  smupvallem  16507  isprm7  16732  hashdvds  16799  pcmpt2  16918  pcfaclem  16923  pcfac  16924  vdwlem6  17011  ramtlecl  17025  prmlem1  17132  prmlem2  17144  znfld  21526  lmnn  25220  mbflimsup  25624  mbfi1fseqlem6  25678  dvfsumge  25985  plyco0  26154  coeeulem  26186  radcnvlem2  26380  log2tlbnd  26912  lgamgulmlem4  26999  lgamcvg2  27022  chtub  27180  chpval2  27186  chpchtsum  27187  bcmax  27246  bpos1lem  27250  bpos1  27251  bposlem3  27254  bposlem4  27255  bposlem5  27256  bposlem6  27257  lgslem1  27265  lgsdirprm  27299  lgseisen  27347  dchrisumlema  27456  dchrisumlem2  27458  dchrisum0lem1  27484  axlowdimlem3  28928  axlowdimlem6  28931  axlowdimlem7  28932  axlowdimlem16  28941  axlowdimlem17  28942  dlwwlknondlwlknonf1olem1  30350  minvecolem3  30862  minvecolem4  30866  breprexplemc  34669  subfacval3  35216  climuzcnv  35698  knoppndvlem6  36540  poimirlem29  37678  fdc  37774  aks4d1lem1  42080  aks4d1p1  42094  aks4d1p2  42095  aks4d1p3  42096  aks4d1p5  42098  aks4d1p6  42099  aks4d1p7d1  42100  aks4d1p7  42101  aks4d1p8  42105  aks4d1p9  42106  aks6d1c7lem1  42198  aks6d1c7lem2  42199  aks6d1c7  42202  aks5lem6  42210  aks5lem8  42219  jm2.24nn  42958  jm2.23  42995  expdiophlem1  43020  hashnzfz2  44320  bccbc  44344  binomcxplemnn0  44348  ssinc  45091  ssdec  45092  fzdifsuc2  45319  uzfissfz  45333  iuneqfzuzlem  45341  ssuzfz  45356  uzublem  45437  uzinico  45568  fmul01lt1lem1  45593  climsuselem1  45616  climsuse  45617  limsupubuzlem  45721  limsupequzlem  45731  limsupmnfuzlem  45735  limsupre3uzlem  45744  ioodvbdlimc1lem2  45941  ioodvbdlimc2lem  45943  iblspltprt  45982  itgspltprt  45988  stoweidlem11  46020  stirlinglem11  46093  fourierdlem79  46194  fourierdlem103  46218  fourierdlem104  46219  vonioolem1  46689  2ltceilhalf  47337  ceilhalfnn  47345  fmtnoprmfac1  47559  fmtnoprmfac2lem1  47560  lighneallem2  47600  lighneallem4a  47602  gboge9  47758  bgoldbnnsum3prm  47798  nnolog2flm1  48550