Theorem eluzle 12874

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

Syntax hints:   → wi 4   ∈ wcel 2149   class class class wbr 5113  ‘cfv 6537   ≤ cle 11243  ℤcz 12590  ℤ_≥cuz 12861

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-8 2151  ax-9 2159  ax-10 2182  ax-11 2198  ax-12 2219  ax-ext 2741  ax-sep 5261  ax-nul 5271  ax-pr 5405  ax-cnex 11155  ax-resscn 11156

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3or 1102  df-3an 1103  df-tru 1570  df-fal 1580  df-ex 1807  df-nf 1811  df-sb 2098  df-mo 2573  df-eu 2603  df-clab 2748  df-cleq 2761  df-clel 2844  df-nfc 2918  df-ne 2965  df-ral 3086  df-rex 3096  df-rab 3424  df-v 3465  df-dif 3916  df-un 3918  df-in 3920  df-ss 3930  df-nul 4295  df-if 4493  df-pw 4569  df-sn 4595  df-pr 4597  df-op 4601  df-uni 4877  df-br 5114  df-opab 5178  df-mpt 5197  df-id 5557  df-xp 5668  df-rel 5669  df-cnv 5670  df-co 5671  df-dm 5672  df-rn 5673  df-res 5674  df-ima 5675  df-iota 6493  df-fun 6539  df-fn 6540  df-f 6541  df-fv 6545  df-ov 7414  df-neg 11443  df-z 12591  df-uz 12862

This theorem is referenced by:  uztrn  12879  uzneg  12881  uzss  12884  uz11  12886  eluzp1l  12888  eluzadd  12890  eluzsub  12891  subeluzsub  12894  uzm1  12895  uzin  12897  uzind4  12929  uzwo  12934  uzsupss  12963  ge2halflem1  13132  elfz5  13543  elfzle1  13554  elfzle2  13555  elfzle3  13557  elfz1uz  13621  uzsplit  13623  uzdisj  13624  uznfz  13637  elfz2nn0  13645  uzsubfz0  13663  nn0disj  13671  fzouzdisj  13723  fzoun  13724  fldiv4lem1div2uz2  13868  m1modge3gt1  13953  expmulnbnd  14270  seqcoll  14500  swrdlen2  14697  swrdfv2  14698  rexuzre  15403  rlimclim1  15595  isercoll  15718  iseralt  15735  o1fsum  15864  mertenslem1  15937  fprodeq0  16028  efcllem  16130  rpnnen2lem9  16277  smuval2  16539  smupvallem  16540  isprm7  16766  hashdvds  16833  pcmpt2  16952  pcfaclem  16957  pcfac  16958  vdwlem6  17045  ramtlecl  17059  prmlem1  17166  prmlem2  17179  znfld  21678  lmnn  25390  mbflimsup  25793  mbfi1fseqlem6  25847  dvfsumge  26149  plyco0  26317  coeeulem  26349  radcnvlem2  26542  log2tlbnd  27075  lgamgulmlem4  27161  lgamcvg2  27184  chtub  27341  chpval2  27347  chpchtsum  27348  bcmax  27407  bpos1lem  27411  bpos1  27412  bposlem3  27415  bposlem4  27416  bposlem5  27417  bposlem6  27418  lgslem1  27426  lgsdirprm  27460  lgseisen  27508  dchrisumlema  27617  dchrisumlem2  27619  dchrisum0lem1  27645  axlowdimlem3  29234  axlowdimlem6  29237  axlowdimlem7  29238  axlowdimlem16  29247  axlowdimlem17  29248  dlwwlknondlwlknonf1olem1  30655  minvecolem3  31168  minvecolem4  31172  breprexplemc  34963  subfacval3  35579  climuzcnv  36061  knoppndvlem6  36994  poimirlem29  38187  fdc  38283  aks4d1lem1  42718  aks4d1p1  42732  aks4d1p2  42733  aks4d1p3  42734  aks4d1p5  42736  aks4d1p6  42737  aks4d1p7d1  42738  aks4d1p7  42739  aks4d1p8  42743  aks4d1p9  42744  aks6d1c7lem1  42836  aks6d1c7lem2  42837  aks6d1c7  42840  aks5lem6  42848  aks5lem8  42857  jm2.24nn  43577  jm2.23  43614  expdiophlem1  43639  hashnzfz2  44922  bccbc  44946  binomcxplemnn0  44950  ssinc  45696  ssdec  45697  fzdifsuc2  45920  uzfissfz  45933  iuneqfzuzlem  45941  ssuzfz  45956  uzublem  46035  uzinico  46166  fmul01lt1lem1  46191  climsuselem1  46214  climsuse  46215  limsupubuzlem  46317  limsupequzlem  46327  limsupmnfuzlem  46331  limsupre3uzlem  46340  ioodvbdlimc1lem2  46537  ioodvbdlimc2lem  46539  iblspltprt  46578  itgspltprt  46584  stoweidlem11  46616  stirlinglem11  46689  fourierdlem79  46790  fourierdlem103  46814  fourierdlem104  46815  vonioolem1  47285  nnmul2  47955  2ltceilhalf  47957  ceilhalfnn  47965  2timesltsq  48003  2timesltsqm1  48004  fmtnoprmfac1  48205  fmtnoprmfac2lem1  48206  lighneallem2  48246  lighneallem4a  48248  gboge9  48417  bgoldbnnsum3prm  48457  nnolog2flm1  49254