MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  elfz Structured version   Visualization version   GIF version

Theorem elfz 12893
Description: Membership in a finite set of sequential integers. (Contributed by NM, 29-Sep-2005.)
Assertion
Ref Expression
elfz ((𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝐾 ∈ (𝑀...𝑁) ↔ (𝑀𝐾𝐾𝑁)))

Proof of Theorem elfz
StepHypRef Expression
1 elfz1 12892 . . . 4 ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝐾 ∈ (𝑀...𝑁) ↔ (𝐾 ∈ ℤ ∧ 𝑀𝐾𝐾𝑁)))
2 3anass 1089 . . . . 5 ((𝐾 ∈ ℤ ∧ 𝑀𝐾𝐾𝑁) ↔ (𝐾 ∈ ℤ ∧ (𝑀𝐾𝐾𝑁)))
32baib 536 . . . 4 (𝐾 ∈ ℤ → ((𝐾 ∈ ℤ ∧ 𝑀𝐾𝐾𝑁) ↔ (𝑀𝐾𝐾𝑁)))
41, 3sylan9bb 510 . . 3 (((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ 𝐾 ∈ ℤ) → (𝐾 ∈ (𝑀...𝑁) ↔ (𝑀𝐾𝐾𝑁)))
543impa 1104 . 2 ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐾 ∈ ℤ) → (𝐾 ∈ (𝑀...𝑁) ↔ (𝑀𝐾𝐾𝑁)))
653comr 1119 1 ((𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝐾 ∈ (𝑀...𝑁) ↔ (𝑀𝐾𝐾𝑁)))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 207  wa 396  w3a 1081  wcel 2107   class class class wbr 5063  (class class class)co 7150  cle 10670  cz 11975  ...cfz 12887
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1904  ax-6 1963  ax-7 2008  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2153  ax-12 2169  ax-ext 2798  ax-sep 5200  ax-nul 5207  ax-pr 5326  ax-cnex 10587  ax-resscn 10588
This theorem depends on definitions:  df-bi 208  df-an 397  df-or 844  df-3or 1082  df-3an 1083  df-tru 1533  df-ex 1774  df-nf 1778  df-sb 2063  df-mo 2620  df-eu 2652  df-clab 2805  df-cleq 2819  df-clel 2898  df-nfc 2968  df-ral 3148  df-rex 3149  df-rab 3152  df-v 3502  df-sbc 3777  df-dif 3943  df-un 3945  df-in 3947  df-ss 3956  df-nul 4296  df-if 4471  df-sn 4565  df-pr 4567  df-op 4571  df-uni 4838  df-br 5064  df-opab 5126  df-id 5459  df-xp 5560  df-rel 5561  df-cnv 5562  df-co 5563  df-dm 5564  df-iota 6313  df-fun 6356  df-fv 6362  df-ov 7153  df-oprab 7154  df-mpo 7155  df-neg 10867  df-z 11976  df-fz 12888
This theorem is referenced by:  elfz5  12895  fzadd2  12937  fznatpl1  12956  fzrev  12965  fzctr  13014  elfzo  13035  seqf1olem1  13404  bcval5  13673  pfxccat3a  14095  isprm3  16022  hashdvds  16107  eulerthlem2  16114  prmreclem5  16251  aannenlem1  24851  basellem3  25593  chtub  25721  bcmono  25786  bposlem1  25793  lgseisenlem1  25884  lgsquadlem1  25889  2lgslem1a  25900  axlowdimlem3  26663  axlowdimlem7  26667  axlowdimlem16  26676  axlowdimlem17  26677  axlowdim  26680  submateqlem1  30977  lmatfvlem  30985  bcneg1  32871  poimirlem15  34793  poimirlem24  34802  poimirlem28  34806  mblfinlem2  34816  itg2addnclem2  34830  fzmul  34903  cntotbnd  34961  fzsplit1nn0  39235  irrapxlem3  39305  pellexlem5  39314  acongrep  39461  fzneg  39463  jm2.23  39477  fmul01  41745  fmuldfeq  41748  stoweidlem26  42196  fourierdlem11  42288  fourierdlem12  42289  fourierdlem15  42292  fourierdlem79  42355  smfmullem4  42954
  Copyright terms: Public domain W3C validator