---

Step * of Lemma isosc-bisectors-between_1

No Annotations
∀e:HeytingGeometry. ∀a,b,c,m,a',b',m':Point.
  (c # ab ⇒ ac ≅ bc ⇒ (c-a'-a ∧ c-b'-b) ⇒ a=m=b ⇒ a'=m'=b' ⇒ aa' ≅ bb' ⇒ c-m'-m)
BY
{ (Auto
   THEN (Assert a' # b'c BY
               (InstLemma `geo-triangle-colinear` [⌜e⌝;⌜a⌝;⌜c⌝;⌜b⌝;⌜a'⌝]⋅ THEN Auto))
   THEN (FLemma `midpoint-sep` [-3] THENA Auto)
   THEN (Assert c # m' BY
               (D -4 THEN InstLemma `geo-triangle-colinear` [⌜e⌝;⌜a'⌝;⌜b'⌝;⌜c⌝;⌜m'⌝]⋅ THEN Auto))
   THEN (FLemma `midpoint-sep` [-6] THENA Auto)
   THEN (Assert c # m BY
               (D -7 THEN InstLemma `geo-triangle-colinear` [⌜e⌝;⌜a⌝;⌜b⌝;⌜c⌝;⌜m⌝]⋅ THEN Auto))) }

1
1. e : HeytingGeometry
2. a : Point
3. b : Point
4. c : Point
5. m : Point
6. a' : Point
7. b' : Point
8. m' : Point
9. c # ab
10. ac ≅ bc
11. c-a'-a
12. c-b'-b
13. a=m=b
14. a'=m'=b'
15. aa' ≅ bb'
16. a' # b'c
17. a' # m' ∧ b' # m'
18. c # m'
19. a # m ∧ b # m
20. c # m
⊢ c-m'-m

---

Latex:

---

Latex:
No  Annotations
\mforall{}e:HeytingGeometry.  \mforall{}a,b,c,m,a',b',m':Point.
    (c  \#  ab  {}\mRightarrow{}  ac  \mcong{}  bc  {}\mRightarrow{}  (c-a'-a  \mwedge{}  c-b'-b)  {}\mRightarrow{}  a=m=b  {}\mRightarrow{}  a'=m'=b'  {}\mRightarrow{}  aa'  \mcong{}  bb'  {}\mRightarrow{}  c-m'-m)


By

---

Latex:
(Auto
  THEN  (Assert  a'  \#  b'c  BY
                          (InstLemma  `geo-triangle-colinear`  [\mkleeneopen{}e\mkleeneclose{};\mkleeneopen{}a\mkleeneclose{};\mkleeneopen{}c\mkleeneclose{};\mkleeneopen{}b\mkleeneclose{};\mkleeneopen{}a'\mkleeneclose{}]\mcdot{}  THEN  Auto))
  THEN  (FLemma  `midpoint-sep`  [-3]  THENA  Auto)
  THEN  (Assert  c  \#  m'  BY
                          (D  -4  THEN  InstLemma  `geo-triangle-colinear`  [\mkleeneopen{}e\mkleeneclose{};\mkleeneopen{}a'\mkleeneclose{};\mkleeneopen{}b'\mkleeneclose{};\mkleeneopen{}c\mkleeneclose{};\mkleeneopen{}m'\mkleeneclose{}]\mcdot{}  THEN  Auto))
  THEN  (FLemma  `midpoint-sep`  [-6]  THENA  Auto)
  THEN  (Assert  c  \#  m  BY
                          (D  -7  THEN  InstLemma  `geo-triangle-colinear`  [\mkleeneopen{}e\mkleeneclose{};\mkleeneopen{}a\mkleeneclose{};\mkleeneopen{}b\mkleeneclose{};\mkleeneopen{}c\mkleeneclose{};\mkleeneopen{}m\mkleeneclose{}]\mcdot{}  THEN  Auto)))

---

Home Index