Theorem eluz 12869

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

Assertion

Ref	Expression
eluz	⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑁 ∈ (ℤ≥‘𝑀) ↔ 𝑀 ≤ 𝑁))

Proof of Theorem eluz

Step	Hyp	Ref	Expression
1		eluz1 12859	. 2 ⊢ (𝑀 ∈ ℤ → (𝑁 ∈ (ℤ≥‘𝑀) ↔ (𝑁 ∈ ℤ ∧ 𝑀 ≤ 𝑁)))
2	1	baibd 538	1 ⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑁 ∈ (ℤ≥‘𝑀) ↔ 𝑀 ≤ 𝑁))

Syntax hints:   → wi 4   ↔ wb 205   ∧ wa 394   ∈ wcel 2098   class class class wbr 5149  ‘cfv 6549   ≤ cle 11281  ℤcz 12591  ℤ_≥cuz 12855

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-10 2129  ax-11 2146  ax-12 2166  ax-ext 2696  ax-sep 5300  ax-nul 5307  ax-pr 5429  ax-cnex 11196  ax-resscn 11197

This theorem depends on definitions:  df-bi 206  df-an 395  df-or 846  df-3or 1085  df-3an 1086  df-tru 1536  df-fal 1546  df-ex 1774  df-nf 1778  df-sb 2060  df-mo 2528  df-eu 2557  df-clab 2703  df-cleq 2717  df-clel 2802  df-nfc 2877  df-ral 3051  df-rex 3060  df-rab 3419  df-v 3463  df-dif 3947  df-un 3949  df-in 3951  df-ss 3961  df-nul 4323  df-if 4531  df-sn 4631  df-pr 4633  df-op 4637  df-uni 4910  df-br 5150  df-opab 5212  df-mpt 5233  df-id 5576  df-xp 5684  df-rel 5685  df-cnv 5686  df-co 5687  df-dm 5688  df-iota 6501  df-fun 6551  df-fv 6557  df-ov 7422  df-neg 11479  df-z 12592  df-uz 12856

This theorem is referenced by:  uzneg  12875  uztric  12879  uzwo3  12960  fzn  13552  fzsplit2  13561  fznn  13604  uzsplit  13608  elfz2nn0  13627  fzouzsplit  13702  faclbnd  14285  bcval5  14313  fz1isolem  14458  seqcoll  14461  rexuzre  15335  caurcvg  15659  caucvg  15661  summolem2a  15697  fsum0diaglem  15758  climcnds  15833  mertenslem1  15866  ntrivcvgmullem  15883  prodmolem2a  15914  ruclem10  16219  eulerthlem2  16754  pcpremul  16815  pcdvdsb  16841  pcadd  16861  pcfac  16871  pcbc  16872  prmunb  16886  prmreclem5  16892  vdwnnlem3  16969  lt6abl  19862  ovolunlem1a  25469  mbflimsup  25639  plyco0  26171  plyeq0lem  26189  aannenlem1  26308  aaliou3lem2  26323  aaliou3lem8  26325  chtublem  27189  bcmax  27256  bpos1lem  27260  bposlem1  27262  axlowdimlem16  28840  fzsplit3  32644  cycpmco2lem7  32945  ballotlem2  34239  ballotlemimin  34256  breprexplemc  34395  elfzm12  35410  poimirlem3  37227  poimirlem4  37228  poimirlem28  37252  mblfinlem2  37262  incsequz  37352  incsequz2  37353  aks4d1p1  41679  primrootspoweq0  41709  aks6d1c2  41733  sticksstones12a  41760  sticksstones12  41761  aks6d1c6lem3  41775  nacsfix  42274  ellz1  42329  eluzrabdioph  42368  monotuz  42504  expdiophlem1  42584  nznngen  43895  fzisoeu  44820  fmul01  45106  climsuselem1  45133  climsuse  45134  iblspltprt  45499  itgspltprt  45505  wallispilem5  45595  stirlinglem8  45607  dirkertrigeqlem1  45624  fourierdlem12  45645  ssfz12  46832