Nuprl Lemma : Euclid-Prop6-lemma
∀e:EuclideanPlane. ∀a,b,c:Point.
(cab ≅a cba
⇒ c # ab
⇒ (∃x:Point
(Colinear(c;a;x) ∧ ax ≅ bc ∧ (c leftof ab ⇒ x leftof ab) ∧ (c leftof ba ⇒ x leftof ba) ∧ Cong3(axb,bca))))
Proof
Definitions occuring in Statement :
geo-cong-tri: Cong3(abc,a'b'c'),
geo-cong-angle: abc ≅a xyz,
euclidean-plane: EuclideanPlane,
geo-colinear: Colinear(a;b;c),
geo-congruent: ab ≅ cd,
geo-lsep: a # bc,
geo-left: a leftof bc,
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],
implies: P ⇒ Q,
member: t ∈ T,
sq_exists: ∃x:A [B[x]],
uall: ∀[x:A]. B[x],
subtype_rel: A ⊆r B,
guard: {T},
uimplies: b supposing a,
prop: ℙ,
basic-geometry: BasicGeometry,
and: P ∧ Q,
exists: ∃x:A. B[x],
cand: A c∧ B,
uiff: uiff(P;Q),
sq_stable: SqStable(P),
oriented-plane: OrientedPlane,
squash: ↓T,
geo-lsep: a # bc,
or: P ∨ Q,
geo-tri: Triangle(a;b;c),
iff: P ⇐⇒ Q,
rev_implies: P ⇐ Q,
not: ¬A,
false: False
Latex:
\mforall{}e:EuclideanPlane. \mforall{}a,b,c:Point.
(cab \mcong{}\msuba{} cba
{}\mRightarrow{} c \# ab
{}\mRightarrow{} (\mexists{}x:Point
(Colinear(c;a;x)
\mwedge{} ax \mcong{} bc
\mwedge{} (c leftof ab {}\mRightarrow{} x leftof ab)
\mwedge{} (c leftof ba {}\mRightarrow{} x leftof ba)
\mwedge{} Cong3(axb,bca))))
Date html generated:
2020_05_20-AM-10_06_21
Last ObjectModification:
2020_01_27-PM-10_00_00
Theory : euclidean!plane!geometry
Home
Index