Nuprl Lemma : eu-seg-length-test-ext
∀e:EuclideanPlane. ∀[a,b,c,d,x,y:Point]. (ba=xy) supposing (dc=yx and ab=cd)
Proof
Definitions occuring in Statement :
euclidean-plane: EuclideanPlane,
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 :
record-select: r.x,
stable__eu-congruent,
sq_stable__from_stable,
sq_stable__eu-congruent,
eu-seg-congruent-iff-length,
eu-congruent-iff-length,
eu-seg-length-test,
member: t ∈ T
Lemmas referenced :
stable__eu-congruent,
sq_stable__from_stable,
sq_stable__eu-congruent,
eu-seg-congruent-iff-length,
eu-congruent-iff-length,
eu-seg-length-test
Rules used in proof :
equalitySymmetry,
equalityTransitivity,
sqequalHypSubstitution,
thin,
sqequalRule,
hypothesis,
extract_by_obid,
instantiate,
cut,
sqequalReflexivity,
computationStep,
sqequalTransitivity,
sqequalSubstitution,
introduction
Latex:
\mforall{}e:EuclideanPlane. \mforall{}[a,b,c,d,x,y:Point]. (ba=xy) supposing (dc=yx and ab=cd)
Date html generated:
2016_07_08-PM-05_54_25
Last ObjectModification:
2016_07_05-PM-03_04_14
Theory : euclidean!geometry
Home
Index