Theorem eluz 12578

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

Syntax hints:   → wi 4   ↔ wb 205   ∧ wa 395   ∈ wcel 2109   class class class wbr 5078  ‘cfv 6430   ≤ cle 10994  ℤcz 12302  ℤ_≥cuz 12564

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1801  ax-4 1815  ax-5 1916  ax-6 1974  ax-7 2014  ax-8 2111  ax-9 2119  ax-10 2140  ax-11 2157  ax-12 2174  ax-ext 2710  ax-sep 5226  ax-nul 5233  ax-pr 5355  ax-cnex 10911  ax-resscn 10912

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 844  df-3or 1086  df-3an 1087  df-tru 1544  df-fal 1554  df-ex 1786  df-nf 1790  df-sb 2071  df-mo 2541  df-eu 2570  df-clab 2717  df-cleq 2731  df-clel 2817  df-nfc 2890  df-ral 3070  df-rex 3071  df-rab 3074  df-v 3432  df-dif 3894  df-un 3896  df-in 3898  df-ss 3908  df-nul 4262  df-if 4465  df-sn 4567  df-pr 4569  df-op 4573  df-uni 4845  df-br 5079  df-opab 5141  df-mpt 5162  df-id 5488  df-xp 5594  df-rel 5595  df-cnv 5596  df-co 5597  df-dm 5598  df-iota 6388  df-fun 6432  df-fv 6438  df-ov 7271  df-neg 11191  df-z 12303  df-uz 12565

This theorem is referenced by:  uzneg  12584  uztric  12588  uzwo3  12665  fzn  13254  fzsplit2  13263  fznn  13306  uzsplit  13310  elfz2nn0  13329  fzouzsplit  13403  faclbnd  13985  bcval5  14013  fz1isolem  14156  seqcoll  14159  rexuzre  15045  caurcvg  15369  caucvg  15371  summolem2a  15408  fsum0diaglem  15469  climcnds  15544  mertenslem1  15577  ntrivcvgmullem  15594  prodmolem2a  15625  ruclem10  15929  eulerthlem2  16464  pcpremul  16525  pcdvdsb  16551  pcadd  16571  pcfac  16581  pcbc  16582  prmunb  16596  prmreclem5  16602  vdwnnlem3  16679  lt6abl  19477  ovolunlem1a  24641  mbflimsup  24811  plyco0  25334  plyeq0lem  25352  aannenlem1  25469  aaliou3lem2  25484  aaliou3lem8  25486  chtublem  26340  bcmax  26407  bpos1lem  26411  bposlem1  26413  axlowdimlem16  27306  fzsplit3  31094  cycpmco2lem7  31378  ballotlem2  32434  ballotlemimin  32451  breprexplemc  32591  elfzm12  33612  poimirlem3  35759  poimirlem4  35760  poimirlem28  35784  mblfinlem2  35794  incsequz  35885  incsequz2  35886  aks4d1p1  40064  sticksstones12a  40093  sticksstones12  40094  nacsfix  40514  ellz1  40569  eluzrabdioph  40608  monotuz  40743  expdiophlem1  40823  nznngen  41887  fzisoeu  42793  fmul01  43075  climsuselem1  43102  climsuse  43103  iblspltprt  43468  itgspltprt  43474  wallispilem5  43564  stirlinglem8  43576  dirkertrigeqlem1  43593  fourierdlem12  43614  ssfz12  44758