Step
*
of Lemma
rv-tarski-parallel
∀n:ℕ. ∀a,b,c:ℝ^n. (a ≠ b
⇒ a ≠ c
⇒ (∀d,p:ℝ^n. (b-d-c
⇒ a-d-p
⇒ (∃x,y:ℝ^n. (a-b-x ∧ x-p-y ∧ a-c-y)))))
BY
{ (Auto
THEN D -2
THEN D -3
THEN D -1
THEN D -2
THEN ExRepD
THEN All
Reduce⋅
THEN RenameVar `s' (-4)
THEN (Assert r0 < (r1 - s) BY
(nRAdd ⌜s⌝ 0⋅ THEN Auto))
THEN InstConcl [⌜(r1/r1 - s)*b - s*a⌝;⌜(r1/r1 - s)*c - s*a⌝]⋅
THEN Auto) }
1
1. n : ℕ
2. a : ℝ^n
3. b : ℝ^n
4. c : ℝ^n
5. a ≠ b
6. a ≠ c
7. d : ℝ^n
8. p : ℝ^n
9. t : ℝ
10. r0 < t
11. t < r1
12. req-vec(n;d;t*b + r1 - t*c)
13. b ≠ c
14. s : ℝ
15. r0 < s
16. s < r1
17. req-vec(n;d;s*a + r1 - s*p)
18. a ≠ p
19. r0 < (r1 - s)
⊢ a-b-(r1/r1 - s)*b - s*a
2
1. n : ℕ
2. a : ℝ^n
3. b : ℝ^n
4. c : ℝ^n
5. a ≠ b
6. a ≠ c
7. d : ℝ^n
8. p : ℝ^n
9. t : ℝ
10. r0 < t
11. t < r1
12. req-vec(n;d;t*b + r1 - t*c)
13. b ≠ c
14. s : ℝ
15. r0 < s
16. s < r1
17. req-vec(n;d;s*a + r1 - s*p)
18. a ≠ p
19. r0 < (r1 - s)
20. a-b-(r1/r1 - s)*b - s*a
⊢ (r1/r1 - s)*b - s*a-p-(r1/r1 - s)*c - s*a
3
1. n : ℕ
2. a : ℝ^n
3. b : ℝ^n
4. c : ℝ^n
5. a ≠ b
6. a ≠ c
7. d : ℝ^n
8. p : ℝ^n
9. t : ℝ
10. r0 < t
11. t < r1
12. req-vec(n;d;t*b + r1 - t*c)
13. b ≠ c
14. s : ℝ
15. r0 < s
16. s < r1
17. req-vec(n;d;s*a + r1 - s*p)
18. a ≠ p
19. r0 < (r1 - s)
20. a-b-(r1/r1 - s)*b - s*a
21. (r1/r1 - s)*b - s*a-p-(r1/r1 - s)*c - s*a
⊢ a-c-(r1/r1 - s)*c - s*a
Latex:
Latex:
\mforall{}n:\mBbbN{}. \mforall{}a,b,c:\mBbbR{}\^{}n.
(a \mneq{} b {}\mRightarrow{} a \mneq{} c {}\mRightarrow{} (\mforall{}d,p:\mBbbR{}\^{}n. (b-d-c {}\mRightarrow{} a-d-p {}\mRightarrow{} (\mexists{}x,y:\mBbbR{}\^{}n. (a-b-x \mwedge{} x-p-y \mwedge{} a-c-y)))))
By
Latex:
(Auto
THEN D -2
THEN D -3
THEN D -1
THEN D -2
THEN ExRepD
THEN All
Reduce\mcdot{}
THEN RenameVar `s' (-4)
THEN (Assert r0 < (r1 - s) BY
(nRAdd \mkleeneopen{}s\mkleeneclose{} 0\mcdot{} THEN Auto))
THEN InstConcl [\mkleeneopen{}(r1/r1 - s)*b - s*a\mkleeneclose{};\mkleeneopen{}(r1/r1 - s)*c - s*a\mkleeneclose{}]\mcdot{}
THEN Auto)
Home
Index