Nuprl Lemma : eu-colinear-five-segment

e:EuclideanPlane
  ∀[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))


Proof




Definitions occuring in Statement :  euclidean-plane: EuclideanPlane eu-colinear: Colinear(a;b;c) eu-congruent: ab=cd eu-point: Point uimplies: 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] uimplies: supposing a member: t ∈ T euclidean-plane: EuclideanPlane sq_stable: SqStable(P) implies:  Q and: P ∧ Q prop: not: ¬A false: False squash: T iff: ⇐⇒ Q rev_implies:  Q uiff: uiff(P;Q)
Lemmas referenced :  sq_stable__eu-congruent eu-colinear-cases eu-congruent_wf stable__eu-congruent not_wf equal_wf eu-point_wf eu-between_wf eu-colinear_wf euclidean-plane_wf eu-congruence-identity-sym eu-between-eq-def eu-congruent-preserves-between eu-congruent-iff-length eu-length-flip eu-five-segment eu-between-eq-symmetry eu-inner-five-segment
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity lambdaFormation isect_memberFormation cut introduction extract_by_obid sqequalHypSubstitution dependent_functionElimination thin setElimination rename because_Cache hypothesis isectElimination hypothesisEquality independent_functionElimination productElimination productEquality equalityEquality voidElimination sqequalRule imageMemberEquality baseClosed imageElimination equalitySymmetry hyp_replacement Error :applyLambdaEquality,  independent_isectElimination promote_hyp equalityTransitivity

Latex:
\mforall{}e:EuclideanPlane
    \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  ac=AC  and  Colinear(a;b;c))



Date html generated: 2016_10_26-AM-07_42_42
Last ObjectModification: 2016_07_12-AM-08_09_03

Theory : euclidean!geometry


Home Index