:: by Akihiro Kubo and Yatsuka Nakamura

::

:: Received May 29, 2003

:: Copyright (c) 2003-2017 Association of Mizar Users

definition
end;

:: deftheorem defines cpx2euc EUCLID_3:def 1 :

for z being Complex holds cpx2euc z = |[(Re z),(Im z)]|;

for z being Complex holds cpx2euc z = |[(Re z),(Im z)]|;

definition

let p be Point of (TOP-REAL 2);

correctness

coherence

(p `1) + ((p `2) * <i>) is Element of COMPLEX ;

by XCMPLX_0:def 2;

end;
correctness

coherence

(p `1) + ((p `2) * <i>) is Element of COMPLEX ;

by XCMPLX_0:def 2;

:: deftheorem defines euc2cpx EUCLID_3:def 2 :

for p being Point of (TOP-REAL 2) holds euc2cpx p = (p `1) + ((p `2) * <i>);

for p being Point of (TOP-REAL 2) holds euc2cpx p = (p `1) + ((p `2) * <i>);

theorem Th6: :: EUCLID_3:6

for z1, z2 being Complex holds |[(Re (z1 + z2)),(Im (z1 + z2))]| = |[((Re z1) + (Re z2)),((Im z1) + (Im z2))]|

proof end;

theorem Th8: :: EUCLID_3:8

for p1, p2 being Point of (TOP-REAL 2) holds ((p1 + p2) `1) + (((p1 + p2) `2) * <i>) = ((p1 `1) + (p2 `1)) + (((p1 `2) + (p2 `2)) * <i>)

proof end;

theorem Th12: :: EUCLID_3:12

for p being Point of (TOP-REAL 2) holds ((- p) `1) + (((- p) `2) * <i>) = (- (p `1)) + ((- (p `2)) * <i>)

proof end;

theorem :: EUCLID_3:18

theorem :: EUCLID_3:23

:: deftheorem defines Arg EUCLID_3:def 3 :

for p being Point of (TOP-REAL 2) holds Arg p = Arg (euc2cpx p);

for p being Point of (TOP-REAL 2) holds Arg p = Arg (euc2cpx p);

theorem :: EUCLID_3:26

for z being Element of COMPLEX

for p being Point of (TOP-REAL 2) st ( z = euc2cpx p or p = cpx2euc z ) holds

Arg z = Arg p

for p being Point of (TOP-REAL 2) st ( z = euc2cpx p or p = cpx2euc z ) holds

Arg z = Arg p

proof end;

theorem :: EUCLID_3:27

for x1, x2 being Real

for p being Point of (TOP-REAL 2) st x1 = |.p.| * (cos (Arg p)) & x2 = |.p.| * (sin (Arg p)) holds

p = |[x1,x2]|

for p being Point of (TOP-REAL 2) st x1 = |.p.| * (cos (Arg p)) & x2 = |.p.| * (sin (Arg p)) holds

p = |[x1,x2]|

proof end;

theorem :: EUCLID_3:29

for p being Point of (TOP-REAL 2) st p <> 0. (TOP-REAL 2) holds

( ( Arg p < PI implies Arg (- p) = (Arg p) + PI ) & ( Arg p >= PI implies Arg (- p) = (Arg p) - PI ) )

( ( Arg p < PI implies Arg (- p) = (Arg p) + PI ) & ( Arg p >= PI implies Arg (- p) = (Arg p) - PI ) )

proof end;

theorem :: EUCLID_3:32

for p1, p2 being Point of (TOP-REAL 2) st ( p1 <> p2 or p1 - p2 <> 0. (TOP-REAL 2) ) holds

( Arg (p1 - p2) < PI iff Arg (p2 - p1) >= PI )

( Arg (p1 - p2) < PI iff Arg (p2 - p1) >= PI )

proof end;

definition

let p1, p2, p3 be Point of (TOP-REAL 2);

coherence

angle ((euc2cpx p1),(euc2cpx p2),(euc2cpx p3)) is Real;

;

end;
func angle (p1,p2,p3) -> Real equals :: EUCLID_3:def 4

angle ((euc2cpx p1),(euc2cpx p2),(euc2cpx p3));

