Theorem eluz 12835

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

Syntax hints:   → wi 4   ↔ wb 205   ∧ wa 396   ∈ wcel 2106   class class class wbr 5148  ‘cfv 6543   ≤ cle 11248  ℤcz 12557  ℤ_≥cuz 12821

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2703  ax-sep 5299  ax-nul 5306  ax-pr 5427  ax-cnex 11165  ax-resscn 11166

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3or 1088  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-nf 1786  df-sb 2068  df-mo 2534  df-eu 2563  df-clab 2710  df-cleq 2724  df-clel 2810  df-nfc 2885  df-ral 3062  df-rex 3071  df-rab 3433  df-v 3476  df-dif 3951  df-un 3953  df-in 3955  df-ss 3965  df-nul 4323  df-if 4529  df-sn 4629  df-pr 4631  df-op 4635  df-uni 4909  df-br 5149  df-opab 5211  df-mpt 5232  df-id 5574  df-xp 5682  df-rel 5683  df-cnv 5684  df-co 5685  df-dm 5686  df-iota 6495  df-fun 6545  df-fv 6551  df-ov 7411  df-neg 11446  df-z 12558  df-uz 12822

This theorem is referenced by:  uzneg  12841  uztric  12845  uzwo3  12926  fzn  13516  fzsplit2  13525  fznn  13568  uzsplit  13572  elfz2nn0  13591  fzouzsplit  13666  faclbnd  14249  bcval5  14277  fz1isolem  14421  seqcoll  14424  rexuzre  15298  caurcvg  15622  caucvg  15624  summolem2a  15660  fsum0diaglem  15721  climcnds  15796  mertenslem1  15829  ntrivcvgmullem  15846  prodmolem2a  15877  ruclem10  16181  eulerthlem2  16714  pcpremul  16775  pcdvdsb  16801  pcadd  16821  pcfac  16831  pcbc  16832  prmunb  16846  prmreclem5  16852  vdwnnlem3  16929  lt6abl  19762  ovolunlem1a  25012  mbflimsup  25182  plyco0  25705  plyeq0lem  25723  aannenlem1  25840  aaliou3lem2  25855  aaliou3lem8  25857  chtublem  26711  bcmax  26778  bpos1lem  26782  bposlem1  26784  axlowdimlem16  28212  fzsplit3  32000  cycpmco2lem7  32286  ballotlem2  33482  ballotlemimin  33499  breprexplemc  33639  elfzm12  34655  poimirlem3  36486  poimirlem4  36487  poimirlem28  36511  mblfinlem2  36521  incsequz  36611  incsequz2  36612  aks4d1p1  40936  sticksstones12a  40968  sticksstones12  40969  nacsfix  41440  ellz1  41495  eluzrabdioph  41534  monotuz  41670  expdiophlem1  41750  nznngen  43065  fzisoeu  44000  fmul01  44286  climsuselem1  44313  climsuse  44314  iblspltprt  44679  itgspltprt  44685  wallispilem5  44775  stirlinglem8  44787  dirkertrigeqlem1  44804  fourierdlem12  44825  ssfz12  46012