---

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


1. B : ℚ
2. n : ℕ
3. 0 ≤ B
4. ¬(n = 0 ∈ ℤ)
5. Σ1 ≤ i < n. if (i =z 0) then 0 else (1/i * i) fi  < 2
⊢ (B * (0 + Σ1 ≤ i < n. if (i =z 0) then 0 else (1/i * i) fi )) ≤ (2 * B)
BY
{ xxx(Decide B = 0 ∈ ℚ THENA Auto)xxx }

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

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

---

Latex:

---

Latex:

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


By

---

Latex:
xxx(Decide  B  =  0  THENA  Auto)xxx

---

Home Index