Theorem eluzle 9944

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

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2209   class class class wbr 4130  ‘cfv 5377   ≤ cle 8362  ℤcz 9649  ℤ_≥cuz 9931

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-io 721  ax-5 1500  ax-7 1501  ax-gen 1502  ax-ie1 1546  ax-ie2 1547  ax-8 1557  ax-10 1558  ax-11 1559  ax-i12 1560  ax-bndl 1562  ax-4 1563  ax-17 1579  ax-i9 1583  ax-ial 1587  ax-i5r 1588  ax-14 2212  ax-ext 2220  ax-sep 4249  ax-pow 4311  ax-pr 4346  ax-cnex 8271  ax-resscn 8272

This proof depends on definitions:  df-bi 117  df-3or 1010  df-3an 1011  df-tru 1405  df-nf 1514  df-sb 1816  df-eu 2089  df-mo 2090  df-clab 2225  df-cleq 2231  df-clel 2234  df-nfc 2381  df-ral 2533  df-rex 2534  df-rab 2537  df-v 2823  df-sbc 3052  df-un 3224  df-in 3226  df-ss 3233  df-pw 3690  df-sn 3715  df-pr 3716  df-op 3718  df-uni 3936  df-br 4131  df-opab 4193  df-mpt 4194  df-id 4438  df-xp 4780  df-rel 4781  df-cnv 4782  df-co 4783  df-dm 4784  df-rn 4785  df-res 4786  df-ima 4787  df-iota 5337  df-fun 5379  df-fn 5380  df-f 5381  df-fv 5385  df-ov 6088  df-neg 8502  df-z 9650  df-uz 9932

This theorem is used by:  uztrn  9949  uzneg  9951  uzss  9953  uz11  9955  eluzp1l  9957  uzm1  9963  uzin  9965  uzind4  9998  elfz5  10431  elfzle1  10442  elfzle2  10443  elfzle3  10445  uzsplit  10510  uzdisj  10511  uznfz  10521  elfz2nn0  10530  uzsubfz0  10547  nn0disj  10556  fzouzdisj  10600  fzoun  10601  elfzonelfzo  10659  infssuzex  10677  suprzubdc  10682  fldiv4lem1div2uz2  10756  mulp1mod1  10817  m1modge3gt1  10823  uzennn  10888  seq3split  10940  seq3f1olemqsumk  10964  seq3f1o  10969  seq3coll  11310  swrdlen2  11450  swrdfv2  11451  seq3shft  11619  cvg1nlemcau  11766  resqrexlemcvg  11801  resqrexlemga  11805  summodclem2a  12167  fsum3  12173  fsum3cvg3  12182  fsumadd  12192  sumsnf  12195  fsummulc2  12234  isumshft  12276  divcnv  12283  geolim2  12298  cvgratnnlemseq  12312  cvgratnnlemsumlt  12314  cvgratz  12318  mertenslemi1  12321  prodmodclem3  12361  prodmodclem2a  12362  fprodntrivap  12370  prodsnf  12378  fprodeq0  12403  efcllemp  12444  dvdsbnd  12752  uzwodc  12833  ncoprmgcdne1b  12886  isprm5  12940  hashdvds  13022  pcmpt2  13146  pcfaclem  13151  pcfac  13152  prmlem1  13245  prmlem2  13257  nninfdclemp1  13393  strext  13512  gzsumfzval  13764  gzsumshift  14233  znidom  15076  log2tlbndlog2  16181  chtqub  16257  bcmax  16266  bpos1lem  16270  bpos1  16271  bposlem3  16274  bposlem4  16275  bposlem5  16276  bposlem6  16277  lgslem1  16285  lgsdirprm  16319  lgseisen  16359  cvgcmp2nlemabs  17247