environ
vocabularies HIDDEN, NUMBERS, XCMPLX_0, REAL_1, PRE_TOPC, EUCLID, COMPLEX1, RELAT_1, SUBSET_1, MCART_1, ARYTM_3, ARYTM_1, SUPINF_2, CARD_1, SQUARE_1, FINSEQ_1, FUNCT_1, RVSUM_1, CARD_3, ORDINAL4, COMPTRIG, SIN_COS, XXREAL_0, XXREAL_1, COMPLEX2, PROB_2, RLTOPSP1, XBOOLE_0, TARSKI, STRUCT_0, TOPMETR, EUCLID_3;
notations HIDDEN, TARSKI, XBOOLE_0, SUBSET_1, SQUARE_1, RELAT_1, SIN_COS, FUNCT_1, FUNCT_2, ORDINAL1, NUMBERS, XCMPLX_0, XXREAL_0, COMPLEX1, XREAL_0, REAL_1, FINSEQ_1, RVSUM_1, STRUCT_0, PRE_TOPC, RLTOPSP1, EUCLID, COMPTRIG, COMPLEX2, RLVECT_1, TOPMETR, RCOMP_1;
definitions XBOOLE_0, TARSKI;
theorems XCMPLX_1, SQUARE_1, FUNCT_1, TOPREAL3, COMPLEX1, XBOOLE_0, FUNCT_2, RVSUM_1, FINSEQ_1, EUCLID, JGRAPH_3, COMPLEX2, XREAL_0, EUCLID_2, XCMPLX_0, TOPMETR, XREAL_1, COMPTRIG, VALUED_1, RLTOPSP1, RLVECT_1, RLVECT_4;
schemes DOMAIN_1, FUNCT_2;
registrations RELSET_1, NUMBERS, XCMPLX_0, XXREAL_0, STRUCT_0, MONOID_0, EUCLID, TOPMETR, VALUED_0, XREAL_0, ORDINAL1, SIN_COS, SQUARE_1;
constructors HIDDEN, REAL_1, SQUARE_1, BINOP_2, RCOMP_1, SIN_COS, COMPTRIG, COMPLEX2, MONOID_0, TOPMETR, TOPREAL1, COMPLEX1;
requirements HIDDEN, BOOLE, SUBSET, REAL, NUMERALS, ARITHM;
equalities XBOOLE_0, EUCLID, COMPLEX1, ALGSTR_0, RLTOPSP1;
expansions XBOOLE_0, COMPLEX1;
theorem
for
p1,
p2,
p3 being
Point of
(TOP-REAL 2) st
p2 <> p1 &
p1 <> p3 &
p3 <> p2 &
angle (
p2,
p1,
p3)
< PI holds
((angle (p2,p1,p3)) + (angle (p1,p3,p2))) + (angle (p3,p2,p1)) = PI
theorem Th51:
for
n being
Element of
NAT for
p1,
p2,
p3,
p0 being
Point of
(TOP-REAL n) st
p2 - p1,
p3 - p1 are_lindependent2 &
p0 in plane (
p1,
p2,
p3) holds
ex
a1,
a2,
a3 being
Real st
(
p0 = ((a1 * p1) + (a2 * p2)) + (a3 * p3) &
(a1 + a2) + a3 = 1 & ( for
b1,
b2,
b3 being
Real st
p0 = ((b1 * p1) + (b2 * p2)) + (b3 * p3) &
(b1 + b2) + b3 = 1 holds
(
b1 = a1 &
b2 = a2 &
b3 = a3 ) ) )
definition
let n be
Element of
NAT ;
let p1,
p2,
p3,
p be
Point of
(TOP-REAL n);
assume A1:
(
p2 - p1,
p3 - p1 are_lindependent2 &
p in plane (
p1,
p2,
p3) )
;
existence
ex b1, a2, a3 being Real st
( (b1 + a2) + a3 = 1 & p = ((b1 * p1) + (a2 * p2)) + (a3 * p3) )
uniqueness
for b1, b2 being Real st ex a2, a3 being Real st
( (b1 + a2) + a3 = 1 & p = ((b1 * p1) + (a2 * p2)) + (a3 * p3) ) & ex a2, a3 being Real st
( (b2 + a2) + a3 = 1 & p = ((b2 * p1) + (a2 * p2)) + (a3 * p3) ) holds
b1 = b2
end;
::
deftheorem Def11 defines
tricord1 EUCLID_3:def 11 :
for n being Element of NAT
for p1, p2, p3, p being Point of (TOP-REAL n) st p2 - p1,p3 - p1 are_lindependent2 & p in plane (p1,p2,p3) holds
for b6 being Real holds
( b6 = tricord1 (p1,p2,p3,p) iff ex a2, a3 being Real st
( (b6 + a2) + a3 = 1 & p = ((b6 * p1) + (a2 * p2)) + (a3 * p3) ) );
definition
let n be
Element of
NAT ;
let p1,
p2,
p3,
p be
Point of
(TOP-REAL n);
assume A1:
(
p2 - p1,
p3 - p1 are_lindependent2 &
p in plane (
p1,
p2,
p3) )
;
existence
ex b1, a1, a3 being Real st
( (a1 + b1) + a3 = 1 & p = ((a1 * p1) + (b1 * p2)) + (a3 * p3) )
uniqueness
for b1, b2 being Real st ex a1, a3 being Real st
( (a1 + b1) + a3 = 1 & p = ((a1 * p1) + (b1 * p2)) + (a3 * p3) ) & ex a1, a3 being Real st
( (a1 + b2) + a3 = 1 & p = ((a1 * p1) + (b2 * p2)) + (a3 * p3) ) holds
b1 = b2
end;
::
deftheorem Def12 defines
tricord2 EUCLID_3:def 12 :
for n being Element of NAT
for p1, p2, p3, p being Point of (TOP-REAL n) st p2 - p1,p3 - p1 are_lindependent2 & p in plane (p1,p2,p3) holds
for b6 being Real holds
( b6 = tricord2 (p1,p2,p3,p) iff ex a1, a3 being Real st
( (a1 + b6) + a3 = 1 & p = ((a1 * p1) + (b6 * p2)) + (a3 * p3) ) );
definition
let n be
Element of
NAT ;
let p1,
p2,
p3,
p be
Point of
(TOP-REAL n);
assume A1:
(
p2 - p1,
p3 - p1 are_lindependent2 &
p in plane (
p1,
p2,
p3) )
;
existence
ex b1, a1, a2 being Real st
( (a1 + a2) + b1 = 1 & p = ((a1 * p1) + (a2 * p2)) + (b1 * p3) )
uniqueness
for b1, b2 being Real st ex a1, a2 being Real st
( (a1 + a2) + b1 = 1 & p = ((a1 * p1) + (a2 * p2)) + (b1 * p3) ) & ex a1, a2 being Real st
( (a1 + a2) + b2 = 1 & p = ((a1 * p1) + (a2 * p2)) + (b2 * p3) ) holds
b1 = b2
end;
::
deftheorem Def13 defines
tricord3 EUCLID_3:def 13 :
for n being Element of NAT
for p1, p2, p3, p being Point of (TOP-REAL n) st p2 - p1,p3 - p1 are_lindependent2 & p in plane (p1,p2,p3) holds
for b6 being Real holds
( b6 = tricord3 (p1,p2,p3,p) iff ex a1, a2 being Real st
( (a1 + a2) + b6 = 1 & p = ((a1 * p1) + (a2 * p2)) + (b6 * p3) ) );
definition
let p1,
p2,
p3 be
Point of
(TOP-REAL 2);
existence
ex b1 being Function of (TOP-REAL 2),R^1 st
for p being Point of (TOP-REAL 2) holds b1 . p = tricord1 (p1,p2,p3,p)
uniqueness
for b1, b2 being Function of (TOP-REAL 2),R^1 st ( for p being Point of (TOP-REAL 2) holds b1 . p = tricord1 (p1,p2,p3,p) ) & ( for p being Point of (TOP-REAL 2) holds b2 . p = tricord1 (p1,p2,p3,p) ) holds
b1 = b2
end;
definition
let p1,
p2,
p3 be
Point of
(TOP-REAL 2);
existence
ex b1 being Function of (TOP-REAL 2),R^1 st
for p being Point of (TOP-REAL 2) holds b1 . p = tricord2 (p1,p2,p3,p)
uniqueness
for b1, b2 being Function of (TOP-REAL 2),R^1 st ( for p being Point of (TOP-REAL 2) holds b1 . p = tricord2 (p1,p2,p3,p) ) & ( for p being Point of (TOP-REAL 2) holds b2 . p = tricord2 (p1,p2,p3,p) ) holds
b1 = b2
end;
definition
let p1,
p2,
p3 be
Point of
(TOP-REAL 2);
existence
ex b1 being Function of (TOP-REAL 2),R^1 st
for p being Point of (TOP-REAL 2) holds b1 . p = tricord3 (p1,p2,p3,p)
uniqueness
for b1, b2 being Function of (TOP-REAL 2),R^1 st ( for p being Point of (TOP-REAL 2) holds b1 . p = tricord3 (p1,p2,p3,p) ) & ( for p being Point of (TOP-REAL 2) holds b2 . p = tricord3 (p1,p2,p3,p) ) holds
b1 = b2
end;
theorem
for
p1,
p2,
p3,
p being
Point of
(TOP-REAL 2) st
p2 - p1,
p3 - p1 are_lindependent2 holds
(
p in outside_of_triangle (
p1,
p2,
p3) iff (
tricord1 (
p1,
p2,
p3,
p)
< 0 or
tricord2 (
p1,
p2,
p3,
p)
< 0 or
tricord3 (
p1,
p2,
p3,
p)
< 0 ) )
theorem Th56:
for
p1,
p2,
p3,
p being
Point of
(TOP-REAL 2) st
p2 - p1,
p3 - p1 are_lindependent2 holds
(
p in Triangle (
p1,
p2,
p3) iff (
tricord1 (
p1,
p2,
p3,
p)
>= 0 &
tricord2 (
p1,
p2,
p3,
p)
>= 0 &
tricord3 (
p1,
p2,
p3,
p)
>= 0 & (
tricord1 (
p1,
p2,
p3,
p)
= 0 or
tricord2 (
p1,
p2,
p3,
p)
= 0 or
tricord3 (
p1,
p2,
p3,
p)
= 0 ) ) )
theorem
for
p1,
p2,
p3,
p being
Point of
(TOP-REAL 2) st
p2 - p1,
p3 - p1 are_lindependent2 holds
(
p in Triangle (
p1,
p2,
p3) iff ( (
tricord1 (
p1,
p2,
p3,
p)
= 0 &
tricord2 (
p1,
p2,
p3,
p)
>= 0 &
tricord3 (
p1,
p2,
p3,
p)
>= 0 ) or (
tricord1 (
p1,
p2,
p3,
p)
>= 0 &
tricord2 (
p1,
p2,
p3,
p)
= 0 &
tricord3 (
p1,
p2,
p3,
p)
>= 0 ) or (
tricord1 (
p1,
p2,
p3,
p)
>= 0 &
tricord2 (
p1,
p2,
p3,
p)
>= 0 &
tricord3 (
p1,
p2,
p3,
p)
= 0 ) ) )
by Th56;
theorem Th58:
for
p1,
p2,
p3,
p being
Point of
(TOP-REAL 2) st
p2 - p1,
p3 - p1 are_lindependent2 holds
(
p in inside_of_triangle (
p1,
p2,
p3) iff (
tricord1 (
p1,
p2,
p3,
p)
> 0 &
tricord2 (
p1,
p2,
p3,
p)
> 0 &
tricord3 (
p1,
p2,
p3,
p)
> 0 ) )