Nuprl Lemma : p5eu

`∀e:EuclideanPlane. ∀a,b,c:Point.  ((ab=ac ∧ Triangle(a;b;c)) `` (∃j,k:Point. jbc = kcb))`

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` all: `∀x:A. B[x]` exists: `∃x:A. B[x]` implies: `P `` Q` and: `P ∧ Q`
Definitions unfolded in proof :  all: `∀x:A. B[x]` implies: `P `` Q` and: `P ∧ Q` member: `t ∈ T` prop: `ℙ` uall: `∀[x:A]. B[x]` euclidean-plane: `EuclideanPlane` eu-tri: `Triangle(a;b;c)` exists: `∃x:A. B[x]` so_lambda: `λ2x.t[x]` so_apply: `x[s]` eu-cong-angle: `abc = xyz` cand: `A c∧ B` not: `¬A` false: `False` uimplies: `b supposing a` uiff: `uiff(P;Q)`
Lemmas referenced :  eu-congruent_wf eu-tri_wf eu-point_wf euclidean-plane_wf not_wf equal_wf eu-extend-exists eu-cong-angle_wf exists_wf eu-between-eq_wf eu-congruence-identity-sym false_wf eu-between-eq-trivial-right eu-congruent-iff-length eu-congruent-flip eu-congruent-refl eu-length-flip eu-three-segment eu-five-segment'
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity lambdaFormation sqequalHypSubstitution productElimination thin productEquality cut introduction extract_by_obid isectElimination setElimination rename hypothesisEquality hypothesis dependent_functionElimination dependent_set_memberEquality dependent_pairFormation sqequalRule lambdaEquality because_Cache equalitySymmetry hyp_replacement Error :applyLambdaEquality,  independent_functionElimination independent_isectElimination voidElimination equalityTransitivity equalityEquality universeEquality independent_pairFormation

Latex:
\mforall{}e:EuclideanPlane.  \mforall{}a,b,c:Point.    ((ab=ac  \mwedge{}  Triangle(a;b;c))  {}\mRightarrow{}  (\mexists{}j,k:Point.  jbc  =  kcb))

Date html generated: 2016_10_26-AM-07_45_51
Last ObjectModification: 2016_07_12-AM-08_13_24

Theory : euclidean!geometry

Home Index