Step
*
1
of Lemma
eu-seg-extend_functionality
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
⊢ s1 + t1 ≡ s2 + t2
BY
{ (((Assert ¬(s1.1 = s1.2 ∈ Point) BY
((D 0 THENM DVar `s1') THEN Auto))
THEN (Assert ¬(s2.1 = s2.2 ∈ Point) BY
((D 0 THENM DVar `s2') THEN Auto))
)
THEN (RepUR ``eu-seg-extend eu-seg-congruent eu-seg1 eu-seg2`` 0 THEN Folds ``eu-seg1 es-seg2`` 0)
THEN (InstHyp [⌜s1.1⌝;⌜s1.2⌝;⌜t1.1⌝;⌜t1.2⌝] 5⋅ THENA Auto)
THEN (InstHyp [⌜s2.1⌝;⌜s2.2⌝;⌜t2.1⌝;⌜t2.2⌝] 5⋅ THENA Auto)
THEN Fold `eu-seg2` 0
THEN RepeatFor 2 (MoveToConcl (-1))
THEN GenConclTerms Auto [⌜(extend s1.1s1.2 by t1.1t1.2)⌝; ⌜(extend s2.1s2.2 by t2.1t2.2)⌝]⋅) }
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
⊢ (s1.1_s1.2_v ∧ s1.2v=t1.1t1.2) ⇒ (s2.1_s2.2_v1 ∧ s2.2v1=t2.1t2.2) ⇒ s1.1v=s2.1v1
Latex:
Latex:
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
\mvdash{} s1 + t1 \mequiv{} s2 + t2
By
Latex:
(((Assert \mneg{}(s1.1 = s1.2) BY
((D 0 THENM DVar `s1') THEN Auto))
THEN (Assert \mneg{}(s2.1 = s2.2) BY
((D 0 THENM DVar `s2') THEN Auto))
)
THEN (RepUR ``eu-seg-extend eu-seg-congruent eu-seg1 eu-seg2`` 0 THEN Folds ``eu-seg1 es-seg2`` 0)
THEN (InstHyp [\mkleeneopen{}s1.1\mkleeneclose{};\mkleeneopen{}s1.2\mkleeneclose{};\mkleeneopen{}t1.1\mkleeneclose{};\mkleeneopen{}t1.2\mkleeneclose{}] 5\mcdot{} THENA Auto)
THEN (InstHyp [\mkleeneopen{}s2.1\mkleeneclose{};\mkleeneopen{}s2.2\mkleeneclose{};\mkleeneopen{}t2.1\mkleeneclose{};\mkleeneopen{}t2.2\mkleeneclose{}] 5\mcdot{} THENA Auto)
THEN Fold `eu-seg2` 0
THEN RepeatFor 2 (MoveToConcl (-1))
THEN GenConclTerms Auto [\mkleeneopen{}(extend s1.1s1.2 by t1.1t1.2)\mkleeneclose{}; \mkleeneopen{}(extend s2.1s2.2 by t2.1t2.2)\mkleeneclose{}]\mcdot{})
Home
Index