Theorem eluz 12917

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

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395   ∈ wcel 2108   class class class wbr 5166  ‘cfv 6573   ≤ cle 11325  ℤcz 12639  ℤ_≥cuz 12903

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-10 2141  ax-11 2158  ax-12 2178  ax-ext 2711  ax-sep 5317  ax-nul 5324  ax-pr 5447  ax-cnex 11240  ax-resscn 11241

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 847  df-3or 1088  df-3an 1089  df-tru 1540  df-fal 1550  df-ex 1778  df-nf 1782  df-sb 2065  df-mo 2543  df-eu 2572  df-clab 2718  df-cleq 2732  df-clel 2819  df-nfc 2895  df-ral 3068  df-rex 3077  df-rab 3444  df-v 3490  df-dif 3979  df-un 3981  df-in 3983  df-ss 3993  df-nul 4353  df-if 4549  df-pw 4624  df-sn 4649  df-pr 4651  df-op 4655  df-uni 4932  df-br 5167  df-opab 5229  df-mpt 5250  df-id 5593  df-xp 5706  df-rel 5707  df-cnv 5708  df-co 5709  df-dm 5710  df-iota 6525  df-fun 6575  df-fv 6581  df-ov 7451  df-neg 11523  df-z 12640  df-uz 12904

This theorem is referenced by:  uzneg  12923  uztric  12927  uzwo3  13008  fzn  13600  fzsplit2  13609  fznn  13652  uzsplit  13656  elfz2nn0  13675  fzouzsplit  13751  faclbnd  14339  bcval5  14367  fz1isolem  14510  seqcoll  14513  rexuzre  15401  caurcvg  15725  caucvg  15727  summolem2a  15763  fsum0diaglem  15824  climcnds  15899  mertenslem1  15932  ntrivcvgmullem  15949  prodmolem2a  15982  ruclem10  16287  eulerthlem2  16829  pcpremul  16890  pcdvdsb  16916  pcadd  16936  pcfac  16946  pcbc  16947  prmunb  16961  prmreclem5  16967  vdwnnlem3  17044  lt6abl  19937  ovolunlem1a  25550  mbflimsup  25720  plyco0  26251  plyeq0lem  26269  aannenlem1  26388  aaliou3lem2  26403  aaliou3lem8  26405  chtublem  27273  bcmax  27340  bpos1lem  27344  bposlem1  27346  axlowdimlem16  28990  fzsplit3  32799  cycpmco2lem7  33125  ballotlem2  34453  ballotlemimin  34470  breprexplemc  34609  elfzm12  35643  poimirlem3  37583  poimirlem4  37584  poimirlem28  37608  mblfinlem2  37618  incsequz  37708  incsequz2  37709  aks4d1p1  42033  primrootspoweq0  42063  aks6d1c2  42087  sticksstones12a  42114  sticksstones12  42115  aks6d1c6lem3  42129  nacsfix  42668  ellz1  42723  eluzrabdioph  42762  monotuz  42898  expdiophlem1  42978  nznngen  44285  fzisoeu  45215  fmul01  45501  climsuselem1  45528  climsuse  45529  iblspltprt  45894  itgspltprt  45900  wallispilem5  45990  stirlinglem8  46002  dirkertrigeqlem1  46019  fourierdlem12  46040  ssfz12  47229