Nuprl Lemma : geo-lt-angle-in-half-plane-implies-left2

e:EuclideanPlane. ∀w,x,y,z:Point.  (xyz < wyz  leftof zy  leftof zy  leftof xy)


Proof




Definitions occuring in Statement :  geo-lt-angle: abc < xyz euclidean-plane: EuclideanPlane geo-left: leftof bc geo-point: Point all: x:A. B[x] implies:  Q
Definitions unfolded in proof :  all: x:A. B[x] implies:  Q member: t ∈ T uall: [x:A]. B[x] subtype_rel: A ⊆B guard: {T} uimplies: supposing a prop: and: P ∧ Q cand: c∧ B geo-lt-angle: abc < xyz exists: x:A. B[x] geo-lsep: bc or: P ∨ Q geo-out: out(p ab) basic-geometry: BasicGeometry geo-colinear-set: geo-colinear-set(e; L) l_all: (∀x∈L.P[x]) top: Top int_seg: {i..j-} lelt: i ≤ j < k decidable: Dec(P) not: ¬A satisfiable_int_formula: satisfiable_int_formula(fmla) false: False select: L[n] cons: [a b] subtract: m oriented-plane: OrientedPlane
Lemmas referenced :  geo-left_wf euclidean-plane-structure-subtype euclidean-plane-subtype subtype_rel_transitivity euclidean-plane_wf euclidean-plane-structure_wf geo-primitives_wf geo-lt-angle_wf geo-point_wf lsep-all-sym2 geo-lt-angle-symm lsep-all-sym colinear-lsep geo-sep-sym geo-colinear-is-colinear-set geo-out-colinear length_of_cons_lemma istype-void length_of_nil_lemma decidable__le full-omega-unsat intformnot_wf intformle_wf itermConstant_wf istype-int int_formula_prop_not_lemma int_formula_prop_le_lemma int_term_value_constant_lemma int_formula_prop_wf decidable__lt intformless_wf int_formula_prop_less_lemma istype-le istype-less_than colinear-lsep2 geo-between-implies-colinear left-implies-sep interior-angles-unique2-symm lsep-symmetry geo-out_weakening geo-eq_weakening out-preserves-lsep cong-angle-preserves-lsep_strong geo-between-sep lsep-implies-sep geo-between_wf geo-cong-angle-symm2 out-preserves-angle-cong_1 geo-left-out-1 geo-left-out-3 geo-left-out-2 geo-out_inversion geo-lt-angle-symm2 geo-cong-angle-symmetry geo-lt-angle-left2 left-symmetry lt-angle-irrefl
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity lambdaFormation_alt cut universeIsType introduction extract_by_obid sqequalHypSubstitution isectElimination thin hypothesisEquality applyEquality hypothesis instantiate independent_isectElimination sqequalRule because_Cache dependent_functionElimination inhabitedIsType independent_functionElimination productElimination inrFormation_alt isect_memberEquality_alt voidElimination dependent_set_memberEquality_alt natural_numberEquality independent_pairFormation unionElimination approximateComputation dependent_pairFormation_alt lambdaEquality_alt productIsType functionIsType

Latex:
\mforall{}e:EuclideanPlane.  \mforall{}w,x,y,z:Point.    (xyz  <  wyz  {}\mRightarrow{}  w  leftof  zy  {}\mRightarrow{}  x  leftof  zy  {}\mRightarrow{}  w  leftof  xy)



Date html generated: 2019_10_16-PM-02_29_18
Last ObjectModification: 2019_09_24-PM-03_26_19

Theory : euclidean!plane!geometry


Home Index