Theorem eluz 11701

Description: Membership in an upper set of integers. (Contributed by NM, 2-Oct-2005.)

Assertion

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

Proof of Theorem eluz

Step	Hyp	Ref	Expression
1		eluz1 11691	. 2 |- ( M e. ZZ -> ( N e. ( ZZ>= ` M ) <-> ( N e. ZZ /\ M <_ N ) ) )
2	1	baibd 948	1 |- ( ( M e. ZZ /\ N e. ZZ ) -> ( N e. ( ZZ>= ` M ) <-> M <_ N ) )

Syntax hints:   -> wi 4   <-> wb 196   /\ wa 384   e. wcel 1990   class class class wbr 4653   ` cfv 5888   <_ cle 10075   ZZcz 11377   ZZ>=cuz 11687

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602  ax-sep 4781  ax-nul 4789  ax-pr 4906  ax-cnex 9992  ax-resscn 9993

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3or 1038  df-3an 1039  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-eu 2474  df-mo 2475  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-ral 2917  df-rex 2918  df-rab 2921  df-v 3202  df-sbc 3436  df-dif 3577  df-un 3579  df-in 3581  df-ss 3588  df-nul 3916  df-if 4087  df-sn 4178  df-pr 4180  df-op 4184  df-uni 4437  df-br 4654  df-opab 4713  df-mpt 4730  df-id 5024  df-xp 5120  df-rel 5121  df-cnv 5122  df-co 5123  df-dm 5124  df-iota 5851  df-fun 5890  df-fv 5896  df-ov 6653  df-neg 10269  df-z 11378  df-uz 11688

This theorem is referenced by:  uzneg  11706  uztric  11709  uzwo3  11783  fzn  12357  fzsplit2  12366  fznn  12408  uzsplit  12412  elfz2nn0  12431  fzouzsplit  12503  faclbnd  13077  bcval5  13105  fz1isolem  13245  seqcoll  13248  rexuzre  14092  caurcvg  14407  caucvg  14409  summolem2a  14446  fsum0diaglem  14508  climcnds  14583  mertenslem1  14616  ntrivcvgmullem  14633  prodmolem2a  14664  ruclem10  14968  eulerthlem2  15487  pcpremul  15548  pcdvdsb  15573  pcadd  15593  pcfac  15603  pcbc  15604  prmunb  15618  prmreclem5  15624  vdwnnlem3  15701  lt6abl  18296  ovolunlem1a  23264  mbflimsup  23433  plyco0  23948  plyeq0lem  23966  aannenlem1  24083  aaliou3lem2  24098  aaliou3lem8  24100  chtublem  24936  bcmax  25003  bpos1lem  25007  bposlem1  25009  axlowdimlem16  25837  fzsplit3  29553  ballotlem2  30550  ballotlemimin  30567  breprexplemc  30710  elfzm12  31569  poimirlem3  33412  poimirlem4  33413  poimirlem28  33437  mblfinlem2  33447  incsequz  33544  incsequz2  33545  nacsfix  37275  ellz1  37330  eluzrabdioph  37370  monotuz  37506  expdiophlem1  37588  nznngen  38515  fzisoeu  39514  fmul01  39812  climsuselem1  39839  climsuse  39840  iblspltprt  40189  itgspltprt  40195  wallispilem5  40286  stirlinglem8  40298  dirkertrigeqlem1  40315  fourierdlem12  40336  ssfz12  41324