Step * 2 1 1 1 of Lemma unique-angles-in-half-plane

.....aux..... 
1. EuclideanPlane
2. c' Point
3. Point
4. Point
5. Point
6. Point
7. Point
8. Point
9. bc
10. leftof yz
11. Point
12. acb ≅a fzy
13. leftof yz  leftof yz
14. leftof zy  leftof zy
15. leftof zy  leftof zy
16. f1 Point
17. f2 Point
18. acb ≅a f1zy
19. acb ≅a f2zy
20. leftof yz  f1 leftof yz
21. leftof zy  f1 leftof zy
22. leftof zy  f1 leftof zy
23. leftof yz  f2 leftof yz
24. leftof zy  f2 leftof zy
25. leftof zy  f2 leftof zy
26. f2 z
27. y
28. f1 z
29. y
30. a' Point
31. x' Point
32. z' Point
33. B(zf2a')
34. B(zyc')
35. B(zf1x')
36. B(zyc')
37. za' ≅ zx'
38. zc' ≅ zc'
39. a'c' ≅ x'c'
40. z' ≡ c'
41. ya' ≅ yx'
42. f2 leftof yz
43. f1 leftof yz
44. leftof yz
⊢ x' ≡ a'
BY
(((Assert x' leftof yz BY
           (InstLemma `left-convex` [⌜e⌝;⌜y⌝;⌜z⌝;⌜f1⌝;⌜x'⌝]⋅ THEN Auto))
    THEN (Assert a' leftof yz BY
                (InstLemma `left-convex` [⌜e⌝;⌜y⌝;⌜z⌝;⌜f2⌝;⌜a'⌝]⋅ THEN Auto))
    )
   THEN InstLemma `Euclid-Prop7` [⌜e⌝;⌜y⌝;⌜z⌝;⌜a'⌝;⌜x'⌝]⋅
   THEN Auto) }


Latex:


Latex:
.....aux..... 
1.  e  :  EuclideanPlane
2.  c'  :  Point
3.  a  :  Point
4.  b  :  Point
5.  c  :  Point
6.  x  :  Point
7.  y  :  Point
8.  z  :  Point
9.  a  \#  bc
10.  x  leftof  yz
11.  f  :  Point
12.  acb  \mcong{}\msuba{}  fzy
13.  x  leftof  yz  \mLeftarrow{}{}  f  leftof  yz
14.  x  leftof  zy  {}\mRightarrow{}  f  leftof  zy
15.  x  leftof  zy  \mLeftarrow{}{}  f  leftof  zy
16.  f1  :  Point
17.  f2  :  Point
18.  acb  \mcong{}\msuba{}  f1zy
19.  acb  \mcong{}\msuba{}  f2zy
20.  x  leftof  yz  \mLeftarrow{}{}  f1  leftof  yz
21.  x  leftof  zy  {}\mRightarrow{}  f1  leftof  zy
22.  x  leftof  zy  \mLeftarrow{}{}  f1  leftof  zy
23.  x  leftof  yz  \mLeftarrow{}{}  f2  leftof  yz
24.  x  leftof  zy  {}\mRightarrow{}  f2  leftof  zy
25.  x  leftof  zy  \mLeftarrow{}{}  f2  leftof  zy
26.  f2  \#  z
27.  z  \#  y
28.  f1  \#  z
29.  z  \#  y
30.  a'  :  Point
31.  x'  :  Point
32.  z'  :  Point
33.  B(zf2a')
34.  B(zyc')
35.  B(zf1x')
36.  B(zyc')
37.  za'  \mcong{}  zx'
38.  zc'  \mcong{}  zc'
39.  a'c'  \mcong{}  x'c'
40.  z'  \mequiv{}  c'
41.  ya'  \mcong{}  yx'
42.  f2  leftof  yz
43.  f1  leftof  yz
44.  f  leftof  yz
\mvdash{}  x'  \mequiv{}  a'


By


Latex:
(((Assert  x'  leftof  yz  BY
                  (InstLemma  `left-convex`  [\mkleeneopen{}e\mkleeneclose{};\mkleeneopen{}y\mkleeneclose{};\mkleeneopen{}z\mkleeneclose{};\mkleeneopen{}f1\mkleeneclose{};\mkleeneopen{}x'\mkleeneclose{}]\mcdot{}  THEN  Auto))
    THEN  (Assert  a'  leftof  yz  BY
                            (InstLemma  `left-convex`  [\mkleeneopen{}e\mkleeneclose{};\mkleeneopen{}y\mkleeneclose{};\mkleeneopen{}z\mkleeneclose{};\mkleeneopen{}f2\mkleeneclose{};\mkleeneopen{}a'\mkleeneclose{}]\mcdot{}  THEN  Auto))
    )
  THEN  InstLemma  `Euclid-Prop7`  [\mkleeneopen{}e\mkleeneclose{};\mkleeneopen{}y\mkleeneclose{};\mkleeneopen{}z\mkleeneclose{};\mkleeneopen{}a'\mkleeneclose{};\mkleeneopen{}x'\mkleeneclose{}]\mcdot{}
  THEN  Auto)




Home Index