Step
*
of Lemma
hp-angle-sum-lt
∀e:EuclideanPlane. ∀a,b,c,x,y,z,i,j,k,a',b',c',x',y',z',i',j',k':Point.
(abc ≅a a'b'c'
⇒ abc + xyz ≅ ijk
⇒ a'b'c' + x'y'z' ≅ i'j'k'
⇒ i # jk
⇒ i' # j'k'
⇒ x # yz
⇒ xyz < x'y'z'
⇒ ijk < i'j'k')
BY
{ (((Auto THEN Unfold `hp-angle-sum` -5)
THEN (Unfold `hp-angle-sum` -6 THEN ExRepD)
THEN (Assert p' # j'k' BY
((InstLemma `out-preserves-lsep` [⌜e⌝;⌜j'⌝;⌜i'⌝;⌜k'⌝;⌜d'⌝;⌜f'⌝]⋅ THENA EAuto 1)
THEN (InstLemma `colinear-lsep` [⌜e⌝;⌜d'⌝;⌜f'⌝;⌜j'⌝;⌜p'⌝]⋅ THENA Auto)
THEN InstLemma `out-preserves-lsep` [⌜e⌝;⌜j'⌝;⌜p'⌝;⌜f'⌝;⌜p'⌝;⌜k'⌝]⋅
THEN EAuto 1)))
THEN (Assert xyz < p'j'k' BY
((InstLemma `geo-cong-angle-preserves-lt-angle2` [⌜e⌝;⌜x⌝;⌜y⌝;⌜z⌝;⌜p'⌝;⌜j'⌝;⌜k'⌝;⌜x'⌝;⌜y'⌝;⌜z'⌝]⋅
THEN Auto
)
THENA (InstLemma `out-preserves-angle-cong_1` [⌜e⌝;⌜k'⌝;⌜j'⌝;⌜p⌝;⌜x'⌝;⌜y'⌝;⌜z'⌝;⌜k'⌝;⌜p'⌝;⌜x'⌝;⌜z'⌝]⋅
THEN EAuto 1
)
))
) }
1
.....aux.....
1. e : EuclideanPlane
2. a : Point
3. b : Point
4. c : Point
5. x : Point
6. y : Point
7. z : Point
8. i : Point
9. j : Point
10. k : Point
11. a' : Point
12. b' : Point
13. c' : Point
14. x' : Point
15. y' : Point
16. z' : Point
17. i' : Point
18. j' : Point
19. k' : Point
20. abc ≅a a'b'c'
21. p1 : Point
22. p2 : Point
23. d1 : Point
24. f1 : Point
25. abc ≅a ijp1
26. kjp1 ≅a xyz
27. j_p2_p1
28. out(j id1)
29. out(j kf1)
30. d1-p2-f1
31. p : Point
32. p' : Point
33. d' : Point
34. f' : Point
35. a'b'c' ≅a i'j'p
36. k'j'p ≅a x'y'z'
37. j'_p'_p
38. out(j' i'd')
39. out(j' k'f')
40. d'-p'-f'
41. i # jk
42. i' # j'k'
43. x # yz
44. xyz < x'y'z'
45. p' # j'k'
⊢ out(j' pp')
2
.....aux.....
1. e : EuclideanPlane
2. a : Point
3. b : Point
4. c : Point
5. x : Point
6. y : Point
7. z : Point
8. i : Point
9. j : Point
10. k : Point
11. a' : Point
12. b' : Point
13. c' : Point
14. x' : Point
15. y' : Point
16. z' : Point
17. i' : Point
18. j' : Point
19. k' : Point
20. abc ≅a a'b'c'
21. p1 : Point
22. p2 : Point
23. d1 : Point
24. f1 : Point
25. abc ≅a ijp1
26. kjp1 ≅a xyz
27. j_p2_p1
28. out(j id1)
29. out(j kf1)
30. d1-p2-f1
31. p : Point
32. p' : Point
33. d' : Point
34. f' : Point
35. a'b'c' ≅a i'j'p
36. k'j'p ≅a x'y'z'
37. j'_p'_p
38. out(j' i'd')
39. out(j' k'f')
40. d'-p'-f'
41. i # jk
42. i' # j'k'
43. x # yz
44. xyz < x'y'z'
45. p' # j'k'
⊢ out(y' x'x')
3
.....aux.....
1. e : EuclideanPlane
2. a : Point
3. b : Point
4. c : Point
5. x : Point
6. y : Point
7. z : Point
8. i : Point
9. j : Point
10. k : Point
11. a' : Point
12. b' : Point
13. c' : Point
14. x' : Point
15. y' : Point
16. z' : Point
17. i' : Point
18. j' : Point
19. k' : Point
20. abc ≅a a'b'c'
21. p1 : Point
22. p2 : Point
23. d1 : Point
24. f1 : Point
25. abc ≅a ijp1
26. kjp1 ≅a xyz
27. j_p2_p1
28. out(j id1)
29. out(j kf1)
30. d1-p2-f1
31. p : Point
32. p' : Point
33. d' : Point
34. f' : Point
35. a'b'c' ≅a i'j'p
36. k'j'p ≅a x'y'z'
37. j'_p'_p
38. out(j' i'd')
39. out(j' k'f')
40. d'-p'-f'
41. i # jk
42. i' # j'k'
43. x # yz
44. xyz < x'y'z'
45. p' # j'k'
46. k'j'p' ≅a x'y'z'
⊢ p'j'k' ≅a x'y'z'
4
1. e : EuclideanPlane
2. a : Point
3. b : Point
4. c : Point
5. x : Point
6. y : Point
7. z : Point
8. i : Point
9. j : Point
10. k : Point
11. a' : Point
12. b' : Point
13. c' : Point
14. x' : Point
15. y' : Point
16. z' : Point
17. i' : Point
18. j' : Point
19. k' : Point
20. abc ≅a a'b'c'
21. p1 : Point
22. p2 : Point
23. d1 : Point
24. f1 : Point
25. abc ≅a ijp1
26. kjp1 ≅a xyz
27. j_p2_p1
28. out(j id1)
29. out(j kf1)
30. d1-p2-f1
31. p : Point
32. p' : Point
33. d' : Point
34. f' : Point
35. a'b'c' ≅a i'j'p
36. k'j'p ≅a x'y'z'
37. j'_p'_p
38. out(j' i'd')
39. out(j' k'f')
40. d'-p'-f'
41. i # jk
42. i' # j'k'
43. x # yz
44. xyz < x'y'z'
45. p' # j'k'
46. xyz < p'j'k'
⊢ ijk < i'j'k'
Latex:
Latex:
\mforall{}e:EuclideanPlane. \mforall{}a,b,c,x,y,z,i,j,k,a',b',c',x',y',z',i',j',k':Point.
(abc \mcong{}\msuba{} a'b'c'
{}\mRightarrow{} abc + xyz \mcong{} ijk
{}\mRightarrow{} a'b'c' + x'y'z' \mcong{} i'j'k'
{}\mRightarrow{} i \# jk
{}\mRightarrow{} i' \# j'k'
{}\mRightarrow{} x \# yz
{}\mRightarrow{} xyz < x'y'z'
{}\mRightarrow{} ijk < i'j'k')
By
Latex:
(((Auto THEN Unfold `hp-angle-sum` -5)
THEN (Unfold `hp-angle-sum` -6 THEN ExRepD)
THEN (Assert p' \# j'k' BY
((InstLemma `out-preserves-lsep` [\mkleeneopen{}e\mkleeneclose{};\mkleeneopen{}j'\mkleeneclose{};\mkleeneopen{}i'\mkleeneclose{};\mkleeneopen{}k'\mkleeneclose{};\mkleeneopen{}d'\mkleeneclose{};\mkleeneopen{}f'\mkleeneclose{}]\mcdot{} THENA EAuto 1)
THEN (InstLemma `colinear-lsep` [\mkleeneopen{}e\mkleeneclose{};\mkleeneopen{}d'\mkleeneclose{};\mkleeneopen{}f'\mkleeneclose{};\mkleeneopen{}j'\mkleeneclose{};\mkleeneopen{}p'\mkleeneclose{}]\mcdot{} THENA Auto)
THEN InstLemma `out-preserves-lsep` [\mkleeneopen{}e\mkleeneclose{};\mkleeneopen{}j'\mkleeneclose{};\mkleeneopen{}p'\mkleeneclose{};\mkleeneopen{}f'\mkleeneclose{};\mkleeneopen{}p'\mkleeneclose{};\mkleeneopen{}k'\mkleeneclose{}]\mcdot{}
THEN EAuto 1)))
THEN (Assert xyz < p'j'k' BY
((InstLemma `geo-cong-angle-preserves-lt-angle2` [\mkleeneopen{}e\mkleeneclose{};\mkleeneopen{}x\mkleeneclose{};\mkleeneopen{}y\mkleeneclose{};\mkleeneopen{}z\mkleeneclose{};\mkleeneopen{}p'\mkleeneclose{};\mkleeneopen{}j'\mkleeneclose{};\mkleeneopen{}k'\mkleeneclose{};\mkleeneopen{}x'\mkleeneclose{};
\mkleeneopen{}y'\mkleeneclose{};\mkleeneopen{}z'\mkleeneclose{}]\mcdot{}
THEN Auto
)
THENA (InstLemma `out-preserves-angle-cong\_1` [\mkleeneopen{}e\mkleeneclose{};\mkleeneopen{}k'\mkleeneclose{};\mkleeneopen{}j'\mkleeneclose{};\mkleeneopen{}p\mkleeneclose{};\mkleeneopen{}x'\mkleeneclose{};\mkleeneopen{}y'\mkleeneclose{};\mkleeneopen{}z'\mkleeneclose{};\mkleeneopen{}k'\mkleeneclose{};
\mkleeneopen{}p'\mkleeneclose{};\mkleeneopen{}x'\mkleeneclose{};\mkleeneopen{}z'\mkleeneclose{}]\mcdot{}
THEN EAuto 1
)
))
)
Home
Index