Nuprl Lemma : congruence-implies-between

∀e:EuclideanPlane
  ∀[a,b,c,d,A,B,C,D:Point].
    (B(ABC)) supposing 
       ((A # B ⇒ C # B ⇒ (A leftof BD ⇐⇒ C leftof DB)) and 
       B(abc) and 
       d # b and 
       bd ≅ BD and 
       ad ≅ AD and 
       cd ≅ CD and 
       bc ≅ BC and 
       ab ≅ AB)


Proof



Definitions occuring in Statement :  euclidean-plane: EuclideanPlane,  geo-congruent: ab ≅ cd,  geo-between: B(abc),  geo-left: a leftof bc,  geo-sep: a # b,  geo-point: Point,  uimplies: b supposing a,  uall: ∀[x:A]. B[x],  all: ∀x:A. B[x],  iff: P ⇐⇒ Q,  implies: P ⇒ Q
Definitions unfolded in proof :  all: ∀x:A. B[x],  uall: ∀[x:A]. B[x],  member: t ∈ T,  uimplies: b supposing a,  geo-between: B(abc),  and: P ∧ Q,  not: ¬A,  implies: P ⇒ Q,  false: False,  subtype_rel: A ⊆r B,  guard: {T},  prop: ℙ,  iff: P ⇐⇒ Q,  rev_implies: P ⇐ Q,  euclidean-plane: EuclideanPlane,  or: P ∨ Q,  stable: Stable{P},  geo-eq: a ≡ b,  exists: ∃x:A. B[x],  cand: A c∧ B,  basic-geometry: BasicGeometry,  uiff: uiff(P;Q),  oriented-plane: OrientedPlane,  geo-lsep: a # bc
Latex:
\mforall{}e:EuclideanPlane
    \mforall{}[a,b,c,d,A,B,C,D:Point].
        (B(ABC))  supposing 
              ((A  \#  B  {}\mRightarrow{}  C  \#  B  {}\mRightarrow{}  (A  leftof  BD  \mLeftarrow{}{}\mRightarrow{}  C  leftof  DB))  and 
              B(abc)  and 
              d  \#  b  and 
              bd  \mcong{}  BD  and 
              ad  \mcong{}  AD  and 
              cd  \mcong{}  CD  and 
              bc  \mcong{}  BC  and 
              ab  \mcong{}  AB)


Date html generated: 2020_05_20-AM-10_07_45
Last ObjectModification: 2020_01_13-PM-04_07_30

Theory : euclidean!plane!geometry


Home Index