### Nuprl Lemma : circle-circle-continuity1

`∀e:EuclideanPlane. ∀a,b,c,d:Point.`
`  ((¬(a = c ∈ Point))`
`  `` (∃p,q,x,z:Point. (a_x_b ∧ a_b_z ∧ ap=ax ∧ aq=az ∧ cp=cd ∧ cq=cd))`
`  `` (∃y:Point. (ay=ab ∧ cy=cd)))`

Proof

Definitions occuring in Statement :  euclidean-plane: `EuclideanPlane` eu-between-eq: `a_b_c` eu-congruent: `ab=cd` eu-point: `Point` all: `∀x:A. B[x]` exists: `∃x:A. B[x]` not: `¬A` implies: `P `` Q` and: `P ∧ Q` equal: `s = t ∈ T`
Definitions unfolded in proof :  all: `∀x:A. B[x]` implies: `P `` Q` exists: `∃x:A. B[x]` and: `P ∧ Q` member: `t ∈ T` uimplies: `b supposing a` cand: `A c∧ B` prop: `ℙ` uall: `∀[x:A]. B[x]` euclidean-plane: `EuclideanPlane` so_lambda: `λ2x.t[x]` so_apply: `x[s]`
Lemmas referenced :  circle-circle-continuity and_wf eu-congruent_wf exists_wf eu-point_wf eu-between-eq_wf not_wf equal_wf euclidean-plane_wf
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity lambdaFormation sqequalHypSubstitution productElimination thin cut lemma_by_obid dependent_functionElimination hypothesisEquality independent_isectElimination hypothesis dependent_pairFormation independent_pairFormation isectElimination setElimination rename sqequalRule lambdaEquality because_Cache productEquality

Latex:
\mforall{}e:EuclideanPlane.  \mforall{}a,b,c,d:Point.
((\mneg{}(a  =  c))
{}\mRightarrow{}  (\mexists{}p,q,x,z:Point.  (a\_x\_b  \mwedge{}  a\_b\_z  \mwedge{}  ap=ax  \mwedge{}  aq=az  \mwedge{}  cp=cd  \mwedge{}  cq=cd))
{}\mRightarrow{}  (\mexists{}y:Point.  (ay=ab  \mwedge{}  cy=cd)))

Date html generated: 2016_05_18-AM-06_41_44
Last ObjectModification: 2015_12_28-AM-09_23_23

Theory : euclidean!geometry

Home Index