Theorem eluz 12877

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

Syntax hints:   → wi 4   ↔ wb 209   ∧ wa 400   ∈ wcel 2143   class class class wbr 5110  ‘cfv 6538   ≤ cle 11245  ℤcz 12592  ℤ_≥cuz 12863

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-10 2176  ax-11 2192  ax-12 2213  ax-ext 2735  ax-sep 5258  ax-pr 5406  ax-cnex 11157  ax-resscn 11158

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3or 1104  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1810  df-nf 1814  df-sb 2097  df-mo 2567  df-eu 2597  df-clab 2742  df-cleq 2755  df-clel 2838  df-nfc 2912  df-ral 3080  df-rex 3090  df-rab 3417  df-v 3457  df-dif 3909  df-un 3911  df-in 3913  df-ss 3923  df-nul 4288  df-if 4489  df-pw 4565  df-sn 4591  df-pr 4593  df-op 4597  df-uni 4874  df-br 5111  df-opab 5175  df-mpt 5194  df-id 5558  df-xp 5669  df-rel 5670  df-cnv 5671  df-co 5672  df-dm 5673  df-iota 6494  df-fun 6540  df-fv 6546  df-ov 7415  df-neg 11445  df-z 12593  df-uz 12864

This theorem is referenced by:  uzneg  12883  uztric  12887  uzwo3  12968  fzn  13569  fzsplit2  13579  fznn  13622  uzsplit  13626  elfz2nn0  13648  fzouzsplit  13725  faclbnd  14328  bcval5  14356  fz1isolem  14500  seqcoll  14503  rexuzre  15406  caurcvg  15730  caucvg  15732  summolem2a  15768  fsum0diaglem  15829  climcnds  15907  mertenslem1  15940  ntrivcvgmullem  15957  prodmolem2a  15990  ruclem10  16296  eulerthlem2  16842  pcpremul  16904  pcdvdsb  16930  pcadd  16950  pcfac  16960  pcbc  16961  prmunb  16975  prmreclem5  16981  vdwnnlem3  17058  lt6abl  19966  ovolunlem1a  25636  mbflimsup  25806  plyco0  26330  plyeq0lem  26348  aannenlem1  26472  aaliou3lem2  26487  aaliou3lem8  26489  chtublem  27356  bcmax  27423  bpos1lem  27427  bposlem1  27429  axlowdimlem16  29288  fzsplit3  33119  cycpmco2lem7  33433  ballotlem2  34860  ballotlemimin  34877  breprexplemc  35000  elfzm12  36148  poimirlem3  38255  poimirlem4  38256  poimirlem28  38280  mblfinlem2  38290  incsequz  38380  incsequz2  38381  aks4d1p1  42824  primrootspoweq0  42854  aks6d1c2  42878  sticksstones12a  42905  sticksstones12  42906  aks6d1c6lem3  42920  nacsfix  43426  ellz1  43481  eluzrabdioph  43516  monotuz  43651  expdiophlem1  43731  nznngen  45009  fzisoeu  46002  fmul01  46279  climsuselem1  46306  climsuse  46307  iblspltprt  46670  itgspltprt  46676  wallispilem5  46766  stirlinglem8  46778  dirkertrigeqlem1  46795  fourierdlem12  46816  ssfz12  48034