Step * 1 3 of Lemma Euclid-Prop7'


1. EuclideanPlane
2. Point
3. Point
4. Point
5. Point
6. b
7. ac ≅ ad
8. bc ≅ bd
9. leftof ba)  leftof ba)
10. leftof ba)  ¬leftof ba
11. d
12. Point
13. B(cmd)
14. cm ≅ md
15. Colinear(a;b;m)
16. ¬leftof ab
17. leftof ab
⊢ False
BY
(StableCases ⌜ab⌝⋅ THENA Auto) }

1
1. EuclideanPlane
2. Point
3. Point
4. Point
5. Point
6. b
7. ac ≅ ad
8. bc ≅ bd
9. leftof ba)  leftof ba)
10. leftof ba)  ¬leftof ba
11. d
12. Point
13. B(cmd)
14. cm ≅ md
15. Colinear(a;b;m)
16. ¬leftof ab
17. leftof ab
18. ab
⊢ False

2
1. EuclideanPlane
2. Point
3. Point
4. Point
5. Point
6. b
7. ac ≅ ad
8. bc ≅ bd
9. leftof ba)  leftof ba)
10. leftof ba)  ¬leftof ba
11. d
12. Point
13. B(cmd)
14. cm ≅ md
15. Colinear(a;b;m)
16. ¬leftof ab
17. leftof ab
18. ¬ab
⊢ False


Latex:


Latex:

1.  e  :  EuclideanPlane
2.  a  :  Point
3.  b  :  Point
4.  c  :  Point
5.  d  :  Point
6.  a  \#  b
7.  ac  \mcong{}  ad
8.  bc  \mcong{}  bd
9.  (\mneg{}c  leftof  ba)  {}\mRightarrow{}  (\mneg{}d  leftof  ba)
10.  (\mneg{}c  leftof  ba)  \mLeftarrow{}{}  \mneg{}d  leftof  ba
11.  c  \#  d
12.  m  :  Point
13.  B(cmd)
14.  cm  \mcong{}  md
15.  Colinear(a;b;m)
16.  \mneg{}c  leftof  ab
17.  d  leftof  ab
\mvdash{}  False


By


Latex:
(StableCases  \mkleeneopen{}c  \#  ab\mkleeneclose{}\mcdot{}  THENA  Auto)




Home Index