---

Step * 1 1 2 1 2 1 1 of Lemma rv-be-five-segment


1. a : ℝ^2
2. b : ℝ^2
3. c : ℝ^2
4. d : ℝ^2
5. A : ℝ^2
6. B : ℝ^2
7. C : ℝ^2
8. D : ℝ^2
9. (cd=CD) supposing (bd=BD and ad=AD and bc=BC and ab=AB and A-B-C and a-b-c)
10. a ≠ b
11. a_b_c
12. A_B_C
13. ab=AB
14. bc=CC
15. ad=AD
16. bd=BD
17. a-b-c
18. ¬A-B-C
19. A ≠ B
20. req-vec(2;B;C)
⊢ cd=CD
BY
{ ((Assert CC=bc BY (ParallelOp -7 THEN Auto)) THEN (FLemma `rv-congruent-implies-eq` [-1] THENA Auto)) }

1
1. a : ℝ^2
2. b : ℝ^2
3. c : ℝ^2
4. d : ℝ^2
5. A : ℝ^2
6. B : ℝ^2
7. C : ℝ^2
8. D : ℝ^2
9. (cd=CD) supposing (bd=BD and ad=AD and bc=BC and ab=AB and A-B-C and a-b-c)
10. a ≠ b
11. a_b_c
12. A_B_C
13. ab=AB
14. bc=CC
15. ad=AD
16. bd=BD
17. a-b-c
18. ¬A-B-C
19. A ≠ B
20. req-vec(2;B;C)
21. CC=bc
22. req-vec(2;b;c)
⊢ cd=CD

---

Latex:

---

Latex:

1.  a  :  \mBbbR{}\^{}2
2.  b  :  \mBbbR{}\^{}2
3.  c  :  \mBbbR{}\^{}2
4.  d  :  \mBbbR{}\^{}2
5.  A  :  \mBbbR{}\^{}2
6.  B  :  \mBbbR{}\^{}2
7.  C  :  \mBbbR{}\^{}2
8.  D  :  \mBbbR{}\^{}2
9.  (cd=CD)  supposing  (bd=BD  and  ad=AD  and  bc=BC  and  ab=AB  and  A-B-C  and  a-b-c)
10.  a  \mneq{}  b
11.  a\_b\_c
12.  A\_B\_C
13.  ab=AB
14.  bc=CC
15.  ad=AD
16.  bd=BD
17.  a-b-c
18.  \mneg{}A-B-C
19.  A  \mneq{}  B
20.  req-vec(2;B;C)
\mvdash{}  cd=CD


By

---

Latex:
((Assert  CC=bc  BY
                (ParallelOp  -7  THEN  Auto))
  THEN  (FLemma  `rv-congruent-implies-eq`  [-1]  THENA  Auto)
  )

---

Home Index