Theorem elfzd 13657

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   ∧ w3a 1103   ∈ wcel 2146   class class class wbr 5105  (class class class)co 7427   ≤ cle 11354  ℤcz 12703  ...cfz 13649

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1944  ax-6 2001  ax-7 2042  ax-8 2148  ax-9 2156  ax-10 2179  ax-11 2196  ax-12 2215  ax-ext 2735  ax-sep 5251  ax-nul 5262  ax-pr 5394  ax-un 7758  ax-cnex 11266  ax-resscn 11267

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3or 1104  df-3an 1105  df-tru 1572  df-fal 1582  df-ex 1812  df-nf 1816  df-sb 2101  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 3416  df-v 3455  df-sbc 3742  df-csb 3851  df-ss 3900  df-dif 4049  df-in 4093  df-un 4153  df-nul 4281  df-if 4485  df-pw 4561  df-sn 4588  df-pr 4590  df-op 4838  df-uni 4870  df-iun 4955  df-br 5106  df-opab 5170  df-mpt 5189  df-id 5549  df-xp 5660  df-rel 5661  df-cnv 5662  df-co 5663  df-dm 5664  df-rn 5665  df-res 5666  df-ima 5667  df-iota 6500  df-fun 6548  df-fn 6549  df-f 6550  df-fv 6554  df-ov 7430  df-oprab 7431  df-mpo 7432  df-1st 8008  df-2nd 8009  df-neg 11554  df-z 12704  df-fz 13650

This theorem is used by:  ssfzunsnext  13713  fzoun  13841  seqf1olem1  14194  bcval5  14472  hashdvds  16964  prmreclem5  17110  chnpolfz  18819  basellem3  27422  bcmono  27616  lgseisenlem1  27714  lgsquadlem1  27719  wwlksnextproplem2  30511  pfxlsw2ccat  33566  wrdt2ind  33569  gsumwrd2dccatlem  33691  cyc3conja  33771  selvply1rhmlemb  34204  rtelextdg2  34412  submateqlem1  34492  oddpwdc  35039  ballotlemsdom  35197  ballotlemsel1i  35198  ballotlemsima  35201  ballotlemfrcn0  35215  fsum2dsub  35289  circlemeth  35322  itg2addnclem2  38730  fzsplitnr  43173  lcmineqlem18  43236  aks4d1p5  43270  aks4d1p8  43277  aks4d1p9  43278  aks6d1c1  43306  aks6d1c5lem1  43326  2np3bcnp1  43334  sticksstones6  43341  sticksstones7  43342  sticksstones10  43345  sticksstones12a  43347  sticksstones12  43348  sticksstones22  43358  aks6d1c6lem4  43363  bcled  43368  bcle2d  43369  grpods  43384  unitscyglem2  43386  unitscyglem4  43388  fzsplit1nn0  43905  irrapxlem3  43971  jm2.23  44143  binomcxplemnn0  45473  monoords  46452  uzfissfz  46477  iuneqfzuzlem  46485  ssuzfz  46500  uzublem  46579  fmul01  46731  fmuldfeq  46734  fmul01lt1lem1  46735  fmul01lt1lem2  46736  mccllem  46748  sumnnodd  46781  limsupubuzlem  46861  dvnmul  47092  dvnprodlem1  47095  dvnprodlem2  47096  iblspltprt  47122  itgspltprt  47128  stoweidlem3  47152  stoweidlem20  47169  stoweidlem26  47175  stoweidlem34  47183  stoweidlem51  47200  fourierdlem11  47267  fourierdlem12  47268  fourierdlem14  47270  fourierdlem15  47271  fourierdlem41  47297  fourierdlem48  47303  fourierdlem49  47304  fourierdlem50  47305  fourierdlem79  47334  fourierdlem92  47347  fourierdlem93  47348  elaa2lem  47382  etransclem3  47386  etransclem7  47390  etransclem27  47410  etransclem28  47411  etransclem35  47418  etransclem38  47421  etransclem44  47427  iundjiun  47609  caratheodorylem1  47675  gpgedgvtx1  49299  veronesev1lem  51187  veronesev2lem  51188  veronesev3lem  51189  veronesev4lem  51190  veronesev5lem  51191  veronesev6lem  51192