### Nuprl Lemma : euclid-P2

e:EuclideanPlane. ∀A,B,C:Point.  ∃L:Point. AL=BC supposing ¬(A B ∈ Point)

Proof

Definitions occuring in Statement :  euclidean-plane: EuclideanPlane eu-congruent: ab=cd eu-point: Point uimplies: supposing a all: x:A. B[x] exists: x:A. B[x] not: ¬A equal: t ∈ T
Definitions unfolded in proof :  all: x:A. B[x] uimplies: supposing a member: t ∈ T not: ¬A implies:  Q false: False uall: [x:A]. B[x] euclidean-plane: EuclideanPlane prop: and: P ∧ Q exists: x:A. B[x]
Lemmas referenced :  eu-point_wf not_wf equal_wf euclidean-plane_wf eu-congruent_wf eu-extend-exists
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity lambdaFormation isect_memberFormation cut introduction sqequalRule sqequalHypSubstitution lambdaEquality dependent_functionElimination thin hypothesisEquality voidElimination equalityEquality lemma_by_obid isectElimination setElimination rename hypothesis independent_functionElimination equalitySymmetry dependent_set_memberEquality productElimination dependent_pairFormation

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

Date html generated: 2016_05_18-AM-06_45_58
Last ObjectModification: 2015_12_28-AM-09_21_53

Theory : euclidean!geometry

Home Index