---

Step * of Lemma small-sparse-rep

∀r:{-2..3-}
  (∃L:{-1..2-} List [((r = Σi<||L||.L[i]*2^i ∈ ℤ)
                    ∧ (||L|| = 2 ∈ ℤ)
                    ∧ (∀i:ℕ||L|| - 1. ((L[i] = 0 ∈ ℤ) ∨ (L[i + 1] = 0 ∈ ℤ))))])
BY
{ TACTIC:((D 0 THENA Auto) THEN IntSegCases (-1)) }

1
1. r : ℤ
2. r = (-2) ∈ ℤ
⊢ ∃L:{-1..2-} List [(((-2) = Σi<||L||.L[i]*2^i ∈ ℤ)
                   ∧ (||L|| = 2 ∈ ℤ)
                   ∧ (∀i:ℕ||L|| - 1. ((L[i] = 0 ∈ ℤ) ∨ (L[i + 1] = 0 ∈ ℤ))))]

2
1. r : ℤ
2. r = (-1) ∈ ℤ
⊢ ∃L:{-1..2-} List [(((-1) = Σi<||L||.L[i]*2^i ∈ ℤ)
                   ∧ (||L|| = 2 ∈ ℤ)
                   ∧ (∀i:ℕ||L|| - 1. ((L[i] = 0 ∈ ℤ) ∨ (L[i + 1] = 0 ∈ ℤ))))]

3
1. r : ℤ
2. r = 0 ∈ ℤ
⊢ ∃L:{-1..2-} List [((0 = Σi<||L||.L[i]*2^i ∈ ℤ)
                   ∧ (||L|| = 2 ∈ ℤ)
                   ∧ (∀i:ℕ||L|| - 1. ((L[i] = 0 ∈ ℤ) ∨ (L[i + 1] = 0 ∈ ℤ))))]

4
1. r : ℤ
2. r = 1 ∈ ℤ
⊢ ∃L:{-1..2-} List [((1 = Σi<||L||.L[i]*2^i ∈ ℤ)
                   ∧ (||L|| = 2 ∈ ℤ)
                   ∧ (∀i:ℕ||L|| - 1. ((L[i] = 0 ∈ ℤ) ∨ (L[i + 1] = 0 ∈ ℤ))))]

5
1. r : ℤ
2. r = 2 ∈ ℤ
⊢ ∃L:{-1..2-} List [((2 = Σi<||L||.L[i]*2^i ∈ ℤ)
                   ∧ (||L|| = 2 ∈ ℤ)
                   ∧ (∀i:ℕ||L|| - 1. ((L[i] = 0 ∈ ℤ) ∨ (L[i + 1] = 0 ∈ ℤ))))]

---

Latex:

---

Latex:
\mforall{}r:\{-2..3\msupminus{}\}
    (\mexists{}L:\{-1..2\msupminus{}\}  List  [((r  =  \mSigma{}i<||L||.L[i]*2\^{}i)
                                        \mwedge{}  (||L||  =  2)
                                        \mwedge{}  (\mforall{}i:\mBbbN{}||L||  -  1.  ((L[i]  =  0)  \mvee{}  (L[i  +  1]  =  0))))])


By

---

Latex:
TACTIC:((D  0  THENA  Auto)  THEN  IntSegCases  (-1))

---

Home Index