---

Step * 1 1 1 of Lemma rv-T'-implies-rv-T


1. n : ℕ+
2. a : ℝ^n
3. b : ℝ^n
4. c : ℝ^n
5. rv-T'(n;a;b;c)
6. a ≠ c
7. k : ℕ+
⊢ ∃s:ℝ. ((s ∈ ((r(-1)/r(k)), (r(k + 1)/r(k)))) ∧ req-vec(n;b;s*a + r1 - s*c))
BY
{ ((D -3 With ⌜(r(k + 1)/r(k))*a + (r(-1)/r(k))*c⌝  THENA Auto)
   THEN (D -1 With ⌜(r(k + 1)/r(k))*c + (r(-1)/r(k))*a⌝  THENA Auto)
   THEN (D -1 THENA (BLemma `rv-between-small-expand` THEN Auto))
   THEN (D -1 THENA ((BLemma `rv-between-symmetry` THENA Auto) THEN BLemma `rv-between-small-expand` THEN EAuto 1))) }

1
1. n : ℕ+
2. a : ℝ^n
3. b : ℝ^n
4. c : ℝ^n
5. a ≠ c
6. k : ℕ+
7. (r(k + 1)/r(k))*a + (r(-1)/r(k))*c-b-(r(k + 1)/r(k))*c + (r(-1)/r(k))*a
⊢ ∃s:ℝ. ((s ∈ ((r(-1)/r(k)), (r(k + 1)/r(k)))) ∧ req-vec(n;b;s*a + r1 - s*c))

---

Latex:

---

Latex:

1.  n  :  \mBbbN{}\msupplus{}
2.  a  :  \mBbbR{}\^{}n
3.  b  :  \mBbbR{}\^{}n
4.  c  :  \mBbbR{}\^{}n
5.  rv-T'(n;a;b;c)
6.  a  \mneq{}  c
7.  k  :  \mBbbN{}\msupplus{}
\mvdash{}  \mexists{}s:\mBbbR{}.  ((s  \mmember{}  ((r(-1)/r(k)),  (r(k  +  1)/r(k))))  \mwedge{}  req-vec(n;b;s*a  +  r1  -  s*c))


By

---

Latex:
((D  -3  With  \mkleeneopen{}(r(k  +  1)/r(k))*a  +  (r(-1)/r(k))*c\mkleeneclose{}    THENA  Auto)
  THEN  (D  -1  With  \mkleeneopen{}(r(k  +  1)/r(k))*c  +  (r(-1)/r(k))*a\mkleeneclose{}    THENA  Auto)
  THEN  (D  -1  THENA  (BLemma  `rv-between-small-expand`  THEN  Auto))
  THEN  (D  -1
              THENA  ((BLemma  `rv-between-symmetry`  THENA  Auto)
                            THEN  BLemma  `rv-between-small-expand`
                            THEN  EAuto  1)
              ))

---

Home Index