Nuprl Lemma : eu-colinear-cases

`∀e:EuclideanStructure`
`  ∀[a,b,c:Point].`
`    ∀X:ℙ`
`      (Stable{X}`
`      `` (((¬(a = b ∈ Point)) ∧ (c = a ∈ Point)) `` X)`
`      `` (((¬(a = b ∈ Point)) ∧ (c = b ∈ Point)) `` X)`
`      `` (((¬(a = b ∈ Point)) ∧ c-a-b) `` X)`
`      `` (((¬(a = b ∈ Point)) ∧ a-c-b) `` X)`
`      `` (((¬(a = b ∈ Point)) ∧ a-b-c) `` X)`
`      `` ((¬Colinear(a;b;c)) `` X)`
`      `` X)`

Proof

Definitions occuring in Statement :  eu-colinear: `Colinear(a;b;c)` eu-between: `a-b-c` eu-point: `Point` euclidean-structure: `EuclideanStructure` stable: `Stable{P}` uall: `∀[x:A]. B[x]` prop: `ℙ` all: `∀x:A. B[x]` not: `¬A` implies: `P `` Q` and: `P ∧ Q` equal: `s = t ∈ T`
Definitions unfolded in proof :  all: `∀x:A. B[x]` uall: `∀[x:A]. B[x]` implies: `P `` Q` stable: `Stable{P}` uimplies: `b supposing a` not: `¬A` member: `t ∈ T` prop: `ℙ` false: `False` iff: `P `⇐⇒` Q` and: `P ∧ Q` or: `P ∨ Q`
Lemmas referenced :  not_wf eu-colinear_wf and_wf equal_wf eu-point_wf eu-between_wf stable_wf euclidean-structure_wf eu-not-not-colinear or_wf
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity lambdaFormation isect_memberFormation sqequalHypSubstitution independent_isectElimination thin cut lemma_by_obid isectElimination hypothesisEquality hypothesis functionEquality universeEquality independent_functionElimination voidElimination dependent_functionElimination productElimination unionElimination independent_pairFormation

Latex:
\mforall{}e:EuclideanStructure
\mforall{}[a,b,c:Point].
\mforall{}X:\mBbbP{}
(Stable\{X\}
{}\mRightarrow{}  (((\mneg{}(a  =  b))  \mwedge{}  (c  =  a))  {}\mRightarrow{}  X)
{}\mRightarrow{}  (((\mneg{}(a  =  b))  \mwedge{}  (c  =  b))  {}\mRightarrow{}  X)
{}\mRightarrow{}  (((\mneg{}(a  =  b))  \mwedge{}  c-a-b)  {}\mRightarrow{}  X)
{}\mRightarrow{}  (((\mneg{}(a  =  b))  \mwedge{}  a-c-b)  {}\mRightarrow{}  X)
{}\mRightarrow{}  (((\mneg{}(a  =  b))  \mwedge{}  a-b-c)  {}\mRightarrow{}  X)
{}\mRightarrow{}  ((\mneg{}Colinear(a;b;c))  {}\mRightarrow{}  X)
{}\mRightarrow{}  X)

Date html generated: 2016_05_18-AM-06_35_44
Last ObjectModification: 2015_12_28-AM-09_28_57

Theory : euclidean!geometry

Home Index