Theorem eluz 12872

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

Syntax hints:   → wi 4   ↔ wb 209   ∧ wa 400   ∈ wcel 2149   class class class wbr 5110  ‘cfv 6533   ≤ cle 11240  ℤcz 12587  ℤ_≥cuz 12858

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-8 2151  ax-9 2159  ax-10 2182  ax-11 2198  ax-12 2219  ax-ext 2741  ax-sep 5258  ax-pr 5402  ax-cnex 11152  ax-resscn 11153

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3or 1102  df-3an 1103  df-tru 1570  df-fal 1580  df-ex 1807  df-nf 1811  df-sb 2098  df-mo 2573  df-eu 2603  df-clab 2748  df-cleq 2761  df-clel 2844  df-nfc 2918  df-ral 3086  df-rex 3096  df-rab 3424  df-v 3465  df-dif 3916  df-un 3918  df-in 3920  df-ss 3930  df-nul 4295  df-if 4490  df-pw 4566  df-sn 4592  df-pr 4594  df-op 4598  df-uni 4874  df-br 5111  df-opab 5175  df-mpt 5194  df-id 5554  df-xp 5665  df-rel 5666  df-cnv 5667  df-co 5668  df-dm 5669  df-iota 6489  df-fun 6535  df-fv 6541  df-ov 7411  df-neg 11440  df-z 12588  df-uz 12859

This theorem is referenced by:  uzneg  12878  uztric  12882  uzwo3  12963  fzn  13564  fzsplit2  13573  fznn  13616  uzsplit  13620  elfz2nn0  13642  fzouzsplit  13719  faclbnd  14322  bcval5  14350  fz1isolem  14494  seqcoll  14497  rexuzre  15400  caurcvg  15724  caucvg  15726  summolem2a  15762  fsum0diaglem  15823  climcnds  15901  mertenslem1  15934  ntrivcvgmullem  15951  prodmolem2a  15984  ruclem10  16291  eulerthlem2  16837  pcpremul  16899  pcdvdsb  16925  pcadd  16945  pcfac  16955  pcbc  16956  prmunb  16970  prmreclem5  16976  vdwnnlem3  17053  lt6abl  19961  ovolunlem1a  25620  mbflimsup  25790  plyco0  26314  plyeq0lem  26332  aannenlem1  26454  aaliou3lem2  26469  aaliou3lem8  26471  chtublem  27337  bcmax  27404  bpos1lem  27408  bposlem1  27410  axlowdimlem16  29244  fzsplit3  33075  cycpmco2lem7  33389  ballotlem2  34820  ballotlemimin  34837  breprexplemc  34960  elfzm12  36062  poimirlem3  38157  poimirlem4  38158  poimirlem28  38182  mblfinlem2  38192  incsequz  38282  incsequz2  38283  aks4d1p1  42728  primrootspoweq0  42758  aks6d1c2  42782  sticksstones12a  42809  sticksstones12  42810  aks6d1c6lem3  42824  nacsfix  43328  ellz1  43383  eluzrabdioph  43418  monotuz  43553  expdiophlem1  43633  nznngen  44911  fzisoeu  45904  fmul01  46181  climsuselem1  46208  climsuse  46209  iblspltprt  46572  itgspltprt  46578  wallispilem5  46668  stirlinglem8  46680  dirkertrigeqlem1  46697  fourierdlem12  46718  ssfz12  47933