Theorem eluz 12793

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

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395   ∈ wcel 2114   class class class wbr 5086  ‘cfv 6492   ≤ cle 11171  ℤcz 12515  ℤ_≥cuz 12779

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-10 2147  ax-11 2163  ax-12 2185  ax-ext 2709  ax-sep 5231  ax-pr 5370  ax-cnex 11085  ax-resscn 11086

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3or 1088  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-nf 1786  df-sb 2069  df-mo 2540  df-eu 2570  df-clab 2716  df-cleq 2729  df-clel 2812  df-nfc 2886  df-ral 3053  df-rex 3063  df-rab 3391  df-v 3432  df-dif 3893  df-un 3895  df-in 3897  df-ss 3907  df-nul 4275  df-if 4468  df-pw 4544  df-sn 4569  df-pr 4571  df-op 4575  df-uni 4852  df-br 5087  df-opab 5149  df-mpt 5168  df-id 5519  df-xp 5630  df-rel 5631  df-cnv 5632  df-co 5633  df-dm 5634  df-iota 6448  df-fun 6494  df-fv 6500  df-ov 7363  df-neg 11371  df-z 12516  df-uz 12780

This theorem is referenced by:  uzneg  12799  uztric  12803  uzwo3  12884  fzn  13485  fzsplit2  13494  fznn  13537  uzsplit  13541  elfz2nn0  13563  fzouzsplit  13640  faclbnd  14243  bcval5  14271  fz1isolem  14414  seqcoll  14417  rexuzre  15306  caurcvg  15630  caucvg  15632  summolem2a  15668  fsum0diaglem  15729  climcnds  15807  mertenslem1  15840  ntrivcvgmullem  15857  prodmolem2a  15890  ruclem10  16197  eulerthlem2  16743  pcpremul  16805  pcdvdsb  16831  pcadd  16851  pcfac  16861  pcbc  16862  prmunb  16876  prmreclem5  16882  vdwnnlem3  16959  lt6abl  19861  ovolunlem1a  25473  mbflimsup  25643  plyco0  26167  plyeq0lem  26185  aannenlem1  26305  aaliou3lem2  26320  aaliou3lem8  26322  chtublem  27188  bcmax  27255  bpos1lem  27259  bposlem1  27261  axlowdimlem16  29040  fzsplit3  32881  cycpmco2lem7  33208  ballotlem2  34649  ballotlemimin  34666  breprexplemc  34792  elfzm12  35873  poimirlem3  37958  poimirlem4  37959  poimirlem28  37983  mblfinlem2  37993  incsequz  38083  incsequz2  38084  aks4d1p1  42529  primrootspoweq0  42559  aks6d1c2  42583  sticksstones12a  42610  sticksstones12  42611  aks6d1c6lem3  42625  nacsfix  43158  ellz1  43213  eluzrabdioph  43252  monotuz  43387  expdiophlem1  43467  nznngen  44761  fzisoeu  45751  fmul01  46028  climsuselem1  46055  climsuse  46056  iblspltprt  46419  itgspltprt  46425  wallispilem5  46515  stirlinglem8  46527  dirkertrigeqlem1  46544  fourierdlem12  46565  ssfz12  47774