let A, B, C be Point of (TOP-REAL 2); :: thesis: ( A,B,C are_collinear iff the_area_of_polygon3 (A,B,C) = 0 )
hereby :: thesis: ( the_area_of_polygon3 (A,B,C) = 0 implies A,B,C are_collinear )
assume A,B,C are_collinear ; :: thesis: the_area_of_polygon3 (A,B,C) = 0
per cases then ( A in LSeg (B,C) or B in LSeg (C,A) or C in LSeg (A,B) ) by TOPREAL9:67;
suppose A in LSeg (B,C) ; :: thesis: the_area_of_polygon3 (A,B,C) = 0
then consider lambda being Real such that
A1: ( A = ((1 - lambda) * B) + (lambda * C) & 0 <= lambda & lambda <= 1 ) ;
the_area_of_polygon3 (A,B,C) = ((1 - lambda) * (the_area_of_polygon3 (B,B,C))) + (lambda * (the_area_of_polygon3 (C,B,C))) by Th7, A1;
hence the_area_of_polygon3 (A,B,C) = 0 ; :: thesis: verum
end;
suppose B in LSeg (C,A) ; :: thesis: the_area_of_polygon3 (A,B,C) = 0
then consider lambda being Real such that
A2: ( B = ((1 - lambda) * C) + (lambda * A) & 0 <= lambda & lambda <= 1 ) ;
the_area_of_polygon3 (A,B,C) = - (the_area_of_polygon3 ((((1 - lambda) * C) + (lambda * A)),A,C)) by A2
.= (- ((1 - lambda) * (the_area_of_polygon3 (C,A,C)))) - (lambda * (the_area_of_polygon3 (A,A,C))) by Th7 ;
hence the_area_of_polygon3 (A,B,C) = 0 ; :: thesis: verum
end;
suppose C in LSeg (A,B) ; :: thesis: the_area_of_polygon3 (A,B,C) = 0
then consider lambda being Real such that
A3: ( C = ((1 - lambda) * A) + (lambda * B) & 0 <= lambda & lambda <= 1 ) ;
the_area_of_polygon3 (A,B,C) = - (the_area_of_polygon3 ((((1 - lambda) * A) + (lambda * B)),B,A)) by A3
.= (- ((1 - lambda) * (the_area_of_polygon3 (A,B,A)))) - (lambda * (the_area_of_polygon3 (B,B,A))) by Th7 ;
hence the_area_of_polygon3 (A,B,C) = 0 ; :: thesis: verum
end;
end;
end;
assume the_area_of_polygon3 (A,B,C) = 0 ; :: thesis: A,B,C are_collinear
then ((|.(A - B).| * |.(C - B).|) * (sin (angle (C,B,A)))) / 2 = 0 by EUCLID_6:5;
per cases then ( |.(A - B).| = 0 or |.(C - B).| = 0 or sin (angle (C,B,A)) = 0 ) ;
suppose |.(A - B).| = 0 ; :: thesis: A,B,C are_collinear
then A = B by EUCLID_6:42;
then not A,B,C are_mutually_distinct by ZFMISC_1:def 5;
hence A,B,C are_collinear by EUCLID_6:20; :: thesis: verum
end;
suppose |.(C - B).| = 0 ; :: thesis: A,B,C are_collinear
then C = B by EUCLID_6:42;
then not A,B,C are_mutually_distinct by ZFMISC_1:def 5;
hence A,B,C are_collinear by EUCLID_6:20; :: thesis: verum
end;
suppose A4: sin (angle (C,B,A)) = 0 ; :: thesis: A,B,C are_collinear
( (2 * PI) * 0 <= angle (C,B,A) & angle (C,B,A) < (2 * PI) + ((2 * PI) * 0) ) by COMPLEX2:70;
then ( angle (C,B,A) = (2 * PI) * 0 or angle (C,B,A) = PI + ((2 * PI) * 0) ) by A4, SIN_COS6:21;
per cases then ( angle (C,B,A) = 0 or angle (C,B,A) = PI ) ;
suppose angle (C,B,A) = 0 ; :: thesis: A,B,C are_collinear
then ( angle (B,C,A) = PI or angle (B,A,C) = PI or not C,B,A are_mutually_distinct ) by Th8;
then ( C in LSeg (B,A) or A in LSeg (B,C) or not C <> B or not C <> A or not B <> A ) by EUCLID_6:11, ZFMISC_1:def 5;
then ( C in LSeg (B,A) or A in LSeg (B,C) or not A,B,C are_mutually_distinct ) by ZFMISC_1:def 5;
hence A,B,C are_collinear by EUCLID_6:20, TOPREAL9:67; :: thesis: verum
end;
end;
end;
end;