### Nuprl Lemma : eu-sas

`∀e:EuclideanPlane. ∀a,b,c,A,B,C:Point.`
`  ((ab=AB ∧ ac=AC) ∧ bac = BAC) `` bc=BC supposing Triangle(a;b;c) ∧ Triangle(A;B;C)`

Proof

Definitions occuring in Statement :  eu-cong-angle: `abc = xyz` eu-tri: `Triangle(a;b;c)` euclidean-plane: `EuclideanPlane` eu-congruent: `ab=cd` eu-point: `Point` uimplies: `b supposing a` all: `∀x:A. B[x]` implies: `P `` Q` and: `P ∧ Q`
Definitions unfolded in proof :  all: `∀x:A. B[x]` uimplies: `b supposing a` member: `t ∈ T` and: `P ∧ Q` eu-tri: `Triangle(a;b;c)` not: `¬A` implies: `P `` Q` false: `False` uall: `∀[x:A]. B[x]` euclidean-plane: `EuclideanPlane` prop: `ℙ` eu-cong-angle: `abc = xyz` exists: `∃x:A. B[x]` uiff: `uiff(P;Q)`
Lemmas referenced :  eu-inner-five-segment' eu-five-segment' eu-inner-three-segment eu-congruent-trivial equal_wf eu-length-flip eu-congruent-iff-length eu-between-eq-symmetry euclidean-plane_wf eu-tri_wf eu-cong-angle_wf eu-congruent_wf eu-point_wf
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity lambdaFormation isect_memberFormation cut introduction sqequalRule sqequalHypSubstitution productElimination thin independent_pairEquality lambdaEquality dependent_functionElimination hypothesisEquality voidElimination equalityEquality lemma_by_obid isectElimination setElimination rename hypothesis productEquality because_Cache independent_isectElimination equalityTransitivity equalitySymmetry independent_functionElimination

Latex:
\mforall{}e:EuclideanPlane.  \mforall{}a,b,c,A,B,C:Point.
((ab=AB  \mwedge{}  ac=AC)  \mwedge{}  bac  =  BAC)  {}\mRightarrow{}  bc=BC  supposing  Triangle(a;b;c)  \mwedge{}  Triangle(A;B;C)

Date html generated: 2016_06_16-PM-01_32_40
Last ObjectModification: 2016_06_01-PM-02_41_14

Theory : euclidean!geometry

Home Index