---

Step * 1 1 1 1 1 2 1 1 1 1 1 1 1 1 3 1 1 1 1 1 of Lemma Rolles-theorem


1. k : ℕ+
2. v : ℝ
3. v1 : ℝ
4. z : {z:ℝ| r0 < z} 
5. |v| ≤ ((r1/r(2 * k)) * z)
6. (v1 + v) = r0
7. (((r1/r(k)) * z) ≤ v1) ∨ (v1 ≤ ((r(-1)/r(k)) * z))
⊢ False
BY
{ (Assert v = -(v1) BY
         (nRAdd ⌜v1⌝ 0⋅ THEN Auto)) }

1
1. k : ℕ+
2. v : ℝ
3. v1 : ℝ
4. z : {z:ℝ| r0 < z} 
5. |v| ≤ ((r1/r(2 * k)) * z)
6. (v1 + v) = r0
7. (((r1/r(k)) * z) ≤ v1) ∨ (v1 ≤ ((r(-1)/r(k)) * z))
8. v = -(v1)
⊢ False

---

Latex:

---

Latex:

1.  k  :  \mBbbN{}\msupplus{}
2.  v  :  \mBbbR{}
3.  v1  :  \mBbbR{}
4.  z  :  \{z:\mBbbR{}|  r0  <  z\} 
5.  |v|  \mleq{}  ((r1/r(2  *  k))  *  z)
6.  (v1  +  v)  =  r0
7.  (((r1/r(k))  *  z)  \mleq{}  v1)  \mvee{}  (v1  \mleq{}  ((r(-1)/r(k))  *  z))
\mvdash{}  False


By

---

Latex:
(Assert  v  =  -(v1)  BY
              (nRAdd  \mkleeneopen{}v1\mkleeneclose{}  0\mcdot{}  THEN  Auto))

---

Home Index