Theorem eluz 12887

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

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   ∧ wa 401   ∈ wcel 2146   class class class wbr 5111  ‘cfv 6540   ≤ cle 11255  ℤcz 12602  ℤ_≥cuz 12873

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2148  ax-9 2156  ax-10 2179  ax-11 2195  ax-12 2216  ax-ext 2737  ax-sep 5259  ax-pr 5406  ax-cnex 11167  ax-resscn 11168

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3or 1104  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-nf 1817  df-sb 2100  df-mo 2569  df-eu 2599  df-clab 2744  df-cleq 2757  df-clel 2840  df-nfc 2914  df-ral 3082  df-rex 3092  df-rab 3419  df-v 3459  df-dif 3909  df-un 3911  df-in 3913  df-ss 3923  df-nul 4287  df-if 4490  df-pw 4566  df-sn 4592  df-pr 4594  df-op 4598  df-uni 4875  df-br 5112  df-opab 5176  df-mpt 5195  df-id 5558  df-xp 5669  df-rel 5670  df-cnv 5671  df-co 5672  df-dm 5673  df-iota 6496  df-fun 6542  df-fv 6548  df-ov 7419  df-neg 11455  df-z 12603  df-uz 12874

This theorem is used by:  uzneg  12893  uztric  12897  uzwo3  12978  fzn  13579  fzsplit2  13589  fznn  13632  uzsplit  13636  elfz2nn0  13658  fzouzsplit  13735  faclbnd  14339  bcval5  14367  fz1isolem  14511  seqcoll  14514  rexuzre  15423  caurcvg  15747  caucvg  15749  summolem2a  15784  fsum0diaglem  15845  climcnds  15923  mertenslem1  15956  ntrivcvgmullem  15973  prodmolem2a  16006  ruclem10  16312  eulerthlem2  16858  pcpremul  16920  pcdvdsb  16946  pcadd  16966  pcfac  16976  pcbc  16977  prmunb  16991  prmreclem5  16997  vdwnnlem3  17074  lt6abl  19988  ovolunlem1a  25684  mbflimsup  25854  plyco0  26378  plyeq0lem  26396  aannenlem1  26520  aaliou3lem2  26535  aaliou3lem8  26537  chtublem  27404  bcmax  27471  bpos1lem  27475  bposlem1  27477  axlowdimlem16  29336  fzsplit3  33167  cycpmco2lem7  33475  ballotlem2  34903  ballotlemimin  34920  breprexplemc  35043  elfzm12  36180  poimirlem3  38307  poimirlem4  38308  poimirlem28  38332  mblfinlem2  38342  incsequz  38432  incsequz2  38433  aks4d1p1  42876  primrootspoweq0  42906  aks6d1c2  42930  sticksstones12a  42957  sticksstones12  42958  aks6d1c6lem3  42972  nacsfix  43476  ellz1  43531  eluzrabdioph  43566  monotuz  43701  expdiophlem1  43781  nznngen  45059  fzisoeu  46052  fmul01  46329  climsuselem1  46356  climsuse  46357  iblspltprt  46720  itgspltprt  46726  wallispilem5  46816  stirlinglem8  46828  dirkertrigeqlem1  46845  fourierdlem12  46866  ssfz12  48084