Nuprl Lemma : cong-tri-implies-all-cong-angle
∀e:BasicGeometry. ∀a,b,c,x,y,z:Point.
(Cong3(abc,xyz) ⇒ a # b ⇒ b # c ⇒ c # a ⇒ x # y ⇒ y # z ⇒ z # x ⇒ {abc ≅a xyz ∧ bca ≅a yzx ∧ cab ≅a zxy})
Proof
Definitions occuring in Statement :
geo-cong-tri: Cong3(abc,a'b'c'),
geo-cong-angle: abc ≅a xyz,
basic-geometry: BasicGeometry,
geo-sep: a # b,
geo-point: Point,
guard: {T},
all: ∀x:A. B[x],
implies: P ⇒ Q,
and: P ∧ Q
Definitions unfolded in proof :
guard: {T},
all: ∀x:A. B[x],
implies: P ⇒ Q,
and: P ∧ Q,
cand: A c∧ B,
member: t ∈ T,
uall: ∀[x:A]. B[x],
uimplies: b supposing a,
subtype_rel: A ⊆r B,
prop: ℙ
Latex:
\mforall{}e:BasicGeometry. \mforall{}a,b,c,x,y,z:Point.
(Cong3(abc,xyz)
{}\mRightarrow{} a \# b
{}\mRightarrow{} b \# c
{}\mRightarrow{} c \# a
{}\mRightarrow{} x \# y
{}\mRightarrow{} y \# z
{}\mRightarrow{} z \# x
{}\mRightarrow{} \{abc \mcong{}\msuba{} xyz \mwedge{} bca \mcong{}\msuba{} yzx \mwedge{} cab \mcong{}\msuba{} zxy\})
Date html generated:
2020_05_20-AM-09_54_42
Last ObjectModification:
2020_01_14-AM-10_03_05
Theory : euclidean!plane!geometry
Home
Index