Nuprl Lemma : Prop23-construction-lemma

e:EuclideanPlane. ∀p,q,r,a,a':Point.
  (p qr  a ≠ a'  (∃b,c1,c2:Point. (((pq ≅ ab ∧ out(a a'b)) ∧ pr ≅ ac1 ∧ bc2 > bc1) ∧ qr ≅ bc2 ∧ ac1 > ac2)))


Proof




Definitions occuring in Statement :  geo-out: out(p ab) euclidean-plane: EuclideanPlane geo-lsep: bc geo-gt: cd > ab geo-congruent: ab ≅ cd geo-sep: a ≠ b geo-point: Point all: x:A. B[x] exists: x:A. B[x] implies:  Q and: P ∧ Q
Definitions unfolded in proof :  all: x:A. B[x] implies:  Q member: t ∈ T and: P ∧ Q basic-geometry: BasicGeometry euclidean-plane: EuclideanPlane exists: x:A. B[x] subtype_rel: A ⊆B uall: [x:A]. B[x] guard: {T} uimplies: supposing a basic-geometry-: BasicGeometry- iff: ⇐⇒ Q prop: geo-strict-between: a-b-c geo-out: out(p ab) uiff: uiff(P;Q) squash: T true: True rev_implies:  Q or: P ∨ Q l_member: (x ∈ l) nat: decidable: Dec(P) not: ¬A satisfiable_int_formula: satisfiable_int_formula(fmla) top: Top false: False select: L[n] cons: [a b] subtract: m cand: c∧ B less_than: a < b less_than': less_than'(a;b) ge: i ≥  append: as bs so_lambda: so_lambda(x,y,z.t[x; y; z]) so_apply: x[s1;s2;s3] geo-colinear-set: geo-colinear-set(e; L) l_all: (∀x∈L.P[x]) int_seg: {i..j-} lelt: i ≤ j < k geo-gt: cd > ab geo-eq: a ≡ b
Lemmas referenced :  Euclid-Prop20_cycle geo-proper-extend-exists geo-O_wf geo-X_wf geo-sep-sym geo-sep-O-X geo-strict-between-sep3 euclidean-plane-structure-subtype euclidean-plane-subtype subtype_rel_transitivity euclidean-plane_wf euclidean-plane-structure_wf geo-primitives_wf lsep-implies-sep geo-out-iff-between1 euclidean-plane-axioms geo-between-symmetry geo-strict-between-implies-between geo-out_inversion geo-congruent_wf geo-out_wf geo-gt_wf geo-sep_wf geo-lsep_wf geo-point_wf Prop22-symmetric-point-construction-lemma extend-using-SC geo-congruent-iff-length geo-length-flip geo-add-length-between geo-add-length_wf geo-length_wf geo-mk-seg_wf squash_wf true_wf geo-length-type_wf equal_wf istype-universe geo-add-length_functionality_wrt_cong subtype_rel_self iff_weakening_equal geo-lt_wf geo-lt-out-to-between geo-strict-between-sep1 geo-between-outer-trans geo-between-exchange4 geo-between-implies-out2 geo-strict-between-sym basic-geometry_wf geo-add-length-comm geo-length_wf1 geo-add-length_wf1 geo-zero-point-sep-iff-sep geo-lt-sep geo-length-equality geo-lt-add1-iff geo-between-out geo-strict-between-sep2 geo-out_transitivity geo-lt-add1-iff2 geo-between-inner-trans geo-add-length-assoc geo-sep-or colinear-implies-midpoint geo-colinear-append cons_wf nil_wf decidable__le full-omega-unsat intformnot_wf intformle_wf itermConstant_wf istype-int int_formula_prop_not_lemma istype-void int_formula_prop_le_lemma int_term_value_constant_lemma int_formula_prop_wf istype-le length_of_cons_lemma length_of_nil_lemma istype-less_than length_wf select_wf nat_properties intformand_wf itermVar_wf int_formula_prop_and_lemma int_term_value_var_lemma l_member_wf geo-colinear-is-colinear-set geo-strict-between-implies-colinear list_ind_cons_lemma list_ind_nil_lemma geo-out-colinear geo-between-implies-colinear decidable__lt intformless_wf int_formula_prop_less_lemma midpoint-sep geo-between-same-side-or geo-between-exchange3 geo-congruent-refl geo-between_wf geo-construction-unicity congruence-preserves-between_symmetric-points2 geo-strict-between-trans3 geo-strict-between_wf geo-strict-between-trans geo-between-same geo-eq_inversion geo-construction-unicity-from-first geo-congruent-preserves-gt geo-between-sep geo-between-outer-trans2 geo-congruent-sep
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity lambdaFormation_alt cut introduction extract_by_obid sqequalHypSubstitution dependent_functionElimination thin hypothesisEquality independent_functionElimination hypothesis productElimination sqequalRule setElimination rename because_Cache applyEquality instantiate isectElimination independent_isectElimination dependent_pairFormation_alt productIsType universeIsType inhabitedIsType equalityTransitivity equalitySymmetry dependent_set_memberEquality_alt independent_pairFormation equalityIstype applyLambdaEquality lambdaEquality_alt imageElimination natural_numberEquality imageMemberEquality baseClosed universeEquality hyp_replacement unionElimination approximateComputation isect_memberEquality_alt voidElimination int_eqEquality

Latex:
\mforall{}e:EuclideanPlane.  \mforall{}p,q,r,a,a':Point.
    (p  \#  qr
    {}\mRightarrow{}  a  \mneq{}  a'
    {}\mRightarrow{}  (\mexists{}b,c1,c2:Point.  (((pq  \mcong{}  ab  \mwedge{}  out(a  a'b))  \mwedge{}  pr  \mcong{}  ac1  \mwedge{}  bc2  >  bc1)  \mwedge{}  qr  \mcong{}  bc2  \mwedge{}  ac1  >  ac2)))



Date html generated: 2019_10_16-PM-02_30_18
Last ObjectModification: 2019_03_14-AM-08_51_03

Theory : euclidean!plane!geometry


Home Index