correctness angle ((euc2cpx p1),(euc2cpx p2),(euc2cpx p3));

coherence

angle ((euc2cpx p1),(euc2cpx p2),(euc2cpx p3)) is Real;

;

:: deftheorem defines angle EUCLID_3:def 4 :

for p1, p2, p3 being Point of (TOP-REAL 2) holds angle (p1,p2,p3) = angle ((euc2cpx p1),(euc2cpx p2),(euc2cpx p3));

for p1, p2, p3 being Point of (TOP-REAL 2) holds angle (p1,p2,p3) = angle ((euc2cpx p1),(euc2cpx p2),(euc2cpx p3));

theorem :: EUCLID_3:35

for p1, p2, p3 being Point of (TOP-REAL 2) holds angle (p1,p2,p3) = angle ((p1 - p2),(0. (TOP-REAL 2)),(p3 - p2))

proof end;

theorem :: EUCLID_3:36

for p1, p2, p3 being Point of (TOP-REAL 2) st angle (p1,p2,p3) = 0 holds

( Arg (p1 - p2) = Arg (p3 - p2) & angle (p3,p2,p1) = 0 )

( Arg (p1 - p2) = Arg (p3 - p2) & angle (p3,p2,p1) = 0 )

proof end;

theorem :: EUCLID_3:37

for p1, p2, p3 being Point of (TOP-REAL 2) st angle (p1,p2,p3) <> 0 holds

angle (p3,p2,p1) = (2 * PI) - (angle (p1,p2,p3))

angle (p3,p2,p1) = (2 * PI) - (angle (p1,p2,p3))

proof end;

theorem :: EUCLID_3:38

for p1, p2, p3 being Point of (TOP-REAL 2) st angle (p3,p2,p1) <> 0 holds

angle (p3,p2,p1) = (2 * PI) - (angle (p1,p2,p3))

angle (p3,p2,p1) = (2 * PI) - (angle (p1,p2,p3))

proof end;

theorem :: EUCLID_3:43

for p1, p2, p3 being Point of (TOP-REAL 2) st p1 <> 0. (TOP-REAL 2) & p2 <> 0. (TOP-REAL 2) holds

( |(p1,p2)| = 0 iff ( angle (p1,(0. (TOP-REAL 2)),p2) = PI / 2 or angle (p1,(0. (TOP-REAL 2)),p2) = (3 / 2) * PI ) )

( |(p1,p2)| = 0 iff ( angle (p1,(0. (TOP-REAL 2)),p2) = PI / 2 or angle (p1,(0. (TOP-REAL 2)),p2) = (3 / 2) * PI ) )

proof end;

theorem :: EUCLID_3:44

for p1, p2 being Point of (TOP-REAL 2) st p1 <> 0. (TOP-REAL 2) & p2 <> 0. (TOP-REAL 2) holds

( ( ( not (- ((p1 `1) * (p2 `2))) + ((p1 `2) * (p2 `1)) = |.p1.| * |.p2.| & not (- ((p1 `1) * (p2 `2))) + ((p1 `2) * (p2 `1)) = - (|.p1.| * |.p2.|) ) or angle (p1,(0. (TOP-REAL 2)),p2) = PI / 2 or angle (p1,(0. (TOP-REAL 2)),p2) = (3 / 2) * PI ) & ( ( not angle (p1,(0. (TOP-REAL 2)),p2) = PI / 2 & not angle (p1,(0. (TOP-REAL 2)),p2) = (3 / 2) * PI ) or (- ((p1 `1) * (p2 `2))) + ((p1 `2) * (p2 `1)) = |.p1.| * |.p2.| or (- ((p1 `1) * (p2 `2))) + ((p1 `2) * (p2 `1)) = - (|.p1.| * |.p2.|) ) )

