Theorem eluz 12701

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

Syntax hints:   → wi 4   ↔ wb 205   ∧ wa 397   ∈ wcel 2106   class class class wbr 5096  ‘cfv 6483   ≤ cle 11115  ℤcz 12424  ℤ_≥cuz 12687

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2708  ax-sep 5247  ax-nul 5254  ax-pr 5376  ax-cnex 11032  ax-resscn 11033

This theorem depends on definitions:  df-bi 206  df-an 398  df-or 846  df-3or 1088  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-nf 1786  df-sb 2068  df-mo 2539  df-eu 2568  df-clab 2715  df-cleq 2729  df-clel 2815  df-nfc 2887  df-ral 3063  df-rex 3072  df-rab 3405  df-v 3444  df-dif 3904  df-un 3906  df-in 3908  df-ss 3918  df-nul 4274  df-if 4478  df-sn 4578  df-pr 4580  df-op 4584  df-uni 4857  df-br 5097  df-opab 5159  df-mpt 5180  df-id 5522  df-xp 5630  df-rel 5631  df-cnv 5632  df-co 5633  df-dm 5634  df-iota 6435  df-fun 6485  df-fv 6491  df-ov 7344  df-neg 11313  df-z 12425  df-uz 12688

This theorem is referenced by:  uzneg  12707  uztric  12711  uzwo3  12788  fzn  13377  fzsplit2  13386  fznn  13429  uzsplit  13433  elfz2nn0  13452  fzouzsplit  13527  faclbnd  14109  bcval5  14137  fz1isolem  14279  seqcoll  14282  rexuzre  15163  caurcvg  15487  caucvg  15489  summolem2a  15526  fsum0diaglem  15587  climcnds  15662  mertenslem1  15695  ntrivcvgmullem  15712  prodmolem2a  15743  ruclem10  16047  eulerthlem2  16580  pcpremul  16641  pcdvdsb  16667  pcadd  16687  pcfac  16697  pcbc  16698  prmunb  16712  prmreclem5  16718  vdwnnlem3  16795  lt6abl  19590  ovolunlem1a  24765  mbflimsup  24935  plyco0  25458  plyeq0lem  25476  aannenlem1  25593  aaliou3lem2  25608  aaliou3lem8  25610  chtublem  26464  bcmax  26531  bpos1lem  26535  bposlem1  26537  axlowdimlem16  27613  fzsplit3  31400  cycpmco2lem7  31684  ballotlem2  32753  ballotlemimin  32770  breprexplemc  32910  elfzm12  33930  poimirlem3  35936  poimirlem4  35937  poimirlem28  35961  mblfinlem2  35971  incsequz  36062  incsequz2  36063  aks4d1p1  40389  sticksstones12a  40421  sticksstones12  40422  nacsfix  40847  ellz1  40902  eluzrabdioph  40941  monotuz  41077  expdiophlem1  41157  nznngen  42307  fzisoeu  43226  fmul01  43509  climsuselem1  43536  climsuse  43537  iblspltprt  43902  itgspltprt  43908  wallispilem5  43998  stirlinglem8  44010  dirkertrigeqlem1  44027  fourierdlem12  44048  ssfz12  45224