Theorem eluzle 12858

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

Syntax hints:   → wi 4   ∈ wcel 2107   class class class wbr 5117  ‘cfv 6528   ≤ cle 11263  ℤcz 12581  ℤ_≥cuz 12845

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1794  ax-4 1808  ax-5 1909  ax-6 1966  ax-7 2006  ax-8 2109  ax-9 2117  ax-10 2140  ax-11 2156  ax-12 2176  ax-ext 2706  ax-sep 5264  ax-nul 5274  ax-pr 5400  ax-cnex 11178  ax-resscn 11179

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1542  df-fal 1552  df-ex 1779  df-nf 1783  df-sb 2064  df-mo 2538  df-eu 2567  df-clab 2713  df-cleq 2726  df-clel 2808  df-nfc 2884  df-ral 3051  df-rex 3060  df-rab 3414  df-v 3459  df-dif 3927  df-un 3929  df-in 3931  df-ss 3941  df-nul 4307  df-if 4499  df-pw 4575  df-sn 4600  df-pr 4602  df-op 4606  df-uni 4882  df-br 5118  df-opab 5180  df-mpt 5200  df-id 5546  df-xp 5658  df-rel 5659  df-cnv 5660  df-co 5661  df-dm 5662  df-rn 5663  df-res 5664  df-ima 5665  df-iota 6481  df-fun 6530  df-fn 6531  df-f 6532  df-fv 6536  df-ov 7403  df-neg 11462  df-z 12582  df-uz 12846

This theorem is referenced by:  uztrn  12863  uzneg  12865  uzss  12868  uz11  12870  eluzp1l  12872  eluzadd  12874  eluzsub  12875  subeluzsub  12882  uzm1  12883  uzin  12885  uzind4  12915  uzwo  12920  uzsupss  12949  ge2halflem1  13117  elfz5  13523  elfzle1  13534  elfzle2  13535  elfzle3  13537  elfz1uz  13601  uzsplit  13603  uzdisj  13604  uznfz  13617  elfz2nn0  13625  uzsubfz0  13643  nn0disj  13651  fzouzdisj  13702  fzoun  13703  fldiv4lem1div2uz2  13843  m1modge3gt1  13926  expmulnbnd  14243  seqcoll  14472  swrdlen2  14667  swrdfv2  14668  rexuzre  15360  rlimclim1  15550  isercoll  15673  iseralt  15690  o1fsum  15818  mertenslem1  15889  fprodeq0  15980  efcllem  16082  rpnnen2lem9  16227  smuval2  16488  smupvallem  16489  isprm7  16714  hashdvds  16781  pcmpt2  16900  pcfaclem  16905  pcfac  16906  vdwlem6  16993  ramtlecl  17007  prmlem1  17114  prmlem2  17126  znfld  21508  lmnn  25202  mbflimsup  25606  mbfi1fseqlem6  25660  dvfsumge  25967  plyco0  26136  coeeulem  26168  radcnvlem2  26362  log2tlbnd  26893  lgamgulmlem4  26980  lgamcvg2  27003  chtub  27161  chpval2  27167  chpchtsum  27168  bcmax  27227  bpos1lem  27231  bpos1  27232  bposlem3  27235  bposlem4  27236  bposlem5  27237  bposlem6  27238  lgslem1  27246  lgsdirprm  27280  lgseisen  27328  dchrisumlema  27437  dchrisumlem2  27439  dchrisum0lem1  27465  axlowdimlem3  28857  axlowdimlem6  28860  axlowdimlem7  28861  axlowdimlem16  28870  axlowdimlem17  28871  dlwwlknondlwlknonf1olem1  30279  minvecolem3  30791  minvecolem4  30795  breprexplemc  34593  subfacval3  35140  climuzcnv  35622  knoppndvlem6  36464  poimirlem29  37602  fdc  37698  aks4d1lem1  42004  aks4d1p1  42018  aks4d1p2  42019  aks4d1p3  42020  aks4d1p5  42022  aks4d1p6  42023  aks4d1p7d1  42024  aks4d1p7  42025  aks4d1p8  42029  aks4d1p9  42030  aks6d1c7lem1  42122  aks6d1c7lem2  42123  aks6d1c7  42126  aks5lem6  42134  aks5lem8  42143  jm2.24nn  42915  jm2.23  42952  expdiophlem1  42977  hashnzfz2  44278  bccbc  44302  binomcxplemnn0  44306  ssinc  45045  ssdec  45046  fzdifsuc2  45273  uzfissfz  45287  iuneqfzuzlem  45295  ssuzfz  45310  uzublem  45391  uzinico  45523  fmul01lt1lem1  45549  climsuselem1  45572  climsuse  45573  limsupubuzlem  45677  limsupequzlem  45687  limsupmnfuzlem  45691  limsupre3uzlem  45700  ioodvbdlimc1lem2  45897  ioodvbdlimc2lem  45899  iblspltprt  45938  itgspltprt  45944  stoweidlem11  45976  stirlinglem11  46049  fourierdlem79  46150  fourierdlem103  46174  fourierdlem104  46175  vonioolem1  46645  fmtnoprmfac1  47505  fmtnoprmfac2lem1  47506  lighneallem2  47546  lighneallem4a  47548  gboge9  47704  bgoldbnnsum3prm  47744  2ltceilhalf  47968  nnolog2flm1  48464