( ( ( not (- ((p1 `1) * (p2 `2))) + ((p1 `2) * (p2 `1)) = |.p1.| * |.p2.| & not (- ((p1 `1) * (p2 `2))) + ((p1 `2) * (p2 `1)) = - (|.p1.| * |.p2.|) ) or angle (p1,(0. (TOP-REAL 2)),p2) = PI / 2 or angle (p1,(0. (TOP-REAL 2)),p2) = (3 / 2) * PI ) & ( ( not angle (p1,(0. (TOP-REAL 2)),p2) = PI / 2 & not angle (p1,(0. (TOP-REAL 2)),p2) = (3 / 2) * PI ) or (- ((p1 `1) * (p2 `2))) + ((p1 `2) * (p2 `1)) = |.p1.| * |.p2.| or (- ((p1 `1) * (p2 `2))) + ((p1 `2) * (p2 `1)) = - (|.p1.| * |.p2.|) ) )

proof end;

theorem :: EUCLID_3:45

for p1, p2, p3 being Point of (TOP-REAL 2) st p1 <> p2 & p3 <> p2 holds

( |((p1 - p2),(p3 - p2))| = 0 iff ( angle (p1,p2,p3) = PI / 2 or angle (p1,p2,p3) = (3 / 2) * PI ) )

( |((p1 - p2),(p3 - p2))| = 0 iff ( angle (p1,p2,p3) = PI / 2 or angle (p1,p2,p3) = (3 / 2) * PI ) )

proof end;

:: Pythagorean Theorem

theorem :: EUCLID_3:46

for p1, p2, p3 being Point of (TOP-REAL 2) st p1 <> p2 & p3 <> p2 & ( angle (p1,p2,p3) = PI / 2 or angle (p1,p2,p3) = (3 / 2) * PI ) holds

(|.(p1 - p2).| ^2) + (|.(p3 - p2).| ^2) = |.(p1 - p3).| ^2

(|.(p1 - p2).| ^2) + (|.(p3 - p2).| ^2) = |.(p1 - p3).| ^2

proof end;

theorem :: EUCLID_3:47

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

((angle (p2,p1,p3)) + (angle (p1,p3,p2))) + (angle (p3,p2,p1)) = PI

proof end;

definition

let n be Element of NAT ;

let p1, p2, p3 be Point of (TOP-REAL n);

coherence

((LSeg (p1,p2)) \/ (LSeg (p2,p3))) \/ (LSeg (p3,p1)) is Subset of (TOP-REAL n);

;

end;
let p1, p2, p3 be Point of (TOP-REAL n);

func Triangle (p1,p2,p3) -> Subset of (TOP-REAL n) equals :: EUCLID_3:def 5

((LSeg (p1,p2)) \/ (LSeg (p2,p3))) \/ (LSeg (p3,p1));

correctness ((LSeg (p1,p2)) \/ (LSeg (p2,p3))) \/ (LSeg (p3,p1));

coherence

((LSeg (p1,p2)) \/ (LSeg (p2,p3))) \/ (LSeg (p3,p1)) is Subset of (TOP-REAL n);

;

:: deftheorem defines Triangle EUCLID_3:def 5 :

for n being Element of NAT

for p1, p2, p3 being Point of (TOP-REAL n) holds Triangle (p1,p2,p3) = ((LSeg (p1,p2)) \/ (LSeg (p2,p3))) \/ (LSeg (p3,p1));

for n being Element of NAT

for p1, p2, p3 being Point of (TOP-REAL n) holds Triangle (p1,p2,p3) = ((LSeg (p1,p2)) \/ (LSeg (p2,p3))) \/ (LSeg (p3,p1));

definition

let n be Element of NAT ;

let p1, p2, p3 be Point of (TOP-REAL n);

coherence

{ p where p is Point of (TOP-REAL n) : ex a1, a2, a3 being Real st

( 0 <= a1 & 0 <= a2 & 0 <= a3 & (a1 + a2) + a3 = 1 & p = ((a1 * p1) + (a2 * p2)) + (a3 * p3) ) } is Subset of (TOP-REAL n);

end;
let p1, p2, p3 be Point of (TOP-REAL n);

func closed_inside_of_triangle (p1,p2,p3) -> Subset of (TOP-REAL n) equals :: EUCLID_3:def 6

{ p where p is Point of (TOP-REAL n) : ex a1, a2, a3 being Real st

( 0 <= a1 & 0 <= a2 & 0 <= a3 & (a1 + a2) + a3 = 1 & p = ((a1 * p1) + (a2 * p2)) + (a3 * p3) ) } ;

