### Nuprl Lemma : euclid-P1-ext

`∀e:EuclideanPlane. ∀A,B:Point.  ∃C:Point. (AC=AB ∧ BC=AB ∧ AC=BC) supposing ¬(A = B ∈ Point)`

Proof

Definitions occuring in Statement :  euclidean-plane: `EuclideanPlane` eu-congruent: `ab=cd` eu-point: `Point` uimplies: `b supposing a` all: `∀x:A. B[x]` exists: `∃x:A. B[x]` not: `¬A` and: `P ∧ Q` equal: `s = t ∈ T`
Definitions unfolded in proof :  spreadn: spread7 stable__eu-congruent sq_stable__from_stable sq_stable__eu-congruent eu-seg-congruent-iff-length eu-congruent-iff-length record-select: `r.x` eu-extend: `(extend ab by cd)` eu-extend-exists uimplies: `b supposing a` so_apply: `x[s1;s2]` top: `Top` so_lambda: `λ2x y.t[x; y]` so_apply: `x[s1;s2;s3;s4]` so_lambda: `so_lambda(x,y,z,w.t[x; y; z; w])` uall: `∀[x:A]. B[x]` circle-circle-continuity1 euclid-P1 member: `t ∈ T`
Lemmas referenced :  stable__eu-congruent sq_stable__from_stable sq_stable__eu-congruent eu-seg-congruent-iff-length eu-congruent-iff-length eu-extend-exists circle-circle-continuity1 euclid-P1
Rules used in proof :  equalitySymmetry equalityTransitivity independent_isectElimination voidEquality voidElimination isect_memberEquality baseClosed isectElimination sqequalHypSubstitution thin sqequalRule hypothesis extract_by_obid instantiate cut sqequalReflexivity computationStep sqequalTransitivity sqequalSubstitution introduction

Latex:
\mforall{}e:EuclideanPlane.  \mforall{}A,B:Point.    \mexists{}C:Point.  (AC=AB  \mwedge{}  BC=AB  \mwedge{}  AC=BC)  supposing  \mneg{}(A  =  B)

Date html generated: 2016_07_08-PM-05_54_28
Last ObjectModification: 2016_07_05-PM-03_04_23

Theory : euclidean!geometry

Home Index