Nuprl Lemma : eu-perp-three

`∀e:EuclideanPlane. ∀x,a,b,c:Point.  (Perp-in(x; ba; ca) `` (x = a ∈ Point))`

Proof

Definitions occuring in Statement :  eu-perp-in: `Perp-in(x; ab; cd)` euclidean-plane: `EuclideanPlane` eu-point: `Point` all: `∀x:A. B[x]` implies: `P `` Q` equal: `s = t ∈ T`
Definitions unfolded in proof :  all: `∀x:A. B[x]` implies: `P `` Q` eu-perp-in: `Perp-in(x; ab; cd)` and: `P ∧ Q` member: `t ∈ T` prop: `ℙ` uall: `∀[x:A]. B[x]` euclidean-plane: `EuclideanPlane` iff: `P `⇐⇒` Q` eu-colinear-set: `eu-colinear-set(e;L)` l_all: `(∀x∈L.P[x])` top: `Top` int_seg: `{i..j-}` lelt: `i ≤ j < k` le: `A ≤ B` less_than': `less_than'(a;b)` false: `False` not: `¬A` less_than: `a < b` squash: `↓T` true: `True` select: `L[n]` cons: `[a / b]` subtract: `n - m` eu-perpendicular: `Per(a;b;c)` exists: `∃x:A. B[x]` uimplies: `b supposing a` eu-midpoint: `a=m=b`
Lemmas referenced :  eu-between-eq-same2 eu-congruence-identity-sym lelt_wf false_wf length_of_nil_lemma length_of_cons_lemma eu-colinear-is-colinear-set eu-colinear-def euclidean-plane_wf eu-point_wf eu-perp-in_wf
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity lambdaFormation cut sqequalHypSubstitution productElimination thin hypothesis lemma_by_obid isectElimination hypothesisEquality setElimination rename dependent_functionElimination because_Cache independent_functionElimination sqequalRule isect_memberEquality voidElimination voidEquality dependent_set_memberEquality natural_numberEquality independent_pairFormation introduction imageMemberEquality baseClosed independent_isectElimination equalitySymmetry

Latex:
\mforall{}e:EuclideanPlane.  \mforall{}x,a,b,c:Point.    (Perp-in(x;  ba;  ca)  {}\mRightarrow{}  (x  =  a))

Date html generated: 2016_05_18-AM-06_43_34
Last ObjectModification: 2016_01_16-PM-10_28_45

Theory : euclidean!geometry

Home Index