### Nuprl Lemma : eu-five-segment'

`∀e:EuclideanPlane`
`  ∀[a,b,c,A,B,C:Point].`
`    (∀d,D:Point.  (cd=CD) supposing (bd=BD and ad=AD)) supposing `
`       (bc=BC and `
`       ab=AB and `
`       A_B_C and `
`       a_b_c and `
`       (¬(a = b ∈ Point)))`

Proof

Definitions occuring in Statement :  euclidean-plane: `EuclideanPlane` eu-between-eq: `a_b_c` eu-congruent: `ab=cd` eu-point: `Point` uimplies: `b supposing a` uall: `∀[x:A]. B[x]` all: `∀x:A. B[x]` not: `¬A` equal: `s = t ∈ T`
Definitions unfolded in proof :  prop: `ℙ` euclidean-plane: `EuclideanPlane` false: `False` implies: `P `` Q` not: `¬A` member: `t ∈ T` uimplies: `b supposing a` uall: `∀[x:A]. B[x]` all: `∀x:A. B[x]`
Lemmas referenced :  eu-point_wf eu-five-segment eu-congruent_wf eu-between-eq_wf not_wf equal_wf euclidean-plane_wf
Rules used in proof :  independent_isectElimination hypothesis rename setElimination isectElimination lemma_by_obid equalityEquality voidElimination hypothesisEquality thin dependent_functionElimination lambdaEquality sqequalHypSubstitution sqequalRule introduction cut isect_memberFormation lambdaFormation sqequalReflexivity computationStep sqequalTransitivity sqequalSubstitution

Latex:
\mforall{}e:EuclideanPlane
\mforall{}[a,b,c,A,B,C:Point].
(bc=BC  and
ab=AB  and
A\_B\_C  and
a\_b\_c  and
(\mneg{}(a  =  b)))

Date html generated: 2016_05_18-AM-06_35_17
Last ObjectModification: 2016_01_02-PM-00_16_04

Theory : euclidean!geometry

Home Index