Step
*
1
1
3
of Lemma
rectangle-sides-cong
1. g : EuclideanPlane
2. a : Point
3. b : Point
4. c : Point
5. d : Point
6. e : Point
7. f : Point
8. e # ac
9. f # eb
10. ac ⊥b be
11. df ⊥e eb
12. d-e-f
13. a-b-c
14. ab ≅ eb
15. bc ≅ eb
16. de ≅ eb
17. ef ≅ eb
18. ae ≅ ce
19. db ≅ fb
20. db ≅ ae
21. feb ≅a deb
22. abe ≅a cbe
23. a leftof eb
24. f leftof be
⊢ {ad ≅ fc ∧ dc ≅ fa}
BY
{ (((InstLemma `use-plane-sep_strict` [⌜g⌝;⌜e⌝;⌜b⌝;⌜a⌝;⌜f⌝]⋅ THENA Auto) THEN ExRepD)
THEN (Assert B(exb) BY
(gColinearCases (-2) THENA Auto))
) }
1
.....aux.....
1. g : EuclideanPlane
2. a : Point
3. b : Point
4. c : Point
5. d : Point
6. e : Point
7. f : Point
8. e # ac
9. f # eb
10. ac ⊥b be
11. df ⊥e eb
12. d-e-f
13. a-b-c
14. ab ≅ eb
15. bc ≅ eb
16. de ≅ eb
17. ef ≅ eb
18. ae ≅ ce
19. db ≅ fb
20. db ≅ ae
21. feb ≅a deb
22. abe ≅a cbe
23. a leftof eb
24. f leftof be
25. x : Point
26. Colinear(e;b;x)
27. a-x-f
28. e ≡ b
⊢ B(exb)
2
.....aux.....
1. g : EuclideanPlane
2. a : Point
3. b : Point
4. c : Point
5. d : Point
6. e : Point
7. f : Point
8. e # ac
9. f # eb
10. ac ⊥b be
11. df ⊥e eb
12. d-e-f
13. a-b-c
14. ab ≅ eb
15. bc ≅ eb
16. de ≅ eb
17. ef ≅ eb
18. ae ≅ ce
19. db ≅ fb
20. db ≅ ae
21. feb ≅a deb
22. abe ≅a cbe
23. a leftof eb
24. f leftof be
25. x : Point
26. Colinear(e;b;x)
27. a-x-f
28. b ≡ x
⊢ B(exb)
3
.....aux.....
1. g : EuclideanPlane
2. a : Point
3. b : Point
4. c : Point
5. d : Point
6. e : Point
7. f : Point
8. e # ac
9. f # eb
10. ac ⊥b be
11. df ⊥e eb
12. d-e-f
13. a-b-c
14. ab ≅ eb
15. bc ≅ eb
16. de ≅ eb
17. ef ≅ eb
18. ae ≅ ce
19. db ≅ fb
20. db ≅ ae
21. feb ≅a deb
22. abe ≅a cbe
23. a leftof eb
24. f leftof be
25. x : Point
26. Colinear(e;b;x)
27. a-x-f
28. x ≡ e
⊢ B(exb)
4
.....aux.....
1. g : EuclideanPlane
2. a : Point
3. b : Point
4. c : Point
5. d : Point
6. e : Point
7. f : Point
8. e # ac
9. f # eb
10. ac ⊥b be
11. df ⊥e eb
12. d-e-f
13. a-b-c
14. ab ≅ eb
15. bc ≅ eb
16. de ≅ eb
17. ef ≅ eb
18. ae ≅ ce
19. db ≅ fb
20. db ≅ ae
21. feb ≅a deb
22. abe ≅a cbe
23. a leftof eb
24. f leftof be
25. x : Point
26. Colinear(e;b;x)
27. a-x-f
28. e-b-x
⊢ B(exb)
5
.....aux.....
1. g : EuclideanPlane
2. a : Point
3. b : Point
4. c : Point
5. d : Point
6. e : Point
7. f : Point
8. e # ac
9. f # eb
10. ac ⊥b be
11. df ⊥e eb
12. d-e-f
13. a-b-c
14. ab ≅ eb
15. bc ≅ eb
16. de ≅ eb
17. ef ≅ eb
18. ae ≅ ce
19. db ≅ fb
20. db ≅ ae
21. feb ≅a deb
22. abe ≅a cbe
23. a leftof eb
24. f leftof be
25. x : Point
26. Colinear(e;b;x)
27. a-x-f
28. b-x-e
⊢ B(exb)
6
.....aux.....
1. g : EuclideanPlane
2. a : Point
3. b : Point
4. c : Point
5. d : Point
6. e : Point
7. f : Point
8. e # ac
9. f # eb
10. ac ⊥b be
11. df ⊥e eb
12. d-e-f
13. a-b-c
14. ab ≅ eb
15. bc ≅ eb
16. de ≅ eb
17. ef ≅ eb
18. ae ≅ ce
19. db ≅ fb
20. db ≅ ae
21. feb ≅a deb
22. abe ≅a cbe
23. a leftof eb
24. f leftof be
25. x : Point
26. Colinear(e;b;x)
27. a-x-f
28. x-e-b
⊢ B(exb)
7
1. g : EuclideanPlane
2. a : Point
3. b : Point
4. c : Point
5. d : Point
6. e : Point
7. f : Point
8. e # ac
9. f # eb
10. ac ⊥b be
11. df ⊥e eb
12. d-e-f
13. a-b-c
14. ab ≅ eb
15. bc ≅ eb
16. de ≅ eb
17. ef ≅ eb
18. ae ≅ ce
19. db ≅ fb
20. db ≅ ae
21. feb ≅a deb
22. abe ≅a cbe
23. a leftof eb
24. f leftof be
25. x : Point
26. Colinear(e;b;x)
27. a-x-f
28. B(exb)
⊢ ad ≅ fc ∧ dc ≅ fa
Latex:
Latex:
1. g : EuclideanPlane
2. a : Point
3. b : Point
4. c : Point
5. d : Point
6. e : Point
7. f : Point
8. e \# ac
9. f \# eb
10. ac \mbot{}b be
11. df \mbot{}e eb
12. d-e-f
13. a-b-c
14. ab \mcong{} eb
15. bc \mcong{} eb
16. de \mcong{} eb
17. ef \mcong{} eb
18. ae \mcong{} ce
19. db \mcong{} fb
20. db \mcong{} ae
21. feb \mcong{}\msuba{} deb
22. abe \mcong{}\msuba{} cbe
23. a leftof eb
24. f leftof be
\mvdash{} \{ad \mcong{} fc \mwedge{} dc \mcong{} fa\}
By
Latex:
(((InstLemma `use-plane-sep\_strict` [\mkleeneopen{}g\mkleeneclose{};\mkleeneopen{}e\mkleeneclose{};\mkleeneopen{}b\mkleeneclose{};\mkleeneopen{}a\mkleeneclose{};\mkleeneopen{}f\mkleeneclose{}]\mcdot{} THENA Auto) THEN ExRepD)
THEN (Assert B(exb) BY
(gColinearCases (-2) THENA Auto))
)
Home
Index