Nuprl Lemma : eu-not-not-colinear

`∀e:EuclideanStructure`
`  ∀[a,b,c:Point].`
`    (¬¬Colinear(a;b;c) `⇐⇒` (¬(a = b ∈ Point)) ∧ (¬¬((c = a ∈ Point) ∨ (c = b ∈ Point) ∨ c-a-b ∨ a-c-b ∨ a-b-c)))`

Proof

Definitions occuring in Statement :  eu-colinear: `Colinear(a;b;c)` eu-between: `a-b-c` eu-point: `Point` euclidean-structure: `EuclideanStructure` uall: `∀[x:A]. B[x]` all: `∀x:A. B[x]` iff: `P `⇐⇒` Q` not: `¬A` or: `P ∨ Q` and: `P ∧ Q` equal: `s = t ∈ T`
Definitions unfolded in proof :  iff: `P `⇐⇒` Q` and: `P ∧ Q` implies: `P `` Q` not: `¬A` false: `False` member: `t ∈ T` prop: `ℙ` uall: `∀[x:A]. B[x]` rev_implies: `P `` Q` cand: `A c∧ B` uiff: `uiff(P;Q)` uimplies: `b supposing a` or: `P ∨ Q` all: `∀x:A. B[x]` guard: `{T}`
Lemmas referenced :  and_wf not_wf equal_wf eu-point_wf eu-between_wf or_wf not_over_or eu-colinear_wf iff_wf euclidean-structure_wf eu-colinear-def
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity independent_pairFormation lambdaFormation cut thin sqequalHypSubstitution hypothesis independent_functionElimination productElimination voidElimination lemma_by_obid isectElimination hypothesisEquality addLevel impliesFunctionality independent_isectElimination levelHypothesis promote_hyp andLevelFunctionality sqequalRule impliesLevelFunctionality productEquality because_Cache equalityEquality isect_memberFormation introduction independent_pairEquality lambdaEquality dependent_functionElimination isect_memberEquality inlFormation inrFormation

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

Date html generated: 2016_05_18-AM-06_32_50
Last ObjectModification: 2015_12_28-AM-09_28_50

Theory : euclidean!geometry

Home Index