Nuprl Lemma : eu-inner-five-segment

  ∀[a,b,c,d,A,B,C,D:Point].  (bd=BD) supposing (cd=CD and ad=AD and bc=BC and ac=AC and A_B_C and a_b_c)


Definitions occuring in Statement :  euclidean-plane: EuclideanPlane eu-between-eq: 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 stable: Stable{P} not: ¬A prop: squash: T guard: {T} and: P ∧ Q false: False exists: x:A. B[x] cand: c∧ B uiff: uiff(P;Q)
Lemmas referenced :  sq_stable__eu-congruent stable__eu-congruent not_wf eu-congruent_wf eu-between-eq_wf eu-point_wf euclidean-plane_wf eu-between-eq-same eu-congruence-identity-sym equal_wf and_wf false_wf eu-extend-exists eu-congruence-identity eu-five-segment eu-congruent-iff-length eu-between-eq-symmetry eu-between-eq-inner-trans eu-length-flip
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 independent_isectElimination sqequalRule imageMemberEquality baseClosed imageElimination promote_hyp equalitySymmetry hyp_replacement Error :applyLambdaEquality,  dependent_set_memberEquality independent_pairFormation applyEquality lambdaEquality productElimination setEquality voidElimination dependent_pairFormation equalityTransitivity equalityEquality universeEquality productEquality

        (bd=BD)  supposing  (cd=CD  and  ad=AD  and  bc=BC  and  ac=AC  and  A\_B\_C  and  a\_b\_c)

Date html generated: 2016_10_26-AM-07_42_21
Last ObjectModification: 2016_07_12-AM-08_08_46

Theory : euclidean!geometry

Home Index