### Nuprl Lemma : eu-cong3-to-conga

`∀e:EuclideanPlane. ∀a,b,c,d,E,f:Point.`
`  ((∃a',c',d',f':Point. (out(b a'a) ∧ out(b c'c) ∧ out(E d'd) ∧ out(E f'f) ∧ Cong3(a'bc',d'Ef'))) `` abc = dEf)`

Proof

Definitions occuring in Statement :  eu-out: `out(p ab)` eu-cong-tri: `Cong3(abc,a'b'c')` eu-cong-angle: `abc = xyz` euclidean-plane: `EuclideanPlane` 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` exists: `∃x:A. B[x]` and: `P ∧ Q` member: `t ∈ T` prop: `ℙ` uall: `∀[x:A]. B[x]` euclidean-plane: `EuclideanPlane` so_lambda: `λ2x.t[x]` so_apply: `x[s]` eu-cong-angle: `abc = xyz` not: `¬A` eu-out: `out(p ab)` cand: `A c∧ B` false: `False` eu-cong-tri: `Cong3(abc,a'b'c')` uiff: `uiff(P;Q)` uimplies: `b supposing a` eu-five-seg-compressed: `FSC(a;b;c;d  a';b';c';d')` stable: `Stable{P}` iff: `P `⇐⇒` Q` rev_implies: `P `` Q` or: `P ∨ Q` guard: `{T}` append: `as @ bs` so_lambda: `so_lambda(x,y,z.t[x; y; z])` top: `Top` so_apply: `x[s1;s2;s3]` eu-colinear-set: `eu-colinear-set(e;L)` l_all: `(∀x∈L.P[x])` int_seg: `{i..j-}` lelt: `i ≤ j < k` le: `A ≤ B` less_than': `less_than'(a;b)` less_than: `a < b` squash: `↓T` true: `True` select: `L[n]` cons: `[a / b]` subtract: `n - m`
Lemmas referenced :  exists_wf eu-point_wf eu-out_wf eu-cong-tri_wf euclidean-plane_wf equal_wf eu-extend-exists not_wf eu-between-eq_wf eu-congruent_wf eu-out-refl eu-cong3-to-conga-aux eu-congruent-iff-length eu-length-flip eu-fsc-ap stable__colinear eu-colinear_wf eu-colinear-append cons_wf nil_wf cons_member l_member_wf eu-colinear-is-colinear-set eu-between-eq-implies-colinear list_ind_cons_lemma list_ind_nil_lemma length_of_cons_lemma length_of_nil_lemma false_wf lelt_wf eu-between-eq-exchange3 eu-between-eq-symmetry eu-between-eq-exchange4
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity lambdaFormation sqequalHypSubstitution productElimination thin cut introduction extract_by_obid isectElimination setElimination rename because_Cache hypothesis sqequalRule lambdaEquality productEquality hypothesisEquality independent_pairFormation independent_functionElimination equalitySymmetry voidElimination dependent_functionElimination dependent_set_memberEquality dependent_pairFormation independent_isectElimination equalityTransitivity inlFormation inrFormation isect_memberEquality voidEquality natural_numberEquality imageMemberEquality baseClosed

Latex:
\mforall{}e:EuclideanPlane.  \mforall{}a,b,c,d,E,f:Point.
((\mexists{}a',c',d',f':Point.  (out(b  a'a)  \mwedge{}  out(b  c'c)  \mwedge{}  out(E  d'd)  \mwedge{}  out(E  f'f)  \mwedge{}  Cong3(a'bc',d'Ef')))
{}\mRightarrow{}  abc  =  dEf)

Date html generated: 2016_10_26-AM-07_45_33
Last ObjectModification: 2016_08_04-PM-06_59_09

Theory : euclidean!geometry

Home Index