Step * 1 1 of Lemma rectangle-sides-cong


1. EuclideanPlane
2. Point
3. Point
4. Point
5. Point
6. Point
7. Point
8. ac
9. eb
10. ac  ⊥be
11. df  ⊥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
⊢ {ad ≅ fc ∧ dc ≅ fa}
BY
(((Assert eb BY Auto) THEN (Assert eb BY Auto)) THEN -1 THEN -2) }

1
1. EuclideanPlane
2. Point
3. Point
4. Point
5. Point
6. Point
7. Point
8. ac
9. eb
10. ac  ⊥be
11. df  ⊥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. leftof eb
24. leftof eb
⊢ {ad ≅ fc ∧ dc ≅ fa}

2
1. EuclideanPlane
2. Point
3. Point
4. Point
5. Point
6. Point
7. Point
8. ac
9. eb
10. ac  ⊥be
11. df  ⊥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. leftof be
24. leftof eb
⊢ {ad ≅ fc ∧ dc ≅ fa}

3
1. EuclideanPlane
2. Point
3. Point
4. Point
5. Point
6. Point
7. Point
8. ac
9. eb
10. ac  ⊥be
11. df  ⊥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. leftof eb
24. leftof be
⊢ {ad ≅ fc ∧ dc ≅ fa}

4
1. EuclideanPlane
2. Point
3. Point
4. Point
5. Point
6. Point
7. Point
8. ac
9. eb
10. ac  ⊥be
11. df  ⊥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. leftof be
24. leftof be
⊢ {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
\mvdash{}  \{ad  \mcong{}  fc  \mwedge{}  dc  \mcong{}  fa\}


By


Latex:
(((Assert  a  \#  eb  BY  Auto)  THEN  (Assert  f  \#  eb  BY  Auto))  THEN  D  -1  THEN  D  -2)




Home Index