---

Step * of Lemma geo-colinear-cong-tri-exists

No Annotations
∀[e:BasicGeometry]. ∀[a,b,c,a',c':Point].
  (Colinear(a;b;c) ⇒ ac ≅ a'c' ⇒ (¬¬(∃b':Point. (Cong3(abc,a'b'c') ∧ Colinear(a';b';c')))))
BY
{ (Auto
   THEN (gColinearCases 7⋅ THEN Try ((D 7 THEN Trivial)))
   THEN Try (((RemoveDoubleNegation THENA Auto)
              THEN Unfold `geo-cong-tri` 0
              THEN gEliminatePoint' (-1)
              THEN Complete (Auto)))) }

1
1. e : BasicGeometry
2. a : Point
3. b : Point
4. c : Point
5. a' : Point
6. c' : Point
7. Colinear(a;b;c)
8. ac ≅ a'c'
9. c ≡ a
⊢ ¬¬(∃b':Point. (Cong3(abc,a'b'c') ∧ Colinear(a';b';c')))

2
1. e : BasicGeometry
2. a : Point
3. b : Point
4. c : Point
5. a' : Point
6. c' : Point
7. Colinear(a;b;c)
8. ac ≅ a'c'
9. a-b-c
⊢ ¬¬(∃b':Point. (Cong3(abc,a'b'c') ∧ Colinear(a';b';c')))

3
1. e : BasicGeometry
2. a : Point
3. b : Point
4. c : Point
5. a' : Point
6. c' : Point
7. Colinear(a;b;c)
8. ac ≅ a'c'
9. b-c-a
⊢ ¬¬(∃b':Point. (Cong3(abc,a'b'c') ∧ Colinear(a';b';c')))

4
1. e : BasicGeometry
2. a : Point
3. b : Point
4. c : Point
5. a' : Point
6. c' : Point
7. Colinear(a;b;c)
8. ac ≅ a'c'
9. c-a-b
⊢ ¬¬(∃b':Point. (Cong3(abc,a'b'c') ∧ Colinear(a';b';c')))

---

Latex:

---

Latex:
No  Annotations
\mforall{}[e:BasicGeometry].  \mforall{}[a,b,c,a',c':Point].
    (Colinear(a;b;c)  {}\mRightarrow{}  ac  \mcong{}  a'c'  {}\mRightarrow{}  (\mneg{}\mneg{}(\mexists{}b':Point.  (Cong3(abc,a'b'c')  \mwedge{}  Colinear(a';b';c')))))


By

---

Latex:
(Auto
  THEN  (gColinearCases  7\mcdot{}  THEN  Try  ((D  7  THEN  Trivial)))
  THEN  Try  (((RemoveDoubleNegation  THENA  Auto)
                        THEN  Unfold  `geo-cong-tri`  0
                        THEN  gEliminatePoint'  (-1)
                        THEN  Complete  (Auto))))

---

Home Index