Nuprl Lemma : use-basic-geo-axioms-lemma

∀g:EuclideanPlane
  (((∀a,b,c,d:Point.  (ab>cd ⇒ ab ≥ cd)) ∧ (∀a,b,c:Point.  (ba>ac ⇒ b # c)) ∧ (∀a,b,c:Point.  bc ≥ aa))
  ∧ (∀a,b,c,d,e,f:Point.  (ab>cd ⇒ cd ≥ ef ⇒ ab>ef))
  ∧ (∀a,b,c,d,e,f:Point.  (ab ≥ cd ⇒ cd>ef ⇒ ab>ef))
  ∧ (∀a,b,c:Point.  (B(abc) ⇒ b # c ⇒ ac>ab))
  ∧ (∀a,b,c:Point.  (a leftof bc ⇒ b leftof ca))
  ∧ (∀a,b,c:Point.  (a leftof bc ⇒ b # c))
  ∧ (∀a,b,c,d:Point.  (B(abd) ⇒ B(bcd) ⇒ B(abc)))
  ∧ (∀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)))
  ∧ (∀a,b,x,y,z:Point.  (x leftof ab ⇒ y leftof ab ⇒ B(xzy) ⇒ z leftof ab))
  ∧ (∀a,b,c,y:Point.  (a # bc ⇒ y # b ⇒ (¬y # ab) ⇒ y # bc)))


Proof



Definitions occuring in Statement :  euclidean-plane: EuclideanPlane,  geo-ge: ab ≥ cd,  geo-congruent: ab ≅ cd,  geo-between: B(abc),  geo-lsep: a # bc,  geo-left: a leftof bc,  geo-sep: a # b,  geo-gt-prim: ab>cd,  geo-point: Point,  all: ∀x:A. B[x],  not: ¬A,  implies: P ⇒ Q,  and: P ∧ Q
Definitions unfolded in proof :  all: ∀x:A. B[x],  euclidean-plane: EuclideanPlane,  member: t ∈ T,  prop: ℙ,  and: P ∧ Q,  uall: ∀[x:A]. B[x],  subtype_rel: A ⊆r B,  implies: P ⇒ Q,  so_lambda: λ2x.t[x],  so_apply: x[s],  sq_stable: SqStable(P),  squash: ↓T,  not: ¬A,  false: False,  basic-geo-axioms: BasicGeometryAxioms(g),  cand: A c∧ B,  geo-ge: ab ≥ cd,  geo-between: B(abc),  geo-congruent: ab ≅ cd,  geo-colinear: Colinear(a;b;c)
Latex:
\mforall{}g:EuclideanPlane
    (((\mforall{}a,b,c,d:Point.    (ab>cd  {}\mRightarrow{}  ab  \mgeq{}  cd))
      \mwedge{}  (\mforall{}a,b,c:Point.    (ba>ac  {}\mRightarrow{}  b  \#  c))
      \mwedge{}  (\mforall{}a,b,c:Point.    bc  \mgeq{}  aa))
    \mwedge{}  (\mforall{}a,b,c,d,e,f:Point.    (ab>cd  {}\mRightarrow{}  cd  \mgeq{}  ef  {}\mRightarrow{}  ab>ef))
    \mwedge{}  (\mforall{}a,b,c,d,e,f:Point.    (ab  \mgeq{}  cd  {}\mRightarrow{}  cd>ef  {}\mRightarrow{}  ab>ef))
    \mwedge{}  (\mforall{}a,b,c:Point.    (B(abc)  {}\mRightarrow{}  b  \#  c  {}\mRightarrow{}  ac>ab))
    \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,c,d:Point.    (B(abd)  {}\mRightarrow{}  B(bcd)  {}\mRightarrow{}  B(abc)))
    \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)))
    \mwedge{}  (\mforall{}a,b,x,y,z:Point.    (x  leftof  ab  {}\mRightarrow{}  y  leftof  ab  {}\mRightarrow{}  B(xzy)  {}\mRightarrow{}  z  leftof  ab))
    \mwedge{}  (\mforall{}a,b,c,y:Point.    (a  \#  bc  {}\mRightarrow{}  y  \#  b  {}\mRightarrow{}  (\mneg{}y  \#  ab)  {}\mRightarrow{}  y  \#  bc)))


Date html generated: 2020_05_20-AM-09_44_06
Last ObjectModification: 2020_01_27-PM-05_19_46

Theory : euclidean!plane!geometry


Home Index