---

Step * 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'
10. ac ≅ a'c'
11. a' ≠ b'
12. a' ≠ c'
13. ¬a'_b'_c'
14. a'_c'_b'
15. |a'b'| = |a'c'| + |c'b'| ∈ Length
16. |ac| = |ab| + |bc| ∈ Length
⊢ False
BY
{ ∀h:hyp. ((RWO "geo-congruent-iff-length" h THENA Auto) THEN (RW (SweepUpC (HypC h)) (-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'b'| + |bc| ∈ 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  \00D0  a'b'
10.  ac  \00D0  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.  |ac|  =  |ab|  +  |bc|
\mvdash{}  False


By

---

Latex:
\mforall{}h:hyp.  ((RWO  "geo-congruent-iff-length"  h  THENA  Auto)
                  THEN  (RW  (SweepUpC  (HypC  h))  (-1)  THENA  Auto)
                  ) 

---

Home Index