Theorem eluz 12756

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

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395   ∈ wcel 2113   class class class wbr 5095  ‘cfv 6489   ≤ cle 11158  ℤcz 12479  ℤ_≥cuz 12742

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-10 2146  ax-11 2162  ax-12 2182  ax-ext 2705  ax-sep 5238  ax-nul 5248  ax-pr 5374  ax-cnex 11073  ax-resscn 11074

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-nf 1785  df-sb 2068  df-mo 2537  df-eu 2566  df-clab 2712  df-cleq 2725  df-clel 2808  df-nfc 2882  df-ral 3049  df-rex 3058  df-rab 3397  df-v 3439  df-dif 3901  df-un 3903  df-in 3905  df-ss 3915  df-nul 4283  df-if 4477  df-pw 4553  df-sn 4578  df-pr 4580  df-op 4584  df-uni 4861  df-br 5096  df-opab 5158  df-mpt 5177  df-id 5516  df-xp 5627  df-rel 5628  df-cnv 5629  df-co 5630  df-dm 5631  df-iota 6445  df-fun 6491  df-fv 6497  df-ov 7358  df-neg 11358  df-z 12480  df-uz 12743

This theorem is referenced by:  uzneg  12762  uztric  12766  uzwo3  12847  fzn  13447  fzsplit2  13456  fznn  13499  uzsplit  13503  elfz2nn0  13525  fzouzsplit  13601  faclbnd  14204  bcval5  14232  fz1isolem  14375  seqcoll  14378  rexuzre  15267  caurcvg  15591  caucvg  15593  summolem2a  15629  fsum0diaglem  15690  climcnds  15765  mertenslem1  15798  ntrivcvgmullem  15815  prodmolem2a  15848  ruclem10  16155  eulerthlem2  16700  pcpremul  16762  pcdvdsb  16788  pcadd  16808  pcfac  16818  pcbc  16819  prmunb  16833  prmreclem5  16839  vdwnnlem3  16916  lt6abl  19815  ovolunlem1a  25444  mbflimsup  25614  plyco0  26144  plyeq0lem  26162  aannenlem1  26283  aaliou3lem2  26298  aaliou3lem8  26300  chtublem  27169  bcmax  27236  bpos1lem  27240  bposlem1  27242  axlowdimlem16  28956  fzsplit3  32801  cycpmco2lem7  33142  ballotlem2  34574  ballotlemimin  34591  breprexplemc  34717  elfzm12  35791  poimirlem3  37736  poimirlem4  37737  poimirlem28  37761  mblfinlem2  37771  incsequz  37861  incsequz2  37862  aks4d1p1  42242  primrootspoweq0  42272  aks6d1c2  42296  sticksstones12a  42323  sticksstones12  42324  aks6d1c6lem3  42338  nacsfix  42869  ellz1  42924  eluzrabdioph  42963  monotuz  43098  expdiophlem1  43178  nznngen  44473  fzisoeu  45464  fmul01  45742  climsuselem1  45769  climsuse  45770  iblspltprt  46133  itgspltprt  46139  wallispilem5  46229  stirlinglem8  46241  dirkertrigeqlem1  46258  fourierdlem12  46279  ssfz12  47476