---

Step * of Lemma divisibility-by-3-rule

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

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

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

---

Latex:

---

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


By

---

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

---

Home Index