---

Step * of Lemma geo-lt-angle-construction

∀e:EuclideanPlane. ∀a,b,c,x,y,z:Point.
  (xyz < abc ⇒ x # yz ⇒ a # bc ⇒ (∃a',x',z':Point. (xya' ≅a abc ∧ x'-z'-a' ∧ out(y xx') ∧ out(y zz'))))
BY
{ (Auto
   THEN Unfold `geo-lt-angle` -3
   THEN ExRepD
   THEN (Assert ∃x1,z1:Point. (out(y xx1) ∧ out(y zz1) ∧ x1y ≅ x'b ∧ z1y ≅ p'b ∧ x'p' ≅ x1z1) BY
               (InstLemma  `cong-angle-out-exists1` [⌜e⌝;⌜x'⌝;⌜b⌝;⌜p'⌝;⌜x⌝;⌜y⌝;⌜z⌝]⋅ THENA Auto))) }

1
.....aux..... 
1. e : EuclideanPlane
2. a : Point
3. b : Point
4. c : Point
5. x : Point
6. y : Point
7. z : Point
8. ¬out(b ac)
9. p : Point
10. p' : Point
11. x' : Point
12. z' : Point
13. xyz ≅a abp
14. b_p'_p
15. out(b ax')
16. out(b cz')
17. ¬a_b_p
18. x'_p'_z'
19. p' ≠ z'
20. x # yz
21. a # bc
⊢ x'bp' ≅a xyz

2
.....aux..... 
1. e : EuclideanPlane
2. a : Point
3. b : Point
4. c : Point
5. x : Point
6. y : Point
7. z : Point
8. ¬out(b ac)
9. p : Point
10. p' : Point
11. x' : Point
12. z' : Point
13. xyz ≅a abp
14. b_p'_p
15. out(b ax')
16. out(b cz')
17. ¬a_b_p
18. x'_p'_z'
19. p' ≠ z'
20. x # yz
21. a # bc
22. ∃x'@0,z':Point. (out(y x'@0x) ∧ out(y z'z) ∧ Cong3(x'@0yz',x'bp'))
⊢ ∃x1,z1:Point. (out(y xx1) ∧ out(y zz1) ∧ x1y ≅ x'b ∧ z1y ≅ p'b ∧ x'p' ≅ x1z1)

3
1. e : EuclideanPlane
2. a : Point
3. b : Point
4. c : Point
5. x : Point
6. y : Point
7. z : Point
8. ¬out(b ac)
9. p : Point
10. p' : Point
11. x' : Point
12. z' : Point
13. xyz ≅a abp
14. b_p'_p
15. out(b ax')
16. out(b cz')
17. ¬a_b_p
18. x'_p'_z'
19. p' ≠ z'
20. x # yz
21. a # bc
22. ∃x1,z1:Point. (out(y xx1) ∧ out(y zz1) ∧ x1y ≅ x'b ∧ z1y ≅ p'b ∧ x'p' ≅ x1z1)
⊢ ∃a',x',z':Point. (xya' ≅a abc ∧ x'-z'-a' ∧ out(y xx') ∧ out(y zz'))

---

Latex:

---

Latex:
\mforall{}e:EuclideanPlane.  \mforall{}a,b,c,x,y,z:Point.
    (xyz  <  abc
    {}\mRightarrow{}  x  \#  yz
    {}\mRightarrow{}  a  \#  bc
    {}\mRightarrow{}  (\mexists{}a',x',z':Point.  (xya'  \mcong{}\msuba{}  abc  \mwedge{}  x'-z'-a'  \mwedge{}  out(y  xx')  \mwedge{}  out(y  zz'))))


By

---

Latex:
(Auto
  THEN  Unfold  `geo-lt-angle`  -3
  THEN  ExRepD
  THEN  (Assert  \mexists{}x1,z1:Point.  (out(y  xx1)  \mwedge{}  out(y  zz1)  \mwedge{}  x1y  \mcong{}  x'b  \mwedge{}  z1y  \mcong{}  p'b  \mwedge{}  x'p'  \mcong{}  x1z1)  BY
                          (InstLemma    `cong-angle-out-exists1`  [\mkleeneopen{}e\mkleeneclose{};\mkleeneopen{}x'\mkleeneclose{};\mkleeneopen{}b\mkleeneclose{};\mkleeneopen{}p'\mkleeneclose{};\mkleeneopen{}x\mkleeneclose{};\mkleeneopen{}y\mkleeneclose{};\mkleeneopen{}z\mkleeneclose{}]\mcdot{}  THENA  Auto)))

---

Home Index