Theorem elfzd 13575

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 1128	. . 3 ⊢ (𝜑 → (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐾 ∈ ℤ))
5		elfzd.4	. . 3 ⊢ (𝜑 → 𝑀 ≤ 𝐾)
6		elfzd.5	. . 3 ⊢ (𝜑 → 𝐾 ≤ 𝑁)
7	4, 5, 6	jca32 515	. 2 ⊢ (𝜑 → ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐾 ∈ ℤ) ∧ (𝑀 ≤ 𝐾 ∧ 𝐾 ≤ 𝑁)))
8		elfz2 13574	. 2 ⊢ (𝐾 ∈ (𝑀...𝑁) ↔ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐾 ∈ ℤ) ∧ (𝑀 ≤ 𝐾 ∧ 𝐾 ≤ 𝑁)))
9	7, 8	sylibr 234	1 ⊢ (𝜑 → 𝐾 ∈ (𝑀...𝑁))

Syntax hints:   → wi 4   ∧ wa 395   ∧ w3a 1087   ∈ wcel 2108   class class class wbr 5166  (class class class)co 7448   ≤ cle 11325  ℤcz 12639  ...cfz 13567

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-un 7770  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-sbc 3805  df-csb 3922  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-iun 5017  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-rn 5711  df-res 5712  df-ima 5713  df-iota 6525  df-fun 6575  df-fn 6576  df-f 6577  df-fv 6581  df-ov 7451  df-oprab 7452  df-mpo 7453  df-1st 8030  df-2nd 8031  df-neg 11523  df-z 12640  df-fz 13568

This theorem is referenced by:  ssfzunsnext  13629  fzoun  13753  seqf1olem1  14092  bcval5  14367  hashdvds  16822  prmreclem5  16967  basellem3  27144  bcmono  27339  lgseisenlem1  27437  lgsquadlem1  27442  wwlksnextproplem2  29943  pfxlsw2ccat  32917  wrdt2ind  32920  cyc3conja  33150  rtelextdg2  33718  submateqlem1  33753  oddpwdc  34319  ballotlemsdom  34476  ballotlemsel1i  34477  ballotlemsima  34480  ballotlemfrcn0  34494  fsum2dsub  34584  circlemeth  34617  itg2addnclem2  37632  fzsplitnr  41940  lcmineqlem18  42003  aks4d1p5  42037  aks4d1p8  42044  aks4d1p9  42045  aks6d1c1  42073  aks6d1c5lem1  42093  2np3bcnp1  42101  sticksstones6  42108  sticksstones7  42109  sticksstones10  42112  sticksstones12a  42114  sticksstones12  42115  sticksstones22  42125  aks6d1c6lem4  42130  bcled  42135  bcle2d  42136  grpods  42151  unitscyglem2  42153  unitscyglem4  42155  metakunt1  42162  metakunt2  42163  metakunt5  42166  metakunt10  42171  metakunt15  42176  metakunt16  42177  metakunt21  42182  metakunt22  42183  metakunt24  42185  metakunt26  42187  metakunt28  42189  metakunt29  42190  metakunt30  42191  prodsplit  42197  fzsplit1nn0  42710  irrapxlem3  42780  jm2.23  42953  binomcxplemnn0  44318  monoords  45212  uzfissfz  45241  iuneqfzuzlem  45249  ssuzfz  45264  uzublem  45345  fmul01  45501  fmuldfeq  45504  fmul01lt1lem1  45505  fmul01lt1lem2  45506  mccllem  45518  sumnnodd  45551  limsupubuzlem  45633  dvnmul  45864  dvnprodlem1  45867  dvnprodlem2  45868  iblspltprt  45894  itgspltprt  45900  stoweidlem3  45924  stoweidlem20  45941  stoweidlem26  45947  stoweidlem34  45955  stoweidlem51  45972  fourierdlem11  46039  fourierdlem12  46040  fourierdlem14  46042  fourierdlem15  46043  fourierdlem41  46069  fourierdlem48  46075  fourierdlem49  46076  fourierdlem50  46077  fourierdlem79  46106  fourierdlem92  46119  fourierdlem93  46120  elaa2lem  46154  etransclem3  46158  etransclem7  46162  etransclem27  46182  etransclem28  46183  etransclem35  46190  etransclem38  46193  etransclem44  46199  iundjiun  46381  caratheodorylem1  46447