Nuprl Lemma : geo-colinear-five-segment

∀e:BasicGeometry
  ∀[a,b,c,d,A,B,C,D:Point].
    (cd ≅ CD) supposing (bd ≅ BD and ad ≅ AD and bc ≅ BC and ab ≅ AB and ac ≅ AC and Colinear(a;b;c) and a # b)


Proof



Definitions occuring in Statement :  basic-geometry: BasicGeometry,  geo-colinear: Colinear(a;b;c),  geo-congruent: ab ≅ cd,  geo-sep: a # b,  geo-point: Point,  uimplies: b supposing a,  uall: ∀[x:A]. B[x],  all: ∀x:A. B[x]
Definitions unfolded in proof :  all: ∀x:A. B[x],  uall: ∀[x:A]. B[x],  member: t ∈ T,  uimplies: b supposing a,  subtype_rel: A ⊆r B,  basic-geometry: BasicGeometry,  euclidean-plane: EuclideanPlane,  basic-geometry-: BasicGeometry-,  guard: {T},  implies: P ⇒ Q,  prop: ℙ,  geo-congruent: ab ≅ cd,  not: ¬A,  false: False,  uiff: uiff(P;Q),  and: P ∧ Q
Latex:
\mforall{}e:BasicGeometry
    \mforall{}[a,b,c,d,A,B,C,D:Point].
        (cd  \mcong{}  CD)  supposing 
              (bd  \mcong{}  BD  and 
              ad  \mcong{}  AD  and 
              bc  \mcong{}  BC  and 
              ab  \mcong{}  AB  and 
              ac  \mcong{}  AC  and 
              Colinear(a;b;c)  and 
              a  \#  b)


Date html generated: 2020_05_20-AM-09_52_32
Last ObjectModification: 2019_12_20-PM-08_45_04

Theory : euclidean!plane!geometry


Home Index