---

Step * of Lemma divisibility-by-9-rule

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

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

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

---

Latex:

---

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


By

---

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

---

Home Index