### Nuprl Lemma : p4eu

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

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-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` cand: `A c∧ B` prop: `ℙ` eu-cong-angle: `abc = xyz` exists: `∃x:A. B[x]` so_lambda: `λ2x.t[x]` so_apply: `x[s]` uiff: `uiff(P;Q)` eu-cong-tri: `Cong3(abc,a'b'c')`
Lemmas referenced :  eu-point_wf eu-congruent_wf eu-cong-angle_wf eu-tri_wf euclidean-plane_wf eu-sas equal_wf not_wf eu-congruence-identity false_wf eu-between-eq_wf exists_wf eu-between-eq-trivial-right eu-congruent-iff-length eu-length-flip
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 extract_by_obid isectElimination setElimination rename hypothesis independent_pairFormation productEquality because_Cache independent_isectElimination independent_functionElimination equalitySymmetry hyp_replacement Error :applyLambdaEquality,  equalityTransitivity universeEquality dependent_pairFormation

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

Date html generated: 2016_10_26-AM-07_46_19
Last ObjectModification: 2016_07_12-AM-08_16_54

Theory : euclidean!geometry

Home Index