### Nuprl Lemma : eu-seg-congruent-iff-length

`∀e:EuclideanPlane. ∀[s,t:Segment].  uiff(s ≡ t;|s| = |t| ∈ {p:Point| O_X_p} )`

Proof

Definitions occuring in Statement :  eu-length: `|s|` eu-seg-congruent: `s1 ≡ s2` eu-segment: `Segment` euclidean-plane: `EuclideanPlane` eu-between-eq: `a_b_c` eu-X: `X` eu-O: `O` eu-point: `Point` uiff: `uiff(P;Q)` uall: `∀[x:A]. B[x]` all: `∀x:A. B[x]` set: `{x:A| B[x]} ` equal: `s = t ∈ T`
Definitions unfolded in proof :  all: `∀x:A. B[x]` uall: `∀[x:A]. B[x]` uiff: `uiff(P;Q)` and: `P ∧ Q` uimplies: `b supposing a` eu-length: `|s|` member: `t ∈ T` euclidean-plane: `EuclideanPlane` prop: `ℙ` eu-seg-congruent: `s1 ≡ s2` rev_uimplies: `rev_uimplies(P;Q)` sq_stable: `SqStable(P)` implies: `P `` Q` squash: `↓T`
Lemmas referenced :  sq_stable__eu-congruent eu-extend-equal-iff-congruent eu-length_wf eu-seg-congruent_wf eu-between-eq_wf eu-seg2_wf eu-seg1_wf eu-point_wf equal_wf not_wf eu-X_wf eu-not-colinear-OXY eu-O_wf eu-extend-property
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity lambdaFormation isect_memberFormation independent_pairFormation cut dependent_set_memberEquality sqequalRule lemma_by_obid sqequalHypSubstitution dependent_functionElimination thin because_Cache isectElimination setElimination rename hypothesisEquality hypothesis productElimination introduction axiomEquality setEquality independent_isectElimination independent_functionElimination applyEquality lambdaEquality imageMemberEquality baseClosed imageElimination

Latex:
\mforall{}e:EuclideanPlane.  \mforall{}[s,t:Segment].    uiff(s  \mequiv{}  t;|s|  =  |t|)

Date html generated: 2016_05_18-AM-06_37_35
Last ObjectModification: 2016_01_16-PM-10_31_11

Theory : euclidean!geometry

Home Index