Step
*
1
1
of Lemma
geo-inner-five-segment
1. e : EuclideanPlane
2. a : Point
3. b : Point
4. c : Point
5. d : Point
6. A : Point
7. B : Point
8. C : Point
9. D : Point
10. B(abc)
11. B(ABC)
12. ac ≅ AC
13. bc ≅ BC
14. ad ≅ AD
15. cd ≅ CD
16. ¬bd ≅ BD
17. a # c
18. A # C
19. E : Point
20. B(acE)
21. cE ≅ ca
22. C # c
23. X : Point
24. B(ACX) ∧ CX ≅ CA
⊢ False
BY
{ ((Assert ca ≅ ac BY
Auto)
THEN (FLemma `geo-congruent-transitivity` [-1;12] THENA Auto)
THEN (FLemma `geo-congruent-transitivity` [-1;-6] THENA Auto)
THEN (Assert AC ≅ CA BY
Auto)
THEN (FLemma `geo-congruent-transitivity` [-1;-2] THENA Auto)
THEN (Assert CA ≅ CX BY
EAuto 1)
THEN (FLemma `geo-congruent-transitivity` [-1;-2] THENA Auto)) }
1
1. e : EuclideanPlane
2. a : Point
3. b : Point
4. c : Point
5. d : Point
6. A : Point
7. B : Point
8. C : Point
9. D : Point
10. B(abc)
11. B(ABC)
12. ac ≅ AC
13. bc ≅ BC
14. ad ≅ AD
15. cd ≅ CD
16. ¬bd ≅ BD
17. a # c
18. A # C
19. E : Point
20. B(acE)
21. cE ≅ ca
22. C # c
23. X : Point
24. B(ACX) ∧ CX ≅ CA
25. ca ≅ ac
26. ca ≅ AC
27. cE ≅ AC
28. AC ≅ CA
29. cE ≅ CA
30. CA ≅ CX
31. cE ≅ CX
⊢ False
Latex:
Latex:
1. e : EuclideanPlane
2. a : Point
3. b : Point
4. c : Point
5. d : Point
6. A : Point
7. B : Point
8. C : Point
9. D : Point
10. B(abc)
11. B(ABC)
12. ac \mcong{} AC
13. bc \mcong{} BC
14. ad \mcong{} AD
15. cd \mcong{} CD
16. \mneg{}bd \mcong{} BD
17. a \# c
18. A \# C
19. E : Point
20. B(acE)
21. cE \mcong{} ca
22. C \# c
23. X : Point
24. B(ACX) \mwedge{} CX \mcong{} CA
\mvdash{} False
By
Latex:
((Assert ca \mcong{} ac BY
Auto)
THEN (FLemma `geo-congruent-transitivity` [-1;12] THENA Auto)
THEN (FLemma `geo-congruent-transitivity` [-1;-6] THENA Auto)
THEN (Assert AC \mcong{} CA BY
Auto)
THEN (FLemma `geo-congruent-transitivity` [-1;-2] THENA Auto)
THEN (Assert CA \mcong{} CX BY
EAuto 1)
THEN (FLemma `geo-congruent-transitivity` [-1;-2] THENA Auto))
Home
Index