Theorem eluzle 9659

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

Syntax hints:   → wi 4   ∈ wcel 2175   class class class wbr 4043  ‘cfv 5270   ≤ cle 8107  ℤcz 9371  ℤ_≥cuz 9647

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-io 710  ax-5 1469  ax-7 1470  ax-gen 1471  ax-ie1 1515  ax-ie2 1516  ax-8 1526  ax-10 1527  ax-11 1528  ax-i12 1529  ax-bndl 1531  ax-4 1532  ax-17 1548  ax-i9 1552  ax-ial 1556  ax-i5r 1557  ax-14 2178  ax-ext 2186  ax-sep 4161  ax-pow 4217  ax-pr 4252  ax-cnex 8015  ax-resscn 8016

This theorem depends on definitions:  df-bi 117  df-3or 981  df-3an 982  df-tru 1375  df-nf 1483  df-sb 1785  df-eu 2056  df-mo 2057  df-clab 2191  df-cleq 2197  df-clel 2200  df-nfc 2336  df-ral 2488  df-rex 2489  df-rab 2492  df-v 2773  df-sbc 2998  df-un 3169  df-in 3171  df-ss 3178  df-pw 3617  df-sn 3638  df-pr 3639  df-op 3641  df-uni 3850  df-br 4044  df-opab 4105  df-mpt 4106  df-id 4339  df-xp 4680  df-rel 4681  df-cnv 4682  df-co 4683  df-dm 4684  df-rn 4685  df-res 4686  df-ima 4687  df-iota 5231  df-fun 5272  df-fn 5273  df-f 5274  df-fv 5278  df-ov 5946  df-neg 8245  df-z 9372  df-uz 9648

This theorem is referenced by:  uztrn  9664  uzneg  9666  uzss  9668  uz11  9670  eluzp1l  9672  uzm1  9678  uzin  9680  uzind4  9708  elfz5  10138  elfzle1  10148  elfzle2  10149  elfzle3  10151  uzsplit  10213  uzdisj  10214  uznfz  10224  elfz2nn0  10233  uzsubfz0  10250  nn0disj  10259  fzouzdisj  10302  elfzonelfzo  10357  infssuzex  10374  suprzubdc  10377  fldiv4lem1div2uz2  10447  mulp1mod1  10508  m1modge3gt1  10514  uzennn  10579  seq3split  10631  seq3f1olemqsumk  10655  seq3f1o  10660  seq3coll  10985  seq3shft  11120  cvg1nlemcau  11266  resqrexlemcvg  11301  resqrexlemga  11305  summodclem2a  11663  fsum3  11669  fsum3cvg3  11678  fsumadd  11688  sumsnf  11691  fsummulc2  11730  isumshft  11772  divcnv  11779  geolim2  11794  cvgratnnlemseq  11808  cvgratnnlemsumlt  11810  cvgratz  11814  mertenslemi1  11817  prodmodclem3  11857  prodmodclem2a  11858  fprodntrivap  11866  prodsnf  11874  fprodeq0  11899  efcllemp  11940  dvdsbnd  12248  uzwodc  12329  ncoprmgcdne1b  12382  isprm5  12435  hashdvds  12514  pcmpt2  12638  pcfaclem  12643  pcfac  12644  nninfdclemp1  12792  strext  12908  gsumfzval  13194  znidom  14390  lgslem1  15448  lgsdirprm  15482  lgseisen  15522  cvgcmp2nlemabs  15933