---

Step * 1 1 1 of Lemma eu-exists-middle


1. e : EuclideanStructure@i'
2. euclidean-axioms(e)@i'
3. a : Point@i
4. b : Point@i
5. c : {p:Point| ¬Colinear(a;b;p)} @i
⊢ (middle(a;b;c) = middle(a;b;c) ∈ Point) ∧ amiddle(a;b;c)=bmiddle(a;b;c) ∧ amiddle(a;b;c)=cmiddle(a;b;c)
BY
{ D 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))
∧ (∀[a,b,c:Point].  a = b ∈ Point supposing ab=cc)
∧ (∀[q:Point]. ∀[a:{a:Point| ¬(q = a ∈ Point)} ]. ∀[b,c:Point].  (q_a_(extend qa by bc) ∧ a(extend qa by bc)=bc))
∧ (∀[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))))
∧ (∀[a,b:Point].  (¬a-b-a))
∧ (∀[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)
∧ (∀[a,b,p,q,r:Point].  (Colinear(p;q;r)) supposing (ra=rb and qa=qb and pa=pb and (¬(a = b ∈ Point))))
∧ (∀[a,b:Point]. ∀[c:{c:Point| ¬Colinear(a;b;c)} ].  let x = middle(a;b;c) in ax=bx ∧ ax=cx)
∧ (∀[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))} ]\000C.
     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))
∧ (∀[a,b,c:Point].  c-b-a supposing a-b-c)
∧ (∀[a,b,c,d:Point].  (a-b-c) supposing (b-c-d and a-b-d))@i'
4. a : Point@i
5. b : Point@i
6. c : {p:Point| ¬Colinear(a;b;p)} @i
⊢ (middle(a;b;c) = middle(a;b;c) ∈ Point) ∧ amiddle(a;b;c)=bmiddle(a;b;c) ∧ amiddle(a;b;c)=cmiddle(a;b;c)

---

Latex:

---

Latex:

1.  e  :  EuclideanStructure@i'
2.  euclidean-axioms(e)@i'
3.  a  :  Point@i
4.  b  :  Point@i
5.  c  :  \{p:Point|  \mneg{}Colinear(a;b;p)\}  @i
\mvdash{}  (middle(a;b;c)  =  middle(a;b;c))  \mwedge{}  amiddle(a;b;c)=bmiddle(a;b;c)  \mwedge{}  amiddle(a;b;c)=cmiddle(a;b;c)


By

---

Latex:
D  2

---

Home Index