Step * 1 1 1 3 2 2 2 1 of Lemma Euclid-Prop21


1. EuclideanPlane
2. Point
3. Point
4. Point
5. Point
6. leftof bc
7. leftof bc
8. leftof ca
9. leftof ab
10. leftof bd
11. leftof db
12. 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