correctness { p where p is Point of (TOP-REAL n) : ex a1, a2, a3 being Real st

( 0 <= a1 & 0 <= a2 & 0 <= a3 & (a1 + a2) + a3 = 1 & p = ((a1 * p1) + (a2 * p2)) + (a3 * p3) ) } ;

coherence

{ p where p is Point of (TOP-REAL n) : ex a1, a2, a3 being Real st

( 0 <= a1 & 0 <= a2 & 0 <= a3 & (a1 + a2) + a3 = 1 & p = ((a1 * p1) + (a2 * p2)) + (a3 * p3) ) } is Subset of (TOP-REAL n);

proof end;

:: deftheorem defines closed_inside_of_triangle EUCLID_3:def 6 :

for n being Element of NAT

for p1, p2, p3 being Point of (TOP-REAL n) holds closed_inside_of_triangle (p1,p2,p3) = { p where p is Point of (TOP-REAL n) : ex a1, a2, a3 being Real st

( 0 <= a1 & 0 <= a2 & 0 <= a3 & (a1 + a2) + a3 = 1 & p = ((a1 * p1) + (a2 * p2)) + (a3 * p3) ) } ;

for n being Element of NAT

for p1, p2, p3 being Point of (TOP-REAL n) holds closed_inside_of_triangle (p1,p2,p3) = { p where p is Point of (TOP-REAL n) : ex a1, a2, a3 being Real st

( 0 <= a1 & 0 <= a2 & 0 <= a3 & (a1 + a2) + a3 = 1 & p = ((a1 * p1) + (a2 * p2)) + (a3 * p3) ) } ;

definition

let n be Element of NAT ;

let p1, p2, p3 be Point of (TOP-REAL n);

coherence

(closed_inside_of_triangle (p1,p2,p3)) \ (Triangle (p1,p2,p3)) is Subset of (TOP-REAL n);

;

end;
let p1, p2, p3 be Point of (TOP-REAL n);

func inside_of_triangle (p1,p2,p3) -> Subset of (TOP-REAL n) equals :: EUCLID_3:def 7

(closed_inside_of_triangle (p1,p2,p3)) \ (Triangle (p1,p2,p3));

correctness (closed_inside_of_triangle (p1,p2,p3)) \ (Triangle (p1,p2,p3));

coherence

(closed_inside_of_triangle (p1,p2,p3)) \ (Triangle (p1,p2,p3)) is Subset of (TOP-REAL n);

;

:: deftheorem defines inside_of_triangle EUCLID_3:def 7 :

for n being Element of NAT

for p1, p2, p3 being Point of (TOP-REAL n) holds inside_of_triangle (p1,p2,p3) = (closed_inside_of_triangle (p1,p2,p3)) \ (Triangle (p1,p2,p3));

for n being Element of NAT

for p1, p2, p3 being Point of (TOP-REAL n) holds inside_of_triangle (p1,p2,p3) = (closed_inside_of_triangle (p1,p2,p3)) \ (Triangle (p1,p2,p3));

definition

let n be Element of NAT ;

let p1, p2, p3 be Point of (TOP-REAL n);

coherence

{ p where p is Point of (TOP-REAL n) : ex a1, a2, a3 being Real st

( ( 0 > a1 or 0 > a2 or 0 > a3 ) & (a1 + a2) + a3 = 1 & p = ((a1 * p1) + (a2 * p2)) + (a3 * p3) ) } is Subset of (TOP-REAL n);

end;
let p1, p2, p3 be Point of (TOP-REAL n);

func outside_of_triangle (p1,p2,p3) -> Subset of (TOP-REAL n) equals :: EUCLID_3:def 8

{ p where p is Point of (TOP-REAL n) : ex a1, a2, a3 being Real st

( ( 0 > a1 or 0 > a2 or 0 > a3 ) & (a1 + a2) + a3 = 1 & p = ((a1 * p1) + (a2 * p2)) + (a3 * p3) ) } ;

correctness { p where p is Point of (TOP-REAL n) : ex a1, a2, a3 being Real st

( ( 0 > a1 or 0 > a2 or 0 > a3 ) & (a1 + a2) + a3 = 1 & p = ((a1 * p1) + (a2 * p2)) + (a3 * p3) ) } ;

