Nuprl Lemma : lsep-lt-straight-angle

e:EuclideanPlane. ∀a,b,c,x,y,z:Point.  (a bc  x-y-z  abc < xyz)


Proof




Definitions occuring in Statement :  geo-lt-angle: abc < xyz euclidean-plane: EuclideanPlane geo-lsep: bc geo-strict-between: a-b-c geo-point: Point all: x:A. B[x] implies:  Q
Definitions unfolded in proof :  all: x:A. B[x] implies:  Q member: t ∈ T subtype_rel: A ⊆B uall: [x:A]. B[x] guard: {T} uimplies: supposing a exists: x:A. B[x] and: P ∧ Q prop: basic-geometry: BasicGeometry basic-geometry-: BasicGeometry- geo-lt-angle: abc < xyz cand: c∧ B oriented-plane: OrientedPlane 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) or: P ∨ Q not: ¬A satisfiable_int_formula: satisfiable_int_formula(fmla) false: False select: L[n] cons: [a b] subtract: m
Lemmas referenced :  Euclid-Prop23_half-plane2 geo-sep-sym geo-strict-between-sep2 euclidean-plane-structure-subtype euclidean-plane-subtype subtype_rel_transitivity euclidean-plane_wf euclidean-plane-structure_wf geo-primitives_wf geo-strict-between_wf geo-lsep_wf geo-point_wf geo-not-bet-and-out geo-strict-between-implies-between geo-between-trivial2 geo-out_weakening geo-eq_weakening geo-strict-between-sep3 lsep-not-between colinear-lsep-cycle lsep-all-sym2 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 lsep-all-sym geo-between-symmetry geo-between-inner-trans euclidean-plane-axioms geo-cong-angle_wf geo-between_wf geo-out_wf geo-sep_wf geo-cong-angle-symm2 lsep-implies-sep geo-out_inversion left-implies-sep geo-cong-angle-symmetry out-preserves-angle-cong_1
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity lambdaFormation_alt cut introduction extract_by_obid sqequalHypSubstitution dependent_functionElimination thin hypothesisEquality independent_functionElimination hypothesis because_Cache applyEquality instantiate isectElimination independent_isectElimination sqequalRule productElimination universeIsType inhabitedIsType independent_pairFormation dependent_pairFormation_alt isect_memberEquality_alt voidElimination dependent_set_memberEquality_alt natural_numberEquality unionElimination approximateComputation lambdaEquality_alt productIsType functionIsType

Latex:
\mforall{}e:EuclideanPlane.  \mforall{}a,b,c,x,y,z:Point.    (a  \#  bc  {}\mRightarrow{}  x-y-z  {}\mRightarrow{}  abc  <  xyz)



Date html generated: 2019_10_16-PM-02_32_08
Last ObjectModification: 2019_09_24-PM-03_09_21

Theory : euclidean!plane!geometry


Home Index