Theorem eluz 12749

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

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395   ∈ wcel 2109   class class class wbr 5092  ‘cfv 6482   ≤ cle 11150  ℤcz 12471  ℤ_≥cuz 12735

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 5235  ax-nul 5245  ax-pr 5371  ax-cnex 11065  ax-resscn 11066

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 3395  df-v 3438  df-dif 3906  df-un 3908  df-in 3910  df-ss 3920  df-nul 4285  df-if 4477  df-pw 4553  df-sn 4578  df-pr 4580  df-op 4584  df-uni 4859  df-br 5093  df-opab 5155  df-mpt 5174  df-id 5514  df-xp 5625  df-rel 5626  df-cnv 5627  df-co 5628  df-dm 5629  df-iota 6438  df-fun 6484  df-fv 6490  df-ov 7352  df-neg 11350  df-z 12472  df-uz 12736

This theorem is referenced by:  uzneg  12755  uztric  12759  uzwo3  12844  fzn  13443  fzsplit2  13452  fznn  13495  uzsplit  13499  elfz2nn0  13521  fzouzsplit  13597  faclbnd  14197  bcval5  14225  fz1isolem  14368  seqcoll  14371  rexuzre  15260  caurcvg  15584  caucvg  15586  summolem2a  15622  fsum0diaglem  15683  climcnds  15758  mertenslem1  15791  ntrivcvgmullem  15808  prodmolem2a  15841  ruclem10  16148  eulerthlem2  16693  pcpremul  16755  pcdvdsb  16781  pcadd  16801  pcfac  16811  pcbc  16812  prmunb  16826  prmreclem5  16832  vdwnnlem3  16909  lt6abl  19774  ovolunlem1a  25395  mbflimsup  25565  plyco0  26095  plyeq0lem  26113  aannenlem1  26234  aaliou3lem2  26249  aaliou3lem8  26251  chtublem  27120  bcmax  27187  bpos1lem  27191  bposlem1  27193  axlowdimlem16  28906  fzsplit3  32745  cycpmco2lem7  33083  ballotlem2  34473  ballotlemimin  34490  breprexplemc  34616  elfzm12  35668  poimirlem3  37623  poimirlem4  37624  poimirlem28  37648  mblfinlem2  37658  incsequz  37748  incsequz2  37749  aks4d1p1  42069  primrootspoweq0  42099  aks6d1c2  42123  sticksstones12a  42150  sticksstones12  42151  aks6d1c6lem3  42165  nacsfix  42705  ellz1  42760  eluzrabdioph  42799  monotuz  42934  expdiophlem1  43014  nznngen  44309  fzisoeu  45302  fmul01  45581  climsuselem1  45608  climsuse  45609  iblspltprt  45974  itgspltprt  45980  wallispilem5  46070  stirlinglem8  46082  dirkertrigeqlem1  46099  fourierdlem12  46120  ssfz12  47318