coherence

{ p where p is Point of (TOP-REAL n) : ex a1, a2, a3 being Real st

( ( 0 > a1 or 0 > a2 or 0 > a3 ) & (a1 + a2) + a3 = 1 & p = ((a1 * p1) + (a2 * p2)) + (a3 * p3) ) } is Subset of (TOP-REAL n);

proof end;

:: deftheorem defines outside_of_triangle EUCLID_3:def 8 :

for n being Element of NAT

for p1, p2, p3 being Point of (TOP-REAL n) holds outside_of_triangle (p1,p2,p3) = { p where p is Point of (TOP-REAL n) : ex a1, a2, a3 being Real st

( ( 0 > a1 or 0 > a2 or 0 > a3 ) & (a1 + a2) + a3 = 1 & p = ((a1 * p1) + (a2 * p2)) + (a3 * p3) ) } ;

for n being Element of NAT

for p1, p2, p3 being Point of (TOP-REAL n) holds outside_of_triangle (p1,p2,p3) = { p where p is Point of (TOP-REAL n) : ex a1, a2, a3 being Real st

( ( 0 > a1 or 0 > a2 or 0 > a3 ) & (a1 + a2) + a3 = 1 & p = ((a1 * p1) + (a2 * p2)) + (a3 * p3) ) } ;

definition

let n be Element of NAT ;

let p1, p2, p3 be Point of (TOP-REAL n);

coherence

(outside_of_triangle (p1,p2,p3)) \/ (closed_inside_of_triangle (p1,p2,p3)) is Subset of (TOP-REAL n);

;

end;
let p1, p2, p3 be Point of (TOP-REAL n);

func plane (p1,p2,p3) -> Subset of (TOP-REAL n) equals :: EUCLID_3:def 9

(outside_of_triangle (p1,p2,p3)) \/ (closed_inside_of_triangle (p1,p2,p3));

correctness (outside_of_triangle (p1,p2,p3)) \/ (closed_inside_of_triangle (p1,p2,p3));

coherence

(outside_of_triangle (p1,p2,p3)) \/ (closed_inside_of_triangle (p1,p2,p3)) is Subset of (TOP-REAL n);

;

:: deftheorem defines plane EUCLID_3:def 9 :

for n being Element of NAT

for p1, p2, p3 being Point of (TOP-REAL n) holds plane (p1,p2,p3) = (outside_of_triangle (p1,p2,p3)) \/ (closed_inside_of_triangle (p1,p2,p3));

for n being Element of NAT

for p1, p2, p3 being Point of (TOP-REAL n) holds plane (p1,p2,p3) = (outside_of_triangle (p1,p2,p3)) \/ (closed_inside_of_triangle (p1,p2,p3));

theorem Th48: :: EUCLID_3:48

for n being Element of NAT

for p1, p2, p3, p being Point of (TOP-REAL n) st p in plane (p1,p2,p3) holds

ex a1, a2, a3 being Real st

( (a1 + a2) + a3 = 1 & p = ((a1 * p1) + (a2 * p2)) + (a3 * p3) )

for p1, p2, p3, p being Point of (TOP-REAL n) st p in plane (p1,p2,p3) holds

ex a1, a2, a3 being Real st

( (a1 + a2) + a3 = 1 & p = ((a1 * p1) + (a2 * p2)) + (a3 * p3) )

proof end;

theorem :: EUCLID_3:49

for n being Element of NAT

for p1, p2, p3 being Point of (TOP-REAL n) holds Triangle (p1,p2,p3) c= closed_inside_of_triangle (p1,p2,p3)

for p1, p2, p3 being Point of (TOP-REAL n) holds Triangle (p1,p2,p3) c= closed_inside_of_triangle (p1,p2,p3)

proof end;

:: deftheorem defines are_lindependent2 EUCLID_3:def 10 :

for n being Element of NAT

for q1, q2 being Point of (TOP-REAL n) holds

( q1,q2 are_lindependent2 iff for a1, a2 being Real st (a1 * q1) + (a2 * q2) = 0. (TOP-REAL n) holds

( a1 = 0 & a2 = 0 ) );

