Theorem eluz 12096

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

Syntax hints:   → wi 4   ↔ wb 207   ∧ wa 396   ∈ wcel 2079   class class class wbr 4956  ‘cfv 6217   ≤ cle 10511  ℤcz 11818  ℤ_≥cuz 12082

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1775  ax-4 1789  ax-5 1886  ax-6 1945  ax-7 1990  ax-8 2081  ax-9 2089  ax-10 2110  ax-11 2124  ax-12 2139  ax-13 2342  ax-ext 2767  ax-sep 5088  ax-nul 5095  ax-pr 5214  ax-cnex 10428  ax-resscn 10429

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 843  df-3or 1079  df-3an 1080  df-tru 1523  df-ex 1760  df-nf 1764  df-sb 2041  df-mo 2574  df-eu 2610  df-clab 2774  df-cleq 2786  df-clel 2861  df-nfc 2933  df-ral 3108  df-rex 3109  df-rab 3112  df-v 3434  df-sbc 3702  df-dif 3857  df-un 3859  df-in 3861  df-ss 3869  df-nul 4207  df-if 4376  df-sn 4467  df-pr 4469  df-op 4473  df-uni 4740  df-br 4957  df-opab 5019  df-mpt 5036  df-id 5340  df-xp 5441  df-rel 5442  df-cnv 5443  df-co 5444  df-dm 5445  df-iota 6181  df-fun 6219  df-fv 6225  df-ov 7010  df-neg 10709  df-z 11819  df-uz 12083

This theorem is referenced by:  uzneg  12101  uztric  12104  uzwo3  12181  fzn  12762  fzsplit2  12771  fznn  12814  uzsplit  12818  elfz2nn0  12837  fzouzsplit  12910  faclbnd  13488  bcval5  13516  fz1isolem  13655  seqcoll  13658  rexuzre  14534  caurcvg  14855  caucvg  14857  summolem2a  14893  fsum0diaglem  14952  climcnds  15027  mertenslem1  15061  ntrivcvgmullem  15078  prodmolem2a  15109  ruclem10  15413  eulerthlem2  15936  pcpremul  15997  pcdvdsb  16022  pcadd  16042  pcfac  16052  pcbc  16053  prmunb  16067  prmreclem5  16073  vdwnnlem3  16150  lt6abl  18724  ovolunlem1a  23768  mbflimsup  23938  plyco0  24453  plyeq0lem  24471  aannenlem1  24588  aaliou3lem2  24603  aaliou3lem8  24605  chtublem  25457  bcmax  25524  bpos1lem  25528  bposlem1  25530  axlowdimlem16  26414  fzsplit3  30175  ballotlem2  31319  ballotlemimin  31336  breprexplemc  31476  elfzm12  32471  poimirlem3  34372  poimirlem4  34373  poimirlem28  34397  mblfinlem2  34407  incsequz  34501  incsequz2  34502  nacsfix  38744  ellz1  38799  eluzrabdioph  38839  monotuz  38974  expdiophlem1  39054  nznngen  40138  fzisoeu  41061  fmul01  41357  climsuselem1  41384  climsuse  41385  iblspltprt  41753  itgspltprt  41759  wallispilem5  41850  stirlinglem8  41862  dirkertrigeqlem1  41879  fourierdlem12  41900  ssfz12  42984