### Nuprl Lemma : euclid-P3-ext

`∀e:EuclideanPlane. ∀A,B,C1,C2:Point.  ∃E:Point. (A_E_B ∧ AE=C1C2) supposing (¬(C1 = C2 ∈ Point)) ∧ |C1C2| < |AB|`

Proof

Definitions occuring in Statement :  eu-lt: `p < q` eu-length: `|s|` eu-mk-seg: `ab` euclidean-plane: `EuclideanPlane` eu-between-eq: `a_b_c` eu-congruent: `ab=cd` eu-point: `Point` uimplies: `b supposing a` all: `∀x:A. B[x]` exists: `∃x:A. B[x]` not: `¬A` and: `P ∧ Q` equal: `s = t ∈ T`
Definitions unfolded in proof :  member: `t ∈ T` euclid-P3 eu-extend-exists eu-extend: `(extend ab by cd)` record-select: `r.x` stable__eu-between-eq uall: `∀[x:A]. B[x]` so_lambda: `so_lambda(x,y,z,w.t[x; y; z; w])` so_apply: `x[s1;s2;s3;s4]` top: `Top` uimplies: `b supposing a` strict4: `strict4(F)` and: `P ∧ Q` all: `∀x:A. B[x]` implies: `P `` Q` has-value: `(a)↓` prop: `ℙ` guard: `{T}` or: `P ∨ Q` squash: `↓T` so_lambda: `λ2x y.t[x; y]` so_apply: `x[s1;s2]` eu-between-eq-def eu-extend-property sq_stable__eu-congruent sq_stable__from_stable stable__eu-congruent
Lemmas referenced :  euclid-P3 lifting-strict-spread has-value_wf_base base_wf is-exception_wf eu-extend-exists stable__eu-between-eq eu-between-eq-def eu-extend-property sq_stable__eu-congruent sq_stable__from_stable stable__eu-congruent
Rules used in proof :  introduction sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity cut instantiate extract_by_obid hypothesis sqequalRule thin sqequalHypSubstitution isectElimination baseClosed isect_memberEquality voidElimination voidEquality independent_isectElimination independent_pairFormation lambdaFormation callbyvalueApply baseApply closedConclusion hypothesisEquality applyExceptionCases inrFormation imageMemberEquality imageElimination exceptionSqequal inlFormation equalityTransitivity equalitySymmetry

Latex:
\mforall{}e:EuclideanPlane.  \mforall{}A,B,C1,C2:Point.
\mexists{}E:Point.  (A\_E\_B  \mwedge{}  AE=C1C2)  supposing  (\mneg{}(C1  =  C2))  \mwedge{}  |C1C2|  <  |AB|

Date html generated: 2016_10_26-AM-07_46_11
Last ObjectModification: 2016_08_29-PM-03_33_31

Theory : euclidean!geometry

Home Index