for n being Element of NAT

for q1, q2 being Point of (TOP-REAL n) holds

( q1,q2 are_lindependent2 iff for a1, a2 being Real st (a1 * q1) + (a2 * q2) = 0. (TOP-REAL n) holds

( a1 = 0 & a2 = 0 ) );

notation

let n be Element of NAT ;

let q1, q2 be Point of (TOP-REAL n);

antonym q1,q2 are_ldependent2 for q1,q2 are_lindependent2 ;

end;
let q1, q2 be Point of (TOP-REAL n);

antonym q1,q2 are_ldependent2 for q1,q2 are_lindependent2 ;

theorem Th50: :: EUCLID_3:50

for n being Element of NAT

for q1, q2 being Point of (TOP-REAL n) st q1,q2 are_lindependent2 holds

( q1 <> q2 & q1 <> 0. (TOP-REAL n) & q2 <> 0. (TOP-REAL n) )

for q1, q2 being Point of (TOP-REAL n) st q1,q2 are_lindependent2 holds

( q1 <> q2 & q1 <> 0. (TOP-REAL n) & q2 <> 0. (TOP-REAL n) )

proof end;

theorem Th51: :: EUCLID_3:51

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

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

proof end;

theorem Th52: :: EUCLID_3:52

for n being Element of NAT

for p1, p2, p3, p0 being Point of (TOP-REAL n) st ex a1, a2, a3 being Real st

( p0 = ((a1 * p1) + (a2 * p2)) + (a3 * p3) & (a1 + a2) + a3 = 1 ) holds

p0 in plane (p1,p2,p3)

for p1, p2, p3, p0 being Point of (TOP-REAL n) st ex a1, a2, a3 being Real st

( p0 = ((a1 * p1) + (a2 * p2)) + (a3 * p3) & (a1 + a2) + a3 = 1 ) holds

p0 in plane (p1,p2,p3)

proof end;

theorem :: EUCLID_3:53

for n being Element of NAT

for p1, p2, p3 being Point of (TOP-REAL n) holds plane (p1,p2,p3) = { p where p is Point of (TOP-REAL n) : ex a1, a2, a3 being Real st

( (a1 + a2) + a3 = 1 & p = ((a1 * p1) + (a2 * p2)) + (a3 * p3) ) }

for p1, p2, p3 being Point of (TOP-REAL n) holds plane (p1,p2,p3) = { p where p is Point of (TOP-REAL n) : ex a1, a2, a3 being Real st

( (a1 + a2) + a3 = 1 & p = ((a1 * p1) + (a2 * p2)) + (a3 * p3) ) }

proof end;

theorem Th54: :: EUCLID_3:54

for p1, p2, p3 being Point of (TOP-REAL 2) st p2 - p1,p3 - p1 are_lindependent2 holds

plane (p1,p2,p3) = REAL 2

plane (p1,p2,p3) = REAL 2

proof end;

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

ex b_{1}, a2, a3 being Real st

( (b_{1} + a2) + a3 = 1 & p = ((b_{1} * p1) + (a2 * p2)) + (a3 * p3) )

for b_{1}, b_{2} being Real st ex a2, a3 being Real st

( (b_{1} + a2) + a3 = 1 & p = ((b_{1} * p1) + (a2 * p2)) + (a3 * p3) ) & ex a2, a3 being Real st

( (b_{2} + a2) + a3 = 1 & p = ((b_{2} * p1) + (a2 * p2)) + (a3 * p3) ) holds

b_{1} = b_{2}

end;
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) ) ;

func tricord1 (p1,p2,p3,p) -> Real means :Def11: :: EUCLID_3:def 11

ex a2, a3 being Real st

( (it + a2) + a3 = 1 & p = ((it * p1) + (a2 * p2)) + (a3 * p3) );

existence ex a2, a3 being Real st

( (it + a2) + a3 = 1 & p = ((it * p1) + (a2 * p2)) + (a3 * p3) );

ex b

