Nuprl Lemma : p8eu

`∀e:EuclideanPlane. ∀a,b,c,x,y,z:Point.`
`  Cong3(abc,xyz) `` (abc = xyz ∧ bac = yxz ∧ bca = yzx) supposing Triangle(a;b;c) ∧ Triangle(x;y;z)`

Proof

Definitions occuring in Statement :  eu-cong-tri: `Cong3(abc,a'b'c')` eu-cong-angle: `abc = xyz` eu-tri: `Triangle(a;b;c)` euclidean-plane: `EuclideanPlane` eu-point: `Point` uimplies: `b supposing a` all: `∀x:A. B[x]` implies: `P `` Q` and: `P ∧ Q`
Definitions unfolded in proof :  so_apply: `x[s]` so_lambda: `λ2x.t[x]` uiff: `uiff(P;Q)` exists: `∃x:A. B[x]` prop: `ℙ` eu-cong-angle: `abc = xyz` eu-cong-tri: `Cong3(abc,a'b'c')` cand: `A c∧ B` euclidean-plane: `EuclideanPlane` uall: `∀[x:A]. B[x]` false: `False` implies: `P `` Q` not: `¬A` eu-tri: `Triangle(a;b;c)` and: `P ∧ Q` member: `t ∈ T` uimplies: `b supposing a` all: `∀x:A. B[x]`
Rules used in proof :  equalityTransitivity independent_isectElimination dependent_pairFormation productEquality because_Cache equalitySymmetry independent_functionElimination independent_pairFormation hypothesis rename setElimination isectElimination extract_by_obid equalityEquality voidElimination hypothesisEquality dependent_functionElimination lambdaEquality independent_pairEquality thin productElimination sqequalHypSubstitution sqequalRule introduction cut isect_memberFormation lambdaFormation sqequalReflexivity computationStep sqequalTransitivity sqequalSubstitution

Latex:
\mforall{}e:EuclideanPlane.  \mforall{}a,b,c,x,y,z:Point.
Cong3(abc,xyz)  {}\mRightarrow{}  (abc  =  xyz  \mwedge{}  bac  =  yxz  \mwedge{}  bca  =  yzx)  supposing  Triangle(a;b;c)  \mwedge{}  Triangle(x;y;z)

Date html generated: 2016_07_08-PM-05_54_27
Last ObjectModification: 2016_07_05-PM-03_04_37

Theory : euclidean!geometry

Home Index