Theorem eluzle 12595

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

Syntax hints:   → wi 4   ∈ wcel 2106   class class class wbr 5074  ‘cfv 6433   ≤ cle 11010  ℤcz 12319  ℤ_≥cuz 12582

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  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 2709  ax-sep 5223  ax-nul 5230  ax-pr 5352  ax-cnex 10927  ax-resscn 10928

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3or 1087  df-3an 1088  df-tru 1542  df-fal 1552  df-ex 1783  df-nf 1787  df-sb 2068  df-mo 2540  df-eu 2569  df-clab 2716  df-cleq 2730  df-clel 2816  df-nfc 2889  df-ral 3069  df-rex 3070  df-rab 3073  df-v 3434  df-dif 3890  df-un 3892  df-in 3894  df-ss 3904  df-nul 4257  df-if 4460  df-pw 4535  df-sn 4562  df-pr 4564  df-op 4568  df-uni 4840  df-br 5075  df-opab 5137  df-mpt 5158  df-id 5489  df-xp 5595  df-rel 5596  df-cnv 5597  df-co 5598  df-dm 5599  df-rn 5600  df-res 5601  df-ima 5602  df-iota 6391  df-fun 6435  df-fn 6436  df-f 6437  df-fv 6441  df-ov 7278  df-neg 11208  df-z 12320  df-uz 12583

This theorem is referenced by:  uztrn  12600  uzneg  12602  uzss  12605  uz11  12607  eluzp1l  12609  subeluzsub  12615  uzm1  12616  uzin  12618  uzind4  12646  uzwo  12651  uzsupss  12680  elfz5  13248  elfzle1  13259  elfzle2  13260  elfzle3  13262  elfz1uz  13326  uzsplit  13328  uzdisj  13329  uznfz  13339  elfz2nn0  13347  uzsubfz0  13364  nn0disj  13372  fzouzdisj  13423  fzoun  13424  fldiv4lem1div2uz2  13556  m1modge3gt1  13638  expmulnbnd  13950  seqcoll  14178  swrdlen2  14373  swrdfv2  14374  rexuzre  15064  rlimclim1  15254  isercoll  15379  iseralt  15396  o1fsum  15525  mertenslem1  15596  fprodeq0  15685  efcllem  15787  rpnnen2lem9  15931  smuval2  16189  smupvallem  16190  isprm7  16413  hashdvds  16476  pcmpt2  16594  pcfaclem  16599  pcfac  16600  vdwlem6  16687  ramtlecl  16701  prmlem1  16809  prmlem2  16821  znfld  20768  lmnn  24427  mbflimsup  24830  mbfi1fseqlem6  24885  dvfsumge  25186  plyco0  25353  coeeulem  25385  radcnvlem2  25573  log2tlbnd  26095  lgamgulmlem4  26181  lgamcvg2  26204  chtub  26360  chpval2  26366  chpchtsum  26367  bcmax  26426  bpos1lem  26430  bpos1  26431  bposlem3  26434  bposlem4  26435  bposlem5  26436  bposlem6  26437  lgslem1  26445  lgsdirprm  26479  lgseisen  26527  dchrisumlema  26636  dchrisumlem2  26638  dchrisum0lem1  26664  axlowdimlem3  27312  axlowdimlem6  27315  axlowdimlem7  27316  axlowdimlem16  27325  axlowdimlem17  27326  dlwwlknondlwlknonf1olem1  28728  minvecolem3  29238  minvecolem4  29242  breprexplemc  32612  subfacval3  33151  climuzcnv  33629  knoppndvlem6  34697  poimirlem29  35806  fdc  35903  aks4d1lem1  40070  aks4d1p1  40084  aks4d1p2  40085  aks4d1p3  40086  aks4d1p5  40088  aks4d1p6  40089  aks4d1p7d1  40090  aks4d1p7  40091  aks4d1p8  40095  aks4d1p9  40096  jm2.24nn  40781  jm2.23  40818  expdiophlem1  40843  hashnzfz2  41939  bccbc  41963  binomcxplemnn0  41967  ssinc  42637  ssdec  42638  fzdifsuc2  42849  uzfissfz  42865  iuneqfzuzlem  42873  ssuzfz  42888  uzublem  42970  uzinico  43098  fmul01lt1lem1  43125  climsuselem1  43148  climsuse  43149  limsupubuzlem  43253  limsupequzlem  43263  limsupmnfuzlem  43267  limsupre3uzlem  43276  ioodvbdlimc1lem2  43473  ioodvbdlimc2lem  43475  iblspltprt  43514  itgspltprt  43520  stoweidlem11  43552  stirlinglem11  43625  fourierdlem79  43726  fourierdlem103  43750  fourierdlem104  43751  vonioolem1  44218  fmtnoprmfac1  45017  fmtnoprmfac2lem1  45018  lighneallem2  45058  lighneallem4a  45060  gboge9  45216  bgoldbnnsum3prm  45256  nnolog2flm1  45936