Nuprl Lemma : eu-eq_dist-axiomA9
∀e:EuclideanPlane. ∀a1,a2,a3,a4,a5,a6,b:Point. (D(a1;a2;a3;a4;a5;a6) ⇒ (a4 ≠ b ∨ D(a1;a2;a3;b;a5;a6)))
Proof
Definitions occuring in Statement :
dist: D(a;b;c;d;e;f),
euclidean-plane: EuclideanPlane,
geo-sep: a ≠ b,
geo-point: Point,
all: ∀x:A. B[x],
implies: P ⇒ Q,
or: P ∨ Q
Definitions unfolded in proof :
uimplies: b supposing a,
guard: {T},
subtype_rel: A ⊆r B,
prop: ℙ,
or: P ∨ Q,
rev_implies: P ⇐ Q,
and: P ∧ Q,
iff: P ⇐⇒ Q,
euclidean-plane: EuclideanPlane,
uall: ∀[x:A]. B[x],
basic-geometry: BasicGeometry,
member: t ∈ T,
implies: P ⇒ Q,
all: ∀x:A. B[x]
Lemmas referenced :
geo-point_wf,
dist_wf,
geo-primitives_wf,
euclidean-plane-structure_wf,
euclidean-plane_wf,
subtype_rel_transitivity,
euclidean-plane-subtype,
euclidean-plane-structure-subtype,
geo-sep_wf,
geo-sep-or,
geo-length_wf,
geo-add-length_wf,
geo-lt_wf,
geo-add-length_wf1,
geo-mk-seg_wf,
geo-length_wf1,
geo-sep-iff-or-lt,
dist-lemma-lt,
dist-lemma-lt2,
geo-add-length-cancel-left-lt,
geo-le_weakening-lt,
geo-lt_transitivity,
geo-lt-lengths-to-sep,
geo-sep-sym
Rules used in proof :
unionElimination,
equalitySymmetry,
equalityTransitivity,
independent_isectElimination,
instantiate,
dependent_set_memberEquality_alt,
inhabitedIsType,
lambdaEquality_alt,
applyEquality,
universeIsType,
inlFormation_alt,
productElimination,
because_Cache,
rename,
setElimination,
isectElimination,
sqequalRule,
hypothesis,
independent_functionElimination,
hypothesisEquality,
thin,
dependent_functionElimination,
sqequalHypSubstitution,
extract_by_obid,
introduction,
cut,
lambdaFormation_alt,
sqequalReflexivity,
computationStep,
sqequalTransitivity,
sqequalSubstitution,
inrFormation_alt
Latex:
\mforall{}e:EuclideanPlane. \mforall{}a1,a2,a3,a4,a5,a6,b:Point.
(D(a1;a2;a3;a4;a5;a6) {}\mRightarrow{} (a4 \mneq{} b \mvee{} D(a1;a2;a3;b;a5;a6)))
Date html generated:
2019_10_16-PM-02_57_56
Last ObjectModification:
2019_04_22-PM-01_32_18
Theory : euclidean!plane!geometry
Home
Index