Theorem eluzle 9094

Description: Implication of membership in an upper set of integers. (Contributed by NM, 6-Sep-2005.)

Assertion

Ref	Expression
eluzle	|- ( N e. ( ZZ>= ` M ) -> M <_ N )

Proof of Theorem eluzle

Step	Hyp	Ref	Expression
1		eluz2 9088	. 2 |- ( N e. ( ZZ>= ` M ) <-> ( M e. ZZ /\ N e. ZZ /\ M <_ N ) )
2	1	simp3bi 961	1 |- ( N e. ( ZZ>= ` M ) -> M <_ N )

Syntax hints:   -> wi 4   e. wcel 1439   class class class wbr 3853   ` cfv 5030   <_ cle 7586   ZZcz 8813   ZZ>=cuz 9082

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-io 666  ax-5 1382  ax-7 1383  ax-gen 1384  ax-ie1 1428  ax-ie2 1429  ax-8 1441  ax-10 1442  ax-11 1443  ax-i12 1444  ax-bndl 1445  ax-4 1446  ax-14 1451  ax-17 1465  ax-i9 1469  ax-ial 1473  ax-i5r 1474  ax-ext 2071  ax-sep 3965  ax-pow 4017  ax-pr 4047  ax-cnex 7499  ax-resscn 7500

This theorem depends on definitions:  df-bi 116  df-3or 926  df-3an 927  df-tru 1293  df-nf 1396  df-sb 1694  df-eu 1952  df-mo 1953  df-clab 2076  df-cleq 2082  df-clel 2085  df-nfc 2218  df-ral 2365  df-rex 2366  df-rab 2369  df-v 2624  df-sbc 2844  df-un 3006  df-in 3008  df-ss 3015  df-pw 3437  df-sn 3458  df-pr 3459  df-op 3461  df-uni 3662  df-br 3854  df-opab 3908  df-mpt 3909  df-id 4131  df-xp 4460  df-rel 4461  df-cnv 4462  df-co 4463  df-dm 4464  df-rn 4465  df-res 4466  df-ima 4467  df-iota 4995  df-fun 5032  df-fn 5033  df-f 5034  df-fv 5038  df-ov 5671  df-neg 7719  df-z 8814  df-uz 9083

This theorem is referenced by:  uztrn  9098  uzneg  9100  uzss  9102  uz11  9104  eluzp1l  9106  uzm1  9112  uzin  9114  uzind4  9139  elfz5  9495  elfzle1  9504  elfzle2  9505  elfzle3  9507  uzsplit  9569  uzdisj  9570  uznfz  9580  elfz2nn0  9589  uzsubfz0  9603  nn0disj  9612  fzouzdisj  9654  elfzonelfzo  9704  mulp1mod1  9835  m1modge3gt1  9841  seq3split  9970  seq3f1olemqsumk  9991  seq3f1o  9996  iseqcoll  10310  seq3shft  10335  cvg1nlemcau  10480  resqrexlemcvg  10515  resqrexlemga  10519  isummolem2a  10834  fisum  10841  fsum3  10842  fsum3cvg3  10852  fsumadd  10863  sumsnf  10866  fsummulc2  10905  isumshft  10947  divcnv  10954  geolim2  10969  cvgratnnlemseq  10983  cvgratnnlemsumlt  10985  cvgratz  10989  mertenslemi1  10992  efcllemp  11011  infssuzex  11286  dvdsbnd  11289  ncoprmgcdne1b  11412  hashdvds  11538