Nuprl Lemma : hp-angle-sum-lt

∀e:EuclideanPlane. ∀a,b,c,x,y,z,i,j,k,a',b',c',x',y',z',i',j',k':Point.
  (abc ≅a a'b'c'
  ⇒ abc + xyz ≅ ijk
  ⇒ a'b'c' + x'y'z' ≅ i'j'k'
  ⇒ i # jk
  ⇒ i' # j'k'
  ⇒ x # yz
  ⇒ xyz < x'y'z'
  ⇒ ijk < i'j'k')


Proof



Definitions occuring in Statement :  hp-angle-sum: abc + xyz ≅ def,  geo-lt-angle: abc < xyz,  geo-cong-angle: abc ≅a xyz,  euclidean-plane: EuclideanPlane,  geo-lsep: a # bc,  geo-point: Point,  all: ∀x:A. B[x],  implies: P ⇒ Q
Definitions unfolded in proof :  all: ∀x:A. B[x],  implies: P ⇒ Q,  hp-angle-sum: abc + xyz ≅ def,  exists: ∃x:A. B[x],  and: P ∧ Q,  member: t ∈ T,  guard: {T},  cand: A c∧ B,  subtype_rel: A ⊆r B,  uall: ∀[x:A]. B[x],  uimplies: b supposing a,  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),  or: P ∨ Q,  not: ¬A,  satisfiable_int_formula: satisfiable_int_formula(fmla),  prop: ℙ,  false: False,  select: L[n],  cons: [a / b],  subtract: n - m,  geo-out: out(p ab),  geo-cong-angle: abc ≅a xyz,  geo-lt-angle: abc < xyz,  geo-strict-between: a-b-c,  basic-geometry-: BasicGeometry-,  l_member: (x ∈ l),  nat: ℕ,  le: A ≤ B,  less_than': less_than'(a;b),  less_than: a < b,  squash: ↓T,  true: True,  ge: i ≥ j ,  append: as @ bs,  so_lambda: so_lambda(x,y,z.t[x; y; z]),  so_apply: x[s1;s2;s3],  oriented-plane: OrientedPlane
Lemmas referenced :  out-preserves-lsep,  lsep-symmetry,  lsep-all-sym,  colinear-lsep,  geo-strict-between-sep3,  euclidean-plane-structure-subtype,  euclidean-plane-subtype,  subtype_rel_transitivity,  euclidean-plane_wf,  euclidean-plane-structure_wf,  geo-primitives_wf,  geo-colinear-is-colinear-set,  geo-strict-between-implies-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,  geo-cong-angle-preserves-lt-angle2,  geo-lt-angle_wf,  geo-lsep_wf,  hp-angle-sum_wf,  geo-cong-angle_wf,  geo-point_wf,  geo-out_weakening,  geo-sep-sym,  lsep-implies-sep,  geo-eq_weakening,  geo-out_inversion,  out-preserves-angle-cong_1,  geo-between-sep,  geo-between_wf,  geo-between-trivial,  geo-cong-angle-symmetry,  euclidean-plane-axioms,  geo-between-implies-colinear,  cong-angle-preserves-lsep_strong,  geo-cong-angle-symm2,  geo-out-interior-point-exists,  colinear-lsep-cycle,  geo-out_transitivity,  geo-strict-between_wf,  geo-cong-angle-transitivity,  out-cong-angle,  geo-out-colinear,  not-lsep-if-colinear,  geo-out_wf,  geo-between-symmetry,  geo-strict-between-implies-between,  geo-between-inner-trans,  geo-between-outer-trans,  geo-strict-between-sep2,  geo-sep_wf,  hp-angle-sum-eq,  geo-strict-between-sym,  geo-strict-between-trans,  geo-strict-between-trans2,  geo-strict-between-sep1,  geo-colinear-append,  cons_wf,  nil_wf,  length_wf,  select_wf,  nat_properties,  intformand_wf,  itermVar_wf,  int_formula_prop_and_lemma,  int_term_value_var_lemma,  l_member_wf,  list_ind_cons_lemma,  list_ind_nil_lemma,  lsep-not-between
Rules used in proof :  sqequalSubstitution,  sqequalTransitivity,  computationStep,  sqequalReflexivity,  lambdaFormation_alt,  sqequalHypSubstitution,  productElimination,  thin,  cut,  introduction,  extract_by_obid,  dependent_functionElimination,  hypothesisEquality,  independent_functionElimination,  because_Cache,  hypothesis,  applyEquality,  instantiate,  isectElimination,  independent_isectElimination,  sqequalRule,  isect_memberEquality_alt,  voidElimination,  dependent_set_memberEquality_alt,  natural_numberEquality,  independent_pairFormation,  unionElimination,  approximateComputation,  dependent_pairFormation_alt,  lambdaEquality_alt,  universeIsType,  productIsType,  inhabitedIsType,  functionIsType,  imageMemberEquality,  baseClosed,  setElimination,  rename,  equalityIstype,  int_eqEquality,  equalityTransitivity,  equalitySymmetry
Latex:
\mforall{}e:EuclideanPlane.  \mforall{}a,b,c,x,y,z,i,j,k,a',b',c',x',y',z',i',j',k':Point.
    (abc  \mcong{}\msuba{}  a'b'c'
    {}\mRightarrow{}  abc  +  xyz  \mcong{}  ijk
    {}\mRightarrow{}  a'b'c'  +  x'y'z'  \mcong{}  i'j'k'
    {}\mRightarrow{}  i  \#  jk
    {}\mRightarrow{}  i'  \#  j'k'
    {}\mRightarrow{}  x  \#  yz
    {}\mRightarrow{}  xyz  <  x'y'z'
    {}\mRightarrow{}  ijk  <  i'j'k')


Date html generated: 2019_10_16-PM-02_27_37
Last ObjectModification: 2019_09_24-PM-03_01_12

Theory : euclidean!plane!geometry


Home Index