---

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


1. L : {-1..2-} List
2. [n] : ℕ
3. m : ℤ
4. |m| ≤ n
5. ¬(m = 0 ∈ ℤ)
6. 0 < n
7. ∀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)
8. k : ℤ
9. r : {-2..3-}
10. [%7] : (m = ((4 * k) + r) ∈ ℤ) ∧ ((|r| = 2 ∈ ℤ) ⇒ (↑isEven(k)))
11. [%9] : (k = Σi<||L||.L[i]*2^i ∈ ℤ)
∧ (0 < ||L|| ⇒ (¬(last(L) = 0 ∈ ℤ)))
∧ (∀i:ℕ||L|| - 1. ((L[i] = 0 ∈ ℤ) ∨ (L[i + 1] = 0 ∈ ℤ)))
12. L1 : {-1..2-} List
13. [%10] : (r = Σi<||L1||.L1[i]*2^i ∈ ℤ) ∧ (||L1|| = 2 ∈ ℤ) ∧ (∀i:ℕ||L1|| - 1. ((L1[i] = 0 ∈ ℤ) ∨ (L1[i + 1] = 0 ∈ ℤ)))
14. ¬(L1[1] = 0 ∈ ℤ)
⊢ ∃L:{-1..2-} List [((r = Σi<||L||.L[i]*2^i ∈ ℤ)
                   ∧ (0 < ||L|| ⇒ (¬(last(L) = 0 ∈ ℤ)))
                   ∧ (∀i:ℕ||L|| - 1. ((L[i] = 0 ∈ ℤ) ∨ (L[i + 1] = 0 ∈ ℤ))))]
BY
{ TACTIC:(With ⌜L1⌝ (D 0)⋅ THEN Auto) }

1
1. L : {-1..2-} List
2. n : ℕ
3. m : ℤ
4. |m| ≤ n
5. ¬(m = 0 ∈ ℤ)
6. 0 < n
7. ∀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)
8. k : ℤ
9. r : {-2..3-}
10. m = ((4 * k) + r) ∈ ℤ
11. (|r| = 2 ∈ ℤ) ⇒ (↑isEven(k))
12. k = Σi<||L||.L[i]*2^i ∈ ℤ
13. 0 < ||L|| ⇒ (¬(last(L) = 0 ∈ ℤ))
14. ∀i:ℕ||L|| - 1. ((L[i] = 0 ∈ ℤ) ∨ (L[i + 1] = 0 ∈ ℤ))
15. L1 : {-1..2-} List
16. r = Σi<||L1||.L1[i]*2^i ∈ ℤ
17. ||L1|| = 2 ∈ ℤ
18. ∀i:ℕ||L1|| - 1. ((L1[i] = 0 ∈ ℤ) ∨ (L1[i + 1] = 0 ∈ ℤ))
19. ¬(L1[1] = 0 ∈ ℤ)
20. r = Σi<||L1||.L1[i]*2^i ∈ ℤ
21. 0 < ||L1||
⊢ ¬(last(L1) = 0 ∈ ℤ)

---

Latex:

---

Latex:

1.  L  :  \{-1..2\msupminus{}\}  List
2.  [n]  :  \mBbbN{}
3.  m  :  \mBbbZ{}
4.  |m|  \mleq{}  n
5.  \mneg{}(m  =  0)
6.  0  <  n
7.  \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)
8.  k  :  \mBbbZ{}
9.  r  :  \{-2..3\msupminus{}\}
10.  [\%7]  :  (m  =  ((4  *  k)  +  r))  \mwedge{}  ((|r|  =  2)  {}\mRightarrow{}  (\muparrow{}isEven(k)))
11.  [\%9]  :  (k  =  \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)))
12.  L1  :  \{-1..2\msupminus{}\}  List
13.  [\%10]  :  (r  =  \mSigma{}i<||L1||.L1[i]*2\^{}i)
\mwedge{}  (||L1||  =  2)
\mwedge{}  (\mforall{}i:\mBbbN{}||L1||  -  1.  ((L1[i]  =  0)  \mvee{}  (L1[i  +  1]  =  0)))
14.  \mneg{}(L1[1]  =  0)
\mvdash{}  \mexists{}L:\{-1..2\msupminus{}\}  List  [((r  =  \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:
TACTIC:(With  \mkleeneopen{}L1\mkleeneclose{}  (D  0)\mcdot{}  THEN  Auto)

---

Home Index