Theorem elfzd 13463

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

Syntax hints:   → wi 4   ∧ wa 395   ∧ w3a 1087   ∈ wcel 2114   class class class wbr 5086  (class class class)co 7361   ≤ cle 11174  ℤcz 12518  ...cfz 13455

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-10 2147  ax-11 2163  ax-12 2185  ax-ext 2709  ax-sep 5232  ax-nul 5242  ax-pr 5371  ax-un 7683  ax-cnex 11088  ax-resscn 11089

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3or 1088  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-nf 1786  df-sb 2069  df-mo 2540  df-eu 2570  df-clab 2716  df-cleq 2729  df-clel 2812  df-nfc 2886  df-ne 2934  df-ral 3053  df-rex 3063  df-rab 3391  df-v 3432  df-sbc 3730  df-csb 3839  df-dif 3893  df-un 3895  df-in 3897  df-ss 3907  df-nul 4275  df-if 4468  df-pw 4544  df-sn 4569  df-pr 4571  df-op 4575  df-uni 4852  df-iun 4936  df-br 5087  df-opab 5149  df-mpt 5168  df-id 5520  df-xp 5631  df-rel 5632  df-cnv 5633  df-co 5634  df-dm 5635  df-rn 5636  df-res 5637  df-ima 5638  df-iota 6449  df-fun 6495  df-fn 6496  df-f 6497  df-fv 6501  df-ov 7364  df-oprab 7365  df-mpo 7366  df-1st 7936  df-2nd 7937  df-neg 11374  df-z 12519  df-fz 13456

This theorem is referenced by:  ssfzunsnext  13517  fzoun  13645  seqf1olem1  13997  bcval5  14274  hashdvds  16739  prmreclem5  16885  chnpolfz  18593  basellem3  27063  bcmono  27257  lgseisenlem1  27355  lgsquadlem1  27360  wwlksnextproplem2  29996  pfxlsw2ccat  33028  wrdt2ind  33031  gsumwrd2dccatlem  33156  cyc3conja  33236  rtelextdg2  33890  submateqlem1  33970  oddpwdc  34517  ballotlemsdom  34675  ballotlemsel1i  34676  ballotlemsima  34679  ballotlemfrcn0  34693  fsum2dsub  34770  circlemeth  34803  itg2addnclem2  38010  fzsplitnr  42439  lcmineqlem18  42502  aks4d1p5  42536  aks4d1p8  42543  aks4d1p9  42544  aks6d1c1  42572  aks6d1c5lem1  42592  2np3bcnp1  42600  sticksstones6  42607  sticksstones7  42608  sticksstones10  42611  sticksstones12a  42613  sticksstones12  42614  sticksstones22  42624  aks6d1c6lem4  42629  bcled  42634  bcle2d  42635  grpods  42650  unitscyglem2  42652  unitscyglem4  42654  fzsplit1nn0  43203  irrapxlem3  43273  jm2.23  43445  binomcxplemnn0  44797  monoords  45751  uzfissfz  45777  iuneqfzuzlem  45785  ssuzfz  45800  uzublem  45879  fmul01  46031  fmuldfeq  46034  fmul01lt1lem1  46035  fmul01lt1lem2  46036  mccllem  46048  sumnnodd  46081  limsupubuzlem  46161  dvnmul  46392  dvnprodlem1  46395  dvnprodlem2  46396  iblspltprt  46422  itgspltprt  46428  stoweidlem3  46452  stoweidlem20  46469  stoweidlem26  46475  stoweidlem34  46483  stoweidlem51  46500  fourierdlem11  46567  fourierdlem12  46568  fourierdlem14  46570  fourierdlem15  46571  fourierdlem41  46597  fourierdlem48  46603  fourierdlem49  46604  fourierdlem50  46605  fourierdlem79  46634  fourierdlem92  46647  fourierdlem93  46648  elaa2lem  46682  etransclem3  46686  etransclem7  46690  etransclem27  46710  etransclem28  46711  etransclem35  46718  etransclem38  46721  etransclem44  46727  iundjiun  46909  caratheodorylem1  46975  gpgedgvtx1  48553