Step
*
3
2
3
1
of Lemma
opp-side_half-plane-angle-congruence-lemma
1. e : EuclideanPlane
2. b : Point
3. p : Point
4. b' : Point
5. p' : Point
6. a : Point
7. c : Point
8. a' : Point
9. c' : Point
10. d : Point
11. a leftof bp
12. c leftof pb
13. a' leftof b'p'
14. c' leftof p'b'
15. abp ≅a a'b'p'
16. pbc ≅a p'b'c'
17. a-d-c
18. out(b dp)
19. b ≠ d
20. a'' : Point
21. c'' : Point
22. out(b' a'a'')
23. out(b' c'c'')
24. ba ≅ b'a''
25. bc ≅ b'c''
26. d'' : Point
27. out(b' d''p')
28. b' ≠ d''
29. b'd'' ≅ bd
30. ba ≅ b'a''
31. bc ≅ b'c''
32. bd ≅ b'd''
33. ad ≅ a''d''
34. dc ≅ d''c''
35. out(b' d''p')
36. C : Point
37. a''-d''-C
38. d''C ≅ dc
39. bc ≅ b'C
⊢ a''_d''_c''
BY
{ (InstLemma `Euclid-Prop7` [⌜e⌝;⌜d''⌝;⌜b'⌝;⌜C⌝;⌜c''⌝]⋅ THENA Auto) }
1
.....wf.....
1. e : EuclideanPlane
2. b : Point
3. p : Point
4. b' : Point
5. p' : Point
6. a : Point
7. c : Point
8. a' : Point
9. c' : Point
10. d : Point
11. a leftof bp
12. c leftof pb
13. a' leftof b'p'
14. c' leftof p'b'
15. abp ≅a a'b'p'
16. pbc ≅a p'b'c'
17. a-d-c
18. out(b dp)
19. b ≠ d
20. a'' : Point
21. c'' : Point
22. out(b' a'a'')
23. out(b' c'c'')
24. ba ≅ b'a''
25. bc ≅ b'c''
26. d'' : Point
27. out(b' d''p')
28. b' ≠ d''
29. b'd'' ≅ bd
30. ba ≅ b'a''
31. bc ≅ b'c''
32. bd ≅ b'd''
33. ad ≅ a''d''
34. dc ≅ d''c''
35. out(b' d''p')
36. C : Point
37. a''-d''-C
38. d''C ≅ dc
39. bc ≅ b'C
⊢ C ∈ {c:Point| c leftof d''b'}
2
.....wf.....
1. e : EuclideanPlane
2. b : Point
3. p : Point
4. b' : Point
5. p' : Point
6. a : Point
7. c : Point
8. a' : Point
9. c' : Point
10. d : Point
11. a leftof bp
12. c leftof pb
13. a' leftof b'p'
14. c' leftof p'b'
15. abp ≅a a'b'p'
16. pbc ≅a p'b'c'
17. a-d-c
18. out(b dp)
19. b ≠ d
20. a'' : Point
21. c'' : Point
22. out(b' a'a'')
23. out(b' c'c'')
24. ba ≅ b'a''
25. bc ≅ b'c''
26. d'' : Point
27. out(b' d''p')
28. b' ≠ d''
29. b'd'' ≅ bd
30. ba ≅ b'a''
31. bc ≅ b'c''
32. bd ≅ b'd''
33. ad ≅ a''d''
34. dc ≅ d''c''
35. out(b' d''p')
36. C : Point
37. a''-d''-C
38. d''C ≅ dc
39. bc ≅ b'C
⊢ c'' ∈ {p:Point| p leftof d''b'}
3
1. e : EuclideanPlane
2. b : Point
3. p : Point
4. b' : Point
5. p' : Point
6. a : Point
7. c : Point
8. a' : Point
9. c' : Point
10. d : Point
11. a leftof bp
12. c leftof pb
13. a' leftof b'p'
14. c' leftof p'b'
15. abp ≅a a'b'p'
16. pbc ≅a p'b'c'
17. a-d-c
18. out(b dp)
19. b ≠ d
20. a'' : Point
21. c'' : Point
22. out(b' a'a'')
23. out(b' c'c'')
24. ba ≅ b'a''
25. bc ≅ b'c''
26. d'' : Point
27. out(b' d''p')
28. b' ≠ d''
29. b'd'' ≅ bd
30. ba ≅ b'a''
31. bc ≅ b'c''
32. bd ≅ b'd''
33. ad ≅ a''d''
34. dc ≅ d''c''
35. out(b' d''p')
36. C : Point
37. a''-d''-C
38. d''C ≅ dc
39. bc ≅ b'C
40. C ≡ c''
⊢ a''_d''_c''
Latex:
Latex:
1. e : EuclideanPlane
2. b : Point
3. p : Point
4. b' : Point
5. p' : Point
6. a : Point
7. c : Point
8. a' : Point
9. c' : Point
10. d : Point
11. a leftof bp
12. c leftof pb
13. a' leftof b'p'
14. c' leftof p'b'
15. abp \mcong{}\msuba{} a'b'p'
16. pbc \mcong{}\msuba{} p'b'c'
17. a-d-c
18. out(b dp)
19. b \mneq{} d
20. a'' : Point
21. c'' : Point
22. out(b' a'a'')
23. out(b' c'c'')
24. ba \mcong{} b'a''
25. bc \mcong{} b'c''
26. d'' : Point
27. out(b' d''p')
28. b' \mneq{} d''
29. b'd'' \mcong{} bd
30. ba \mcong{} b'a''
31. bc \mcong{} b'c''
32. bd \mcong{} b'd''
33. ad \mcong{} a''d''
34. dc \mcong{} d''c''
35. out(b' d''p')
36. C : Point
37. a''-d''-C
38. d''C \mcong{} dc
39. bc \mcong{} b'C
\mvdash{} a''\_d''\_c''
By
Latex:
(InstLemma `Euclid-Prop7` [\mkleeneopen{}e\mkleeneclose{};\mkleeneopen{}d''\mkleeneclose{};\mkleeneopen{}b'\mkleeneclose{};\mkleeneopen{}C\mkleeneclose{};\mkleeneopen{}c''\mkleeneclose{}]\mcdot{} THENA Auto)
Home
Index