Theorem eluzle 12792

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

Syntax hints:   → wi 4   ∈ wcel 2119   class class class wbr 5072  ‘cfv 6485   ≤ cle 11171  ℤcz 12515  ℤ_≥cuz 12779

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-10 2152  ax-11 2168  ax-12 2189  ax-ext 2711  ax-sep 5218  ax-nul 5228  ax-pr 5362  ax-cnex 11085  ax-resscn 11086

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 854  df-3or 1093  df-3an 1094  df-tru 1550  df-fal 1560  df-ex 1787  df-nf 1791  df-sb 2074  df-mo 2543  df-eu 2573  df-clab 2718  df-cleq 2731  df-clel 2814  df-nfc 2888  df-ne 2935  df-ral 3054  df-rex 3064  df-rab 3392  df-v 3433  df-dif 3886  df-un 3888  df-in 3890  df-ss 3900  df-nul 4262  df-if 4455  df-pw 4531  df-sn 4556  df-pr 4558  df-op 4562  df-uni 4839  df-br 5073  df-opab 5135  df-mpt 5154  df-id 5513  df-xp 5624  df-rel 5625  df-cnv 5626  df-co 5627  df-dm 5628  df-rn 5629  df-res 5630  df-ima 5631  df-iota 6441  df-fun 6487  df-fn 6488  df-f 6489  df-fv 6493  df-ov 7359  df-neg 11371  df-z 12516  df-uz 12780

This theorem is referenced by:  uztrn  12797  uzneg  12799  uzss  12802  uz11  12804  eluzp1l  12806  eluzadd  12808  eluzsub  12809  subeluzsub  12812  uzm1  12813  uzin  12815  uzind4  12847  uzwo  12852  uzsupss  12881  ge2halflem1  13050  elfz5  13461  elfzle1  13472  elfzle2  13473  elfzle3  13475  elfz1uz  13539  uzsplit  13541  uzdisj  13542  uznfz  13555  elfz2nn0  13563  uzsubfz0  13581  nn0disj  13589  fzouzdisj  13641  fzoun  13642  fldiv4lem1div2uz2  13786  m1modge3gt1  13871  expmulnbnd  14188  seqcoll  14417  swrdlen2  14614  swrdfv2  14615  rexuzre  15306  rlimclim1  15498  isercoll  15621  iseralt  15638  o1fsum  15767  mertenslem1  15840  fprodeq0  15931  efcllem  16033  rpnnen2lem9  16180  smuval2  16442  smupvallem  16443  isprm7  16669  hashdvds  16736  pcmpt2  16855  pcfaclem  16860  pcfac  16861  vdwlem6  16948  ramtlecl  16962  prmlem1  17069  prmlem2  17081  znfld  21535  lmnn  25248  mbflimsup  25651  mbfi1fseqlem6  25705  dvfsumge  26007  plyco0  26175  coeeulem  26207  radcnvlem2  26397  log2tlbnd  26927  lgamgulmlem4  27013  lgamcvg2  27036  chtub  27193  chpval2  27199  chpchtsum  27200  bcmax  27259  bpos1lem  27263  bpos1  27264  bposlem3  27267  bposlem4  27268  bposlem5  27269  bposlem6  27270  lgslem1  27278  lgsdirprm  27312  lgseisen  27360  dchrisumlema  27469  dchrisumlem2  27471  dchrisum0lem1  27497  axlowdimlem3  29031  axlowdimlem6  29034  axlowdimlem7  29035  axlowdimlem16  29044  axlowdimlem17  29045  dlwwlknondlwlknonf1olem1  30452  minvecolem3  30965  minvecolem4  30969  breprexplemc  34816  subfacval3  35417  climuzcnv  35899  knoppndvlem6  36823  poimirlem29  38016  fdc  38112  aks4d1lem1  42547  aks4d1p1  42561  aks4d1p2  42562  aks4d1p3  42563  aks4d1p5  42565  aks4d1p6  42566  aks4d1p7d1  42567  aks4d1p7  42568  aks4d1p8  42572  aks4d1p9  42573  aks6d1c7lem1  42665  aks6d1c7lem2  42666  aks6d1c7  42669  aks5lem6  42677  aks5lem8  42686  jm2.24nn  43404  jm2.23  43441  expdiophlem1  43466  hashnzfz2  44765  bccbc  44789  binomcxplemnn0  44793  ssinc  45534  ssdec  45535  fzdifsuc2  45758  uzfissfz  45771  iuneqfzuzlem  45779  ssuzfz  45794  uzublem  45873  uzinico  46004  fmul01lt1lem1  46029  climsuselem1  46052  climsuse  46053  limsupubuzlem  46155  limsupequzlem  46165  limsupmnfuzlem  46169  limsupre3uzlem  46178  ioodvbdlimc1lem2  46375  ioodvbdlimc2lem  46377  iblspltprt  46416  itgspltprt  46422  stoweidlem11  46454  stirlinglem11  46527  fourierdlem79  46628  fourierdlem103  46652  fourierdlem104  46653  vonioolem1  47123  nnmul2  47793  2ltceilhalf  47795  ceilhalfnn  47803  2timesltsq  47841  2timesltsqm1  47842  fmtnoprmfac1  48043  fmtnoprmfac2lem1  48044  lighneallem2  48084  lighneallem4a  48086  gboge9  48255  bgoldbnnsum3prm  48295  nnolog2flm1  49081