let A, B, C be Point of (TOP-REAL 2); ( A,B,C are_collinear iff the_area_of_polygon3 (A,B,C) = 0 )
hereby ( the_area_of_polygon3 (A,B,C) = 0 implies A,B,C are_collinear )
assume
A,
B,
C are_collinear
;
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
B in LSeg (
C,
A)
;
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
;
verum end; suppose
C in LSeg (
A,
B)
;
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
;
verum end; end;
end;
assume
the_area_of_polygon3 (A,B,C) = 0
; 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 A4:
sin (angle (C,B,A)) = 0
;
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
;
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;
verum end; end; end; end;