Theorem eluz 12972

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 12962	. 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 6537   ≤ cle 11337  ℤcz 12686  ℤ_≥cuz 12958

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 2733  ax-sep 5249  ax-pr 5391  ax-cnex 11249  ax-resscn 11250

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 2565  df-eu 2595  df-clab 2740  df-cleq 2753  df-clel 2836  df-nfc 2910  df-ral 3078  df-rex 3088  df-rab 3414  df-v 3453  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 5546  df-xp 5657  df-rel 5658  df-cnv 5659  df-co 5660  df-dm 5661  df-iota 6493  df-fun 6539  df-fv 6545  df-ov 7421  df-neg 11537  df-z 12687  df-uz 12959

This theorem is used by:  uzneg  12978  uztric  12982  uzwo3  13063  fzn  13666  fzsplit2  13676  fznn  13719  uzsplit  13723  elfz2nn0  13745  fzouzsplit  13822  faclbnd  14427  bcval5  14455  fz1isolem  14599  seqcoll  14602  rexuzre  15513  caurcvg  15837  caucvg  15839  summolem2a  15874  fsum0diaglem  15935  climcnds  16013  mertenslem1  16046  ntrivcvgmullem  16063  prodmolem2a  16094  ruclem10  16400  eulerthlem2  16952  pcpremul  17014  pcdvdsb  17040  pcadd  17060  pcfac  17070  pcbc  17071  prmunb  17085  prmreclem5  17091  vdwnnlem3  17168  lt6abl  20102  ovolunlem1a  25810  mbflimsup  25980  plyco0  26503  plyeq0lem  26522  aannenlem1  26648  aaliou3lem2  26663  aaliou3lem8  26665  chtublem  27531  bcmax  27598  bpos1lem  27602  bposlem1  27604  axlowdimlem16  29528  fzsplit3  33378  cycpmco2lem7  33686  ballotlem2  35114  ballotlemimin  35131  breprexplemc  35254  elfzm12  36419  poimirlem3  38521  poimirlem4  38522  poimirlem28  38546  mblfinlem2  38556  incsequz  38662  incsequz2  38663  aks4d1p1  43106  primrootspoweq0  43136  aks6d1c2  43160  sticksstones12a  43187  sticksstones12  43188  aks6d1c6lem3  43202  nacsfix  43702  ellz1  43757  eluzrabdioph  43792  monotuz  43927  expdiophlem1  44007  nznngen  45285  fzisoeu  46285  fmul01  46561  climsuselem1  46588  climsuse  46589  iblspltprt  46952  itgspltprt  46958  wallispilem5  47048  stirlinglem8  47060  dirkertrigeqlem1  47077  fourierdlem12  47098  ssfz12  48353