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

.....antecedent..... 
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(bdx)
15. d
16. x
17. |bx| < |ba| |ax|
18. |bx| |xc| < |ba| |ac|
19. |cd| < |cx| |xd|
20. |bx| |bd| |dx| ∈ Length
21. |xb| |bd| |dx| ∈ Length
22. |cx| |bd| |dx| |cx| |bd| |dx| ∈ Length
⊢ |cx| |xd|
BY
(Assert X < |cx| |xd| BY
         (((InstLemma `geo-zero-lt-iff` [⌜g⌝;⌜c⌝;⌜d⌝]⋅ THEN Auto) THEN -1 THEN Auto)
          THEN ((InstLemma  `geo-lt_transitivity` [⌜g⌝;⌜X⌝;⌜|cd|⌝;⌜|cx| |xd|⌝]⋅ THEN Auto)
                THENA (MemTypeCD THEN Auto)
                )
          )) }

1
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(bdx)
15. d
16. x
17. |bx| < |ba| |ax|
18. |bx| |xc| < |ba| |ac|
19. |cd| < |cx| |xd|
20. |bx| |bd| |dx| ∈ Length
21. |xb| |bd| |dx| ∈ Length
22. |cx| |bd| |dx| |cx| |bd| |dx| ∈ Length
23. X < |cx| |xd|
⊢ |cx| |xd|


Latex:


Latex:
.....antecedent..... 
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(bdx)
15.  b  \#  d
16.  d  \#  x
17.  |bx|  <  |ba|  +  |ax|
18.  |bx|  +  |xc|  <  |ba|  +  |ac|
19.  |cd|  <  |cx|  +  |xd|
20.  |bx|  =  |bd|  +  |dx|
21.  |xb|  =  |bd|  +  |dx|
22.  |cx|  +  |bd|  +  |dx|  =  |cx|  +  |bd|  +  |dx|
\mvdash{}  X  \#  |cx|  +  |xd|


By


Latex:
(Assert  X  <  |cx|  +  |xd|  BY
              (((InstLemma  `geo-zero-lt-iff`  [\mkleeneopen{}g\mkleeneclose{};\mkleeneopen{}c\mkleeneclose{};\mkleeneopen{}d\mkleeneclose{}]\mcdot{}  THEN  Auto)  THEN  D  -1  THEN  Auto)
                THEN  ((InstLemma    `geo-lt\_transitivity`  [\mkleeneopen{}g\mkleeneclose{};\mkleeneopen{}X\mkleeneclose{};\mkleeneopen{}|cd|\mkleeneclose{};\mkleeneopen{}|cx|  +  |xd|\mkleeneclose{}]\mcdot{}  THEN  Auto)
                            THENA  (MemTypeCD  THEN  Auto)
                            )
                ))




Home Index