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