---

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


1. x : ℝ
2. i : ℕ@i
3. v : ℝ@i
4. v1 : ℝ@i
⊢ (r0 < v1) ⇒ (r0 < v) ⇒ ((x * x) ≤ (v1/v)) ⇒ ((x^2 * (i + 1)/v1) ≤ (x^2 * i/v))
BY
{ (Auto THEN (Assert v ≠ r0 BY (OrRight THEN Auto)) THEN (Assert v1 ≠ r0 BY (OrRight THEN Auto)) THEN Auto)⋅ }

1
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)

---

Latex:

---

Latex:

1.  x  :  \mBbbR{}
2.  i  :  \mBbbN{}@i
3.  v  :  \mBbbR{}@i
4.  v1  :  \mBbbR{}@i
\mvdash{}  (r0  <  v1)  {}\mRightarrow{}  (r0  <  v)  {}\mRightarrow{}  ((x  *  x)  \mleq{}  (v1/v))  {}\mRightarrow{}  ((x\^{}2  *  (i  +  1)/v1)  \mleq{}  (x\^{}2  *  i/v))


By

---

Latex:
(Auto
  THEN  (Assert  v  \mneq{}  r0  BY
                          (OrRight  THEN  Auto))
  THEN  (Assert  v1  \mneq{}  r0  BY
                          (OrRight  THEN  Auto))
  THEN  Auto)\mcdot{}

---

Home Index