Theorem eluz 12807

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

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395   ∈ wcel 2109   class class class wbr 5107  ‘cfv 6511   ≤ cle 11209  ℤcz 12529  ℤ_≥cuz 12793

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-10 2142  ax-11 2158  ax-12 2178  ax-ext 2701  ax-sep 5251  ax-nul 5261  ax-pr 5387  ax-cnex 11124  ax-resscn 11125

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2533  df-eu 2562  df-clab 2708  df-cleq 2721  df-clel 2803  df-nfc 2878  df-ral 3045  df-rex 3054  df-rab 3406  df-v 3449  df-dif 3917  df-un 3919  df-in 3921  df-ss 3931  df-nul 4297  df-if 4489  df-pw 4565  df-sn 4590  df-pr 4592  df-op 4596  df-uni 4872  df-br 5108  df-opab 5170  df-mpt 5189  df-id 5533  df-xp 5644  df-rel 5645  df-cnv 5646  df-co 5647  df-dm 5648  df-iota 6464  df-fun 6513  df-fv 6519  df-ov 7390  df-neg 11408  df-z 12530  df-uz 12794

This theorem is referenced by:  uzneg  12813  uztric  12817  uzwo3  12902  fzn  13501  fzsplit2  13510  fznn  13553  uzsplit  13557  elfz2nn0  13579  fzouzsplit  13655  faclbnd  14255  bcval5  14283  fz1isolem  14426  seqcoll  14429  rexuzre  15319  caurcvg  15643  caucvg  15645  summolem2a  15681  fsum0diaglem  15742  climcnds  15817  mertenslem1  15850  ntrivcvgmullem  15867  prodmolem2a  15900  ruclem10  16207  eulerthlem2  16752  pcpremul  16814  pcdvdsb  16840  pcadd  16860  pcfac  16870  pcbc  16871  prmunb  16885  prmreclem5  16891  vdwnnlem3  16968  lt6abl  19825  ovolunlem1a  25397  mbflimsup  25567  plyco0  26097  plyeq0lem  26115  aannenlem1  26236  aaliou3lem2  26251  aaliou3lem8  26253  chtublem  27122  bcmax  27189  bpos1lem  27193  bposlem1  27195  axlowdimlem16  28884  fzsplit3  32716  cycpmco2lem7  33089  ballotlem2  34480  ballotlemimin  34497  breprexplemc  34623  elfzm12  35662  poimirlem3  37617  poimirlem4  37618  poimirlem28  37642  mblfinlem2  37652  incsequz  37742  incsequz2  37743  aks4d1p1  42064  primrootspoweq0  42094  aks6d1c2  42118  sticksstones12a  42145  sticksstones12  42146  aks6d1c6lem3  42160  nacsfix  42700  ellz1  42755  eluzrabdioph  42794  monotuz  42930  expdiophlem1  43010  nznngen  44305  fzisoeu  45298  fmul01  45578  climsuselem1  45605  climsuse  45606  iblspltprt  45971  itgspltprt  45977  wallispilem5  46067  stirlinglem8  46079  dirkertrigeqlem1  46096  fourierdlem12  46117  ssfz12  47315