Theorem eluz 12783

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

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395   ∈ wcel 2109   class class class wbr 5102  ‘cfv 6499   ≤ cle 11185  ℤcz 12505  ℤ_≥cuz 12769

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 5246  ax-nul 5256  ax-pr 5382  ax-cnex 11100  ax-resscn 11101

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 3403  df-v 3446  df-dif 3914  df-un 3916  df-in 3918  df-ss 3928  df-nul 4293  df-if 4485  df-pw 4561  df-sn 4586  df-pr 4588  df-op 4592  df-uni 4868  df-br 5103  df-opab 5165  df-mpt 5184  df-id 5526  df-xp 5637  df-rel 5638  df-cnv 5639  df-co 5640  df-dm 5641  df-iota 6452  df-fun 6501  df-fv 6507  df-ov 7372  df-neg 11384  df-z 12506  df-uz 12770

This theorem is referenced by:  uzneg  12789  uztric  12793  uzwo3  12878  fzn  13477  fzsplit2  13486  fznn  13529  uzsplit  13533  elfz2nn0  13555  fzouzsplit  13631  faclbnd  14231  bcval5  14259  fz1isolem  14402  seqcoll  14405  rexuzre  15295  caurcvg  15619  caucvg  15621  summolem2a  15657  fsum0diaglem  15718  climcnds  15793  mertenslem1  15826  ntrivcvgmullem  15843  prodmolem2a  15876  ruclem10  16183  eulerthlem2  16728  pcpremul  16790  pcdvdsb  16816  pcadd  16836  pcfac  16846  pcbc  16847  prmunb  16861  prmreclem5  16867  vdwnnlem3  16944  lt6abl  19801  ovolunlem1a  25373  mbflimsup  25543  plyco0  26073  plyeq0lem  26091  aannenlem1  26212  aaliou3lem2  26227  aaliou3lem8  26229  chtublem  27098  bcmax  27165  bpos1lem  27169  bposlem1  27171  axlowdimlem16  28860  fzsplit3  32689  cycpmco2lem7  33062  ballotlem2  34453  ballotlemimin  34470  breprexplemc  34596  elfzm12  35635  poimirlem3  37590  poimirlem4  37591  poimirlem28  37615  mblfinlem2  37625  incsequz  37715  incsequz2  37716  aks4d1p1  42037  primrootspoweq0  42067  aks6d1c2  42091  sticksstones12a  42118  sticksstones12  42119  aks6d1c6lem3  42133  nacsfix  42673  ellz1  42728  eluzrabdioph  42767  monotuz  42903  expdiophlem1  42983  nznngen  44278  fzisoeu  45271  fmul01  45551  climsuselem1  45578  climsuse  45579  iblspltprt  45944  itgspltprt  45950  wallispilem5  46040  stirlinglem8  46052  dirkertrigeqlem1  46069  fourierdlem12  46090  ssfz12  47288