Theorem eluz 12767

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

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395   ∈ wcel 2109   class class class wbr 5095  ‘cfv 6486   ≤ cle 11169  ℤcz 12489  ℤ_≥cuz 12753

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 5238  ax-nul 5248  ax-pr 5374  ax-cnex 11084  ax-resscn 11085

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 3397  df-v 3440  df-dif 3908  df-un 3910  df-in 3912  df-ss 3922  df-nul 4287  df-if 4479  df-pw 4555  df-sn 4580  df-pr 4582  df-op 4586  df-uni 4862  df-br 5096  df-opab 5158  df-mpt 5177  df-id 5518  df-xp 5629  df-rel 5630  df-cnv 5631  df-co 5632  df-dm 5633  df-iota 6442  df-fun 6488  df-fv 6494  df-ov 7356  df-neg 11368  df-z 12490  df-uz 12754

This theorem is referenced by:  uzneg  12773  uztric  12777  uzwo3  12862  fzn  13461  fzsplit2  13470  fznn  13513  uzsplit  13517  elfz2nn0  13539  fzouzsplit  13615  faclbnd  14215  bcval5  14243  fz1isolem  14386  seqcoll  14389  rexuzre  15278  caurcvg  15602  caucvg  15604  summolem2a  15640  fsum0diaglem  15701  climcnds  15776  mertenslem1  15809  ntrivcvgmullem  15826  prodmolem2a  15859  ruclem10  16166  eulerthlem2  16711  pcpremul  16773  pcdvdsb  16799  pcadd  16819  pcfac  16829  pcbc  16830  prmunb  16844  prmreclem5  16850  vdwnnlem3  16927  lt6abl  19792  ovolunlem1a  25413  mbflimsup  25583  plyco0  26113  plyeq0lem  26131  aannenlem1  26252  aaliou3lem2  26267  aaliou3lem8  26269  chtublem  27138  bcmax  27205  bpos1lem  27209  bposlem1  27211  axlowdimlem16  28920  fzsplit3  32749  cycpmco2lem7  33087  ballotlem2  34459  ballotlemimin  34476  breprexplemc  34602  elfzm12  35650  poimirlem3  37605  poimirlem4  37606  poimirlem28  37630  mblfinlem2  37640  incsequz  37730  incsequz2  37731  aks4d1p1  42052  primrootspoweq0  42082  aks6d1c2  42106  sticksstones12a  42133  sticksstones12  42134  aks6d1c6lem3  42148  nacsfix  42688  ellz1  42743  eluzrabdioph  42782  monotuz  42917  expdiophlem1  42997  nznngen  44292  fzisoeu  45285  fmul01  45565  climsuselem1  45592  climsuse  45593  iblspltprt  45958  itgspltprt  45964  wallispilem5  46054  stirlinglem8  46066  dirkertrigeqlem1  46083  fourierdlem12  46104  ssfz12  47302