---

Step * 1 1 1 of Lemma geo-lt-angle-in-half-plane-implies-left


1. e : EuclideanPlane
2. w : Point
3. x : Point
4. y : Point
5. z : Point
6. xyz < wyz
7. w leftof yz
8. x leftof yz
9. ¬out(y zw)
10. ∃p,p',x',z':Point. (xyz ≅a zyp ∧ y_p'_p ∧ (out(y zx') ∧ out(y wz')) ∧ (¬z_y_p) ∧ x'_p'_z' ∧ p' ≠ z')
⊢ w leftof yx
BY
{ ((ExRepD
    THEN (Assert p' # yw BY
                ((Assert x' # yw BY
                        ((Assert z # yw BY
                                ((Assert w # yz BY (Unfold `geo-lsep` 0 THEN Auto)) THEN Auto))
                         THEN InstLemma `out-preserves-lsep` [⌜e⌝;⌜y⌝;⌜z⌝;⌜w⌝;⌜x'⌝;⌜w⌝]⋅
                         THEN EAuto 1))
                 THEN InstLemma `colinear-lsep` [⌜e⌝;⌜w⌝;⌜y⌝;⌜x'⌝;⌜z'⌝]⋅
                 THEN Auto))
    )
   THEN (InstLemma `interior-angles-unique2` [⌜e⌝;⌜y⌝;⌜z⌝;⌜w⌝;⌜x⌝;⌜x'⌝;⌜z'⌝;⌜p'⌝]⋅ THENA Auto)
   ) }

1
.....antecedent..... 
1. e : EuclideanPlane
2. w : Point
3. x : Point
4. y : Point
5. z : Point
6. xyz < wyz
7. w leftof yz
8. x leftof yz
9. ¬out(y zw)
10. p : Point
11. p' : Point
12. x' : Point
13. z' : Point
14. xyz ≅a zyp
15. y_p'_p
16. out(y zx')
17. out(y wz')
18. ¬z_y_p
19. x'_p'_z'
20. p' ≠ z'
21. p' # yw
⊢ p' leftof yz

2
.....antecedent..... 
1. e : EuclideanPlane
2. w : Point
3. x : Point
4. y : Point
5. z : Point
6. xyz < wyz
7. w leftof yz
8. x leftof yz
9. ¬out(y zw)
10. p : Point
11. p' : Point
12. x' : Point
13. z' : Point
14. xyz ≅a zyp
15. y_p'_p
16. out(y zx')
17. out(y wz')
18. ¬z_y_p
19. x'_p'_z'
20. p' ≠ z'
21. p' # yw
⊢ zyx < zyw

3
.....antecedent..... 
1. e : EuclideanPlane
2. w : Point
3. x : Point
4. y : Point
5. z : Point
6. xyz < wyz
7. w leftof yz
8. x leftof yz
9. ¬out(y zw)
10. p : Point
11. p' : Point
12. x' : Point
13. z' : Point
14. xyz ≅a zyp
15. y_p'_p
16. out(y zx')
17. out(y wz')
18. ¬z_y_p
19. x'_p'_z'
20. p' ≠ z'
21. p' # yw
⊢ zyp' ≅a zyx

4
1. e : EuclideanPlane
2. w : Point
3. x : Point
4. y : Point
5. z : Point
6. xyz < wyz
7. w leftof yz
8. x leftof yz
9. ¬out(y zw)
10. p : Point
11. p' : Point
12. x' : Point
13. z' : Point
14. xyz ≅a zyp
15. y_p'_p
16. out(y zx')
17. out(y wz')
18. ¬z_y_p
19. x'_p'_z'
20. p' ≠ z'
21. p' # yw
22. out(y xp')
⊢ w leftof yx

---

Latex:

---

Latex:

1.  e  :  EuclideanPlane
2.  w  :  Point
3.  x  :  Point
4.  y  :  Point
5.  z  :  Point
6.  xyz  <  wyz
7.  w  leftof  yz
8.  x  leftof  yz
9.  \mneg{}out(y  zw)
10.  \mexists{}p,p',x',z':Point
          (xyz  \mcong{}\msuba{}  zyp  \mwedge{}  y\_p'\_p  \mwedge{}  (out(y  zx')  \mwedge{}  out(y  wz'))  \mwedge{}  (\mneg{}z\_y\_p)  \mwedge{}  x'\_p'\_z'  \mwedge{}  p'  \mneq{}  z')
\mvdash{}  w  leftof  yx


By

---

Latex:
((ExRepD
    THEN  (Assert  p'  \#  yw  BY
                            ((Assert  x'  \#  yw  BY
                                            ((Assert  z  \#  yw  BY
                                                            ((Assert  w  \#  yz  BY  (Unfold  `geo-lsep`  0  THEN  Auto))  THEN  Auto))
                                              THEN  InstLemma  `out-preserves-lsep`  [\mkleeneopen{}e\mkleeneclose{};\mkleeneopen{}y\mkleeneclose{};\mkleeneopen{}z\mkleeneclose{};\mkleeneopen{}w\mkleeneclose{};\mkleeneopen{}x'\mkleeneclose{};\mkleeneopen{}w\mkleeneclose{}]\mcdot{}
                                              THEN  EAuto  1))
                              THEN  InstLemma  `colinear-lsep`  [\mkleeneopen{}e\mkleeneclose{};\mkleeneopen{}w\mkleeneclose{};\mkleeneopen{}y\mkleeneclose{};\mkleeneopen{}x'\mkleeneclose{};\mkleeneopen{}z'\mkleeneclose{}]\mcdot{}
                              THEN  Auto))
    )
  THEN  (InstLemma  `interior-angles-unique2`  [\mkleeneopen{}e\mkleeneclose{};\mkleeneopen{}y\mkleeneclose{};\mkleeneopen{}z\mkleeneclose{};\mkleeneopen{}w\mkleeneclose{};\mkleeneopen{}x\mkleeneclose{};\mkleeneopen{}x'\mkleeneclose{};\mkleeneopen{}z'\mkleeneclose{};\mkleeneopen{}p'\mkleeneclose{}]\mcdot{}  THENA  Auto)
  )

---

Home Index