Theorem eluzle 12978

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

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2145   class class class wbr 5103  ‘cfv 6538   ≤ cle 11344  ℤcz 12693  ℤ_≥cuz 12965

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 2733  ax-sep 5249  ax-nul 5260  ax-pr 5391  ax-cnex 11256  ax-resscn 11257

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 2565  df-eu 2595  df-clab 2740  df-cleq 2753  df-clel 2836  df-nfc 2910  df-ne 2957  df-ral 3078  df-rex 3088  df-rab 3414  df-v 3453  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 5546  df-xp 5657  df-rel 5658  df-cnv 5659  df-co 5660  df-dm 5661  df-rn 5662  df-res 5663  df-ima 5664  df-iota 6494  df-fun 6540  df-fn 6541  df-f 6542  df-fv 6546  df-ov 7423  df-neg 11544  df-z 12694  df-uz 12966

This theorem is used by:  uztrn  12983  uzneg  12985  uzss  12988  uz11  12990  eluzp1l  12992  eluzadd  12994  eluzsub  12995  subeluzsub  12998  uzm1  12999  uzin  13001  uzind4  13033  uzwo  13038  uzsupss  13067  ge2halflem1  13237  elfz5  13648  elfzle1  13660  elfzle2  13661  elfzle3  13663  elfz1uz  13728  uzsplit  13730  uzdisj  13731  uznfz  13744  elfz2nn0  13752  uzsubfz0  13770  nn0disj  13778  fzouzdisj  13830  fzoun  13831  fldiv4lem1div2uz2  13976  m1modge3gt1  14061  expmulnbnd  14379  seqcoll  14609  swrdlen2  14810  swrdfv2  14811  rexuzre  15520  rlimclim1  15712  isercoll  15835  iseralt  15852  o1fsum  15980  mertenslem1  16053  fprodeq0  16142  efcllem  16243  rpnnen2lem9  16390  smuval2  16652  smupvallem  16653  isprm7  16884  hashdvds  16952  pcmpt2  17071  pcfaclem  17076  pcfac  17077  vdwlem6  17164  ramtlecl  17178  prmlem1  17285  prmlem2  17298  znfld  21866  lmnn  25584  mbflimsup  25987  mbfi1fseqlem6  26041  dvfsumge  26342  plyco0  26510  coeeulem  26543  radcnvlem2  26741  log2tlbnd  27273  lgamgulmlem4  27359  lgamcvg2  27382  chtub  27539  chpval2  27545  chpchtsum  27546  bcmax  27605  bpos1lem  27609  bpos1  27610  bposlem3  27613  bposlem4  27614  bposlem5  27615  bposlem6  27616  lgslem1  27624  lgsdirprm  27658  lgseisen  27706  dchrisumlema  27815  dchrisumlem2  27817  dchrisum0lem1  27843  axlowdimlem3  29522  axlowdimlem6  29525  axlowdimlem7  29526  axlowdimlem16  29535  axlowdimlem17  29536  dlwwlknondlwlknonf1olem1  30965  minvecolem3  31478  minvecolem4  31482  breprexplemc  35261  subfacval3  35954  climuzcnv  36436  knoppndvlem6  37383  poimirlem29  38567  fdc  38679  aks4d1lem1  43112  aks4d1p1  43126  aks4d1p2  43127  aks4d1p3  43128  aks4d1p5  43130  aks4d1p6  43131  aks4d1p7d1  43132  aks4d1p7  43133  aks4d1p8  43137  aks4d1p9  43138  aks6d1c7lem1  43230  aks6d1c7lem2  43231  aks6d1c7  43234  aks5lem6  43242  aks5lem8  43251  jm2.24nn  43965  jm2.23  44002  expdiophlem1  44027  hashnzfz2  45304  bccbc  45328  binomcxplemnn0  45332  ssinc  46101  ssdec  46102  fzdifsuc2  46325  uzfissfz  46337  iuneqfzuzlem  46345  ssuzfz  46360  uzublem  46439  uzinico  46570  fmul01lt1lem1  46595  climsuselem1  46618  climsuse  46619  limsupubuzlem  46721  limsupequzlem  46731  limsupmnfuzlem  46735  limsupre3uzlem  46744  ioodvbdlimc1lem2  46941  ioodvbdlimc2lem  46943  iblspltprt  46982  itgspltprt  46988  stoweidlem11  47020  stirlinglem11  47093  fourierdlem79  47194  fourierdlem103  47218  fourierdlem104  47219  vonioolem1  47689  nnmul2  48399  2ltceilhalf  48401  ceilhalfnn  48409  2timesltsq  48447  2timesltsqm1  48448  fmtnoprmfac1  48649  fmtnoprmfac2lem1  48650  lighneallem2  48690  lighneallem4a  48692  gboge9  48861  bgoldbnnsum3prm  48901  nnolog2flm1  49701