Theorem eluzle 12901

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

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2145   class class class wbr 5103  ‘cfv 6533   ≤ cle 11269  ℤcz 12616  ℤ_≥cuz 12888

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-10 2178  ax-11 2194  ax-12 2213  ax-ext 2732  ax-sep 5251  ax-nul 5263  ax-pr 5398  ax-cnex 11181  ax-resscn 11182

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3or 1104  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-nf 1817  df-sb 2100  df-mo 2564  df-eu 2594  df-clab 2739  df-cleq 2752  df-clel 2835  df-nfc 2909  df-ne 2956  df-ral 3077  df-rex 3087  df-rab 3413  df-v 3452  df-dif 3902  df-un 3904  df-in 3906  df-ss 3916  df-nul 4280  df-if 4483  df-pw 4559  df-sn 4585  df-pr 4587  df-op 4591  df-uni 4868  df-br 5104  df-opab 5168  df-mpt 5187  df-id 5550  df-xp 5661  df-rel 5662  df-cnv 5663  df-co 5664  df-dm 5665  df-rn 5666  df-res 5667  df-ima 5668  df-iota 6489  df-fun 6535  df-fn 6536  df-f 6537  df-fv 6541  df-ov 7417  df-neg 11469  df-z 12617  df-uz 12889

This theorem is used by:  uztrn  12906  uzneg  12908  uzss  12911  uz11  12913  eluzp1l  12915  eluzadd  12917  eluzsub  12918  subeluzsub  12921  uzm1  12922  uzin  12924  uzind4  12956  uzwo  12961  uzsupss  12990  ge2halflem1  13160  elfz5  13571  elfzle1  13582  elfzle2  13583  elfzle3  13585  elfz1uz  13650  uzsplit  13652  uzdisj  13653  uznfz  13666  elfz2nn0  13674  uzsubfz0  13692  nn0disj  13700  fzouzdisj  13752  fzoun  13753  fldiv4lem1div2uz2  13898  m1modge3gt1  13983  expmulnbnd  14300  seqcoll  14530  swrdlen2  14731  swrdfv2  14732  rexuzre  15441  rlimclim1  15633  isercoll  15756  iseralt  15773  o1fsum  15901  mertenslem1  15974  fprodeq0  16063  efcllem  16164  rpnnen2lem9  16311  smuval2  16573  smupvallem  16574  isprm7  16800  hashdvds  16867  pcmpt2  16986  pcfaclem  16991  pcfac  16992  vdwlem6  17079  ramtlecl  17093  prmlem1  17200  prmlem2  17213  znfld  21774  lmnn  25492  mbflimsup  25895  mbfi1fseqlem6  25949  dvfsumge  26250  plyco0  26418  coeeulem  26451  radcnvlem2  26651  log2tlbnd  27183  lgamgulmlem4  27269  lgamcvg2  27292  chtub  27449  chpval2  27455  chpchtsum  27456  bcmax  27515  bpos1lem  27519  bpos1  27520  bposlem3  27523  bposlem4  27524  bposlem5  27525  bposlem6  27526  lgslem1  27534  lgsdirprm  27568  lgseisen  27616  dchrisumlema  27725  dchrisumlem2  27727  dchrisum0lem1  27753  axlowdimlem3  29402  axlowdimlem6  29405  axlowdimlem7  29406  axlowdimlem16  29415  axlowdimlem17  29416  dlwwlknondlwlknonf1olem1  30845  minvecolem3  31358  minvecolem4  31362  breprexplemc  35141  subfacval3  35769  climuzcnv  36251  knoppndvlem6  37215  poimirlem29  38399  fdc  38496  aks4d1lem1  42929  aks4d1p1  42943  aks4d1p2  42944  aks4d1p3  42945  aks4d1p5  42947  aks4d1p6  42948  aks4d1p7d1  42949  aks4d1p7  42950  aks4d1p8  42954  aks4d1p9  42955  aks6d1c7lem1  43047  aks6d1c7lem2  43048  aks6d1c7  43051  aks5lem6  43059  aks5lem8  43068  jm2.24nn  43801  jm2.23  43838  expdiophlem1  43863  hashnzfz2  45146  bccbc  45170  binomcxplemnn0  45174  ssinc  45920  ssdec  45921  fzdifsuc2  46144  uzfissfz  46157  iuneqfzuzlem  46165  ssuzfz  46180  uzublem  46259  uzinico  46390  fmul01lt1lem1  46415  climsuselem1  46438  climsuse  46439  limsupubuzlem  46541  limsupequzlem  46551  limsupmnfuzlem  46555  limsupre3uzlem  46564  ioodvbdlimc1lem2  46761  ioodvbdlimc2lem  46763  iblspltprt  46802  itgspltprt  46808  stoweidlem11  46840  stirlinglem11  46913  fourierdlem79  47014  fourierdlem103  47038  fourierdlem104  47039  vonioolem1  47509  nnmul2  48219  2ltceilhalf  48221  ceilhalfnn  48229  2timesltsq  48267  2timesltsqm1  48268  fmtnoprmfac1  48469  fmtnoprmfac2lem1  48470  lighneallem2  48510  lighneallem4a  48512  gboge9  48681  bgoldbnnsum3prm  48721  nnolog2flm1  49521