Theorem eluz 12814

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

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395   ∈ wcel 2109   class class class wbr 5110  ‘cfv 6514   ≤ cle 11216  ℤcz 12536  ℤ_≥cuz 12800

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-10 2142  ax-11 2158  ax-12 2178  ax-ext 2702  ax-sep 5254  ax-nul 5264  ax-pr 5390  ax-cnex 11131  ax-resscn 11132

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2534  df-eu 2563  df-clab 2709  df-cleq 2722  df-clel 2804  df-nfc 2879  df-ral 3046  df-rex 3055  df-rab 3409  df-v 3452  df-dif 3920  df-un 3922  df-in 3924  df-ss 3934  df-nul 4300  df-if 4492  df-pw 4568  df-sn 4593  df-pr 4595  df-op 4599  df-uni 4875  df-br 5111  df-opab 5173  df-mpt 5192  df-id 5536  df-xp 5647  df-rel 5648  df-cnv 5649  df-co 5650  df-dm 5651  df-iota 6467  df-fun 6516  df-fv 6522  df-ov 7393  df-neg 11415  df-z 12537  df-uz 12801

This theorem is referenced by:  uzneg  12820  uztric  12824  uzwo3  12909  fzn  13508  fzsplit2  13517  fznn  13560  uzsplit  13564  elfz2nn0  13586  fzouzsplit  13662  faclbnd  14262  bcval5  14290  fz1isolem  14433  seqcoll  14436  rexuzre  15326  caurcvg  15650  caucvg  15652  summolem2a  15688  fsum0diaglem  15749  climcnds  15824  mertenslem1  15857  ntrivcvgmullem  15874  prodmolem2a  15907  ruclem10  16214  eulerthlem2  16759  pcpremul  16821  pcdvdsb  16847  pcadd  16867  pcfac  16877  pcbc  16878  prmunb  16892  prmreclem5  16898  vdwnnlem3  16975  lt6abl  19832  ovolunlem1a  25404  mbflimsup  25574  plyco0  26104  plyeq0lem  26122  aannenlem1  26243  aaliou3lem2  26258  aaliou3lem8  26260  chtublem  27129  bcmax  27196  bpos1lem  27200  bposlem1  27202  axlowdimlem16  28891  fzsplit3  32723  cycpmco2lem7  33096  ballotlem2  34487  ballotlemimin  34504  breprexplemc  34630  elfzm12  35669  poimirlem3  37624  poimirlem4  37625  poimirlem28  37649  mblfinlem2  37659  incsequz  37749  incsequz2  37750  aks4d1p1  42071  primrootspoweq0  42101  aks6d1c2  42125  sticksstones12a  42152  sticksstones12  42153  aks6d1c6lem3  42167  nacsfix  42707  ellz1  42762  eluzrabdioph  42801  monotuz  42937  expdiophlem1  43017  nznngen  44312  fzisoeu  45305  fmul01  45585  climsuselem1  45612  climsuse  45613  iblspltprt  45978  itgspltprt  45984  wallispilem5  46074  stirlinglem8  46086  dirkertrigeqlem1  46103  fourierdlem12  46124  ssfz12  47319