---

Step * 1 2 1 2 1 1 of Lemma slln-lemma2


∀B:ℚ. ∀n:ℕ.  ((0 ≤ B) ⇒ (Σ0 ≤ i < n. B * if (i =z 0) then 0 else (1/i * i) fi  ≤ (2 * B)))
BY
{ (((Auto THEN RWO "prod_sum_l_q<" 0) THENA Auto) THEN CaseNat 0 `n') }

1
1. B : ℚ@i
2. n : ℕ@i
3. 0 ≤ B@i
4. n = 0 ∈ ℤ
⊢ (B * Σ0 ≤ i < 0. if (i =z 0) then 0 else (1/i * i) fi ) ≤ (2 * B)

2
1. B : ℚ@i
2. n : ℕ@i
3. 0 ≤ B@i
4. ¬(n = 0 ∈ ℤ)
⊢ (B * Σ0 ≤ i < n. if (i =z 0) then 0 else (1/i * i) fi ) ≤ (2 * B)

---

Latex:



\mforall{}B:\mBbbQ{}.  \mforall{}n:\mBbbN{}.    ((0  \mleq{}  B)  {}\mRightarrow{}  (\mSigma{}0  \mleq{}  i  <  n.  B  *  if  (i  =\msubz{}  0)  then  0  else  (1/i  *  i)  fi    \mleq{}  (2  *  B)))


By

(((Auto  THEN  RWO  "prod\_sum\_l\_q<"  0)  THENA  Auto)  THEN  CaseNat  0  `n')

---

Home Index