Theorem elfzd 13520

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

Syntax hints:   → wi 4   ∧ wa 399   ∧ w3a 1098   ∈ wcel 2142   class class class wbr 5100  (class class class)co 7396   ≤ cle 11217  ℤcz 12568  ...cfz 13512

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1815  ax-4 1829  ax-5 1930  ax-6 1987  ax-7 2028  ax-8 2144  ax-9 2152  ax-10 2175  ax-11 2191  ax-12 2212  ax-ext 2734  ax-sep 5246  ax-nul 5256  ax-pr 5390  ax-un 7718  ax-cnex 11129  ax-resscn 11130

This theorem depends on definitions:  df-bi 209  df-an 400  df-or 859  df-3or 1099  df-3an 1100  df-tru 1563  df-fal 1573  df-ex 1800  df-nf 1804  df-sb 2091  df-mo 2566  df-eu 2596  df-clab 2741  df-cleq 2754  df-clel 2837  df-nfc 2911  df-ne 2958  df-ral 3077  df-rex 3087  df-rab 3415  df-v 3456  df-sbc 3745  df-csb 3853  df-dif 3907  df-un 3909  df-in 3911  df-ss 3921  df-nul 4286  df-if 4481  df-pw 4557  df-sn 4583  df-pr 4585  df-op 4589  df-uni 4866  df-iun 4951  df-br 5101  df-opab 5163  df-mpt 5182  df-id 5542  df-xp 5653  df-rel 5654  df-cnv 5655  df-co 5656  df-dm 5657  df-rn 5658  df-res 5659  df-ima 5660  df-iota 6477  df-fun 6523  df-fn 6524  df-f 6525  df-fv 6529  df-ov 7399  df-oprab 7400  df-mpo 7401  df-1st 7970  df-2nd 7971  df-neg 11417  df-z 12569  df-fz 13513

This theorem is referenced by:  ssfzunsnext  13574  fzoun  13702  seqf1olem1  14054  bcval5  14331  hashdvds  16810  prmreclem5  16956  chnpolfz  18665  basellem3  27147  bcmono  27341  lgseisenlem1  27439  lgsquadlem1  27444  wwlksnextproplem2  30110  pfxlsw2ccat  33128  wrdt2ind  33131  gsumwrd2dccatlem  33257  cyc3conja  33337  selvply1rhmlemb  33816  rtelextdg2  34024  submateqlem1  34104  oddpwdc  34651  ballotlemsdom  34809  ballotlemsel1i  34810  ballotlemsima  34813  ballotlemfrcn0  34827  fsum2dsub  34901  circlemeth  34934  itg2addnclem2  38171  fzsplitnr  42600  lcmineqlem18  42663  aks4d1p5  42697  aks4d1p8  42704  aks4d1p9  42705  aks6d1c1  42733  aks6d1c5lem1  42753  2np3bcnp1  42761  sticksstones6  42768  sticksstones7  42769  sticksstones10  42772  sticksstones12a  42774  sticksstones12  42775  sticksstones22  42785  aks6d1c6lem4  42790  bcled  42795  bcle2d  42796  grpods  42811  unitscyglem2  42813  unitscyglem4  42815  fzsplit1nn0  43335  irrapxlem3  43401  jm2.23  43573  binomcxplemnn0  44925  monoords  45876  uzfissfz  45902  iuneqfzuzlem  45910  ssuzfz  45925  uzublem  46004  fmul01  46156  fmuldfeq  46159  fmul01lt1lem1  46160  fmul01lt1lem2  46161  mccllem  46173  sumnnodd  46206  limsupubuzlem  46286  dvnmul  46517  dvnprodlem1  46520  dvnprodlem2  46521  iblspltprt  46547  itgspltprt  46553  stoweidlem3  46577  stoweidlem20  46594  stoweidlem26  46600  stoweidlem34  46608  stoweidlem51  46625  fourierdlem11  46692  fourierdlem12  46693  fourierdlem14  46695  fourierdlem15  46696  fourierdlem41  46722  fourierdlem48  46728  fourierdlem49  46729  fourierdlem50  46730  fourierdlem79  46759  fourierdlem92  46772  fourierdlem93  46773  elaa2lem  46807  etransclem3  46811  etransclem7  46815  etransclem27  46835  etransclem28  46836  etransclem35  46843  etransclem38  46846  etransclem44  46852  iundjiun  47034  caratheodorylem1  47100  gpgedgvtx1  48684