Theorem elfzd 13543

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

Syntax hints:   → wi 4   ∧ wa 400   ∧ w3a 1101   ∈ wcel 2149   class class class wbr 5113  (class class class)co 7411   ≤ cle 11244  ℤcz 12591  ...cfz 13535

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-8 2151  ax-9 2159  ax-10 2182  ax-11 2198  ax-12 2219  ax-ext 2741  ax-sep 5261  ax-nul 5271  ax-pr 5405  ax-un 7733  ax-cnex 11156  ax-resscn 11157

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3or 1102  df-3an 1103  df-tru 1570  df-fal 1580  df-ex 1807  df-nf 1811  df-sb 2098  df-mo 2573  df-eu 2603  df-clab 2748  df-cleq 2761  df-clel 2844  df-nfc 2918  df-ne 2965  df-ral 3086  df-rex 3096  df-rab 3424  df-v 3465  df-sbc 3754  df-csb 3862  df-dif 3916  df-un 3918  df-in 3920  df-ss 3930  df-nul 4295  df-if 4493  df-pw 4569  df-sn 4595  df-pr 4597  df-op 4601  df-uni 4877  df-iun 4962  df-br 5114  df-opab 5178  df-mpt 5197  df-id 5557  df-xp 5668  df-rel 5669  df-cnv 5670  df-co 5671  df-dm 5672  df-rn 5673  df-res 5674  df-ima 5675  df-iota 6493  df-fun 6539  df-fn 6540  df-f 6541  df-fv 6545  df-ov 7414  df-oprab 7415  df-mpo 7416  df-1st 7986  df-2nd 7987  df-neg 11444  df-z 12592  df-fz 13536

This theorem is referenced by:  ssfzunsnext  13597  fzoun  13725  seqf1olem1  14077  bcval5  14354  hashdvds  16834  prmreclem5  16980  chnpolfz  18689  basellem3  27213  bcmono  27407  lgseisenlem1  27505  lgsquadlem1  27510  wwlksnextproplem2  30200  pfxlsw2ccat  33211  wrdt2ind  33214  gsumwrd2dccatlem  33338  cyc3conja  33418  selvply1rhmlemb  33854  rtelextdg2  34062  submateqlem1  34142  oddpwdc  34689  ballotlemsdom  34847  ballotlemsel1i  34848  ballotlemsima  34851  ballotlemfrcn0  34865  fsum2dsub  34939  circlemeth  34972  itg2addnclem2  38211  fzsplitnr  42640  lcmineqlem18  42703  aks4d1p5  42737  aks4d1p8  42744  aks4d1p9  42745  aks6d1c1  42773  aks6d1c5lem1  42793  2np3bcnp1  42801  sticksstones6  42808  sticksstones7  42809  sticksstones10  42812  sticksstones12a  42814  sticksstones12  42815  sticksstones22  42825  aks6d1c6lem4  42830  bcled  42835  bcle2d  42836  grpods  42851  unitscyglem2  42853  unitscyglem4  42855  fzsplit1nn0  43377  irrapxlem3  43443  jm2.23  43615  binomcxplemnn0  44951  monoords  45908  uzfissfz  45934  iuneqfzuzlem  45942  ssuzfz  45957  uzublem  46036  fmul01  46188  fmuldfeq  46191  fmul01lt1lem1  46192  fmul01lt1lem2  46193  mccllem  46205  sumnnodd  46238  limsupubuzlem  46318  dvnmul  46549  dvnprodlem1  46552  dvnprodlem2  46553  iblspltprt  46579  itgspltprt  46585  stoweidlem3  46609  stoweidlem20  46626  stoweidlem26  46632  stoweidlem34  46640  stoweidlem51  46657  fourierdlem11  46724  fourierdlem12  46725  fourierdlem14  46727  fourierdlem15  46728  fourierdlem41  46754  fourierdlem48  46760  fourierdlem49  46761  fourierdlem50  46762  fourierdlem79  46791  fourierdlem92  46804  fourierdlem93  46805  elaa2lem  46839  etransclem3  46843  etransclem7  46847  etransclem27  46867  etransclem28  46868  etransclem35  46875  etransclem38  46878  etransclem44  46884  iundjiun  47066  caratheodorylem1  47132  gpgedgvtx1  48716