Proof of Nuprl Lemma : rectangle-sides-cong

Step * 1 1 4 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 be
24. f leftof be
⊢ {ad ≅ fc ∧ dc ≅ fa}
BY
{ ((Assert d leftof eb BY

          (InstLemma  `left-between-implies-right1` [⌜g⌝;⌜b⌝;⌜e⌝;⌜f⌝;⌜d⌝]⋅ THEN Auto))

   THEN ((InstLemma  `use-plane-sep_strict` [⌜g⌝;⌜e⌝;⌜b⌝;⌜d⌝;⌜a⌝]⋅ 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 be
24. f leftof be
25. d leftof eb
26. x : Point
27. Colinear(e;b;x)
28. d-x-a
29. 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 be
24. f leftof be
25. d leftof eb
26. x : Point
27. Colinear(e;b;x)
28. d-x-a
29. 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 be
24. f leftof be
25. d leftof eb
26. x : Point
27. Colinear(e;b;x)
28. d-x-a
29. 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 be
24. f leftof be
25. d leftof eb
26. x : Point
27. Colinear(e;b;x)
28. d-x-a
29. 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 be
24. f leftof be
25. d leftof eb
26. x : Point
27. Colinear(e;b;x)
28. d-x-a
29. 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 be
24. f leftof be
25. d leftof eb
26. x : Point
27. Colinear(e;b;x)
28. d-x-a
29. 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 be
24. f leftof be
25. d leftof eb
26. x : Point
27. Colinear(e;b;x)
28. d-x-a
29. 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 be 24. f leftof be \mvdash{} \{ad \mcong{} fc \mwedge{} dc \mcong{} fa\} By Latex: ((Assert d leftof eb BY (InstLemma `left-between-implies-right1` [\mkleeneopen{}g\mkleeneclose{};\mkleeneopen{}b\mkleeneclose{};\mkleeneopen{}e\mkleeneclose{};\mkleeneopen{}f\mkleeneclose{};\mkleeneopen{}d\mkleeneclose{}]\mcdot{} THEN Auto)) THEN ((InstLemma `use-plane-sep\_strict` [\mkleeneopen{}g\mkleeneclose{};\mkleeneopen{}e\mkleeneclose{};\mkleeneopen{}b\mkleeneclose{};\mkleeneopen{}d\mkleeneclose{};\mkleeneopen{}a\mkleeneclose{}]\mcdot{} THENA Auto) THEN ExRepD) THEN (Assert B(exb) BY (gColinearCases (-2) THENA Auto))) Home Index