---

Step * 1 1 1 1 of Lemma geo-cong-preserves-bet-out


1. e : BasicGeometry
2. a : Point
3. b : Point
4. c : Point
5. a' : Point
6. b' : Point
7. c' : Point
8. a_b_c
9. |ab| = |a'b'| ∈ Length
10. |ac| = |a'c'| ∈ Length
11. a' ≠ b'
12. a' ≠ c'
13. ¬a'_b'_c'
14. a'_c'_b'
15. |a'b'| = |a'c'| + |c'b'| ∈ Length
16. |a'c'| = |a'c'| + |c'b'| + |bc| ∈ Length
⊢ False
BY
{ ((RWO  "geo-add-length-assoc<" (-1) THENA Auto) THEN (FLemma `geo-add-length-implies-eq-zero` [-1] THENA Auto)) }

1
1. e : BasicGeometry
2. a : Point
3. b : Point
4. c : Point
5. a' : Point
6. b' : Point
7. c' : Point
8. a_b_c
9. |ab| = |a'b'| ∈ Length
10. |ac| = |a'c'| ∈ Length
11. a' ≠ b'
12. a' ≠ c'
13. ¬a'_b'_c'
14. a'_c'_b'
15. |a'b'| = |a'c'| + |c'b'| ∈ Length
16. |a'c'| = |a'c'| + |c'b'| + |bc| ∈ Length
17. |c'b'| + |bc| = 0 ∈ Length
⊢ False

---

Latex:

---

Latex:

1.  e  :  BasicGeometry
2.  a  :  Point
3.  b  :  Point
4.  c  :  Point
5.  a'  :  Point
6.  b'  :  Point
7.  c'  :  Point
8.  a\_b\_c
9.  |ab|  =  |a'b'|
10.  |ac|  =  |a'c'|
11.  a'  \mneq{}  b'
12.  a'  \mneq{}  c'
13.  \mneg{}a'\_b'\_c'
14.  a'\_c'\_b'
15.  |a'b'|  =  |a'c'|  +  |c'b'|
16.  |a'c'|  =  |a'c'|  +  |c'b'|  +  |bc|
\mvdash{}  False


By

---

Latex:
((RWO    "geo-add-length-assoc<"  (-1)  THENA  Auto)
  THEN  (FLemma  `geo-add-length-implies-eq-zero`  [-1]  THENA  Auto)
  )

---

Home Index