begin
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 ) )