Nuprl Lemma : geo-CC-lsep
∀g:EuclideanPlane. ∀a,b,c,d:Point.
(a # c ⇒ (∃p,q:Point. ((ab ≅ ap ∧ cd>cp) ∧ cd ≅ cq ∧ ab>aq)) ⇒ (∃z:Point. ((az ≅ ab ∧ cz ≅ cd) ∧ z # ac)))
Proof
Definitions occuring in Statement :
euclidean-plane: EuclideanPlane,
geo-congruent: ab ≅ cd,
geo-lsep: a # bc,
geo-sep: a # b,
geo-gt-prim: ab>cd,
geo-point: Point,
all: ∀x:A. B[x],
exists: ∃x:A. B[x],
implies: P ⇒ Q,
and: P ∧ Q
Definitions unfolded in proof :
all: ∀x:A. B[x],
member: t ∈ T,
implies: P ⇒ Q,
exists: ∃x:A. B[x],
and: P ∧ Q,
cand: A c∧ B,
geo-lsep: a # bc,
or: P ∨ Q,
uall: ∀[x:A]. B[x],
subtype_rel: A ⊆r B,
prop: ℙ,
guard: {T},
uimplies: b supposing a
Latex:
\mforall{}g:EuclideanPlane. \mforall{}a,b,c,d:Point.
(a \# c
{}\mRightarrow{} (\mexists{}p,q:Point. ((ab \mcong{} ap \mwedge{} cd>cp) \mwedge{} cd \mcong{} cq \mwedge{} ab>aq))
{}\mRightarrow{} (\mexists{}z:Point. ((az \mcong{} ab \mwedge{} cz \mcong{} cd) \mwedge{} z \# ac)))
Date html generated:
2020_05_20-AM-09_47_08
Last ObjectModification:
2019_12_06-PM-03_07_48
Theory : euclidean!plane!geometry
Home
Index