Step * of Lemma straight-angle-sum2

No Annotations
e:EuclideanPlane. ∀a,b,c,x,y,z,i,j,k:Point.  (abc xyz ≅ ijk  out(y xz)  (a-b-c ⇐⇒ i-j-k))
BY
(Auto
   THEN (Unfold `hp-angle-sum` -3 THEN ExRepD)
   THEN ((Assert x ∧ BY
                (D -7 THEN Auto))
         THEN (InstLemma `angle-cong-preserves-zero-angle` [⌜e⌝;⌜k⌝;⌜j⌝;⌜p⌝;⌜x⌝;⌜y⌝;⌜z⌝]⋅ THENA EAuto 1)
         )
   THEN 0
   THEN Auto) }

1
1. EuclideanPlane
2. Point
3. Point
4. Point
5. Point
6. Point
7. Point
8. Point
9. Point
10. Point
11. Point
12. p' Point
13. d' Point
14. f' Point
15. abc ≅a ijp
16. kjp ≅a xyz
17. B(jp'p)
18. out(j id')
19. out(j kf')
20. d'-p'-f'
21. out(y xz)
22. a-b-c
23. x
24. z
25. out(j kp)
⊢ B(ijk)

2
1. EuclideanPlane
2. Point
3. Point
4. Point
5. Point
6. Point
7. Point
8. Point
9. Point
10. Point
11. Point
12. p' Point
13. d' Point
14. f' Point
15. abc ≅a ijp
16. kjp ≅a xyz
17. B(jp'p)
18. out(j id')
19. out(j kf')
20. d'-p'-f'
21. out(y xz)
22. i-j-k
23. x
24. z
25. out(j kp)
⊢ B(abc)


Latex:


Latex:
No  Annotations
\mforall{}e:EuclideanPlane.  \mforall{}a,b,c,x,y,z,i,j,k:Point.    (abc  +  xyz  \mcong{}  ijk  {}\mRightarrow{}  out(y  xz)  {}\mRightarrow{}  (a-b-c  \mLeftarrow{}{}\mRightarrow{}  i-j-k))


By


Latex:
(Auto
  THEN  (Unfold  `hp-angle-sum`  -3  THEN  ExRepD)
  THEN  ((Assert  y  \#  x  \mwedge{}  y  \#  z  BY
                            (D  -7  THEN  Auto))
              THEN  (InstLemma  `angle-cong-preserves-zero-angle`  [\mkleeneopen{}e\mkleeneclose{};\mkleeneopen{}k\mkleeneclose{};\mkleeneopen{}j\mkleeneclose{};\mkleeneopen{}p\mkleeneclose{};\mkleeneopen{}x\mkleeneclose{};\mkleeneopen{}y\mkleeneclose{};\mkleeneopen{}z\mkleeneclose{}]\mcdot{}
                          THENA  EAuto  1
                          )
              )
  THEN  D  0
  THEN  Auto)




Home Index