---

Step * of Lemma divisibility-by-2-rule

∀n:ℕ+. ∀a:ℕn ⟶ ℤ.  (2 | Σi<n.a[i]*10^i ⇐⇒ 2 | a[0])
BY
{ TACTIC:((UnivCD THENA Auto) THEN Assert ⌜Σi<n.a[i]*10^i ≡ 0 mod 2 ⇐⇒ a[0] ≡ 0 mod 2⌝⋅) }

1
.....assertion..... 
1. n : ℕ+
2. a : ℕn ⟶ ℤ
⊢ Σi<n.a[i]*10^i ≡ 0 mod 2 ⇐⇒ a[0] ≡ 0 mod 2

2
1. n : ℕ+
2. a : ℕn ⟶ ℤ
3. Σi<n.a[i]*10^i ≡ 0 mod 2 ⇐⇒ a[0] ≡ 0 mod 2
⊢ 2 | Σi<n.a[i]*10^i ⇐⇒ 2 | a[0]

---

Latex:

---

Latex:
\mforall{}n:\mBbbN{}\msupplus{}.  \mforall{}a:\mBbbN{}n  {}\mrightarrow{}  \mBbbZ{}.    (2  |  \mSigma{}i<n.a[i]*10\^{}i  \mLeftarrow{}{}\mRightarrow{}  2  |  a[0])


By

---

Latex:
TACTIC:((UnivCD  THENA  Auto)  THEN  Assert  \mkleeneopen{}\mSigma{}i<n.a[i]*10\^{}i  \mequiv{}  0  mod  2  \mLeftarrow{}{}\mRightarrow{}  a[0]  \mequiv{}  0  mod  2\mkleeneclose{}\mcdot{})

---

Home Index