Nuprl Lemma : euclid-Prop3-ext
∀e:EuclideanPlane. ∀A:Point. ∀B:{B:Point| A ≠ B} . ∀C1:Point. ∀C2:{C2:Point| C1 ≠ C2} .
(|C1C2| < |AB| ⇒ (∃E:Point [(A_E_B ∧ AE ≅ C1C2)]))
Proof
Definitions occuring in Statement :
geo-lt: p < q,
geo-length: |s|,
geo-mk-seg: ab,
euclidean-plane: EuclideanPlane,
geo-congruent: ab ≅ cd,
geo-between: a_b_c,
geo-sep: a ≠ b,
geo-point: Point,
all: ∀x:A. B[x],
sq_exists: ∃x:A [B[x]],
implies: P ⇒ Q,
and: P ∧ Q,
set: {x:A| B[x]}
Definitions unfolded in proof :
geo-extend-exists,
euclid-Prop3,
member: t ∈ T
Lemmas referenced :
euclid-Prop3,
geo-extend-exists
Rules used in proof :
equalitySymmetry,
equalityTransitivity,
sqequalHypSubstitution,
thin,
sqequalRule,
hypothesis,
extract_by_obid,
instantiate,
cut,
sqequalReflexivity,
computationStep,
sqequalTransitivity,
sqequalSubstitution,
introduction
Latex:
\mforall{}e:EuclideanPlane. \mforall{}A:Point. \mforall{}B:\{B:Point| A \mneq{} B\} . \mforall{}C1:Point. \mforall{}C2:\{C2:Point| C1 \mneq{} C2\} .
(|C1C2| < |AB| {}\mRightarrow{} (\mexists{}E:Point [(A\_E\_B \mwedge{} AE \mcong{} C1C2)]))
Date html generated:
2019_10_16-PM-01_42_01
Last ObjectModification:
2019_08_27-AM-08_38_56
Theory : euclidean!plane!geometry
Home
Index