Step
*
2
1
1
of Lemma
cong-angle-out-exists-iff
1. e : BasicGeometry
2. a : Point
3. b : Point
4. c : Point
5. x : Point
6. y : Point
7. z : Point
8. b ≠ a
9. b ≠ c
10. y ≠ x
11. y ≠ z
12. a' : Point
13. c' : Point
14. x' : Point
15. z' : Point
16. out(b a'a)
17. out(b c'c)
18. out(y x'x)
19. out(y z'z)
20. a' ≠ b
21. b ≠ c'
22. x' ≠ y
23. y ≠ z'
24. A : Point
25. C : Point
26. X : Point
27. Z : Point
28. b_a'_A
29. b_c'_C
30. y_x'_X
31. y_z'_Z
32. bA ≅ yX
33. bC ≅ yZ
34. AC ≅ XZ
⊢ abc ≅a xyz
BY
{ (InstLemma `cong-angle-out-aux2_1` [⌜e⌝;⌜a⌝;⌜b⌝;⌜c⌝;⌜x⌝;⌜y⌝;⌜z⌝;⌜A⌝;⌜C⌝;⌜X⌝;⌜Z⌝]⋅ THEN Auto) }
1
.....antecedent.....
1. e : BasicGeometry
2. a : Point
3. b : Point
4. c : Point
5. x : Point
6. y : Point
7. z : Point
8. b ≠ a
9. b ≠ c
10. y ≠ x
11. y ≠ z
12. a' : Point
13. c' : Point
14. x' : Point
15. z' : Point
16. out(b a'a)
17. out(b c'c)
18. out(y x'x)
19. out(y z'z)
20. a' ≠ b
21. b ≠ c'
22. x' ≠ y
23. y ≠ z'
24. A : Point
25. C : Point
26. X : Point
27. Z : Point
28. b_a'_A
29. b_c'_C
30. y_x'_X
31. y_z'_Z
32. bA ≅ yX
33. bC ≅ yZ
34. AC ≅ XZ
⊢ out(b Aa)
2
.....antecedent.....
1. e : BasicGeometry
2. a : Point
3. b : Point
4. c : Point
5. x : Point
6. y : Point
7. z : Point
8. b ≠ a
9. b ≠ c
10. y ≠ x
11. y ≠ z
12. a' : Point
13. c' : Point
14. x' : Point
15. z' : Point
16. out(b a'a)
17. out(b c'c)
18. out(y x'x)
19. out(y z'z)
20. a' ≠ b
21. b ≠ c'
22. x' ≠ y
23. y ≠ z'
24. A : Point
25. C : Point
26. X : Point
27. Z : Point
28. b_a'_A
29. b_c'_C
30. y_x'_X
31. y_z'_Z
32. bA ≅ yX
33. bC ≅ yZ
34. AC ≅ XZ
⊢ out(b Cc)
3
.....antecedent.....
1. e : BasicGeometry
2. a : Point
3. b : Point
4. c : Point
5. x : Point
6. y : Point
7. z : Point
8. b ≠ a
9. b ≠ c
10. y ≠ x
11. y ≠ z
12. a' : Point
13. c' : Point
14. x' : Point
15. z' : Point
16. out(b a'a)
17. out(b c'c)
18. out(y x'x)
19. out(y z'z)
20. a' ≠ b
21. b ≠ c'
22. x' ≠ y
23. y ≠ z'
24. A : Point
25. C : Point
26. X : Point
27. Z : Point
28. b_a'_A
29. b_c'_C
30. y_x'_X
31. y_z'_Z
32. bA ≅ yX
33. bC ≅ yZ
34. AC ≅ XZ
⊢ out(y Xx)
4
.....antecedent.....
1. e : BasicGeometry
2. a : Point
3. b : Point
4. c : Point
5. x : Point
6. y : Point
7. z : Point
8. b ≠ a
9. b ≠ c
10. y ≠ x
11. y ≠ z
12. a' : Point
13. c' : Point
14. x' : Point
15. z' : Point
16. out(b a'a)
17. out(b c'c)
18. out(y x'x)
19. out(y z'z)
20. a' ≠ b
21. b ≠ c'
22. x' ≠ y
23. y ≠ z'
24. A : Point
25. C : Point
26. X : Point
27. Z : Point
28. b_a'_A
29. b_c'_C
30. y_x'_X
31. y_z'_Z
32. bA ≅ yX
33. bC ≅ yZ
34. AC ≅ XZ
⊢ out(y Zz)
Latex:
Latex:
1. e : BasicGeometry
2. a : Point
3. b : Point
4. c : Point
5. x : Point
6. y : Point
7. z : Point
8. b \mneq{} a
9. b \mneq{} c
10. y \mneq{} x
11. y \mneq{} z
12. a' : Point
13. c' : Point
14. x' : Point
15. z' : Point
16. out(b a'a)
17. out(b c'c)
18. out(y x'x)
19. out(y z'z)
20. a' \mneq{} b
21. b \mneq{} c'
22. x' \mneq{} y
23. y \mneq{} z'
24. A : Point
25. C : Point
26. X : Point
27. Z : Point
28. b\_a'\_A
29. b\_c'\_C
30. y\_x'\_X
31. y\_z'\_Z
32. bA \mcong{} yX
33. bC \mcong{} yZ
34. AC \mcong{} XZ
\mvdash{} abc \mcong{}\msuba{} xyz
By
Latex:
(InstLemma `cong-angle-out-aux2\_1` [\mkleeneopen{}e\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{}X\mkleeneclose{};\mkleeneopen{}Z\mkleeneclose{}]\mcdot{} THEN Auto)
Home
Index