Theorem eluzle 9570

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 9564	. 2 |- ( N e. ( ZZ>= ` M ) <-> ( M e. ZZ /\ N e. ZZ /\ M <_ N ) )
2	1	simp3bi 1016	1 |- ( N e. ( ZZ>= ` M ) -> M <_ N )

Syntax hints:   -> wi 4   e. wcel 2160   class class class wbr 4018   ` cfv 5235   <_ cle 8023   ZZcz 9283   ZZ>=cuz 9558

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 1458  ax-7 1459  ax-gen 1460  ax-ie1 1504  ax-ie2 1505  ax-8 1515  ax-10 1516  ax-11 1517  ax-i12 1518  ax-bndl 1520  ax-4 1521  ax-17 1537  ax-i9 1541  ax-ial 1545  ax-i5r 1546  ax-14 2163  ax-ext 2171  ax-sep 4136  ax-pow 4192  ax-pr 4227  ax-cnex 7932  ax-resscn 7933

This theorem depends on definitions:  df-bi 117  df-3or 981  df-3an 982  df-tru 1367  df-nf 1472  df-sb 1774  df-eu 2041  df-mo 2042  df-clab 2176  df-cleq 2182  df-clel 2185  df-nfc 2321  df-ral 2473  df-rex 2474  df-rab 2477  df-v 2754  df-sbc 2978  df-un 3148  df-in 3150  df-ss 3157  df-pw 3592  df-sn 3613  df-pr 3614  df-op 3616  df-uni 3825  df-br 4019  df-opab 4080  df-mpt 4081  df-id 4311  df-xp 4650  df-rel 4651  df-cnv 4652  df-co 4653  df-dm 4654  df-rn 4655  df-res 4656  df-ima 4657  df-iota 5196  df-fun 5237  df-fn 5238  df-f 5239  df-fv 5243  df-ov 5899  df-neg 8161  df-z 9284  df-uz 9559

This theorem is referenced by:  uztrn  9574  uzneg  9576  uzss  9578  uz11  9580  eluzp1l  9582  uzm1  9588  uzin  9590  uzind4  9618  elfz5  10047  elfzle1  10057  elfzle2  10058  elfzle3  10060  uzsplit  10122  uzdisj  10123  uznfz  10133  elfz2nn0  10142  uzsubfz0  10159  nn0disj  10168  fzouzdisj  10210  elfzonelfzo  10260  mulp1mod1  10396  m1modge3gt1  10402  uzennn  10467  seq3split  10510  seq3f1olemqsumk  10530  seq3f1o  10535  seq3coll  10854  seq3shft  10879  cvg1nlemcau  11025  resqrexlemcvg  11060  resqrexlemga  11064  summodclem2a  11421  fsum3  11427  fsum3cvg3  11436  fsumadd  11446  sumsnf  11449  fsummulc2  11488  isumshft  11530  divcnv  11537  geolim2  11552  cvgratnnlemseq  11566  cvgratnnlemsumlt  11568  cvgratz  11572  mertenslemi1  11575  prodmodclem3  11615  prodmodclem2a  11616  fprodntrivap  11624  prodsnf  11632  fprodeq0  11657  efcllemp  11698  infssuzex  11982  suprzubdc  11985  dvdsbnd  11989  uzwodc  12070  ncoprmgcdne1b  12121  isprm5  12174  hashdvds  12253  pcmpt2  12376  pcfaclem  12381  pcfac  12382  nninfdclemp1  12501  strext  12617  lgslem1  14859  lgsdirprm  14893  cvgcmp2nlemabs  15239