Theorem elfzd 13538

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 524	. 2 ⊢ (𝜑 → ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐾 ∈ ℤ) ∧ (𝑀 ≤ 𝐾 ∧ 𝐾 ≤ 𝑁)))
8		elfz2 13537	. 2 ⊢ (𝐾 ∈ (𝑀...𝑁) ↔ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐾 ∈ ℤ) ∧ (𝑀 ≤ 𝐾 ∧ 𝐾 ≤ 𝑁)))
9	7, 8	sylibr 237	1 ⊢ (𝜑 → 𝐾 ∈ (𝑀...𝑁))

Syntax hints:   → wi 4   ∧ wa 400   ∧ w3a 1103   ∈ wcel 2143   class class class wbr 5109  (class class class)co 7410   ≤ cle 11239  ℤcz 12586  ...cfz 13530

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-10 2176  ax-11 2192  ax-12 2213  ax-ext 2735  ax-sep 5257  ax-nul 5269  ax-pr 5404  ax-un 7732  ax-cnex 11151  ax-resscn 11152

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3or 1104  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1810  df-nf 1814  df-sb 2097  df-mo 2567  df-eu 2597  df-clab 2742  df-cleq 2755  df-clel 2838  df-nfc 2912  df-ne 2959  df-ral 3080  df-rex 3090  df-rab 3417  df-v 3457  df-sbc 3745  df-csb 3854  df-dif 3908  df-un 3910  df-in 3912  df-ss 3922  df-nul 4287  df-if 4488  df-pw 4564  df-sn 4590  df-pr 4592  df-op 4596  df-uni 4873  df-iun 4958  df-br 5110  df-opab 5174  df-mpt 5193  df-id 5556  df-xp 5667  df-rel 5668  df-cnv 5669  df-co 5670  df-dm 5671  df-rn 5672  df-res 5673  df-ima 5674  df-iota 6492  df-fun 6538  df-fn 6539  df-f 6540  df-fv 6544  df-ov 7413  df-oprab 7414  df-mpo 7415  df-1st 7982  df-2nd 7983  df-neg 11439  df-z 12587  df-fz 13531

This theorem is referenced by:  ssfzunsnext  13593  fzoun  13721  seqf1olem1  14073  bcval5  14350  hashdvds  16829  prmreclem5  16975  chnpolfz  18684  basellem3  27247  bcmono  27441  lgseisenlem1  27539  lgsquadlem1  27544  wwlksnextproplem2  30259  pfxlsw2ccat  33270  wrdt2ind  33273  gsumwrd2dccatlem  33397  cyc3conja  33477  selvply1rhmlemb  33909  rtelextdg2  34117  submateqlem1  34197  oddpwdc  34744  ballotlemsdom  34902  ballotlemsel1i  34903  ballotlemsima  34906  ballotlemfrcn0  34920  fsum2dsub  34994  circlemeth  35027  itg2addnclem2  38343  fzsplitnr  42770  lcmineqlem18  42833  aks4d1p5  42867  aks4d1p8  42874  aks4d1p9  42875  aks6d1c1  42903  aks6d1c5lem1  42923  2np3bcnp1  42931  sticksstones6  42938  sticksstones7  42939  sticksstones10  42942  sticksstones12a  42944  sticksstones12  42945  sticksstones22  42955  aks6d1c6lem4  42960  bcled  42965  bcle2d  42966  grpods  42981  unitscyglem2  42983  unitscyglem4  42985  fzsplit1nn0  43505  irrapxlem3  43571  jm2.23  43743  binomcxplemnn0  45079  monoords  46036  uzfissfz  46062  iuneqfzuzlem  46070  ssuzfz  46085  uzublem  46164  fmul01  46316  fmuldfeq  46319  fmul01lt1lem1  46320  fmul01lt1lem2  46321  mccllem  46333  sumnnodd  46366  limsupubuzlem  46446  dvnmul  46677  dvnprodlem1  46680  dvnprodlem2  46681  iblspltprt  46707  itgspltprt  46713  stoweidlem3  46737  stoweidlem20  46754  stoweidlem26  46760  stoweidlem34  46768  stoweidlem51  46785  fourierdlem11  46852  fourierdlem12  46853  fourierdlem14  46855  fourierdlem15  46856  fourierdlem41  46882  fourierdlem48  46888  fourierdlem49  46889  fourierdlem50  46890  fourierdlem79  46919  fourierdlem92  46932  fourierdlem93  46933  elaa2lem  46967  etransclem3  46971  etransclem7  46975  etransclem27  46995  etransclem28  46996  etransclem35  47003  etransclem38  47006  etransclem44  47012  iundjiun  47194  caratheodorylem1  47260  gpgedgvtx1  48847