Theorem eluzle 12891

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

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2146   class class class wbr 5111  ‘cfv 6540   ≤ cle 11259  ℤcz 12606  ℤ_≥cuz 12878

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 2148  ax-9 2156  ax-10 2179  ax-11 2195  ax-12 2216  ax-ext 2737  ax-sep 5259  ax-nul 5271  ax-pr 5406  ax-cnex 11171  ax-resscn 11172

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 2569  df-eu 2599  df-clab 2744  df-cleq 2757  df-clel 2840  df-nfc 2914  df-ne 2961  df-ral 3082  df-rex 3092  df-rab 3419  df-v 3459  df-dif 3909  df-un 3911  df-in 3913  df-ss 3923  df-nul 4287  df-if 4490  df-pw 4566  df-sn 4592  df-pr 4594  df-op 4598  df-uni 4875  df-br 5112  df-opab 5176  df-mpt 5195  df-id 5558  df-xp 5669  df-rel 5670  df-cnv 5671  df-co 5672  df-dm 5673  df-rn 5674  df-res 5675  df-ima 5676  df-iota 6496  df-fun 6542  df-fn 6543  df-f 6544  df-fv 6548  df-ov 7422  df-neg 11459  df-z 12607  df-uz 12879

This theorem is used by:  uztrn  12896  uzneg  12898  uzss  12901  uz11  12903  eluzp1l  12905  eluzadd  12907  eluzsub  12908  subeluzsub  12911  uzm1  12912  uzin  12914  uzind4  12946  uzwo  12951  uzsupss  12980  ge2halflem1  13149  elfz5  13560  elfzle1  13571  elfzle2  13572  elfzle3  13574  elfz1uz  13639  uzsplit  13641  uzdisj  13642  uznfz  13655  elfz2nn0  13663  uzsubfz0  13681  nn0disj  13689  fzouzdisj  13741  fzoun  13742  fldiv4lem1div2uz2  13887  m1modge3gt1  13972  expmulnbnd  14289  seqcoll  14519  swrdlen2  14720  swrdfv2  14721  rexuzre  15428  rlimclim1  15620  isercoll  15743  iseralt  15760  o1fsum  15888  mertenslem1  15961  fprodeq0  16052  efcllem  16153  rpnnen2lem9  16300  smuval2  16562  smupvallem  16563  isprm7  16789  hashdvds  16856  pcmpt2  16975  pcfaclem  16980  pcfac  16981  vdwlem6  17068  ramtlecl  17082  prmlem1  17189  prmlem2  17202  znfld  21760  lmnn  25473  mbflimsup  25876  mbfi1fseqlem6  25930  dvfsumge  26232  plyco0  26400  coeeulem  26432  radcnvlem2  26628  log2tlbnd  27161  lgamgulmlem4  27247  lgamcvg2  27270  chtub  27427  chpval2  27433  chpchtsum  27434  bcmax  27493  bpos1lem  27497  bpos1  27498  bposlem3  27501  bposlem4  27502  bposlem5  27503  bposlem6  27504  lgslem1  27512  lgsdirprm  27546  lgseisen  27594  dchrisumlema  27703  dchrisumlem2  27705  dchrisum0lem1  27731  axlowdimlem3  29349  axlowdimlem6  29352  axlowdimlem7  29353  axlowdimlem16  29362  axlowdimlem17  29363  dlwwlknondlwlknonf1olem1  30786  minvecolem3  31299  minvecolem4  31303  breprexplemc  35084  subfacval3  35718  climuzcnv  36200  knoppndvlem6  37163  poimirlem29  38357  fdc  38454  aks4d1lem1  42887  aks4d1p1  42901  aks4d1p2  42902  aks4d1p3  42903  aks4d1p5  42905  aks4d1p6  42906  aks4d1p7d1  42907  aks4d1p7  42908  aks4d1p8  42912  aks4d1p9  42913  aks6d1c7lem1  43005  aks6d1c7lem2  43006  aks6d1c7  43009  aks5lem6  43017  aks5lem8  43026  jm2.24nn  43744  jm2.23  43781  expdiophlem1  43806  hashnzfz2  45089  bccbc  45113  binomcxplemnn0  45117  ssinc  45863  ssdec  45864  fzdifsuc2  46087  uzfissfz  46100  iuneqfzuzlem  46108  ssuzfz  46123  uzublem  46202  uzinico  46333  fmul01lt1lem1  46358  climsuselem1  46381  climsuse  46382  limsupubuzlem  46484  limsupequzlem  46494  limsupmnfuzlem  46498  limsupre3uzlem  46507  ioodvbdlimc1lem2  46704  ioodvbdlimc2lem  46706  iblspltprt  46745  itgspltprt  46751  stoweidlem11  46783  stirlinglem11  46856  fourierdlem79  46957  fourierdlem103  46981  fourierdlem104  46982  vonioolem1  47452  nnmul2  48125  2ltceilhalf  48127  ceilhalfnn  48135  2timesltsq  48173  2timesltsqm1  48174  fmtnoprmfac1  48375  fmtnoprmfac2lem1  48376  lighneallem2  48416  lighneallem4a  48418  gboge9  48587  bgoldbnnsum3prm  48627  nnolog2flm1  49427