---

Step * of Lemma geo-congruent-preserves-out

∀e:BasicGeometry. ∀a,b,c,a',b',c':Point.  (bc ≅ b'c' ⇒ ac ≅ a'c' ⇒ ab ≅ a'b' ⇒ out(a bc) ⇒ out(a' b'c'))
BY
{ ((Auto THEN (Assert Colinear(a;b;c) BY Auto))
   THEN ((((D 0 THEN GenRepD ⋅) THEN D 11) THEN Auto) THEN (gColinearCases 14 THENA Auto))
   THEN skip{(Try ((D 8 THEN Trivial⋅))
              THEN Try ((gEliminatePoint' (-1) THEN Auto))
              THEN (FLemma `geo-strict-between-implies-between` [-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. bc ≅ b'c'
9. ac ≅ a'c'
10. ab ≅ a'b'
11. a ≠ b
12. a ≠ c
13. ¬((¬a_b_c) ∧ (¬a_c_b))
14. Colinear(a;b;c)
15. b ≡ c
⊢ ¬((¬a'_b'_c') ∧ (¬a'_c'_b'))

2
1. e : BasicGeometry
2. a : Point
3. b : Point
4. c : Point
5. a' : Point
6. b' : Point
7. c' : Point
8. bc ≅ b'c'
9. ac ≅ a'c'
10. ab ≅ a'b'
11. a ≠ b
12. a ≠ c
13. ¬((¬a_b_c) ∧ (¬a_c_b))
14. Colinear(a;b;c)
15. c ≡ a
⊢ ¬((¬a'_b'_c') ∧ (¬a'_c'_b'))

3
1. e : BasicGeometry
2. a : Point
3. b : Point
4. c : Point
5. a' : Point
6. b' : Point
7. c' : Point
8. bc ≅ b'c'
9. ac ≅ a'c'
10. ab ≅ a'b'
11. a ≠ b
12. a ≠ c
13. ¬((¬a_b_c) ∧ (¬a_c_b))
14. Colinear(a;b;c)
15. a-b-c
⊢ ¬((¬a'_b'_c') ∧ (¬a'_c'_b'))

4
1. e : BasicGeometry
2. a : Point
3. b : Point
4. c : Point
5. a' : Point
6. b' : Point
7. c' : Point
8. bc ≅ b'c'
9. ac ≅ a'c'
10. ab ≅ a'b'
11. a ≠ b
12. a ≠ c
13. ¬((¬a_b_c) ∧ (¬a_c_b))
14. Colinear(a;b;c)
15. b-c-a
⊢ ¬((¬a'_b'_c') ∧ (¬a'_c'_b'))

5
1. e : BasicGeometry
2. a : Point
3. b : Point
4. c : Point
5. a' : Point
6. b' : Point
7. c' : Point
8. bc ≅ b'c'
9. ac ≅ a'c'
10. ab ≅ a'b'
11. a ≠ b
12. a ≠ c
13. ¬((¬a_b_c) ∧ (¬a_c_b))
14. Colinear(a;b;c)
15. c-a-b
⊢ ¬((¬a'_b'_c') ∧ (¬a'_c'_b'))

---

Latex:

---

Latex:
\mforall{}e:BasicGeometry.  \mforall{}a,b,c,a',b',c':Point.
    (bc  \mcong{}  b'c'  {}\mRightarrow{}  ac  \mcong{}  a'c'  {}\mRightarrow{}  ab  \mcong{}  a'b'  {}\mRightarrow{}  out(a  bc)  {}\mRightarrow{}  out(a'  b'c'))


By

---

Latex:
((Auto  THEN  (Assert  Colinear(a;b;c)  BY  Auto))
  THEN  ((((D  0  THEN  GenRepD  \mcdot{})  THEN  D  11)  THEN  Auto)  THEN  (gColinearCases  14  THENA  Auto))
  THEN  skip\{(Try  ((D  8  THEN  Trivial\mcdot{}))
                        THEN  Try  ((gEliminatePoint'  (-1)  THEN  Auto))
                        THEN  (FLemma  `geo-strict-between-implies-between`  [-1]  THENA  Auto))\})

---

Home Index