Theorem elfzd 13687

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   ∧ w3a 1103   ∈ wcel 2147   class class class wbr 5108  (class class class)co 7451   ≤ cle 11383  ℤcz 12733  ...cfz 13679

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-10 2180  ax-11 2197  ax-12 2216  ax-ext 2735  ax-sep 5255  ax-nul 5266  ax-pr 5398  ax-un 7783  ax-cnex 11295  ax-resscn 11296

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3or 1104  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-nf 1817  df-sb 2102  df-mo 2567  df-eu 2597  df-clab 2742  df-cleq 2755  df-clel 2839  df-nfc 2913  df-ne 2960  df-ral 3081  df-rex 3091  df-rab 3417  df-v 3456  df-sbc 3743  df-csb 3852  df-ss 3901  df-dif 4050  df-in 4094  df-un 4154  df-nul 4282  df-if 4486  df-pw 4562  df-sn 4589  df-pr 4591  df-op 4841  df-uni 4873  df-iun 4958  df-br 5109  df-opab 5174  df-mpt 5193  df-id 5553  df-xp 5664  df-rel 5665  df-cnv 5666  df-co 5667  df-dm 5668  df-rn 5669  df-res 5670  df-ima 5671  df-iota 6520  df-fun 6568  df-fn 6569  df-f 6570  df-fv 6574  df-ov 7454  df-oprab 7455  df-mpo 7456  df-1st 8035  df-2nd 8036  df-neg 11583  df-z 12734  df-fz 13680

This theorem is used by:  ssfzunsnext  13743  fzoun  13871  seqf1olem1  14224  bcval5  14503  hashdvds  16996  prmreclem5  17142  chnpolfz  18857  basellem3  27467  bcmono  27661  lgseisenlem1  27759  lgsquadlem1  27764  wwlksnextproplem2  30556  pfxlsw2ccat  33609  wrdt2ind  33612  gsumwrd2dccatlem  33737  cyc3conja  33817  selvply1rhmlemb  34262  rtelextdg2  34470  submateqlem1  34550  oddpwdc  35097  ballotlemsdom  35255  ballotlemsel1i  35256  ballotlemsima  35259  ballotlemfrcn0  35273  fsum2dsub  35347  circlemeth  35380  itg2addnclem2  38858  fzsplitnr  43299  lcmineqlem18  43362  aks4d1p5  43396  aks4d1p8  43403  aks4d1p9  43404  aks6d1c1  43432  aks6d1c5lem1  43452  2np3bcnp1  43460  sticksstones6  43467  sticksstones7  43468  sticksstones10  43471  sticksstones12a  43473  sticksstones12  43474  sticksstones22  43484  aks6d1c6lem4  43489  bcled  43494  bcle2d  43495  grpods  43510  unitscyglem2  43512  unitscyglem4  43514  fzsplit1nn0  44031  irrapxlem3  44097  jm2.23  44269  binomcxplemnn0  45594  monoords  46586  uzfissfz  46611  iuneqfzuzlem  46619  ssuzfz  46634  uzublem  46713  fmul01  46865  fmuldfeq  46868  fmul01lt1lem1  46869  fmul01lt1lem2  46870  mccllem  46882  sumnnodd  46915  limsupubuzlem  46995  dvnmul  47226  dvnprodlem1  47229  dvnprodlem2  47230  iblspltprt  47256  itgspltprt  47262  stoweidlem3  47286  stoweidlem20  47303  stoweidlem26  47309  stoweidlem34  47317  stoweidlem51  47334  fourierdlem11  47401  fourierdlem12  47402  fourierdlem14  47404  fourierdlem15  47405  fourierdlem41  47431  fourierdlem48  47437  fourierdlem49  47438  fourierdlem50  47439  fourierdlem79  47468  fourierdlem92  47481  fourierdlem93  47482  elaa2lem  47516  etransclem3  47520  etransclem7  47524  etransclem27  47544  etransclem28  47545  etransclem35  47552  etransclem38  47555  etransclem44  47561  iundjiun  47743  caratheodorylem1  47809  gpgedgvtx1  49433  veronesev1lem  51401  veronesev2lem  51402  veronesev3lem  51403  veronesev4lem  51404  veronesev5lem  51405  veronesev6lem  51406