Step
*
1
1
1
3
2
2
2
1
of Lemma
Euclid-Prop21
1. g : EuclideanPlane
2. a : Point
3. b : Point
4. c : Point
5. d : Point
6. a leftof bc
7. d leftof bc
8. d leftof ca
9. d leftof ab
10. a leftof bd
11. c leftof db
12. x : Point
13. a-x-c
14. b-d-x
15. |bx| < |ba| + |ax|
16. |bx| + |xc| < |ba| + |ac|
17. |cd| < |cx| + |xd|
18. |cd| + |db| < |cx| + |xb|
19. |cd| + |db| < |ba| + |ac|
20. cxb < bdc
21. bac < cxb
22. bac < bdc
⊢ {|cd| + |bd| < |ba| + |ac| ∧ bac < bdc}
BY
{ (ExRepD THEN Auto) }
Latex:
Latex:
1. g : EuclideanPlane
2. a : Point
3. b : Point
4. c : Point
5. d : Point
6. a leftof bc
7. d leftof bc
8. d leftof ca
9. d leftof ab
10. a leftof bd
11. c leftof db
12. x : Point
13. a-x-c
14. b-d-x
15. |bx| < |ba| + |ax|
16. |bx| + |xc| < |ba| + |ac|
17. |cd| < |cx| + |xd|
18. |cd| + |db| < |cx| + |xb|
19. |cd| + |db| < |ba| + |ac|
20. cxb < bdc
21. bac < cxb
22. bac < bdc
\mvdash{} \{|cd| + |bd| < |ba| + |ac| \mwedge{} bac < bdc\}
By
Latex:
(ExRepD THEN Auto)
Home
Index