---

Step * 1 of Lemma cong-angle-out-exists


1. g : EuclideanPlane
2. a : Point
3. b : Point
4. c : Point
5. x : Point
6. y : Point
7. z : Point
8. a' : Point
9. c' : Point
10. p : Point
11. abc ≅a xyz
12. a ≠ b
13. c ≠ b
14. p ≠ b
15. x ≠ y
16. z ≠ y
17. out(b aa')
18. out(b cc')
19. a'-p-c'
20. r1 : Point
21. x-y-r1
22. yr1 ≅ OX
23. r2 : Point
24. z-y-r2
25. yr2 ≅ OX
26. A : Point
27. r1-y-A ∧ yA ≅ ba'
28. C : Point
29. r2-y-C ∧ yC ≅ bc'
⊢ ∃x',z',p':Point
   (((x'-p'-z' ∧ Cong3(a'bc',x'yz')) ∧ out(y xx') ∧ out(y zz')) ∧ (x'p' ≅ a'p ∧ p'z' ≅ pc') ∧ bp ≅ yp' ∧ x'yp' ≅a a'bp)
BY
{ (InstLemma `geo-sas2` [⌜g⌝;⌜b⌝;⌜a'⌝;⌜c'⌝;⌜y⌝;⌜A⌝;⌜C⌝]⋅
   THENA (Auto THEN InstLemma `out-preserves-angle-cong_1` [⌜g⌝;⌜a⌝;⌜b⌝;⌜c⌝;⌜x⌝;⌜y⌝;⌜z⌝;⌜a'⌝;⌜c'⌝;⌜A⌝;⌜C⌝]⋅ THEN Auto)
   ) }

1
.....antecedent..... 
1. g : EuclideanPlane
2. a : Point
3. b : Point
4. c : Point
5. x : Point
6. y : Point
7. z : Point
8. a' : Point
9. c' : Point
10. p : Point
11. abc ≅a xyz
12. a ≠ b
13. c ≠ b
14. p ≠ b
15. x ≠ y
16. z ≠ y
17. out(b aa')
18. out(b cc')
19. a'-p-c'
20. r1 : Point
21. x-y-r1
22. yr1 ≅ OX
23. r2 : Point
24. z-y-r2
25. yr2 ≅ OX
26. A : Point
27. r1-y-A
28. yA ≅ ba'
29. C : Point
30. r2-y-C
31. yC ≅ bc'
32. ba' ≅ yA
33. bc' ≅ yC
⊢ out(y zC)

2
.....antecedent..... 
1. g : EuclideanPlane
2. a : Point
3. b : Point
4. c : Point
5. x : Point
6. y : Point
7. z : Point
8. a' : Point
9. c' : Point
10. p : Point
11. abc ≅a xyz
12. a ≠ b
13. c ≠ b
14. p ≠ b
15. x ≠ y
16. z ≠ y
17. out(b aa')
18. out(b cc')
19. a'-p-c'
20. r1 : Point
21. x-y-r1
22. yr1 ≅ OX
23. r2 : Point
24. z-y-r2
25. yr2 ≅ OX
26. A : Point
27. r1-y-A
28. yA ≅ ba'
29. C : Point
30. r2-y-C
31. yC ≅ bc'
32. ba' ≅ yA
33. bc' ≅ yC
⊢ out(y xA)

3
1. g : EuclideanPlane
2. a : Point
3. b : Point
4. c : Point
5. x : Point
6. y : Point
7. z : Point
8. a' : Point
9. c' : Point
10. p : Point
11. abc ≅a xyz
12. a ≠ b
13. c ≠ b
14. p ≠ b
15. x ≠ y
16. z ≠ y
17. out(b aa')
18. out(b cc')
19. a'-p-c'
20. r1 : Point
21. x-y-r1
22. yr1 ≅ OX
23. r2 : Point
24. z-y-r2
25. yr2 ≅ OX
26. A : Point
27. r1-y-A ∧ yA ≅ ba'
28. C : Point
29. r2-y-C ∧ yC ≅ bc'
30. a'c' ≅ AC
⊢ ∃x',z',p':Point
   (((x'-p'-z' ∧ Cong3(a'bc',x'yz')) ∧ out(y xx') ∧ out(y zz')) ∧ (x'p' ≅ a'p ∧ p'z' ≅ pc') ∧ bp ≅ yp' ∧ x'yp' ≅a a'bp)

---

Latex:

---

Latex:

1.  g  :  EuclideanPlane
2.  a  :  Point
3.  b  :  Point
4.  c  :  Point
5.  x  :  Point
6.  y  :  Point
7.  z  :  Point
8.  a'  :  Point
9.  c'  :  Point
10.  p  :  Point
11.  abc  \mcong{}\msuba{}  xyz
12.  a  \mneq{}  b
13.  c  \mneq{}  b
14.  p  \mneq{}  b
15.  x  \mneq{}  y
16.  z  \mneq{}  y
17.  out(b  aa')
18.  out(b  cc')
19.  a'-p-c'
20.  r1  :  Point
21.  x-y-r1
22.  yr1  \mcong{}  OX
23.  r2  :  Point
24.  z-y-r2
25.  yr2  \mcong{}  OX
26.  A  :  Point
27.  r1-y-A  \mwedge{}  yA  \mcong{}  ba'
28.  C  :  Point
29.  r2-y-C  \mwedge{}  yC  \mcong{}  bc'
\mvdash{}  \mexists{}x',z',p':Point
      (((x'-p'-z'  \mwedge{}  Cong3(a'bc',x'yz'))  \mwedge{}  out(y  xx')  \mwedge{}  out(y  zz'))
      \mwedge{}  (x'p'  \mcong{}  a'p  \mwedge{}  p'z'  \mcong{}  pc')
      \mwedge{}  bp  \mcong{}  yp'
      \mwedge{}  x'yp'  \mcong{}\msuba{}  a'bp)


By

---

Latex:
(InstLemma  `geo-sas2`  [\mkleeneopen{}g\mkleeneclose{};\mkleeneopen{}b\mkleeneclose{};\mkleeneopen{}a'\mkleeneclose{};\mkleeneopen{}c'\mkleeneclose{};\mkleeneopen{}y\mkleeneclose{};\mkleeneopen{}A\mkleeneclose{};\mkleeneopen{}C\mkleeneclose{}]\mcdot{}
  THENA  (Auto
                THEN  InstLemma  `out-preserves-angle-cong\_1`  [\mkleeneopen{}g\mkleeneclose{};\mkleeneopen{}a\mkleeneclose{};\mkleeneopen{}b\mkleeneclose{};\mkleeneopen{}c\mkleeneclose{};\mkleeneopen{}x\mkleeneclose{};\mkleeneopen{}y\mkleeneclose{};\mkleeneopen{}z\mkleeneclose{};\mkleeneopen{}a'\mkleeneclose{};\mkleeneopen{}c'\mkleeneclose{};\mkleeneopen{}A\mkleeneclose{};\mkleeneopen{}C\mkleeneclose{}]\mcdot{}
                THEN  Auto)
  )

---

Home Index