Theorem eluzle 13018

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

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2147   class class class wbr 5108  ‘cfv 6566   ≤ cle 11383  ℤcz 12733  ℤ_≥cuz 13005

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 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-10 2180  ax-11 2197  ax-12 2216  ax-ext 2735  ax-sep 5255  ax-nul 5266  ax-pr 5398  ax-cnex 11295  ax-resscn 11296

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 2102  df-mo 2567  df-eu 2597  df-clab 2742  df-cleq 2755  df-clel 2839  df-nfc 2913  df-ne 2960  df-ral 3081  df-rex 3091  df-rab 3417  df-v 3456  df-ss 3901  df-dif 4050  df-in 4094  df-un 4154  df-nul 4282  df-if 4486  df-pw 4562  df-sn 4589  df-pr 4591  df-op 4841  df-uni 4873  df-br 5109  df-opab 5174  df-mpt 5193  df-id 5553  df-xp 5664  df-rel 5665  df-cnv 5666  df-co 5667  df-dm 5668  df-rn 5669  df-res 5670  df-ima 5671  df-iota 6520  df-fun 6568  df-fn 6569  df-f 6570  df-fv 6574  df-ov 7454  df-neg 11583  df-z 12734  df-uz 13006

This theorem is used by:  uztrn  13023  uzneg  13025  uzss  13028  uz11  13030  eluzp1l  13032  eluzadd  13034  eluzsub  13035  subeluzsub  13038  uzm1  13039  uzin  13041  uzind4  13073  uzwo  13078  uzsupss  13107  ge2halflem1  13277  elfz5  13688  elfzle1  13700  elfzle2  13701  elfzle3  13703  elfz1uz  13768  uzsplit  13770  uzdisj  13771  uznfz  13784  elfz2nn0  13792  uzsubfz0  13810  nn0disj  13818  fzouzdisj  13870  fzoun  13871  m1modge3gt1  14101  expmulnbnd  14420  seqcoll  14650  swrdlen2  14852  swrdfv2  14853  rexuzre  15564  rlimclim1  15756  isercoll  15879  iseralt  15896  o1fsum  16024  mertenslem1  16097  fprodeq0  16186  efcllem  16287  rpnnen2lem9  16434  smuval2  16696  smupvallem  16697  isprm7  16928  hashdvds  16996  pcmpt2  17115  pcfaclem  17120  pcfac  17121  vdwlem6  17208  ramtlecl  17222  prmlem1  17329  prmlem2  17342  znfld  21921  lmnn  25639  mbflimsup  26042  mbfi1fseqlem6  26096  dvfsumge  26397  plyco0  26565  coeeulem  26598  radcnvlem2  26798  log2tlbnd  27330  lgamgulmlem4  27416  lgamcvg2  27439  chtub  27596  chpval2  27602  chpchtsum  27603  bcmax  27662  bpos1lem  27666  bpos1  27667  bposlem3  27670  bposlem4  27671  bposlem5  27672  bposlem6  27673  lgslem1  27681  lgsdirprm  27715  lgseisen  27763  dchrisumlema  27872  dchrisumlem2  27874  dchrisum0lem1  27900  axlowdimlem3  29579  axlowdimlem6  29582  axlowdimlem7  29583  axlowdimlem16  29592  axlowdimlem17  29593  dlwwlknondlwlknonf1olem1  31022  minvecolem3  31535  minvecolem4  31539  breprexplemc  35372  subfacval3  36162  climuzcnv  36644  knoppndvlem6  37598  poimirlem29  38835  fdc  38945  aks4d1lem1  43378  aks4d1p1  43392  aks4d1p2  43393  aks4d1p3  43394  aks4d1p5  43396  aks4d1p6  43397  aks4d1p7d1  43398  aks4d1p7  43399  aks4d1p8  43403  aks4d1p9  43404  aks6d1c7lem1  43496  aks6d1c7lem2  43497  aks6d1c7  43500  aks5lem6  43508  aks5lem8  43517  jm2.24nn  44232  jm2.23  44269  expdiophlem1  44294  hashnzfz2  45566  bccbc  45590  binomcxplemnn0  45594  ssinc  46375  ssdec  46376  fzdifsuc2  46599  uzfissfz  46611  iuneqfzuzlem  46619  ssuzfz  46634  uzublem  46713  uzinico  46844  fmul01lt1lem1  46869  climsuselem1  46892  climsuse  46893  limsupubuzlem  46995  limsupequzlem  47005  limsupmnfuzlem  47009  limsupre3uzlem  47018  ioodvbdlimc1lem2  47215  ioodvbdlimc2lem  47217  iblspltprt  47256  itgspltprt  47262  stoweidlem11  47294  stirlinglem11  47367  fourierdlem79  47468  fourierdlem103  47492  fourierdlem104  47493  vonioolem1  47963  nnmul2  48673  2ltceilhalf  48675  ceilhalfnn  48683  2timesltsq  48721  2timesltsqm1  48722  fmtnoprmfac1  48923  fmtnoprmfac2lem1  48924  lighneallem2  48964  lighneallem4a  48966  gboge9  49135  bgoldbnnsum3prm  49175  nnolog2flm1  50033