---

Step * 7 of Lemma eu-eq_dist-axiomsA


1. g : EuclideanPlane
2. a : Point
3. b : Point
4. c : Point
5. d : Point
6. e : Point
7. f : Point
8. x : Point
9. y : Point
10. D(a;b;c;d;e;f)
11. ¬D(x;y;y;y;e;f)
⊢ D(a;b;c;d;x;y)
BY
{ (((Unfold `dist` -2 THEN Unfold `dist` 0) THEN ExRepD)
   THEN (InstLemma `not-dist-lemma` [⌜g⌝;⌜x⌝;⌜y⌝;⌜e⌝;⌜f⌝]⋅ THENA Auto)
   THEN (Assert ef ≥ xy BY
               (InstLemma `geo-not-gt-to-ge` [⌜g⌝;⌜x⌝;⌜y⌝;⌜e⌝;⌜f⌝]⋅ THEN Auto))) }

1
1. g : EuclideanPlane
2. a : Point
3. b : Point
4. c : Point
5. d : Point
6. e : Point
7. f : Point
8. x : Point
9. y : Point
10. a' : Point
11. b' : Point
12. c' : Point
13. u : {u:Point| c' # u} 
14. B(a'b'c')
15. B(a'uc')
16. ab ≅ a'b'
17. cd ≅ b'c'
18. ef ≅ a'u
19. ¬D(x;y;y;y;e;f)
20. ¬xy > ef
21. ef ≥ xy
⊢ ∃a',b',c':Point. ∃u:{u:Point| c' # u} . (B(a'b'c') ∧ B(a'uc') ∧ ab ≅ a'b' ∧ cd ≅ b'c' ∧ xy ≅ a'u)

---

Latex:

---

Latex:

1.  g  :  EuclideanPlane
2.  a  :  Point
3.  b  :  Point
4.  c  :  Point
5.  d  :  Point
6.  e  :  Point
7.  f  :  Point
8.  x  :  Point
9.  y  :  Point
10.  D(a;b;c;d;e;f)
11.  \mneg{}D(x;y;y;y;e;f)
\mvdash{}  D(a;b;c;d;x;y)


By

---

Latex:
(((Unfold  `dist`  -2  THEN  Unfold  `dist`  0)  THEN  ExRepD)
  THEN  (InstLemma  `not-dist-lemma`  [\mkleeneopen{}g\mkleeneclose{};\mkleeneopen{}x\mkleeneclose{};\mkleeneopen{}y\mkleeneclose{};\mkleeneopen{}e\mkleeneclose{};\mkleeneopen{}f\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  (Assert  ef  \mgeq{}  xy  BY
                          (InstLemma  `geo-not-gt-to-ge`  [\mkleeneopen{}g\mkleeneclose{};\mkleeneopen{}x\mkleeneclose{};\mkleeneopen{}y\mkleeneclose{};\mkleeneopen{}e\mkleeneclose{};\mkleeneopen{}f\mkleeneclose{}]\mcdot{}  THEN  Auto)))

---

Home Index