Step
*
1
1
1
1
of Lemma
eu-seg-extend_functionality
.....antecedent.....
1. e : EuclideanStructure@i'
2. ∀[a,b:Point]. ab=ba@i'
3. ∀[a,b,p,q,r,s:Point]. (pq=rs) supposing (ab=rs and ab=pq)@i'
4. ∀[a,b,c:Point]. a = b ∈ Point supposing ab=cc@i'
5. ∀[q:Point]. ∀[a:{a:Point| ¬(q = a ∈ Point)} ]. ∀[b,c:Point]. (q_a_(extend qa by bc) ∧ a(extend qa by bc)=bc)@i'
6. ∀[a,b,c,d,A,B,C,D:Point].
(cd=CD) supposing (bd=BD and ad=AD and bc=BC and ab=AB and A_B_C and a_b_c and (¬(a = b ∈ Point)))@i'
7. ∀[a,b:Point]. (¬a-b-a)@i'
8. ∀[a,b:Point]. ∀[c:{c:Point| ¬Colinear(a;b;c)} ]. ∀[p:{p:Point| a-p-c} ]. ∀[q:{q:Point| b_q_c} ].
let x = eu-inner-pasch(e;a;b;c;p;q) in
p-x-b ∧ q-x-a@i'
9. ∀[a,b,p,q,r:Point]. (Colinear(p;q;r)) supposing (ra=rb and qa=qb and pa=pb and (¬(a = b ∈ Point)))@i'
10. ∀[a,b:Point]. ∀[c:{c:Point| ¬Colinear(a;b;c)} ]. let x = middle(a;b;c) in ax=bx ∧ ax=cx@i'
11. ∀[a,b:Point]. ∀[x:{x:Point| a_x_b} ]. ∀[y:{y:Point| a_b_y} ]. ∀[p:{p:Point| ap=ax} ]. ∀[q:{q:Point|
aq=ay
∧ (¬(q = p ∈ Point))} ].
let uv = intersect pq (at radius xy) with Oab in
afst(uv)=ab
∧ asnd(uv)=ab
∧ p_fst(uv)_q
∧ snd(uv)_p_q
∧ ¬((fst(uv)) = (snd(uv)) ∈ Point) supposing ¬(x = b ∈ Point)@i'
12. ∀[a,b,c:Point]. c-b-a supposing a-b-c@i'
13. ∀[a,b,c,d:Point]. (a-b-c) supposing (b-c-d and a-b-d)@i'
14. s1 : ProperSegment
15. s2 : ProperSegment
16. t1 : Segment
17. t2 : Segment
18. s1 ≡ s2
19. t1 ≡ t2
20. e ∈ EuclideanPlane
21. ¬(s1.1 = s1.2 ∈ Point)
22. ¬(s2.1 = s2.2 ∈ Point)
23. v : Point@i
24. (extend s1.1s1.2 by t1.1t1.2) = v ∈ Point@i
25. v1 : Point@i
26. (extend s2.1s2.2 by t2.1t2.2) = v1 ∈ Point@i
27. s1.1_s1.2_v@i
28. s1.2v=t1.1t1.2@i
29. s2.1_s2.2_v1@i
30. s2.2v1=t2.1t2.2@i
⊢ s1.2v=s2.2v1
BY
{ (Assert t1.1t1.2=t2.1t2.2 BY
Auto) }
1
1. e : EuclideanStructure@i'
2. ∀[a,b:Point]. ab=ba@i'
3. ∀[a,b,p,q,r,s:Point]. (pq=rs) supposing (ab=rs and ab=pq)@i'
4. ∀[a,b,c:Point]. a = b ∈ Point supposing ab=cc@i'
5. ∀[q:Point]. ∀[a:{a:Point| ¬(q = a ∈ Point)} ]. ∀[b,c:Point]. (q_a_(extend qa by bc) ∧ a(extend qa by bc)=bc)@i'
6. ∀[a,b,c,d,A,B,C,D:Point].
(cd=CD) supposing (bd=BD and ad=AD and bc=BC and ab=AB and A_B_C and a_b_c and (¬(a = b ∈ Point)))@i'
7. ∀[a,b:Point]. (¬a-b-a)@i'
8. ∀[a,b:Point]. ∀[c:{c:Point| ¬Colinear(a;b;c)} ]. ∀[p:{p:Point| a-p-c} ]. ∀[q:{q:Point| b_q_c} ].
let x = eu-inner-pasch(e;a;b;c;p;q) in
p-x-b ∧ q-x-a@i'
9. ∀[a,b,p,q,r:Point]. (Colinear(p;q;r)) supposing (ra=rb and qa=qb and pa=pb and (¬(a = b ∈ Point)))@i'
10. ∀[a,b:Point]. ∀[c:{c:Point| ¬Colinear(a;b;c)} ]. let x = middle(a;b;c) in ax=bx ∧ ax=cx@i'
11. ∀[a,b:Point]. ∀[x:{x:Point| a_x_b} ]. ∀[y:{y:Point| a_b_y} ]. ∀[p:{p:Point| ap=ax} ]. ∀[q:{q:Point|
aq=ay
∧ (¬(q = p ∈ Point))} ].
let uv = intersect pq (at radius xy) with Oab in
afst(uv)=ab
∧ asnd(uv)=ab
∧ p_fst(uv)_q
∧ snd(uv)_p_q
∧ ¬((fst(uv)) = (snd(uv)) ∈ Point) supposing ¬(x = b ∈ Point)@i'
12. ∀[a,b,c:Point]. c-b-a supposing a-b-c@i'
13. ∀[a,b,c,d:Point]. (a-b-c) supposing (b-c-d and a-b-d)@i'
14. s1 : ProperSegment
15. s2 : ProperSegment
16. t1 : Segment
17. t2 : Segment
18. s1 ≡ s2
19. t1 ≡ t2
20. e ∈ EuclideanPlane
21. ¬(s1.1 = s1.2 ∈ Point)
22. ¬(s2.1 = s2.2 ∈ Point)
23. v : Point@i
24. (extend s1.1s1.2 by t1.1t1.2) = v ∈ Point@i
25. v1 : Point@i
26. (extend s2.1s2.2 by t2.1t2.2) = v1 ∈ Point@i
27. s1.1_s1.2_v@i
28. s1.2v=t1.1t1.2@i
29. s2.1_s2.2_v1@i
30. s2.2v1=t2.1t2.2@i
31. t1.1t1.2=t2.1t2.2
⊢ s1.2v=s2.2v1
Latex:
Latex:
.....antecedent.....
1. e : EuclideanStructure@i'
2. \mforall{}[a,b:Point]. ab=ba@i'
3. \mforall{}[a,b,p,q,r,s:Point]. (pq=rs) supposing (ab=rs and ab=pq)@i'
4. \mforall{}[a,b,c:Point]. a = b supposing ab=cc@i'
5. \mforall{}[q:Point]. \mforall{}[a:\{a:Point| \mneg{}(q = a)\} ]. \mforall{}[b,c:Point].
(q\_a\_(extend qa by bc) \mwedge{} a(extend qa by bc)=bc)@i'
6. \mforall{}[a,b,c,d,A,B,C,D:Point].
(cd=CD) supposing (bd=BD and ad=AD and bc=BC and ab=AB and A\_B\_C and a\_b\_c and (\mneg{}(a = b)))@i'
7. \mforall{}[a,b:Point]. (\mneg{}a-b-a)@i'
8. \mforall{}[a,b:Point]. \mforall{}[c:\{c:Point| \mneg{}Colinear(a;b;c)\} ]. \mforall{}[p:\{p:Point| a-p-c\} ]. \mforall{}[q:\{q:Point| b\_q\_c\} ].
let x = eu-inner-pasch(e;a;b;c;p;q) in
p-x-b \mwedge{} q-x-a@i'
9. \mforall{}[a,b,p,q,r:Point]. (Colinear(p;q;r)) supposing (ra=rb and qa=qb and pa=pb and (\mneg{}(a = b)))@i'
10. \mforall{}[a,b:Point]. \mforall{}[c:\{c:Point| \mneg{}Colinear(a;b;c)\} ]. let x = middle(a;b;c) in ax=bx \mwedge{} ax=cx@i'
11. \mforall{}[a,b:Point]. \mforall{}[x:\{x:Point| a\_x\_b\} ]. \mforall{}[y:\{y:Point| a\_b\_y\} ]. \mforall{}[p:\{p:Point| ap=ax\} ].
\mforall{}[q:\{q:Point| aq=ay \mwedge{} (\mneg{}(q = p))\} ].
let uv = intersect pq (at radius xy) with Oab in
afst(uv)=ab
\mwedge{} asnd(uv)=ab
\mwedge{} p\_fst(uv)\_q
\mwedge{} snd(uv)\_p\_q
\mwedge{} \mneg{}((fst(uv)) = (snd(uv))) supposing \mneg{}(x = b)@i'
12. \mforall{}[a,b,c:Point]. c-b-a supposing a-b-c@i'
13. \mforall{}[a,b,c,d:Point]. (a-b-c) supposing (b-c-d and a-b-d)@i'
14. s1 : ProperSegment
15. s2 : ProperSegment
16. t1 : Segment
17. t2 : Segment
18. s1 \mequiv{} s2
19. t1 \mequiv{} t2
20. e \mmember{} EuclideanPlane
21. \mneg{}(s1.1 = s1.2)
22. \mneg{}(s2.1 = s2.2)
23. v : Point@i
24. (extend s1.1s1.2 by t1.1t1.2) = v@i
25. v1 : Point@i
26. (extend s2.1s2.2 by t2.1t2.2) = v1@i
27. s1.1\_s1.2\_v@i
28. s1.2v=t1.1t1.2@i
29. s2.1\_s2.2\_v1@i
30. s2.2v1=t2.1t2.2@i
\mvdash{} s1.2v=s2.2v1
By
Latex:
(Assert t1.1t1.2=t2.1t2.2 BY
Auto)
Home
Index