---

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


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)
BY
{ ((RWO "sum_unroll_base_q" 0 THENA Auto) THEN Reduce 0) }

1
1. B : ℚ@i
2. n : ℕ@i
3. 0 ≤ B@i
4. n = 0 ∈ ℤ
⊢ (B * 0) ≤ (2 * B)

---

Latex:



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


By

((RWO  "sum\_unroll\_base\_q"  0  THENA  Auto)  THEN  Reduce  0)

---

Home Index