Theorem eluzle 12900

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

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

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 11180  ax-resscn 11181

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 7416  df-neg 11468  df-z 12616  df-uz 12888

This theorem is used by:  uztrn  12905  uzneg  12907  uzss  12910  uz11  12912  eluzp1l  12914  eluzadd  12916  eluzsub  12917  subeluzsub  12920  uzm1  12921  uzin  12923  uzind4  12955  uzwo  12960  uzsupss  12989  ge2halflem1  13159  elfz5  13570  elfzle1  13581  elfzle2  13582  elfzle3  13584  elfz1uz  13649  uzsplit  13651  uzdisj  13652  uznfz  13665  elfz2nn0  13673  uzsubfz0  13691  nn0disj  13699  fzouzdisj  13751  fzoun  13752  fldiv4lem1div2uz2  13897  m1modge3gt1  13982  expmulnbnd  14299  seqcoll  14529  swrdlen2  14730  swrdfv2  14731  rexuzre  15440  rlimclim1  15632  isercoll  15755  iseralt  15772  o1fsum  15900  mertenslem1  15973  fprodeq0  16062  efcllem  16163  rpnnen2lem9  16310  smuval2  16572  smupvallem  16573  isprm7  16799  hashdvds  16866  pcmpt2  16985  pcfaclem  16990  pcfac  16991  vdwlem6  17078  ramtlecl  17092  prmlem1  17199  prmlem2  17212  znfld  21773  lmnn  25491  mbflimsup  25894  mbfi1fseqlem6  25948  dvfsumge  26249  plyco0  26417  coeeulem  26450  radcnvlem2  26650  log2tlbnd  27182  lgamgulmlem4  27268  lgamcvg2  27291  chtub  27448  chpval2  27454  chpchtsum  27455  bcmax  27514  bpos1lem  27518  bpos1  27519  bposlem3  27522  bposlem4  27523  bposlem5  27524  bposlem6  27525  lgslem1  27533  lgsdirprm  27567  lgseisen  27615  dchrisumlema  27724  dchrisumlem2  27726  dchrisum0lem1  27752  axlowdimlem3  29401  axlowdimlem6  29404  axlowdimlem7  29405  axlowdimlem16  29414  axlowdimlem17  29415  dlwwlknondlwlknonf1olem1  30844  minvecolem3  31357  minvecolem4  31361  breprexplemc  35140  subfacval3  35768  climuzcnv  36250  knoppndvlem6  37214  poimirlem29  38398  fdc  38495  aks4d1lem1  42928  aks4d1p1  42942  aks4d1p2  42943  aks4d1p3  42944  aks4d1p5  42946  aks4d1p6  42947  aks4d1p7d1  42948  aks4d1p7  42949  aks4d1p8  42953  aks4d1p9  42954  aks6d1c7lem1  43046  aks6d1c7lem2  43047  aks6d1c7  43050  aks5lem6  43058  aks5lem8  43067  jm2.24nn  43800  jm2.23  43837  expdiophlem1  43862  hashnzfz2  45145  bccbc  45169  binomcxplemnn0  45173  ssinc  45919  ssdec  45920  fzdifsuc2  46143  uzfissfz  46156  iuneqfzuzlem  46164  ssuzfz  46179  uzublem  46258  uzinico  46389  fmul01lt1lem1  46414  climsuselem1  46437  climsuse  46438  limsupubuzlem  46540  limsupequzlem  46550  limsupmnfuzlem  46554  limsupre3uzlem  46563  ioodvbdlimc1lem2  46760  ioodvbdlimc2lem  46762  iblspltprt  46801  itgspltprt  46807  stoweidlem11  46839  stirlinglem11  46912  fourierdlem79  47013  fourierdlem103  47037  fourierdlem104  47038  vonioolem1  47508  nnmul2  48218  2ltceilhalf  48220  ceilhalfnn  48228  2timesltsq  48266  2timesltsqm1  48267  fmtnoprmfac1  48468  fmtnoprmfac2lem1  48469  lighneallem2  48509  lighneallem4a  48511  gboge9  48680  bgoldbnnsum3prm  48720  nnolog2flm1  49520