### Nuprl Lemma : circle-circle-continuity2

`∀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) ∧ (¬(x = z ∈ Point))))`
`  `` (∃z1,z2:Point. (az1=ab ∧ az2=ab ∧ cz1=cd ∧ cz2=cd ∧ (¬(z1 = z2 ∈ Point)))))`

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` not: `¬A` false: `False` prop: `ℙ` uall: `∀[x:A]. B[x]` euclidean-plane: `EuclideanPlane` so_lambda: `λ2x.t[x]` so_apply: `x[s]`
Lemmas referenced :  circle-circle-continuity equal_wf eu-point_wf eu-congruent_wf not_wf exists_wf eu-between-eq_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_functionElimination independent_pairFormation equalitySymmetry voidElimination isectElimination setElimination rename productEquality because_Cache sqequalRule lambdaEquality

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)  \mwedge{}  (\mneg{}(x  =  z))))
{}\mRightarrow{}  (\mexists{}z1,z2:Point.  (az1=ab  \mwedge{}  az2=ab  \mwedge{}  cz1=cd  \mwedge{}  cz2=cd  \mwedge{}  (\mneg{}(z1  =  z2)))))

Date html generated: 2016_05_18-AM-06_41_41
Last ObjectModification: 2015_12_28-AM-09_23_48

Theory : euclidean!geometry

Home Index