Nuprl Lemma : greatest-cevian-is-farthest-from-perp

e:EuclideanPlane. ∀a,b,c,d:Point.  (a bc  ad  ⊥bc  (∀x,y:{x:Point| Colinear(b;c;x)} .  (d-x-y  |ax| < |ay|)))


Proof




Definitions occuring in Statement :  geo-perp-in: ab  ⊥cd geo-lt: p < q geo-length: |s| geo-mk-seg: ab euclidean-plane: EuclideanPlane geo-lsep: bc geo-colinear: Colinear(a;b;c) geo-strict-between: a-b-c geo-point: Point all: x:A. B[x] implies:  Q set: {x:A| B[x]} 
Definitions unfolded in proof :  all: x:A. B[x] implies:  Q member: t ∈ T euclidean-plane: EuclideanPlane guard: {T} and: P ∧ Q uall: [x:A]. B[x] subtype_rel: A ⊆B prop: or: P ∨ Q uimplies: supposing a basic-geometry: BasicGeometry cand: c∧ B geo-perp-in: ab  ⊥cd 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) exists: x:A. B[x] false: False select: L[n] cons: [a b] subtract: m sq_stable: SqStable(P) l_member: (x ∈ l) nat: less_than: a < b squash: T less_than': less_than'(a;b) true: True ge: i ≥  append: as bs so_lambda: so_lambda(x,y,z.t[x; y; z]) so_apply: x[s1;s2;s3] geo-midpoint: a=m=b basic-geometry-: BasicGeometry- uiff: uiff(P;Q) geo-cong-tri: Cong3(abc,a'b'c') geo-lsep: bc geo-interior-point: I(abc;d)
Lemmas referenced :  geo-sep-or lsep-implies-sep geo-sep_wf geo-strict-between_wf euclidean-plane-structure-subtype euclidean-plane-subtype subtype_rel_transitivity euclidean-plane_wf euclidean-plane-structure_wf geo-primitives_wf geo-colinear_wf geo-perp-in_wf geo-lsep_wf geo-point_wf colinear-lsep lsep-all-sym geo-sep-sym geo-colinear-is-colinear-set 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-strict-between-sep2 sq_stable__colinear 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 geo-proper-extend-exists geo-reflected-right-triangles-congruent geo-colinear-same right-angle-symmetry geo-strict-between-implies-between geo-congruent-iff-length geo-length-flip colinear-lsep-cycle geo-strict-between-sep1 geo-strict-between-implies-colinear Euclid-Prop21 between-preserves-left-1 left-convex geo-between_wf left-all-symmetry left-convex2 geo-between-symmetry geo-strict-between-sep3 geo-add-length_wf geo-lt_wf geo-length_wf geo-mk-seg_wf geo-lt-angle_wf geo-add-length-lt-cancel-for-double geo-length_wf1 geo-left-out-1 geo-between-out between-preserves-left-2
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity lambdaFormation_alt cut introduction extract_by_obid sqequalHypSubstitution dependent_functionElimination thin setElimination rename hypothesisEquality hypothesis because_Cache independent_functionElimination productElimination dependent_set_memberEquality_alt universeIsType isectElimination applyEquality sqequalRule unionElimination instantiate independent_isectElimination inhabitedIsType setIsType isect_memberEquality_alt voidElimination natural_numberEquality independent_pairFormation approximateComputation dependent_pairFormation_alt lambdaEquality_alt productIsType imageMemberEquality baseClosed equalityIstype int_eqEquality equalityTransitivity equalitySymmetry imageElimination inrFormation_alt applyLambdaEquality hyp_replacement productEquality

Latex:
\mforall{}e:EuclideanPlane.  \mforall{}a,b,c,d:Point.
    (a  \#  bc  {}\mRightarrow{}  ad    \mbot{}d  bc  {}\mRightarrow{}  (\mforall{}x,y:\{x:Point|  Colinear(b;c;x)\}  .    (d-x-y  {}\mRightarrow{}  |ax|  <  |ay|)))



Date html generated: 2019_10_16-PM-02_21_24
Last ObjectModification: 2019_03_20-PM-09_17_03

Theory : euclidean!plane!geometry


Home Index