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: 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]
, 
uimplies: b supposing a
, 
member: t ∈ T
, 
euclidean-plane: EuclideanPlane
, 
sq_stable: SqStable(P)
, 
implies: P 
⇒ Q
, 
and: P ∧ Q
, 
prop: ℙ
, 
not: ¬A
, 
false: False
, 
squash: ↓T
, 
iff: P 
⇐⇒ Q
, 
rev_implies: P 
⇐ 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