---

Step * of Lemma divisibility-by-5-rule

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

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

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

---

Latex:

---

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


By

---

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

---

Home Index