Nuprl Lemma : euclidean-plane-axioms
∀g:EuclideanPlane
(((∀a,b:Point. (a # b ⇒ b # a))
∧ (∀a:Point. (¬a # a))
∧ (∀a,b,x,y:Point. (a ≡ b ⇒ B(xay) ⇒ B(xby)))
∧ ((∀a,b,c:Point. (a ≡ b ⇒ ac ≅ cb)) ∧ (∀a,b,c:Point. (a ≡ b ⇒ ac ≅ bc)))
∧ (∀a,b,c,d:Point. (cd ≥ ab ⇒ a # b ⇒ c # d))
∧ (∀a,b,c:Point. (a ≡ b ⇒ B(abc)))
∧ (∀a,b,c:Point. (B(abc) ⇒ B(cba)))
∧ (∀a,b,c,d:Point. (B(abd) ⇒ B(bcd) ⇒ B(abc)))
∧ (∀a,b:Point. ab ≅ ba)
∧ (∀a,b,p,q,r,s:Point. (ab ≅ pq ⇒ ab ≅ rs ⇒ pq ≅ rs))
∧ (∀a,b:Point. aa ≅ bb)
∧ (∀a,b,c,d,A,B,C,D:Point. (a # b ⇒ B(abc) ⇒ B(ABC) ⇒ ab ≅ AB ⇒ bc ≅ BC ⇒ ad ≅ AD ⇒ bd ≅ BD ⇒ cd ≅ CD)))
∧ (∀a,b,c:Point. (¬a # bc ⇐⇒ Colinear(a;b;c)))
∧ (∀a,b,c:Point. (a leftof bc ⇒ b leftof ca))
∧ (∀a,b,c:Point. (a leftof bc ⇒ b # c))
∧ (∀a,b,x,y,z:Point. (x leftof ab ⇒ y leftof ab ⇒ B(xzy) ⇒ z # ab))
∧ (∀a,b,c,y:Point. (a # bc ⇒ y # b ⇒ Colinear(y;a;b) ⇒ y # bc)))
Proof
Definitions occuring in Statement :
euclidean-plane: EuclideanPlane,
geo-colinear: Colinear(a;b;c),
geo-ge: ab ≥ cd,
geo-eq: a ≡ b,
geo-congruent: ab ≅ cd,
geo-between: B(abc),
geo-lsep: a # bc,
geo-left: a leftof bc,
geo-sep: a # b,
geo-point: Point,
all: ∀x:A. B[x],
iff: P ⇐⇒ Q,
not: ¬A,
implies: P ⇒ Q,
and: P ∧ Q
Definitions unfolded in proof :
all: ∀x:A. B[x],
euclidean-plane: EuclideanPlane,
uall: ∀[x:A]. B[x],
member: t ∈ T,
subtype_rel: A ⊆r B,
prop: ℙ,
implies: P ⇒ Q,
so_lambda: λ2x.t[x],
so_apply: x[s],
sq_stable: SqStable(P),
not: ¬A,
false: False,
and: P ∧ Q,
cand: A c∧ B,
squash: ↓T,
geo-colinear: Colinear(a;b;c),
guard: {T},
uimplies: b supposing a,
basic-geo-axioms: BasicGeometryAxioms(g),
iff: P ⇐⇒ Q,
rev_implies: P ⇐ Q,
geo-eq: a ≡ b,
geo-between: B(abc),
geo-lsep: a # bc,
or: P ∨ Q,
geo-sep: a # b,
geo-ge: ab ≥ cd,
geo-gt-prim: ab>cd,
record-select: r.x,
geo-congruent: ab ≅ cd,
geo-length-sep: ab # cd)
Latex:
\mforall{}g:EuclideanPlane
(((\mforall{}a,b:Point. (a \# b {}\mRightarrow{} b \# a))
\mwedge{} (\mforall{}a:Point. (\mneg{}a \# a))
\mwedge{} (\mforall{}a,b,x,y:Point. (a \mequiv{} b {}\mRightarrow{} B(xay) {}\mRightarrow{} B(xby)))
\mwedge{} ((\mforall{}a,b,c:Point. (a \mequiv{} b {}\mRightarrow{} ac \mcong{} cb)) \mwedge{} (\mforall{}a,b,c:Point. (a \mequiv{} b {}\mRightarrow{} ac \mcong{} bc)))
\mwedge{} (\mforall{}a,b,c,d:Point. (cd \mgeq{} ab {}\mRightarrow{} a \# b {}\mRightarrow{} c \# d))
\mwedge{} (\mforall{}a,b,c:Point. (a \mequiv{} b {}\mRightarrow{} B(abc)))
\mwedge{} (\mforall{}a,b,c:Point. (B(abc) {}\mRightarrow{} B(cba)))
\mwedge{} (\mforall{}a,b,c,d:Point. (B(abd) {}\mRightarrow{} B(bcd) {}\mRightarrow{} B(abc)))
\mwedge{} (\mforall{}a,b:Point. ab \mcong{} ba)
\mwedge{} (\mforall{}a,b,p,q,r,s:Point. (ab \mcong{} pq {}\mRightarrow{} ab \mcong{} rs {}\mRightarrow{} pq \mcong{} rs))
\mwedge{} (\mforall{}a,b:Point. aa \mcong{} bb)
\mwedge{} (\mforall{}a,b,c,d,A,B,C,D:Point.
(a \# b {}\mRightarrow{} B(abc) {}\mRightarrow{} B(ABC) {}\mRightarrow{} ab \mcong{} AB {}\mRightarrow{} bc \mcong{} BC {}\mRightarrow{} ad \mcong{} AD {}\mRightarrow{} bd \mcong{} BD {}\mRightarrow{} cd \mcong{} CD)))
\mwedge{} (\mforall{}a,b,c:Point. (\mneg{}a \# bc \mLeftarrow{}{}\mRightarrow{} Colinear(a;b;c)))
\mwedge{} (\mforall{}a,b,c:Point. (a leftof bc {}\mRightarrow{} b leftof ca))
\mwedge{} (\mforall{}a,b,c:Point. (a leftof bc {}\mRightarrow{} b \# c))
\mwedge{} (\mforall{}a,b,x,y,z:Point. (x leftof ab {}\mRightarrow{} y leftof ab {}\mRightarrow{} B(xzy) {}\mRightarrow{} z \# ab))
\mwedge{} (\mforall{}a,b,c,y:Point. (a \# bc {}\mRightarrow{} y \# b {}\mRightarrow{} Colinear(y;a;b) {}\mRightarrow{} y \# bc)))
Date html generated:
2020_05_20-AM-09_44_33
Last ObjectModification:
2020_01_27-PM-10_41_37
Theory : euclidean!plane!geometry
Home
Index