Nuprl Lemma : geo-axioms-imply
∀g:GeometryPrimitives
(BasicGeometryAxioms(g)
⇒ ((∀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,d:Point. ((¬¬(∃w:Point. (B(cwd) ∧ cw ≅ 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. aa ≅ bb)
∧ (∀a,b,p,q,r,s:Point. (ab ≅ pq ⇒ ab ≅ rs ⇒ pq ≅ rs))
∧ (∀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,x,y:Point. (ax ≅ ay ⇒ bx ≅ by ⇒ cx ≅ cy ⇒ x # y ⇒ (¬a # bc)))))
Proof
Definitions occuring in Statement :
basic-geo-axioms: BasicGeometryAxioms(g),
geo-congruent: ab ≅ cd,
geo-between: B(abc),
geo-lsep: a # bc,
geo-sep: a # b,
geo-primitives: GeometryPrimitives,
geo-point: Point,
all: ∀x:A. B[x],
exists: ∃x:A. B[x],
not: ¬A,
implies: P ⇒ Q,
and: P ∧ Q
Definitions unfolded in proof :
all: ∀x:A. B[x],
implies: P ⇒ Q,
member: t ∈ T,
uall: ∀[x:A]. B[x],
prop: ℙ,
not: ¬A,
false: False,
geo-ge: ab ≥ cd,
basic-geo-axioms: BasicGeometryAxioms(g),
and: P ∧ Q,
cand: A c∧ B,
exists: ∃x:A. B[x],
guard: {T},
geo-sep: a # b,
geo-between: B(abc),
geo-lsep: a # bc,
or: P ∨ Q,
geo-congruent: ab ≅ cd,
geo-length-sep: ab # cd)
Latex:
\mforall{}g:GeometryPrimitives
(BasicGeometryAxioms(g)
{}\mRightarrow{} ((\mforall{}a:Point. (\mneg{}a \# a))
\mwedge{} (\mforall{}a,b,x,y:Point. ((\mneg{}a \# b) {}\mRightarrow{} B(xay) {}\mRightarrow{} B(xby)))
\mwedge{} (\mforall{}a,b,c:Point. ((\mneg{}a \# b) {}\mRightarrow{} ac \mcong{} cb))
\mwedge{} (\mforall{}a,b,c,d:Point. ((\mneg{}\mneg{}(\mexists{}w:Point. (B(cwd) \mwedge{} cw \mcong{} ab))) {}\mRightarrow{} a \# b {}\mRightarrow{} c \# d))
\mwedge{} (\mforall{}a,b,c:Point. ((\mneg{}a \# 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. aa \mcong{} bb)
\mwedge{} (\mforall{}a,b,p,q,r,s:Point. (ab \mcong{} pq {}\mRightarrow{} ab \mcong{} rs {}\mRightarrow{} pq \mcong{} rs))
\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,x,y:Point. (ax \mcong{} ay {}\mRightarrow{} bx \mcong{} by {}\mRightarrow{} cx \mcong{} cy {}\mRightarrow{} x \# y {}\mRightarrow{} (\mneg{}a \# bc)))))
Date html generated:
2020_05_20-AM-09_42_14
Last ObjectModification:
2020_01_27-PM-10_45_21
Theory : euclidean!plane!geometry
Home
Index