Step
*
1
of Lemma
geo-add-length-between-iff
1. e : BasicGeometry
2. a : Point
3. b : Point
4. c : Point
5. |ac| = |ab| + |bc| ∈ Length
⊢ B(abc)
BY
{ ((gSeparatedCases ⌜b⌝ ⌜a⌝⋅ THEN Auto) THEN gSeparatedCases ⌜c⌝ ⌜a⌝⋅ THEN Auto) }
1
1. e : BasicGeometry
2. a : Point
3. b : Point
4. c : Point
5. |ac| = |ab| + |bc| ∈ Length
6. b # a
7. c # a
⊢ B(abc)
2
1. e : BasicGeometry
2. a : Point
3. b : Point
4. c : Point
5. |ac| = |ab| + |bc| ∈ Length
6. b # a
7. c ≡ a
⊢ B(aba)
Latex:
Latex:
1. e : BasicGeometry
2. a : Point
3. b : Point
4. c : Point
5. |ac| = |ab| + |bc|
\mvdash{} B(abc)
By
Latex:
((gSeparatedCases \mkleeneopen{}b\mkleeneclose{} \mkleeneopen{}a\mkleeneclose{}\mcdot{} THEN Auto) THEN gSeparatedCases \mkleeneopen{}c\mkleeneclose{} \mkleeneopen{}a\mkleeneclose{}\mcdot{} THEN Auto)
Home
Index