---

Step * 1 1 1 1 2 1 1 1 of Lemma sine-exists


1. x : ℝ
2. i : ℕ@i
3. v : ℝ@i
4. v1 : ℝ@i
5. r0 < v1
6. r0 < v
7. (x * x) ≤ (v1/v)
8. v ≠ r0
9. v1 ≠ r0
⊢ (x^2 * (i + 1)/v1) ≤ (x^2 * i/v)
BY
{ (nRMul ⌜v⌝ (-3)⋅ THEN (nRMul ⌜v⌝ 0⋅ THEN nRMul ⌜v1⌝ 0⋅)⋅)⋅ }

1
1. x : ℝ
2. i : ℕ@i
3. v : ℝ@i
4. v1 : ℝ@i
5. r0 < v1
6. r0 < v
7. (v * x * x) ≤ v1
8. v ≠ r0
9. v1 ≠ r0
⊢ (x^2 * (i + 1) * v) ≤ (x^2 * i * v1)

---

Latex:

---

Latex:

1.  x  :  \mBbbR{}
2.  i  :  \mBbbN{}@i
3.  v  :  \mBbbR{}@i
4.  v1  :  \mBbbR{}@i
5.  r0  <  v1
6.  r0  <  v
7.  (x  *  x)  \mleq{}  (v1/v)
8.  v  \mneq{}  r0
9.  v1  \mneq{}  r0
\mvdash{}  (x\^{}2  *  (i  +  1)/v1)  \mleq{}  (x\^{}2  *  i/v)


By

---

Latex:
(nRMul  \mkleeneopen{}v\mkleeneclose{}  (-3)\mcdot{}  THEN  (nRMul  \mkleeneopen{}v\mkleeneclose{}  0\mcdot{}  THEN  nRMul  \mkleeneopen{}v1\mkleeneclose{}  0\mcdot{})\mcdot{})\mcdot{}

---

Home Index