Theorem eluz 12746

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

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395   ∈ wcel 2111   class class class wbr 5091  ‘cfv 6481   ≤ cle 11147  ℤcz 12468  ℤ_≥cuz 12732

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 2113  ax-9 2121  ax-10 2144  ax-11 2160  ax-12 2180  ax-ext 2703  ax-sep 5234  ax-nul 5244  ax-pr 5370  ax-cnex 11062  ax-resscn 11063

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 2535  df-eu 2564  df-clab 2710  df-cleq 2723  df-clel 2806  df-nfc 2881  df-ral 3048  df-rex 3057  df-rab 3396  df-v 3438  df-dif 3905  df-un 3907  df-in 3909  df-ss 3919  df-nul 4284  df-if 4476  df-pw 4552  df-sn 4577  df-pr 4579  df-op 4583  df-uni 4860  df-br 5092  df-opab 5154  df-mpt 5173  df-id 5511  df-xp 5622  df-rel 5623  df-cnv 5624  df-co 5625  df-dm 5626  df-iota 6437  df-fun 6483  df-fv 6489  df-ov 7349  df-neg 11347  df-z 12469  df-uz 12733

This theorem is referenced by:  uzneg  12752  uztric  12756  uzwo3  12841  fzn  13440  fzsplit2  13449  fznn  13492  uzsplit  13496  elfz2nn0  13518  fzouzsplit  13594  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  19808  ovolunlem1a  25425  mbflimsup  25595  plyco0  26125  plyeq0lem  26143  aannenlem1  26264  aaliou3lem2  26279  aaliou3lem8  26281  chtublem  27150  bcmax  27217  bpos1lem  27221  bposlem1  27223  axlowdimlem16  28936  fzsplit3  32774  cycpmco2lem7  33099  ballotlem2  34500  ballotlemimin  34517  breprexplemc  34643  elfzm12  35717  poimirlem3  37669  poimirlem4  37670  poimirlem28  37694  mblfinlem2  37704  incsequz  37794  incsequz2  37795  aks4d1p1  42115  primrootspoweq0  42145  aks6d1c2  42169  sticksstones12a  42196  sticksstones12  42197  aks6d1c6lem3  42211  nacsfix  42751  ellz1  42806  eluzrabdioph  42845  monotuz  42980  expdiophlem1  43060  nznngen  44355  fzisoeu  45347  fmul01  45626  climsuselem1  45653  climsuse  45654  iblspltprt  46017  itgspltprt  46023  wallispilem5  46113  stirlinglem8  46125  dirkertrigeqlem1  46142  fourierdlem12  46163  ssfz12  47351