Theorem eluz 12846

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

Syntax hints:   → wi 4   ↔ wb 208   ∧ wa 399   ∈ wcel 2141   class class class wbr 5097  ‘cfv 6515   ≤ cle 11210  ℤcz 12561  ℤ_≥cuz 12832

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1814  ax-4 1828  ax-5 1929  ax-6 1986  ax-7 2027  ax-8 2143  ax-9 2151  ax-10 2174  ax-11 2190  ax-12 2211  ax-ext 2733  ax-sep 5243  ax-pr 5387  ax-cnex 11122  ax-resscn 11123

This theorem depends on definitions:  df-bi 209  df-an 400  df-or 859  df-3or 1098  df-3an 1099  df-tru 1562  df-fal 1572  df-ex 1799  df-nf 1803  df-sb 2090  df-mo 2565  df-eu 2595  df-clab 2740  df-cleq 2753  df-clel 2836  df-nfc 2910  df-ral 3076  df-rex 3086  df-rab 3414  df-v 3455  df-dif 3905  df-un 3907  df-in 3909  df-ss 3919  df-nul 4284  df-if 4478  df-pw 4554  df-sn 4580  df-pr 4582  df-op 4586  df-uni 4863  df-br 5098  df-opab 5160  df-mpt 5179  df-id 5538  df-xp 5649  df-rel 5650  df-cnv 5651  df-co 5652  df-dm 5653  df-iota 6471  df-fun 6517  df-fv 6523  df-ov 7393  df-neg 11410  df-z 12562  df-uz 12833

This theorem is referenced by:  uzneg  12852  uztric  12856  uzwo3  12937  fzn  13538  fzsplit2  13547  fznn  13590  uzsplit  13594  elfz2nn0  13616  fzouzsplit  13693  faclbnd  14296  bcval5  14324  fz1isolem  14467  seqcoll  14470  rexuzre  15370  caurcvg  15694  caucvg  15696  summolem2a  15732  fsum0diaglem  15793  climcnds  15871  mertenslem1  15904  ntrivcvgmullem  15921  prodmolem2a  15954  ruclem10  16261  eulerthlem2  16807  pcpremul  16869  pcdvdsb  16895  pcadd  16915  pcfac  16925  pcbc  16926  prmunb  16940  prmreclem5  16946  vdwnnlem3  17023  lt6abl  19925  ovolunlem1a  25545  mbflimsup  25715  plyco0  26239  plyeq0lem  26257  aannenlem1  26379  aaliou3lem2  26394  aaliou3lem8  26396  chtublem  27262  bcmax  27329  bpos1lem  27333  bposlem1  27335  axlowdimlem16  29114  fzsplit3  32955  cycpmco2lem7  33272  ballotlem2  34746  ballotlemimin  34763  breprexplemc  34886  elfzm12  35985  poimirlem3  38082  poimirlem4  38083  poimirlem28  38107  mblfinlem2  38117  incsequz  38207  incsequz2  38208  aks4d1p1  42653  primrootspoweq0  42683  aks6d1c2  42707  sticksstones12a  42734  sticksstones12  42735  aks6d1c6lem3  42749  nacsfix  43253  ellz1  43308  eluzrabdioph  43343  monotuz  43478  expdiophlem1  43558  nznngen  44852  fzisoeu  45839  fmul01  46116  climsuselem1  46143  climsuse  46144  iblspltprt  46507  itgspltprt  46513  wallispilem5  46603  stirlinglem8  46615  dirkertrigeqlem1  46632  fourierdlem12  46653  ssfz12  47868