Theorem eluz 12901

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

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   ∧ wa 401   ∈ wcel 2145   class class class wbr 5103  ‘cfv 6533   ≤ cle 11268  ℤcz 12615  ℤ_≥cuz 12887

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 2147  ax-9 2155  ax-10 2178  ax-11 2194  ax-12 2213  ax-ext 2732  ax-sep 5251  ax-pr 5398  ax-cnex 11180  ax-resscn 11181

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 2564  df-eu 2594  df-clab 2739  df-cleq 2752  df-clel 2835  df-nfc 2909  df-ral 3077  df-rex 3087  df-rab 3413  df-v 3452  df-dif 3902  df-un 3904  df-in 3906  df-ss 3916  df-nul 4280  df-if 4483  df-pw 4559  df-sn 4585  df-pr 4587  df-op 4591  df-uni 4868  df-br 5104  df-opab 5168  df-mpt 5187  df-id 5550  df-xp 5661  df-rel 5662  df-cnv 5663  df-co 5664  df-dm 5665  df-iota 6489  df-fun 6535  df-fv 6541  df-ov 7416  df-neg 11468  df-z 12616  df-uz 12888

This theorem is used by:  uzneg  12907  uztric  12911  uzwo3  12992  fzn  13594  fzsplit2  13604  fznn  13647  uzsplit  13651  elfz2nn0  13673  fzouzsplit  13750  faclbnd  14354  bcval5  14382  fz1isolem  14526  seqcoll  14529  rexuzre  15440  caurcvg  15764  caucvg  15766  summolem2a  15801  fsum0diaglem  15862  climcnds  15940  mertenslem1  15973  ntrivcvgmullem  15990  prodmolem2a  16021  ruclem10  16327  eulerthlem2  16873  pcpremul  16935  pcdvdsb  16961  pcadd  16981  pcfac  16991  pcbc  16992  prmunb  17006  prmreclem5  17012  vdwnnlem3  17089  lt6abl  20022  ovolunlem1a  25724  mbflimsup  25894  plyco0  26417  plyeq0lem  26436  aannenlem1  26564  aaliou3lem2  26579  aaliou3lem8  26581  chtublem  27447  bcmax  27514  bpos1lem  27518  bposlem1  27520  axlowdimlem16  29414  fzsplit3  33264  cycpmco2lem7  33572  ballotlem2  35000  ballotlemimin  35017  breprexplemc  35140  elfzm12  36254  poimirlem3  38372  poimirlem4  38373  poimirlem28  38397  mblfinlem2  38407  incsequz  38498  incsequz2  38499  aks4d1p1  42942  primrootspoweq0  42972  aks6d1c2  42996  sticksstones12a  43023  sticksstones12  43024  aks6d1c6lem3  43038  nacsfix  43557  ellz1  43612  eluzrabdioph  43647  monotuz  43782  expdiophlem1  43862  nznngen  45140  fzisoeu  46133  fmul01  46410  climsuselem1  46437  climsuse  46438  iblspltprt  46801  itgspltprt  46807  wallispilem5  46897  stirlinglem8  46909  dirkertrigeqlem1  46926  fourierdlem12  46947  ssfz12  48202