---

Step * 2 1 of Lemma out-implies-straightangle


1. e : EuclideanPlane
2. a : Point
3. b : Point
4. c : Point
5. a' : Point
6. b' : Point
7. c' : Point
8. a' ≠ b'
9. c' ≠ b'
10. out(b ac)
11. out(b' a'c')
12. A' : Point
13. a'=b'=A'
14. p : Point
15. A'-b'-p ∧ b'p ≅ ba
16. q : Point
17. A'-b'-q ∧ b'q ≅ bc
⊢ abc ≅a a'b'c'
BY
{ (((Assert out(b' pq) BY
           Auto)
    THEN (InstLemma `geo-out-iff-between1` [⌜e⌝;⌜b'⌝;⌜q⌝;⌜p⌝;⌜A'⌝]⋅ THEN Auto⋅)
    THEN D -2
    THEN EAuto 1)
   THEN (Assert A'-b'-a' BY
               (((Auto THEN D 13) THEN D 11 THEN Auto) THEN D 0 THEN Auto))
   THEN (Assert A'-b'-c' BY
               ((Lemmaize [13;11] THEN Auto)
                THEN (D -1 THEN Auto)
                THEN (InstLemma `geo-out-iff-between1` [⌜e⌝;⌜b'⌝;⌜a'⌝;⌜c'⌝;⌜A'⌝]⋅ THENA Auto)
                THEN (RepeatFor 2 (D -1) THEN Auto)
                THEN D 0
                THEN Auto))
   THEN InstLemma `out-preserves-angle-cong_1` [⌜e⌝;⌜a'⌝;⌜b'⌝;⌜c'⌝;⌜a'⌝;⌜b'⌝;⌜c'⌝;⌜a'⌝;⌜c'⌝;⌜p⌝;⌜q⌝]⋅
   THEN EAuto 1) }

---

Latex:

---

Latex:

1.  e  :  EuclideanPlane
2.  a  :  Point
3.  b  :  Point
4.  c  :  Point
5.  a'  :  Point
6.  b'  :  Point
7.  c'  :  Point
8.  a'  \mneq{}  b'
9.  c'  \mneq{}  b'
10.  out(b  ac)
11.  out(b'  a'c')
12.  A'  :  Point
13.  a'=b'=A'
14.  p  :  Point
15.  A'-b'-p  \mwedge{}  b'p  \mcong{}  ba
16.  q  :  Point
17.  A'-b'-q  \mwedge{}  b'q  \mcong{}  bc
\mvdash{}  abc  \mcong{}\msuba{}  a'b'c'


By

---

Latex:
(((Assert  out(b'  pq)  BY
                  Auto)
    THEN  (InstLemma  `geo-out-iff-between1`  [\mkleeneopen{}e\mkleeneclose{};\mkleeneopen{}b'\mkleeneclose{};\mkleeneopen{}q\mkleeneclose{};\mkleeneopen{}p\mkleeneclose{};\mkleeneopen{}A'\mkleeneclose{}]\mcdot{}  THEN  Auto\mcdot{})
    THEN  D  -2
    THEN  EAuto  1)
  THEN  (Assert  A'-b'-a'  BY
                          (((Auto  THEN  D  13)  THEN  D  11  THEN  Auto)  THEN  D  0  THEN  Auto))
  THEN  (Assert  A'-b'-c'  BY
                          ((Lemmaize  [13;11]  THEN  Auto)
                            THEN  (D  -1  THEN  Auto)
                            THEN  (InstLemma  `geo-out-iff-between1`  [\mkleeneopen{}e\mkleeneclose{};\mkleeneopen{}b'\mkleeneclose{};\mkleeneopen{}a'\mkleeneclose{};\mkleeneopen{}c'\mkleeneclose{};\mkleeneopen{}A'\mkleeneclose{}]\mcdot{}  THENA  Auto)
                            THEN  (RepeatFor  2  (D  -1)  THEN  Auto)
                            THEN  D  0
                            THEN  Auto))
  THEN  InstLemma  `out-preserves-angle-cong\_1`  [\mkleeneopen{}e\mkleeneclose{};\mkleeneopen{}a'\mkleeneclose{};\mkleeneopen{}b'\mkleeneclose{};\mkleeneopen{}c'\mkleeneclose{};\mkleeneopen{}a'\mkleeneclose{};\mkleeneopen{}b'\mkleeneclose{};\mkleeneopen{}c'\mkleeneclose{};\mkleeneopen{}a'\mkleeneclose{};\mkleeneopen{}c'\mkleeneclose{};\mkleeneopen{}p\mkleeneclose{};\mkleeneopen{}q\mkleeneclose{}]\mcdot{}
  THEN  EAuto  1)

---

Home Index