Nuprl Lemma : p8eu
∀e:EuclideanPlane. ∀a,b,c,x,y,z:Point.
Cong3(abc,xyz) ⇒ (abc = xyz ∧ bac = yxz ∧ bca = yzx) supposing Triangle(a;b;c) ∧ Triangle(x;y;z)
Proof
Definitions occuring in Statement :
eu-cong-tri: Cong3(abc,a'b'c'),
eu-cong-angle: abc = xyz,
eu-tri: Triangle(a;b;c),
euclidean-plane: EuclideanPlane,
eu-point: Point,
uimplies: b supposing a,
all: ∀x:A. B[x],
implies: P ⇒ Q,
and: P ∧ Q
Definitions unfolded in proof :
so_apply: x[s],
so_lambda: λ2x.t[x],
uiff: uiff(P;Q),
exists: ∃x:A. B[x],
prop: ℙ,
eu-cong-angle: abc = xyz,
eu-cong-tri: Cong3(abc,a'b'c'),
cand: A c∧ B,
euclidean-plane: EuclideanPlane,
uall: ∀[x:A]. B[x],
false: False,
implies: P ⇒ Q,
not: ¬A,
eu-tri: Triangle(a;b;c),
and: P ∧ Q,
member: t ∈ T,
uimplies: b supposing a,
all: ∀x:A. B[x]
Rules used in proof :
equalityTransitivity,
independent_isectElimination,
dependent_pairFormation,
productEquality,
because_Cache,
equalitySymmetry,
independent_functionElimination,
independent_pairFormation,
hypothesis,
rename,
setElimination,
isectElimination,
extract_by_obid,
equalityEquality,
voidElimination,
hypothesisEquality,
dependent_functionElimination,
lambdaEquality,
independent_pairEquality,
thin,
productElimination,
sqequalHypSubstitution,
sqequalRule,
introduction,
cut,
isect_memberFormation,
lambdaFormation,
sqequalReflexivity,
computationStep,
sqequalTransitivity,
sqequalSubstitution
Latex:
\mforall{}e:EuclideanPlane. \mforall{}a,b,c,x,y,z:Point.
Cong3(abc,xyz) {}\mRightarrow{} (abc = xyz \mwedge{} bac = yxz \mwedge{} bca = yzx) supposing Triangle(a;b;c) \mwedge{} Triangle(x;y;z)
Date html generated:
2016_07_08-PM-05_54_27
Last ObjectModification:
2016_07_05-PM-03_04_37
Theory : euclidean!geometry
Home
Index