Step
*
1
4
of Lemma
cong-angle-out-aux2_1
1. g : BasicGeometry
2. a : Point
3. b : Point
4. c : Point
5. d : Point
6. e : Point
7. f : Point
8. a' : Point
9. c' : Point
10. d' : Point
11. f' : Point
12. a'c' ≅ d'f'
13. out(b a'a)
14. out(b c'c)
15. out(e d'd)
16. out(e f'f)
17. ba' ≅ ed'
18. bc' ≅ ef'
19. A : Point
20. b-a-A
21. aA ≅ ed
22. C : Point
23. b-c-C
24. cC ≅ ef
25. D : Point
26. e-d-D
27. dD ≅ ba
28. F : Point
29. e-f-F
30. fF ≅ bc
31. b_a_A
32. b_c_C
33. e_d_D
34. e_f_F
35. bA ≅ eD
36. bC ≅ eF
37. Colinear(b;a';A)
38. b-a'-A
⊢ AC ≅ DF
BY
{ (((InstLemma `geo-between-out-implies-out` [⌜g⌝;⌜e⌝;⌜D⌝;⌜d⌝;⌜d'⌝]⋅ THEN EAuto 1)
THEN InstLemma `geo-cong-preserves-strict-bet-out` [⌜g⌝;⌜b⌝;⌜a'⌝;⌜A⌝;⌜e⌝;⌜d'⌝;⌜D⌝]⋅
THEN Auto)
THEN (Assert Colinear(b;c';C) BY
Auto)
THEN gColinearCases (-1)
THEN Auto) }
1
1. g : BasicGeometry
2. a : Point
3. b : Point
4. c : Point
5. d : Point
6. e : Point
7. f : Point
8. a' : Point
9. c' : Point
10. d' : Point
11. f' : Point
12. a'c' ≅ d'f'
13. out(b a'a)
14. out(b c'c)
15. out(e d'd)
16. out(e f'f)
17. ba' ≅ ed'
18. bc' ≅ ef'
19. A : Point
20. b-a-A
21. aA ≅ ed
22. C : Point
23. b-c-C
24. cC ≅ ef
25. D : Point
26. e-d-D
27. dD ≅ ba
28. F : Point
29. e-f-F
30. fF ≅ bc
31. b_a_A
32. b_c_C
33. e_d_D
34. e_f_F
35. bA ≅ eD
36. bC ≅ eF
37. Colinear(b;a';A)
38. b-a'-A
39. out(e d'D)
40. e-d'-D
41. Colinear(b;c';C)
42. b ≡ c'
⊢ AC ≅ DF
2
1. g : BasicGeometry
2. a : Point
3. b : Point
4. c : Point
5. d : Point
6. e : Point
7. f : Point
8. a' : Point
9. c' : Point
10. d' : Point
11. f' : Point
12. a'c' ≅ d'f'
13. out(b a'a)
14. out(b c'c)
15. out(e d'd)
16. out(e f'f)
17. ba' ≅ ed'
18. bc' ≅ ef'
19. A : Point
20. b-a-A
21. aA ≅ ed
22. C : Point
23. b-c-C
24. cC ≅ ef
25. D : Point
26. e-d-D
27. dD ≅ ba
28. F : Point
29. e-f-F
30. fF ≅ bc
31. b_a_A
32. b_c_C
33. e_d_D
34. e_f_F
35. bA ≅ eD
36. bC ≅ eF
37. Colinear(b;a';A)
38. b-a'-A
39. out(e d'D)
40. e-d'-D
41. Colinear(b;c';C)
42. c' ≡ C
⊢ AC ≅ DF
3
1. g : BasicGeometry
2. a : Point
3. b : Point
4. c : Point
5. d : Point
6. e : Point
7. f : Point
8. a' : Point
9. c' : Point
10. d' : Point
11. f' : Point
12. a'c' ≅ d'f'
13. out(b a'a)
14. out(b c'c)
15. out(e d'd)
16. out(e f'f)
17. ba' ≅ ed'
18. bc' ≅ ef'
19. A : Point
20. b-a-A
21. aA ≅ ed
22. C : Point
23. b-c-C
24. cC ≅ ef
25. D : Point
26. e-d-D
27. dD ≅ ba
28. F : Point
29. e-f-F
30. fF ≅ bc
31. b_a_A
32. b_c_C
33. e_d_D
34. e_f_F
35. bA ≅ eD
36. bC ≅ eF
37. Colinear(b;a';A)
38. b-a'-A
39. out(e d'D)
40. e-d'-D
41. Colinear(b;c';C)
42. C ≡ b
⊢ AC ≅ DF
4
1. g : BasicGeometry
2. a : Point
3. b : Point
4. c : Point
5. d : Point
6. e : Point
7. f : Point
8. a' : Point
9. c' : Point
10. d' : Point
11. f' : Point
12. a'c' ≅ d'f'
13. out(b a'a)
14. out(b c'c)
15. out(e d'd)
16. out(e f'f)
17. ba' ≅ ed'
18. bc' ≅ ef'
19. A : Point
20. b-a-A
21. aA ≅ ed
22. C : Point
23. b-c-C
24. cC ≅ ef
25. D : Point
26. e-d-D
27. dD ≅ ba
28. F : Point
29. e-f-F
30. fF ≅ bc
31. b_a_A
32. b_c_C
33. e_d_D
34. e_f_F
35. bA ≅ eD
36. bC ≅ eF
37. Colinear(b;a';A)
38. b-a'-A
39. out(e d'D)
40. e-d'-D
41. Colinear(b;c';C)
42. b-c'-C
⊢ AC ≅ DF
5
1. g : BasicGeometry
2. a : Point
3. b : Point
4. c : Point
5. d : Point
6. e : Point
7. f : Point
8. a' : Point
9. c' : Point
10. d' : Point
11. f' : Point
12. a'c' ≅ d'f'
13. out(b a'a)
14. out(b c'c)
15. out(e d'd)
16. out(e f'f)
17. ba' ≅ ed'
18. bc' ≅ ef'
19. A : Point
20. b-a-A
21. aA ≅ ed
22. C : Point
23. b-c-C
24. cC ≅ ef
25. D : Point
26. e-d-D
27. dD ≅ ba
28. F : Point
29. e-f-F
30. fF ≅ bc
31. b_a_A
32. b_c_C
33. e_d_D
34. e_f_F
35. bA ≅ eD
36. bC ≅ eF
37. Colinear(b;a';A)
38. b-a'-A
39. out(e d'D)
40. e-d'-D
41. Colinear(b;c';C)
42. c'-C-b
⊢ AC ≅ DF
6
1. g : BasicGeometry
2. a : Point
3. b : Point
4. c : Point
5. d : Point
6. e : Point
7. f : Point
8. a' : Point
9. c' : Point
10. d' : Point
11. f' : Point
12. a'c' ≅ d'f'
13. out(b a'a)
14. out(b c'c)
15. out(e d'd)
16. out(e f'f)
17. ba' ≅ ed'
18. bc' ≅ ef'
19. A : Point
20. b-a-A
21. aA ≅ ed
22. C : Point
23. b-c-C
24. cC ≅ ef
25. D : Point
26. e-d-D
27. dD ≅ ba
28. F : Point
29. e-f-F
30. fF ≅ bc
31. b_a_A
32. b_c_C
33. e_d_D
34. e_f_F
35. bA ≅ eD
36. bC ≅ eF
37. Colinear(b;a';A)
38. b-a'-A
39. out(e d'D)
40. e-d'-D
41. Colinear(b;c';C)
42. C-b-c'
⊢ AC ≅ DF
Latex:
Latex:
1. g : BasicGeometry
2. a : Point
3. b : Point
4. c : Point
5. d : Point
6. e : Point
7. f : Point
8. a' : Point
9. c' : Point
10. d' : Point
11. f' : Point
12. a'c' \mcong{} d'f'
13. out(b a'a)
14. out(b c'c)
15. out(e d'd)
16. out(e f'f)
17. ba' \mcong{} ed'
18. bc' \mcong{} ef'
19. A : Point
20. b-a-A
21. aA \mcong{} ed
22. C : Point
23. b-c-C
24. cC \mcong{} ef
25. D : Point
26. e-d-D
27. dD \mcong{} ba
28. F : Point
29. e-f-F
30. fF \mcong{} bc
31. b\_a\_A
32. b\_c\_C
33. e\_d\_D
34. e\_f\_F
35. bA \mcong{} eD
36. bC \mcong{} eF
37. Colinear(b;a';A)
38. b-a'-A
\mvdash{} AC \mcong{} DF
By
Latex:
(((InstLemma `geo-between-out-implies-out` [\mkleeneopen{}g\mkleeneclose{};\mkleeneopen{}e\mkleeneclose{};\mkleeneopen{}D\mkleeneclose{};\mkleeneopen{}d\mkleeneclose{};\mkleeneopen{}d'\mkleeneclose{}]\mcdot{} THEN EAuto 1)
THEN InstLemma `geo-cong-preserves-strict-bet-out` [\mkleeneopen{}g\mkleeneclose{};\mkleeneopen{}b\mkleeneclose{};\mkleeneopen{}a'\mkleeneclose{};\mkleeneopen{}A\mkleeneclose{};\mkleeneopen{}e\mkleeneclose{};\mkleeneopen{}d'\mkleeneclose{};\mkleeneopen{}D\mkleeneclose{}]\mcdot{}
THEN Auto)
THEN (Assert Colinear(b;c';C) BY
Auto)
THEN gColinearCases (-1)
THEN Auto)
Home
Index