Theorem elfzd 13452

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

Syntax hints:   → wi 4   ∧ wa 395   ∧ w3a 1086   ∈ wcel 2109   class class class wbr 5102  (class class class)co 7369   ≤ cle 11185  ℤcz 12505  ...cfz 13444

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-10 2142  ax-11 2158  ax-12 2178  ax-ext 2701  ax-sep 5246  ax-nul 5256  ax-pr 5382  ax-un 7691  ax-cnex 11100  ax-resscn 11101

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2533  df-eu 2562  df-clab 2708  df-cleq 2721  df-clel 2803  df-nfc 2878  df-ral 3045  df-rex 3054  df-rab 3403  df-v 3446  df-sbc 3751  df-csb 3860  df-dif 3914  df-un 3916  df-in 3918  df-ss 3928  df-nul 4293  df-if 4485  df-pw 4561  df-sn 4586  df-pr 4588  df-op 4592  df-uni 4868  df-iun 4953  df-br 5103  df-opab 5165  df-mpt 5184  df-id 5526  df-xp 5637  df-rel 5638  df-cnv 5639  df-co 5640  df-dm 5641  df-rn 5642  df-res 5643  df-ima 5644  df-iota 6452  df-fun 6501  df-fn 6502  df-f 6503  df-fv 6507  df-ov 7372  df-oprab 7373  df-mpo 7374  df-1st 7947  df-2nd 7948  df-neg 11384  df-z 12506  df-fz 13445

This theorem is referenced by:  ssfzunsnext  13506  fzoun  13633  seqf1olem1  13982  bcval5  14259  hashdvds  16721  prmreclem5  16867  basellem3  26969  bcmono  27164  lgseisenlem1  27262  lgsquadlem1  27267  wwlksnextproplem2  29813  pfxlsw2ccat  32845  wrdt2ind  32848  gsumwrd2dccatlem  32979  cyc3conja  33087  rtelextdg2  33690  submateqlem1  33770  oddpwdc  34318  ballotlemsdom  34476  ballotlemsel1i  34477  ballotlemsima  34480  ballotlemfrcn0  34494  fsum2dsub  34571  circlemeth  34604  itg2addnclem2  37639  fzsplitnr  41944  lcmineqlem18  42007  aks4d1p5  42041  aks4d1p8  42048  aks4d1p9  42049  aks6d1c1  42077  aks6d1c5lem1  42097  2np3bcnp1  42105  sticksstones6  42112  sticksstones7  42113  sticksstones10  42116  sticksstones12a  42118  sticksstones12  42119  sticksstones22  42129  aks6d1c6lem4  42134  bcled  42139  bcle2d  42140  grpods  42155  unitscyglem2  42157  unitscyglem4  42159  fzsplit1nn0  42715  irrapxlem3  42785  jm2.23  42958  binomcxplemnn0  44311  monoords  45268  uzfissfz  45295  iuneqfzuzlem  45303  ssuzfz  45318  uzublem  45399  fmul01  45551  fmuldfeq  45554  fmul01lt1lem1  45555  fmul01lt1lem2  45556  mccllem  45568  sumnnodd  45601  limsupubuzlem  45683  dvnmul  45914  dvnprodlem1  45917  dvnprodlem2  45918  iblspltprt  45944  itgspltprt  45950  stoweidlem3  45974  stoweidlem20  45991  stoweidlem26  45997  stoweidlem34  46005  stoweidlem51  46022  fourierdlem11  46089  fourierdlem12  46090  fourierdlem14  46092  fourierdlem15  46093  fourierdlem41  46119  fourierdlem48  46125  fourierdlem49  46126  fourierdlem50  46127  fourierdlem79  46156  fourierdlem92  46169  fourierdlem93  46170  elaa2lem  46204  etransclem3  46208  etransclem7  46212  etransclem27  46232  etransclem28  46233  etransclem35  46240  etransclem38  46243  etransclem44  46249  iundjiun  46431  caratheodorylem1  46497  gpgedgvtx1  48026