---

Step * of Lemma qsum-const

∀[n:ℕ]. ∀[q:ℚ].  (Σ0 ≤ i < n. q = (n * q) ∈ ℚ)
BY
{ InductionOnNat }

1
.....basecase..... 
1. n : ℤ
⊢ ∀[q:ℚ]. (Σ0 ≤ i < 0. q = (0 * q) ∈ ℚ)

2
.....upcase..... 
1. n : ℤ
2. 0 < n
3. ∀[q:ℚ]. (Σ0 ≤ i < n - 1. q = ((n - 1) * q) ∈ ℚ)
⊢ ∀[q:ℚ]. (Σ0 ≤ i < n. q = (n * q) ∈ ℚ)

---

Latex:

---

Latex:
\mforall{}[n:\mBbbN{}].  \mforall{}[q:\mBbbQ{}].    (\mSigma{}0  \mleq{}  i  <  n.  q  =  (n  *  q))


By

---

Latex:
InductionOnNat

---

Home Index