---

Step * 2 1 1 1 1 of Lemma rv-circle-circle


1. n : {2...}
2. a : ℝ^n
3. b : ℝ^n
4. c : ℝ^n
5. d : ℝ^n
6. p : ℝ^n
7. ab=ap
8. q : ℝ^n
9. cd=cq
10. x : ℝ^n
11. cp=cx
12. y : ℝ^n
13. aq=ay
14. ¬(a ≠ y ∧ y ≠ b ∧ (¬a-y-b))
15. a ≠ c
16. u : ℝ^n
17. ab=au
18. cd=cu
19. v : ℝ^n
20. ab=av
21. cd=cv
22. x ≠ d
23. y ≠ b
24. d(a;y) < d(a;b)
25. x ≠ c
26. ¬d-x-c
27. c ≠ x
28. x ≠ d
⊢ ¬c-x-d
BY
{ (ParallelOp -3 THEN EAuto 1) }

---

Latex:

---

Latex:

1.  n  :  \{2...\}
2.  a  :  \mBbbR{}\^{}n
3.  b  :  \mBbbR{}\^{}n
4.  c  :  \mBbbR{}\^{}n
5.  d  :  \mBbbR{}\^{}n
6.  p  :  \mBbbR{}\^{}n
7.  ab=ap
8.  q  :  \mBbbR{}\^{}n
9.  cd=cq
10.  x  :  \mBbbR{}\^{}n
11.  cp=cx
12.  y  :  \mBbbR{}\^{}n
13.  aq=ay
14.  \mneg{}(a  \mneq{}  y  \mwedge{}  y  \mneq{}  b  \mwedge{}  (\mneg{}a-y-b))
15.  a  \mneq{}  c
16.  u  :  \mBbbR{}\^{}n
17.  ab=au
18.  cd=cu
19.  v  :  \mBbbR{}\^{}n
20.  ab=av
21.  cd=cv
22.  x  \mneq{}  d
23.  y  \mneq{}  b
24.  d(a;y)  <  d(a;b)
25.  x  \mneq{}  c
26.  \mneg{}d-x-c
27.  c  \mneq{}  x
28.  x  \mneq{}  d
\mvdash{}  \mneg{}c-x-d


By

---

Latex:
(ParallelOp  -3  THEN  EAuto  1)

---

Home Index