( (b

proof end;

uniqueness for b

( (b

( (b

b

proof 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 b_{6} being Real holds

( b_{6} = tricord1 (p1,p2,p3,p) iff ex a2, a3 being Real st

( (b_{6} + a2) + a3 = 1 & p = ((b_{6} * p1) + (a2 * p2)) + (a3 * p3) ) );

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 b

( b

( (b

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

ex b_{1}, a1, a3 being Real st

( (a1 + b_{1}) + a3 = 1 & p = ((a1 * p1) + (b_{1} * p2)) + (a3 * p3) )

for b_{1}, b_{2} being Real st ex a1, a3 being Real st

( (a1 + b_{1}) + a3 = 1 & p = ((a1 * p1) + (b_{1} * p2)) + (a3 * p3) ) & ex a1, a3 being Real st

( (a1 + b_{2}) + a3 = 1 & p = ((a1 * p1) + (b_{2} * p2)) + (a3 * p3) ) holds

b_{1} = b_{2}

end;
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) ) ;

func tricord2 (p1,p2,p3,p) -> Real means :Def12: :: EUCLID_3:def 12

ex a1, a3 being Real st

( (a1 + it) + a3 = 1 & p = ((a1 * p1) + (it * p2)) + (a3 * p3) );

existence ex a1, a3 being Real st

( (a1 + it) + a3 = 1 & p = ((a1 * p1) + (it * p2)) + (a3 * p3) );

ex b

( (a1 + b

proof end;

uniqueness for b

( (a1 + b

( (a1 + b

b

proof 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 b_{6} being Real holds

( b_{6} = tricord2 (p1,p2,p3,p) iff ex a1, a3 being Real st

( (a1 + b_{6}) + a3 = 1 & p = ((a1 * p1) + (b_{6} * p2)) + (a3 * p3) ) );

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 b

( b

( (a1 + b

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

ex b_{1}, a1, a2 being Real st

( (a1 + a2) + b_{1} = 1 & p = ((a1 * p1) + (a2 * p2)) + (b_{1} * p3) )

for b_{1}, b_{2} being Real st ex a1, a2 being Real st

( (a1 + a2) + b_{1} = 1 & p = ((a1 * p1) + (a2 * p2)) + (b_{1} * p3) ) & ex a1, a2 being Real st

( (a1 + a2) + b_{2} = 1 & p = ((a1 * p1) + (a2 * p2)) + (b_{2} * p3) ) holds

b_{1} = b_{2}

end;
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) ) ;

func tricord3 (p1,p2,p3,p) -> Real means :Def13: :: EUCLID_3:def 13

ex a1, a2 being Real st

( (a1 + a2) + it = 1 & p = ((a1 * p1) + (a2 * p2)) + (it * p3) );

existence ex a1, a2 being Real st

( (a1 + a2) + it = 1 & p = ((a1 * p1) + (a2 * p2)) + (it * p3) );

ex b

( (a1 + a2) + b

proof end;

uniqueness for b

( (a1 + a2) + b

( (a1 + a2) + b

b

proof 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 b_{6} being Real holds

( b_{6} = tricord3 (p1,p2,p3,p) iff ex a1, a2 being Real st

( (a1 + a2) + b_{6} = 1 & p = ((a1 * p1) + (a2 * p2)) + (b_{6} * p3) ) );

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 b

( b

( (a1 + a2) + b

definition

let p1, p2, p3 be Point of (TOP-REAL 2);

ex b_{1} being Function of (TOP-REAL 2),R^1 st

for p being Point of (TOP-REAL 2) holds b_{1} . p = tricord1 (p1,p2,p3,p)

for b_{1}, b_{2} being Function of (TOP-REAL 2),R^1 st ( for p being Point of (TOP-REAL 2) holds b_{1} . p = tricord1 (p1,p2,p3,p) ) & ( for p being Point of (TOP-REAL 2) holds b_{2} . p = tricord1 (p1,p2,p3,p) ) holds

b_{1} = b_{2}

end;
func trcmap1 (p1,p2,p3) -> Function of (TOP-REAL 2),R^1 means :: EUCLID_3:def 14

for p being Point of (TOP-REAL 2) holds it . p = tricord1 (p1,p2,p3,p);

existence for p being Point of (TOP-REAL 2) holds it . p = tricord1 (p1,p2,p3,p);

ex b

for p being Point of (TOP-REAL 2) holds b

proof end;

uniqueness for b

b

proof end;

:: deftheorem defines trcmap1 EUCLID_3:def 14 :

for p1, p2, p3 being Point of (TOP-REAL 2)

for b_{4} being Function of (TOP-REAL 2),R^1 holds

( b_{4} = trcmap1 (p1,p2,p3) iff for p being Point of (TOP-REAL 2) holds b_{4} . p = tricord1 (p1,p2,p3,p) );

for p1, p2, p3 being Point of (TOP-REAL 2)

for b

( b

definition

let p1, p2, p3 be Point of (TOP-REAL 2);

ex b_{1} being Function of (TOP-REAL 2),R^1 st

for p being Point of (TOP-REAL 2) holds b_{1} . p = tricord2 (p1,p2,p3,p)

for b_{1}, b_{2} being Function of (TOP-REAL 2),R^1 st ( for p being Point of (TOP-REAL 2) holds b_{1} . p = tricord2 (p1,p2,p3,p) ) & ( for p being Point of (TOP-REAL 2) holds b_{2} . p = tricord2 (p1,p2,p3,p) ) holds

b_{1} = b_{2}

end;
func trcmap2 (p1,p2,p3) -> Function of (TOP-REAL 2),R^1 means :: EUCLID_3:def 15

for p being Point of (TOP-REAL 2) holds it . p = tricord2 (p1,p2,p3,p);

existence for p being Point of (TOP-REAL 2) holds it . p = tricord2 (p1,p2,p3,p);

ex b

for p being Point of (TOP-REAL 2) holds b

proof end;

uniqueness for b

b

proof end;

:: deftheorem defines trcmap2 EUCLID_3:def 15 :

for p1, p2, p3 being Point of (TOP-REAL 2)

for b_{4} being Function of (TOP-REAL 2),R^1 holds

( b_{4} = trcmap2 (p1,p2,p3) iff for p being Point of (TOP-REAL 2) holds b_{4} . p = tricord2 (p1,p2,p3,p) );

for p1, p2, p3 being Point of (TOP-REAL 2)

for b

( b

definition

let p1, p2, p3 be Point of (TOP-REAL 2);

ex b_{1} being Function of (TOP-REAL 2),R^1 st

for p being Point of (TOP-REAL 2) holds b_{1} . p = tricord3 (p1,p2,p3,p)

for b_{1}, b_{2} being Function of (TOP-REAL 2),R^1 st ( for p being Point of (TOP-REAL 2) holds b_{1} . p = tricord3 (p1,p2,p3,p) ) & ( for p being Point of (TOP-REAL 2) holds b_{2} . p = tricord3 (p1,p2,p3,p) ) holds

b_{1} = b_{2}

end;
func trcmap3 (p1,p2,p3) -> Function of (TOP-REAL 2),R^1 means :: EUCLID_3:def 16

for p being Point of (TOP-REAL 2) holds it . p = tricord3 (p1,p2,p3,p);

existence for p being Point of (TOP-REAL 2) holds it . p = tricord3 (p1,p2,p3,p);

ex b

for p being Point of (TOP-REAL 2) holds b

proof end;

uniqueness for b

b

proof end;

:: deftheorem defines trcmap3 EUCLID_3:def 16 :

for p1, p2, p3 being Point of (TOP-REAL 2)

for b_{4} being Function of (TOP-REAL 2),R^1 holds

( b_{4} = trcmap3 (p1,p2,p3) iff for p being Point of (TOP-REAL 2) holds b_{4} . p = tricord3 (p1,p2,p3,p) );

for p1, p2, p3 being Point of (TOP-REAL 2)

for b

( b

theorem :: EUCLID_3:55

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

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

proof end;

theorem Th56: :: EUCLID_3:56

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

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

proof end;

theorem :: EUCLID_3:57

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;

( 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: :: EUCLID_3:58

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

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

proof end;

theorem :: EUCLID_3:59

for p1, p2, p3 being Point of (TOP-REAL 2) st p2 - p1,p3 - p1 are_lindependent2 holds

not inside_of_triangle (p1,p2,p3) is empty

not inside_of_triangle (p1,p2,p3) is empty

proof end;