Step
*
of Lemma
p4eu
∀e:EuclideanPlane. ∀a,b,c,A,B,C:Point.
(ab=AB ∧ ac=AC ∧ bac = BAC)
⇒ (bc=BC ∧ abc = ABC ∧ bca = BCA ∧ Cong3(abc,ABC))
supposing Triangle(a;b;c) ∧ Triangle(A;B;C)
BY
{ Auto }
1
1. e : EuclideanPlane
2. a : Point
3. b : Point
4. c : Point
5. A : Point
6. B : Point
7. C : Point
8. Triangle(a;b;c)
9. Triangle(A;B;C)
10. ab=AB
11. ac=AC
12. bac = BAC
⊢ bc=BC
2
1. e : EuclideanPlane
2. a : Point
3. b : Point
4. c : Point
5. A : Point
6. B : Point
7. C : Point
8. Triangle(a;b;c)
9. Triangle(A;B;C)
10. ab=AB
11. ac=AC
12. bac = BAC
13. bc=BC
⊢ abc = ABC
3
1. e : EuclideanPlane
2. a : Point
3. b : Point
4. c : Point
5. A : Point
6. B : Point
7. C : Point
8. Triangle(a;b;c)
9. Triangle(A;B;C)
10. ab=AB
11. ac=AC
12. bac = BAC
13. bc=BC
14. abc = ABC
⊢ bca = BCA
4
1. e : EuclideanPlane
2. a : Point
3. b : Point
4. c : Point
5. A : Point
6. B : Point
7. C : Point
8. Triangle(a;b;c)
9. Triangle(A;B;C)
10. ab=AB
11. ac=AC
12. bac = BAC
13. bc=BC
14. abc = ABC
15. bca = BCA
⊢ Cong3(abc,ABC)
Latex:
Latex:
\mforall{}e:EuclideanPlane. \mforall{}a,b,c,A,B,C:Point.
(ab=AB \mwedge{} ac=AC \mwedge{} bac = BAC) {}\mRightarrow{} (bc=BC \mwedge{} abc = ABC \mwedge{} bca = BCA \mwedge{} Cong3(abc,ABC))
supposing Triangle(a;b;c) \mwedge{} Triangle(A;B;C)
By
Latex:
Auto
Home
Index