Theorem elfzd 13572

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   ∧ w3a 1103   ∈ wcel 2145   class class class wbr 5103  (class class class)co 7414   ≤ cle 11271  ℤcz 12618  ...cfz 13564

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-10 2178  ax-11 2194  ax-12 2213  ax-ext 2732  ax-sep 5251  ax-nul 5263  ax-pr 5398  ax-un 7737  ax-cnex 11183  ax-resscn 11184

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3or 1104  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-nf 1817  df-sb 2100  df-mo 2564  df-eu 2594  df-clab 2739  df-cleq 2752  df-clel 2835  df-nfc 2909  df-ne 2956  df-ral 3077  df-rex 3087  df-rab 3413  df-v 3452  df-sbc 3740  df-csb 3848  df-dif 3902  df-un 3904  df-in 3906  df-ss 3916  df-nul 4280  df-if 4483  df-pw 4559  df-sn 4585  df-pr 4587  df-op 4591  df-uni 4868  df-iun 4953  df-br 5104  df-opab 5168  df-mpt 5187  df-id 5550  df-xp 5661  df-rel 5662  df-cnv 5663  df-co 5664  df-dm 5665  df-rn 5666  df-res 5667  df-ima 5668  df-iota 6489  df-fun 6535  df-fn 6536  df-f 6537  df-fv 6541  df-ov 7417  df-oprab 7418  df-mpo 7419  df-1st 7987  df-2nd 7988  df-neg 11471  df-z 12619  df-fz 13565

This theorem is used by:  ssfzunsnext  13627  fzoun  13755  seqf1olem1  14108  bcval5  14385  hashdvds  16869  prmreclem5  17015  chnpolfz  18724  basellem3  27322  bcmono  27516  lgseisenlem1  27614  lgsquadlem1  27619  wwlksnextproplem2  30381  pfxlsw2ccat  33395  wrdt2ind  33398  gsumwrd2dccatlem  33520  cyc3conja  33600  selvply1rhmlemb  34032  rtelextdg2  34240  submateqlem1  34320  oddpwdc  34868  ballotlemsdom  35026  ballotlemsel1i  35027  ballotlemsima  35030  ballotlemfrcn0  35044  fsum2dsub  35118  circlemeth  35151  itg2addnclem2  38424  fzsplitnr  42852  lcmineqlem18  42915  aks4d1p5  42949  aks4d1p8  42956  aks4d1p9  42957  aks6d1c1  42985  aks6d1c5lem1  43005  2np3bcnp1  43013  sticksstones6  43020  sticksstones7  43021  sticksstones10  43024  sticksstones12a  43026  sticksstones12  43027  sticksstones22  43037  aks6d1c6lem4  43042  bcled  43047  bcle2d  43048  grpods  43063  unitscyglem2  43065  unitscyglem4  43067  fzsplit1nn0  43602  irrapxlem3  43668  jm2.23  43840  binomcxplemnn0  45176  monoords  46133  uzfissfz  46159  iuneqfzuzlem  46167  ssuzfz  46182  uzublem  46261  fmul01  46413  fmuldfeq  46416  fmul01lt1lem1  46417  fmul01lt1lem2  46418  mccllem  46430  sumnnodd  46463  limsupubuzlem  46543  dvnmul  46774  dvnprodlem1  46777  dvnprodlem2  46778  iblspltprt  46804  itgspltprt  46810  stoweidlem3  46834  stoweidlem20  46851  stoweidlem26  46857  stoweidlem34  46865  stoweidlem51  46882  fourierdlem11  46949  fourierdlem12  46950  fourierdlem14  46952  fourierdlem15  46953  fourierdlem41  46979  fourierdlem48  46985  fourierdlem49  46986  fourierdlem50  46987  fourierdlem79  47016  fourierdlem92  47029  fourierdlem93  47030  elaa2lem  47064  etransclem3  47068  etransclem7  47072  etransclem27  47092  etransclem28  47093  etransclem35  47100  etransclem38  47103  etransclem44  47109  iundjiun  47291  caratheodorylem1  47357  gpgedgvtx1  48981  veronesev1lem  50809  veronesev2lem  50810  veronesev3lem  50811  veronesev4lem  50812  veronesev5lem  50813  veronesev6lem  50814