---

Step * 2 2 1 1 of Lemma rv-tarski-parallel


1. n : ℕ
2. p : ℝ^n
3. t : ℝ
4. s : ℝ
5. i : ℕn
6. v : ℝ
7. v1 : ℝ
8. v2 : ℝ
9. v3 : ℝ
⊢ (r0 < v)
⇒ ((v * (p i)) = ((t * (v2 - s * v1)) + ((r1 - t) * (v3 - s * v1))))
⇒ ((p i) = ((t * (r1/v) * (v2 - s * v1)) + ((r1 - t) * (r1/v) * (v3 - s * v1))))
BY
{ (GenConclTerms Auto [⌜v2 - s * v1⌝;⌜v3 - s * v1⌝;⌜r1 - t⌝]⋅ THEN Auto) }

1
1. n : ℕ
2. p : ℝ^n
3. t : ℝ
4. s : ℝ
5. i : ℕn
6. v : ℝ
7. v1 : ℝ
8. v2 : ℝ
9. v3 : ℝ
10. v4 : ℝ
11. (v2 - s * v1) = v4 ∈ ℝ
12. v5 : ℝ
13. (v3 - s * v1) = v5 ∈ ℝ
14. v6 : ℝ
15. (r1 - t) = v6 ∈ ℝ
16. r0 < v
17. (v * (p i)) = ((t * v4) + (v6 * v5))
⊢ (p i) = ((t * (r1/v) * v4) + (v6 * (r1/v) * v5))

---

Latex:

---

Latex:

1.  n  :  \mBbbN{}
2.  p  :  \mBbbR{}\^{}n
3.  t  :  \mBbbR{}
4.  s  :  \mBbbR{}
5.  i  :  \mBbbN{}n
6.  v  :  \mBbbR{}
7.  v1  :  \mBbbR{}
8.  v2  :  \mBbbR{}
9.  v3  :  \mBbbR{}
\mvdash{}  (r0  <  v)
{}\mRightarrow{}  ((v  *  (p  i))  =  ((t  *  (v2  -  s  *  v1))  +  ((r1  -  t)  *  (v3  -  s  *  v1))))
{}\mRightarrow{}  ((p  i)  =  ((t  *  (r1/v)  *  (v2  -  s  *  v1))  +  ((r1  -  t)  *  (r1/v)  *  (v3  -  s  *  v1))))


By

---

Latex:
(GenConclTerms  Auto  [\mkleeneopen{}v2  -  s  *  v1\mkleeneclose{};\mkleeneopen{}v3  -  s  *  v1\mkleeneclose{};\mkleeneopen{}r1  -  t\mkleeneclose{}]\mcdot{}  THEN  Auto)

---

Home Index