Theorem elfzd 13552

Description: Membership in a finite set of sequential integers. (Contributed by Glauco Siliprandi, 23-Oct-2021.)

Hypotheses

Ref	Expression
elfzd.1	⊢ (𝜑 → 𝑀 ∈ ℤ)
elfzd.2	⊢ (𝜑 → 𝑁 ∈ ℤ)
elfzd.3	⊢ (𝜑 → 𝐾 ∈ ℤ)
elfzd.4	⊢ (𝜑 → 𝑀 ≤ 𝐾)
elfzd.5	⊢ (𝜑 → 𝐾 ≤ 𝑁)

Assertion

Ref	Expression
elfzd	⊢ (𝜑 → 𝐾 ∈ (𝑀...𝑁))

Proof of Theorem elfzd

Step	Hyp	Ref	Expression
1		elfzd.1	. . . 4 ⊢ (𝜑 → 𝑀 ∈ ℤ)
2		elfzd.2	. . . 4 ⊢ (𝜑 → 𝑁 ∈ ℤ)
3		elfzd.3	. . . 4 ⊢ (𝜑 → 𝐾 ∈ ℤ)
4	1, 2, 3	3jca 1127	. . 3 ⊢ (𝜑 → (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐾 ∈ ℤ))
5		elfzd.4	. . 3 ⊢ (𝜑 → 𝑀 ≤ 𝐾)
6		elfzd.5	. . 3 ⊢ (𝜑 → 𝐾 ≤ 𝑁)
7	4, 5, 6	jca32 515	. 2 ⊢ (𝜑 → ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐾 ∈ ℤ) ∧ (𝑀 ≤ 𝐾 ∧ 𝐾 ≤ 𝑁)))
8		elfz2 13551	. 2 ⊢ (𝐾 ∈ (𝑀...𝑁) ↔ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐾 ∈ ℤ) ∧ (𝑀 ≤ 𝐾 ∧ 𝐾 ≤ 𝑁)))
9	7, 8	sylibr 234	1 ⊢ (𝜑 → 𝐾 ∈ (𝑀...𝑁))

Syntax hints:   → wi 4   ∧ wa 395   ∧ w3a 1086   ∈ wcel 2106   class class class wbr 5148  (class class class)co 7431   ≤ cle 11294  ℤcz 12611  ...cfz 13544

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1908  ax-6 1965  ax-7 2005  ax-8 2108  ax-9 2116  ax-10 2139  ax-11 2155  ax-12 2175  ax-ext 2706  ax-sep 5302  ax-nul 5312  ax-pr 5438  ax-un 7754  ax-cnex 11209  ax-resscn 11210

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1540  df-fal 1550  df-ex 1777  df-nf 1781  df-sb 2063  df-mo 2538  df-eu 2567  df-clab 2713  df-cleq 2727  df-clel 2814  df-nfc 2890  df-ral 3060  df-rex 3069  df-rab 3434  df-v 3480  df-sbc 3792  df-csb 3909  df-dif 3966  df-un 3968  df-in 3970  df-ss 3980  df-nul 4340  df-if 4532  df-pw 4607  df-sn 4632  df-pr 4634  df-op 4638  df-uni 4913  df-iun 4998  df-br 5149  df-opab 5211  df-mpt 5232  df-id 5583  df-xp 5695  df-rel 5696  df-cnv 5697  df-co 5698  df-dm 5699  df-rn 5700  df-res 5701  df-ima 5702  df-iota 6516  df-fun 6565  df-fn 6566  df-f 6567  df-fv 6571  df-ov 7434  df-oprab 7435  df-mpo 7436  df-1st 8013  df-2nd 8014  df-neg 11493  df-z 12612  df-fz 13545

This theorem is referenced by:  ssfzunsnext  13606  fzoun  13733  seqf1olem1  14079  bcval5  14354  hashdvds  16809  prmreclem5  16954  basellem3  27141  bcmono  27336  lgseisenlem1  27434  lgsquadlem1  27439  wwlksnextproplem2  29940  pfxlsw2ccat  32920  wrdt2ind  32923  gsumwrd2dccatlem  33052  cyc3conja  33160  rtelextdg2  33733  submateqlem1  33768  oddpwdc  34336  ballotlemsdom  34493  ballotlemsel1i  34494  ballotlemsima  34497  ballotlemfrcn0  34511  fsum2dsub  34601  circlemeth  34634  itg2addnclem2  37659  fzsplitnr  41965  lcmineqlem18  42028  aks4d1p5  42062  aks4d1p8  42069  aks4d1p9  42070  aks6d1c1  42098  aks6d1c5lem1  42118  2np3bcnp1  42126  sticksstones6  42133  sticksstones7  42134  sticksstones10  42137  sticksstones12a  42139  sticksstones12  42140  sticksstones22  42150  aks6d1c6lem4  42155  bcled  42160  bcle2d  42161  grpods  42176  unitscyglem2  42178  unitscyglem4  42180  metakunt1  42187  metakunt2  42188  metakunt5  42191  metakunt10  42196  metakunt15  42201  metakunt16  42202  metakunt21  42207  metakunt22  42208  metakunt24  42210  metakunt26  42212  metakunt28  42214  metakunt29  42215  metakunt30  42216  prodsplit  42222  fzsplit1nn0  42742  irrapxlem3  42812  jm2.23  42985  binomcxplemnn0  44345  monoords  45248  uzfissfz  45276  iuneqfzuzlem  45284  ssuzfz  45299  uzublem  45380  fmul01  45536  fmuldfeq  45539  fmul01lt1lem1  45540  fmul01lt1lem2  45541  mccllem  45553  sumnnodd  45586  limsupubuzlem  45668  dvnmul  45899  dvnprodlem1  45902  dvnprodlem2  45903  iblspltprt  45929  itgspltprt  45935  stoweidlem3  45959  stoweidlem20  45976  stoweidlem26  45982  stoweidlem34  45990  stoweidlem51  46007  fourierdlem11  46074  fourierdlem12  46075  fourierdlem14  46077  fourierdlem15  46078  fourierdlem41  46104  fourierdlem48  46110  fourierdlem49  46111  fourierdlem50  46112  fourierdlem79  46141  fourierdlem92  46154  fourierdlem93  46155  elaa2lem  46189  etransclem3  46193  etransclem7  46197  etransclem27  46217  etransclem28  46218  etransclem35  46225  etransclem38  46228  etransclem44  46234  iundjiun  46416  caratheodorylem1  46482  gpgedgvtx1  47955