---

Step * 1 2 1 of Lemma sparse-signed-rep-exists


1. [n] : ℕ
2. m : ℤ
3. |m| ≤ n
4. ¬(m = 0 ∈ ℤ)
5. 0 < n
6. ∀m@0:ℤ
     ∃L:{-1..2-} List [((m@0 = Σi<||L||.L[i]*2^i ∈ ℤ)
                      ∧ (0 < ||L|| ⇒ (¬(last(L) = 0 ∈ ℤ)))
                      ∧ (∀i:ℕ||L|| - 1. ((L[i] = 0 ∈ ℤ) ∨ (L[i + 1] = 0 ∈ ℤ))))] 
     supposing |m@0| ≤ (n - 1)
⊢ ∃L:{-1..2-} List [((m = Σi<||L||.L[i]*2^i ∈ ℤ)
                   ∧ (0 < ||L|| ⇒ (¬(last(L) = 0 ∈ ℤ)))
                   ∧ (∀i:ℕ||L|| - 1. ((L[i] = 0 ∈ ℤ) ∨ (L[i + 1] = 0 ∈ ℤ))))]
BY
{ ((Evaluate ⌜p
              = special-mod4-decomp(m)
              ∈ {p:ℤ × {-2..3-}| let k,b = p in (m = ((4 * k) + b) ∈ ℤ) ∧ ((|b| = 2 ∈ ℤ) ⇒ (↑isEven(k)))} ⌝ ⋅
    THENA Auto
    )
   THEN Thin (-1)
   THEN D -1
   THEN D -2
   THEN RenameVar `k' (-3)
   THEN RenameVar `r' (-2)
   THEN Reduce (-1)
   THEN (InstHyp [⌜k⌝] (-4)⋅ THENA Auto)) }

1
1. n : ℕ
2. m : ℤ
3. |m| ≤ n
4. ¬(m = 0 ∈ ℤ)
5. 0 < n
6. ∀m@0:ℤ
     ∃L:{-1..2-} List [((m@0 = Σi<||L||.L[i]*2^i ∈ ℤ)
                      ∧ (0 < ||L|| ⇒ (¬(last(L) = 0 ∈ ℤ)))
                      ∧ (∀i:ℕ||L|| - 1. ((L[i] = 0 ∈ ℤ) ∨ (L[i + 1] = 0 ∈ ℤ))))] 
     supposing |m@0| ≤ (n - 1)
7. k : ℤ
8. r : {-2..3-}
9. m = ((4 * k) + r) ∈ ℤ
10. (|r| = 2 ∈ ℤ) ⇒ (↑isEven(k))
⊢ |k| ≤ (n - 1)

2
1. [n] : ℕ
2. m : ℤ
3. |m| ≤ n
4. ¬(m = 0 ∈ ℤ)
5. 0 < n
6. ∀m@0:ℤ
     ∃L:{-1..2-} List [((m@0 = Σi<||L||.L[i]*2^i ∈ ℤ)
                      ∧ (0 < ||L|| ⇒ (¬(last(L) = 0 ∈ ℤ)))
                      ∧ (∀i:ℕ||L|| - 1. ((L[i] = 0 ∈ ℤ) ∨ (L[i + 1] = 0 ∈ ℤ))))] 
     supposing |m@0| ≤ (n - 1)
7. k : ℤ
8. r : {-2..3-}
9. [%7] : (m = ((4 * k) + r) ∈ ℤ) ∧ ((|r| = 2 ∈ ℤ) ⇒ (↑isEven(k)))
10. ∃L:{-1..2-} List [((k = Σi<||L||.L[i]*2^i ∈ ℤ)
                     ∧ (0 < ||L|| ⇒ (¬(last(L) = 0 ∈ ℤ)))
                     ∧ (∀i:ℕ||L|| - 1. ((L[i] = 0 ∈ ℤ) ∨ (L[i + 1] = 0 ∈ ℤ))))]
⊢ ∃L:{-1..2-} List [((m = Σi<||L||.L[i]*2^i ∈ ℤ)
                   ∧ (0 < ||L|| ⇒ (¬(last(L) = 0 ∈ ℤ)))
                   ∧ (∀i:ℕ||L|| - 1. ((L[i] = 0 ∈ ℤ) ∨ (L[i + 1] = 0 ∈ ℤ))))]

---

Latex:

---

Latex:

1.  [n]  :  \mBbbN{}
2.  m  :  \mBbbZ{}
3.  |m|  \mleq{}  n
4.  \mneg{}(m  =  0)
5.  0  <  n
6.  \mforall{}m@0:\mBbbZ{}
          \mexists{}L:\{-1..2\msupminus{}\}  List  [((m@0  =  \mSigma{}i<||L||.L[i]*2\^{}i)
                                            \mwedge{}  (0  <  ||L||  {}\mRightarrow{}  (\mneg{}(last(L)  =  0)))
                                            \mwedge{}  (\mforall{}i:\mBbbN{}||L||  -  1.  ((L[i]  =  0)  \mvee{}  (L[i  +  1]  =  0))))] 
          supposing  |m@0|  \mleq{}  (n  -  1)
\mvdash{}  \mexists{}L:\{-1..2\msupminus{}\}  List  [((m  =  \mSigma{}i<||L||.L[i]*2\^{}i)
                                      \mwedge{}  (0  <  ||L||  {}\mRightarrow{}  (\mneg{}(last(L)  =  0)))
                                      \mwedge{}  (\mforall{}i:\mBbbN{}||L||  -  1.  ((L[i]  =  0)  \mvee{}  (L[i  +  1]  =  0))))]


By

---

Latex:
((Evaluate  \mkleeneopen{}p  =  special-mod4-decomp(m)\mkleeneclose{}  \mcdot{}  THENA  Auto)
  THEN  Thin  (-1)
  THEN  D  -1
  THEN  D  -2
  THEN  RenameVar  `k'  (-3)
  THEN  RenameVar  `r'  (-2)
  THEN  Reduce  (-1)
  THEN  (InstHyp  [\mkleeneopen{}k\mkleeneclose{}]  (-4)\mcdot{}  THENA  Auto))

---

Home Index