Theorem eluzle 12985

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

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2144   class class class wbr 5102  ‘cfv 6543   ≤ cle 11351  ℤcz 12700  ℤ_≥cuz 12972

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-10 2177  ax-11 2193  ax-12 2212  ax-ext 2732  ax-sep 5248  ax-nul 5259  ax-pr 5391  ax-cnex 11263  ax-resscn 11264

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3or 1104  df-3an 1105  df-tru 1572  df-fal 1582  df-ex 1812  df-nf 1816  df-sb 2099  df-mo 2564  df-eu 2594  df-clab 2739  df-cleq 2752  df-clel 2835  df-nfc 2909  df-ne 2956  df-ral 3077  df-rex 3087  df-rab 3413  df-v 3452  df-ss 3897  df-dif 4046  df-in 4090  df-un 4150  df-nul 4278  df-if 4482  df-pw 4558  df-sn 4585  df-pr 4587  df-op 4835  df-uni 4867  df-br 5103  df-opab 5167  df-mpt 5186  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 6497  df-fun 6545  df-fn 6546  df-f 6547  df-fv 6551  df-ov 7427  df-neg 11551  df-z 12701  df-uz 12973

This theorem is used by:  uztrn  12990  uzneg  12992  uzss  12995  uz11  12997  eluzp1l  12999  eluzadd  13001  eluzsub  13002  subeluzsub  13005  uzm1  13006  uzin  13008  uzind4  13040  uzwo  13045  uzsupss  13074  ge2halflem1  13244  elfz5  13655  elfzle1  13667  elfzle2  13668  elfzle3  13670  elfz1uz  13735  uzsplit  13737  uzdisj  13738  uznfz  13751  elfz2nn0  13759  uzsubfz0  13777  nn0disj  13785  fzouzdisj  13837  fzoun  13838  m1modge3gt1  14068  expmulnbnd  14386  seqcoll  14616  swrdlen2  14818  swrdfv2  14819  rexuzre  15529  rlimclim1  15721  isercoll  15844  iseralt  15861  o1fsum  15989  mertenslem1  16062  fprodeq0  16151  efcllem  16252  rpnnen2lem9  16399  smuval2  16661  smupvallem  16662  isprm7  16893  hashdvds  16961  pcmpt2  17080  pcfaclem  17085  pcfac  17086  vdwlem6  17173  ramtlecl  17187  prmlem1  17294  prmlem2  17307  znfld  21875  lmnn  25593  mbflimsup  25996  mbfi1fseqlem6  26050  dvfsumge  26351  plyco0  26519  coeeulem  26552  radcnvlem2  26750  log2tlbnd  27282  lgamgulmlem4  27368  lgamcvg2  27391  chtub  27548  chpval2  27554  chpchtsum  27555  bcmax  27614  bpos1lem  27618  bpos1  27619  bposlem3  27622  bposlem4  27623  bposlem5  27624  bposlem6  27625  lgslem1  27633  lgsdirprm  27667  lgseisen  27715  dchrisumlema  27824  dchrisumlem2  27826  dchrisum0lem1  27852  axlowdimlem3  29531  axlowdimlem6  29534  axlowdimlem7  29535  axlowdimlem16  29544  axlowdimlem17  29545  dlwwlknondlwlknonf1olem1  30974  minvecolem3  31487  minvecolem4  31491  breprexplemc  35311  subfacval3  36072  climuzcnv  36554  knoppndvlem6  37507  poimirlem29  38704  fdc  38816  aks4d1lem1  43249  aks4d1p1  43263  aks4d1p2  43264  aks4d1p3  43265  aks4d1p5  43267  aks4d1p6  43268  aks4d1p7d1  43269  aks4d1p7  43270  aks4d1p8  43274  aks4d1p9  43275  aks6d1c7lem1  43367  aks6d1c7lem2  43368  aks6d1c7  43371  aks5lem6  43379  aks5lem8  43388  jm2.24nn  44103  jm2.23  44140  expdiophlem1  44165  hashnzfz2  45442  bccbc  45466  binomcxplemnn0  45470  ssinc  46238  ssdec  46239  fzdifsuc2  46462  uzfissfz  46474  iuneqfzuzlem  46482  ssuzfz  46497  uzublem  46576  uzinico  46707  fmul01lt1lem1  46732  climsuselem1  46755  climsuse  46756  limsupubuzlem  46858  limsupequzlem  46868  limsupmnfuzlem  46872  limsupre3uzlem  46881  ioodvbdlimc1lem2  47078  ioodvbdlimc2lem  47080  iblspltprt  47119  itgspltprt  47125  stoweidlem11  47157  stirlinglem11  47230  fourierdlem79  47331  fourierdlem103  47355  fourierdlem104  47356  vonioolem1  47826  nnmul2  48536  2ltceilhalf  48538  ceilhalfnn  48546  2timesltsq  48584  2timesltsqm1  48585  fmtnoprmfac1  48786  fmtnoprmfac2lem1  48787  lighneallem2  48827  lighneallem4a  48829  gboge9  48998  bgoldbnnsum3prm  49038  nnolog2flm1  49838