Step * 1 of Lemma hp-angle-sum-subst4


1. EuclideanPlane
2. Point
3. Point
4. Point
5. Point
6. Point
7. Point
8. Point
9. Point
10. Point
11. Point
12. Point
13. Point
14. Point
15. p' Point
16. d' Point
17. f' Point
18. abc ≅a xyp
19. zyp ≅a def
20. y_p'_p
21. out(y xd')
22. out(y zf')
23. d'-p'-f'
24. xyz ≅a ijk
25. x-y-z
26. bc
27. ef
⊢ ∃p,p',d',f':Point. (((abc ≅a ijp ∧ kjp ≅a def) ∧ j_p'_p) ∧ (out(j id') ∧ out(j kf')) ∧ d'-p'-f')
BY
(InstLemma  `Euclid-Prop23` [⌜g⌝;⌜j⌝;⌜i⌝;⌜b⌝;⌜c⌝;⌜a⌝]⋅ THENA Auto) }

1
.....antecedent..... 
1. EuclideanPlane
2. Point
3. Point
4. Point
5. Point
6. Point
7. Point
8. Point
9. Point
10. Point
11. Point
12. Point
13. Point
14. Point
15. p' Point
16. d' Point
17. f' Point
18. abc ≅a xyp
19. zyp ≅a def
20. y_p'_p
21. out(y xd')
22. out(y zf')
23. d'-p'-f'
24. xyz ≅a ijk
25. x-y-z
26. bc
27. ef
⊢ j ≠ i

2
1. EuclideanPlane
2. Point
3. Point
4. Point
5. Point
6. Point
7. Point
8. Point
9. Point
10. Point
11. Point
12. Point
13. Point
14. Point
15. p' Point
16. d' Point
17. f' Point
18. abc ≅a xyp
19. zyp ≅a def
20. y_p'_p
21. out(y xd')
22. out(y zf')
23. d'-p'-f'
24. xyz ≅a ijk
25. x-y-z
26. bc
27. ef
28. ∃x',b':Point. (out(j ib') ∧ x' jb' ∧ x'jb' ≅a abc)
⊢ ∃p,p',d',f':Point. (((abc ≅a ijp ∧ kjp ≅a def) ∧ j_p'_p) ∧ (out(j id') ∧ out(j kf')) ∧ d'-p'-f')


Latex:


Latex:

1.  g  :  EuclideanPlane
2.  a  :  Point
3.  b  :  Point
4.  c  :  Point
5.  d  :  Point
6.  e  :  Point
7.  f  :  Point
8.  x  :  Point
9.  y  :  Point
10.  z  :  Point
11.  i  :  Point
12.  j  :  Point
13.  k  :  Point
14.  p  :  Point
15.  p'  :  Point
16.  d'  :  Point
17.  f'  :  Point
18.  abc  \mcong{}\msuba{}  xyp
19.  zyp  \mcong{}\msuba{}  def
20.  y\_p'\_p
21.  out(y  xd')
22.  out(y  zf')
23.  d'-p'-f'
24.  xyz  \mcong{}\msuba{}  ijk
25.  x-y-z
26.  a  \#  bc
27.  d  \#  ef
\mvdash{}  \mexists{}p,p',d',f':Point.  (((abc  \mcong{}\msuba{}  ijp  \mwedge{}  kjp  \mcong{}\msuba{}  def)  \mwedge{}  j\_p'\_p)  \mwedge{}  (out(j  id')  \mwedge{}  out(j  kf'))  \mwedge{}  d'-p'-f')


By


Latex:
(InstLemma    `Euclid-Prop23`  [\mkleeneopen{}g\mkleeneclose{};\mkleeneopen{}j\mkleeneclose{};\mkleeneopen{}i\mkleeneclose{};\mkleeneopen{}b\mkleeneclose{};\mkleeneopen{}c\mkleeneclose{};\mkleeneopen{}a\mkleeneclose{}]\mcdot{}  THENA  Auto)




Home Index