let A, B, C, A1, B1, C1 be Point of (TOP-REAL 2); for lambda, mu, nu being Real st A,B,C is_a_triangle & A1 = ((1 - lambda) * B) + (lambda * C) & B1 = ((1 - mu) * C) + (mu * A) & C1 = ((1 - nu) * A) + (nu * B) & lambda <> 1 & mu <> 1 & nu <> 1 holds
( A1,B1,C1 are_collinear iff ((lambda / (1 - lambda)) * (mu / (1 - mu))) * (nu / (1 - nu)) = - 1 )
let lambda, mu, nu be Real; ( A,B,C is_a_triangle & A1 = ((1 - lambda) * B) + (lambda * C) & B1 = ((1 - mu) * C) + (mu * A) & C1 = ((1 - nu) * A) + (nu * B) & lambda <> 1 & mu <> 1 & nu <> 1 implies ( A1,B1,C1 are_collinear iff ((lambda / (1 - lambda)) * (mu / (1 - mu))) * (nu / (1 - nu)) = - 1 ) )
assume that
A1:
A,B,C is_a_triangle
and
A2:
A1 = ((1 - lambda) * B) + (lambda * C)
and
A3:
B1 = ((1 - mu) * C) + (mu * A)
and
A4:
C1 = ((1 - nu) * A) + (nu * B)
and
A5:
( lambda <> 1 & mu <> 1 & nu <> 1 )
; ( A1,B1,C1 are_collinear iff ((lambda / (1 - lambda)) * (mu / (1 - mu))) * (nu / (1 - nu)) = - 1 )
A6:
the_area_of_polygon3 (A,B,C) <> 0
by Th9, A1;
set q = ((1 - lambda) * (1 - mu)) * (1 - nu);
A7:
( 1 - lambda <> 0 & 1 - mu <> 0 & 1 - nu <> 0 )
by A5;
( A1,B1,C1 are_collinear iff the_area_of_polygon3 (A1,B1,C1) = 0 )
by Th9;
then
( A1,B1,C1 are_collinear iff ((((1 - lambda) * (1 - mu)) * (1 - nu)) + ((lambda * mu) * nu)) * (the_area_of_polygon3 (A,B,C)) = 0 )
by Th17, A2, A3, A4;
then
( A1,B1,C1 are_collinear iff (1 * (((1 - lambda) * (1 - mu)) * (1 - nu))) + ((lambda * mu) * nu) = 0 )
by A6;
then
( A1,B1,C1 are_collinear iff (((1 - lambda) * (1 - mu)) * (1 - nu)) * (1 + (((lambda * mu) * nu) / (((1 - lambda) * (1 - mu)) * (1 - nu)))) = 0 )
by A7, XCMPLX_1:235;
then
( A1,B1,C1 are_collinear iff 1 + (((lambda * mu) * nu) / (((1 - lambda) * (1 - mu)) * (1 - nu))) = 0 )
by A7;
then
( A1,B1,C1 are_collinear iff - 1 = (lambda * (mu * nu)) / ((1 - lambda) * ((1 - mu) * (1 - nu))) )
;
then
( A1,B1,C1 are_collinear iff - 1 = ((lambda / (1 - lambda)) * (mu * nu)) / ((1 - mu) * (1 - nu)) )
by XCMPLX_1:83;
then
( A1,B1,C1 are_collinear iff - 1 = (lambda / (1 - lambda)) * ((mu * nu) / ((1 - mu) * (1 - nu))) )
by XCMPLX_1:74;
then
( A1,B1,C1 are_collinear iff - 1 = (lambda / (1 - lambda)) * (((mu / (1 - mu)) * nu) / (1 - nu)) )
by XCMPLX_1:83;
then
( A1,B1,C1 are_collinear iff - 1 = (lambda / (1 - lambda)) * ((mu / (1 - mu)) * (nu / (1 - nu))) )
by XCMPLX_1:74;
hence
( A1,B1,C1 are_collinear iff ((lambda / (1 - lambda)) * (mu / (1 - mu))) * (nu / (1 - nu)) = - 1 )
; verum