---

Step * 1 2 1 1 of Lemma divisibility-by-2-rule

.....equality..... 
1. n : ℕ+
2. a : ℕn ⟶ ℤ
3. 10 ≡ 0 mod 2
⊢ Σ(a[i] * 0^i | i < n) = a[0] ∈ ℤ
BY
{ ((InstLemma `isolate_summand` [⌜n⌝;⌜λ2i.a[i] * 0^i⌝;⌜0⌝]⋅ THENA Auto)⋅
   THEN RWO "-1" 0
   THEN Auto
   THEN Reduce 0
   THEN Thin (-1)) }

1
1. n : ℕ+
2. a : ℕn ⟶ ℤ
3. 10 ≡ 0 mod 2
⊢ ((a[0] * 1) + Σ(if (i =z 0) then 0 else a[i] * 0^i fi  | i < n)) = a[0] ∈ ℤ

---

Latex:

---

Latex:
.....equality..... 
1.  n  :  \mBbbN{}\msupplus{}
2.  a  :  \mBbbN{}n  {}\mrightarrow{}  \mBbbZ{}
3.  10  \mequiv{}  0  mod  2
\mvdash{}  \mSigma{}(a[i]  *  0\^{}i  |  i  <  n)  =  a[0]


By

---

Latex:
((InstLemma  `isolate\_summand`  [\mkleeneopen{}n\mkleeneclose{};\mkleeneopen{}\mlambda{}\msubtwo{}i.a[i]  *  0\^{}i\mkleeneclose{};\mkleeneopen{}0\mkleeneclose{}]\mcdot{}  THENA  Auto)\mcdot{}
  THEN  RWO  "-1"  0
  THEN  Auto
  THEN  Reduce  0
  THEN  Thin  (-1))

---

Home Index