---

Step * 1 1 1 1 1 1 1 1 2 1 2 1 2 1 2 1 1 of Lemma perp-in-congruence


1. e : EuclideanPlane
2. b : Point
3. a : Point
4. B : Point
5. A : Point
6. c : Point
7. d : Point
8. C : Point
9. D : Point
10. c # ba
11. C # BA
12. ba ≅ BA
13. bc ≅ BC
14. ac ≅ AC
15. Colinear(B;A;D)
16. RBDC
17. RADC
18. ba  ⊥d dc
19. E : Point
20. bd ≅ BE
21. da ≅ EA
22. ab ≅ AB
23. Colinear(B;E;A)
24. ¬cad ≅a CAE
25. cab ≅a CAB
26. Colinear(a;b;d)
27. d_a_b
28. E_A_B
29. a ≠ d
⊢ RAEC
BY
{ (D -6
   THEN InstLemma `supplementary-angles-preserve-congruence` [⌜e⌝;⌜b⌝;⌜a⌝;⌜c⌝;⌜B⌝;⌜A⌝;⌜C⌝;⌜d⌝;⌜E⌝]⋅
   THEN Auto
   THEN skip{EasyGeometry}) }

1
.....antecedent..... 
1. e : EuclideanPlane
2. b : Point
3. a : Point
4. B : Point
5. A : Point
6. c : Point
7. d : Point
8. C : Point
9. D : Point
10. c # ba
11. C # BA
12. ba ≅ BA
13. bc ≅ BC
14. ac ≅ AC
15. Colinear(B;A;D)
16. RBDC
17. RADC
18. ba  ⊥d dc
19. E : Point
20. bd ≅ BE
21. da ≅ EA
22. ab ≅ AB
23. Colinear(B;E;A)
24. cab ≅a CAB
25. Colinear(a;b;d)
26. d_a_b
27. E_A_B
28. a ≠ d
⊢ bac ≅a BAC

2
.....antecedent..... 
1. e : EuclideanPlane
2. b : Point
3. a : Point
4. B : Point
5. A : Point
6. c : Point
7. d : Point
8. C : Point
9. D : Point
10. c # ba
11. C # BA
12. ba ≅ BA
13. bc ≅ BC
14. ac ≅ AC
15. Colinear(B;A;D)
16. RBDC
17. RADC
18. ba  ⊥d dc
19. E : Point
20. bd ≅ BE
21. da ≅ EA
22. ab ≅ AB
23. Colinear(B;E;A)
24. cab ≅a CAB
25. Colinear(a;b;d)
26. d_a_b
27. E_A_B
28. a ≠ d
⊢ b-a-d

3
.....antecedent..... 
1. e : EuclideanPlane
2. b : Point
3. a : Point
4. B : Point
5. A : Point
6. c : Point
7. d : Point
8. C : Point
9. D : Point
10. c # ba
11. C # BA
12. ba ≅ BA
13. bc ≅ BC
14. ac ≅ AC
15. Colinear(B;A;D)
16. RBDC
17. RADC
18. ba  ⊥d dc
19. E : Point
20. bd ≅ BE
21. da ≅ EA
22. ab ≅ AB
23. Colinear(B;E;A)
24. cab ≅a CAB
25. Colinear(a;b;d)
26. d_a_b
27. E_A_B
28. a ≠ d
⊢ B-A-E

4
1. e : EuclideanPlane
2. b : Point
3. a : Point
4. B : Point
5. A : Point
6. c : Point
7. d : Point
8. C : Point
9. D : Point
10. c # ba
11. C # BA
12. ba ≅ BA
13. bc ≅ BC
14. ac ≅ AC
15. Colinear(B;A;D)
16. RBDC
17. RADC
18. ba  ⊥d dc
19. E : Point
20. bd ≅ BE
21. da ≅ EA
22. ab ≅ AB
23. Colinear(B;E;A)
24. cab ≅a CAB
25. Colinear(a;b;d)
26. d_a_b
27. E_A_B
28. a ≠ d
29. dac ≅a EAC
⊢ cad ≅a CAE

---

Latex:

---

Latex:

1.  e  :  EuclideanPlane
2.  b  :  Point
3.  a  :  Point
4.  B  :  Point
5.  A  :  Point
6.  c  :  Point
7.  d  :  Point
8.  C  :  Point
9.  D  :  Point
10.  c  \#  ba
11.  C  \#  BA
12.  ba  \mcong{}  BA
13.  bc  \mcong{}  BC
14.  ac  \mcong{}  AC
15.  Colinear(B;A;D)
16.  RBDC
17.  RADC
18.  ba    \mbot{}d  dc
19.  E  :  Point
20.  bd  \mcong{}  BE
21.  da  \mcong{}  EA
22.  ab  \mcong{}  AB
23.  Colinear(B;E;A)
24.  \mneg{}cad  \mcong{}\msuba{}  CAE
25.  cab  \mcong{}\msuba{}  CAB
26.  Colinear(a;b;d)
27.  d\_a\_b
28.  E\_A\_B
29.  a  \mneq{}  d
\mvdash{}  RAEC


By

---

Latex:
(D  -6
  THEN  InstLemma  `supplementary-angles-preserve-congruence`  [\mkleeneopen{}e\mkleeneclose{};\mkleeneopen{}b\mkleeneclose{};\mkleeneopen{}a\mkleeneclose{};\mkleeneopen{}c\mkleeneclose{};\mkleeneopen{}B\mkleeneclose{};\mkleeneopen{}A\mkleeneclose{};\mkleeneopen{}C\mkleeneclose{};\mkleeneopen{}d\mkleeneclose{};\mkleeneopen{}E\mkleeneclose{}]\mcdot{}
  THEN  Auto
  THEN  skip\{EasyGeometry\})

---

Home Index