Theorem eluzle 12764

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

Syntax hints:   → wi 4   ∈ wcel 2113   class class class wbr 5098  ‘cfv 6492   ≤ cle 11167  ℤcz 12488  ℤ_≥cuz 12751

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-10 2146  ax-11 2162  ax-12 2184  ax-ext 2708  ax-sep 5241  ax-nul 5251  ax-pr 5377  ax-cnex 11082  ax-resscn 11083

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-nf 1785  df-sb 2068  df-mo 2539  df-eu 2569  df-clab 2715  df-cleq 2728  df-clel 2811  df-nfc 2885  df-ne 2933  df-ral 3052  df-rex 3061  df-rab 3400  df-v 3442  df-dif 3904  df-un 3906  df-in 3908  df-ss 3918  df-nul 4286  df-if 4480  df-pw 4556  df-sn 4581  df-pr 4583  df-op 4587  df-uni 4864  df-br 5099  df-opab 5161  df-mpt 5180  df-id 5519  df-xp 5630  df-rel 5631  df-cnv 5632  df-co 5633  df-dm 5634  df-rn 5635  df-res 5636  df-ima 5637  df-iota 6448  df-fun 6494  df-fn 6495  df-f 6496  df-fv 6500  df-ov 7361  df-neg 11367  df-z 12489  df-uz 12752

This theorem is referenced by:  uztrn  12769  uzneg  12771  uzss  12774  uz11  12776  eluzp1l  12778  eluzadd  12780  eluzsub  12781  subeluzsub  12784  uzm1  12785  uzin  12787  uzind4  12819  uzwo  12824  uzsupss  12853  ge2halflem1  13022  elfz5  13432  elfzle1  13443  elfzle2  13444  elfzle3  13446  elfz1uz  13510  uzsplit  13512  uzdisj  13513  uznfz  13526  elfz2nn0  13534  uzsubfz0  13552  nn0disj  13560  fzouzdisj  13611  fzoun  13612  fldiv4lem1div2uz2  13756  m1modge3gt1  13841  expmulnbnd  14158  seqcoll  14387  swrdlen2  14584  swrdfv2  14585  rexuzre  15276  rlimclim1  15468  isercoll  15591  iseralt  15608  o1fsum  15736  mertenslem1  15807  fprodeq0  15898  efcllem  16000  rpnnen2lem9  16147  smuval2  16409  smupvallem  16410  isprm7  16635  hashdvds  16702  pcmpt2  16821  pcfaclem  16826  pcfac  16827  vdwlem6  16914  ramtlecl  16928  prmlem1  17035  prmlem2  17047  znfld  21515  lmnn  25219  mbflimsup  25623  mbfi1fseqlem6  25677  dvfsumge  25984  plyco0  26153  coeeulem  26185  radcnvlem2  26379  log2tlbnd  26911  lgamgulmlem4  26998  lgamcvg2  27021  chtub  27179  chpval2  27185  chpchtsum  27186  bcmax  27245  bpos1lem  27249  bpos1  27250  bposlem3  27253  bposlem4  27254  bposlem5  27255  bposlem6  27256  lgslem1  27264  lgsdirprm  27298  lgseisen  27346  dchrisumlema  27455  dchrisumlem2  27457  dchrisum0lem1  27483  axlowdimlem3  29017  axlowdimlem6  29020  axlowdimlem7  29021  axlowdimlem16  29030  axlowdimlem17  29031  dlwwlknondlwlknonf1olem1  30439  minvecolem3  30951  minvecolem4  30955  breprexplemc  34789  subfacval3  35383  climuzcnv  35865  knoppndvlem6  36717  poimirlem29  37850  fdc  37946  aks4d1lem1  42316  aks4d1p1  42330  aks4d1p2  42331  aks4d1p3  42332  aks4d1p5  42334  aks4d1p6  42335  aks4d1p7d1  42336  aks4d1p7  42337  aks4d1p8  42341  aks4d1p9  42342  aks6d1c7lem1  42434  aks6d1c7lem2  42435  aks6d1c7  42438  aks5lem6  42446  aks5lem8  42455  jm2.24nn  43201  jm2.23  43238  expdiophlem1  43263  hashnzfz2  44562  bccbc  44586  binomcxplemnn0  44590  ssinc  45331  ssdec  45332  fzdifsuc2  45558  uzfissfz  45571  iuneqfzuzlem  45579  ssuzfz  45594  uzublem  45674  uzinico  45805  fmul01lt1lem1  45830  climsuselem1  45853  climsuse  45854  limsupubuzlem  45956  limsupequzlem  45966  limsupmnfuzlem  45970  limsupre3uzlem  45979  ioodvbdlimc1lem2  46176  ioodvbdlimc2lem  46178  iblspltprt  46217  itgspltprt  46223  stoweidlem11  46255  stirlinglem11  46328  fourierdlem79  46429  fourierdlem103  46453  fourierdlem104  46454  vonioolem1  46924  2ltceilhalf  47574  ceilhalfnn  47582  fmtnoprmfac1  47811  fmtnoprmfac2lem1  47812  lighneallem2  47852  lighneallem4a  47854  gboge9  48010  bgoldbnnsum3prm  48050  nnolog2flm1  48836