Theorem eluz 12800

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

Syntax hints:   → wi 4   ↔ wb 207   ∧ wa 396   ∈ wcel 2119   class class class wbr 5079  ‘cfv 6492   ≤ cle 11178  ℤcz 12522  ℤ_≥cuz 12786

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-10 2152  ax-11 2168  ax-12 2189  ax-ext 2712  ax-sep 5225  ax-pr 5369  ax-cnex 11092  ax-resscn 11093

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 854  df-3or 1093  df-3an 1094  df-tru 1550  df-fal 1560  df-ex 1787  df-nf 1791  df-sb 2074  df-mo 2543  df-eu 2573  df-clab 2719  df-cleq 2732  df-clel 2815  df-nfc 2889  df-ral 3055  df-rex 3065  df-rab 3393  df-v 3434  df-dif 3893  df-un 3895  df-in 3897  df-ss 3907  df-nul 4269  df-if 4462  df-pw 4538  df-sn 4563  df-pr 4565  df-op 4569  df-uni 4846  df-br 5080  df-opab 5142  df-mpt 5161  df-id 5520  df-xp 5631  df-rel 5632  df-cnv 5633  df-co 5634  df-dm 5635  df-iota 6448  df-fun 6494  df-fv 6500  df-ov 7366  df-neg 11378  df-z 12523  df-uz 12787

This theorem is referenced by:  uzneg  12806  uztric  12810  uzwo3  12891  fzn  13492  fzsplit2  13501  fznn  13544  uzsplit  13548  elfz2nn0  13570  fzouzsplit  13647  faclbnd  14250  bcval5  14278  fz1isolem  14421  seqcoll  14424  rexuzre  15313  caurcvg  15637  caucvg  15639  summolem2a  15675  fsum0diaglem  15736  climcnds  15814  mertenslem1  15847  ntrivcvgmullem  15864  prodmolem2a  15897  ruclem10  16204  eulerthlem2  16750  pcpremul  16812  pcdvdsb  16838  pcadd  16858  pcfac  16868  pcbc  16869  prmunb  16883  prmreclem5  16889  vdwnnlem3  16966  lt6abl  19868  ovolunlem1a  25488  mbflimsup  25658  plyco0  26182  plyeq0lem  26200  aannenlem1  26319  aaliou3lem2  26334  aaliou3lem8  26336  chtublem  27199  bcmax  27266  bpos1lem  27270  bposlem1  27272  axlowdimlem16  29051  fzsplit3  32892  cycpmco2lem7  33220  ballotlem2  34680  ballotlemimin  34697  breprexplemc  34823  elfzm12  35910  poimirlem3  37997  poimirlem4  37998  poimirlem28  38022  mblfinlem2  38032  incsequz  38122  incsequz2  38123  aks4d1p1  42568  primrootspoweq0  42598  aks6d1c2  42622  sticksstones12a  42649  sticksstones12  42650  aks6d1c6lem3  42664  nacsfix  43168  ellz1  43223  eluzrabdioph  43258  monotuz  43393  expdiophlem1  43473  nznngen  44767  fzisoeu  45755  fmul01  46032  climsuselem1  46059  climsuse  46060  iblspltprt  46423  itgspltprt  46429  wallispilem5  46519  stirlinglem8  46531  dirkertrigeqlem1  46548  fourierdlem12  46569  ssfz12  47784