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 & (1 - mu) + (lambda * mu) <> 0 & (1 - lambda) + (nu * lambda) <> 0 & (1 - nu) + (mu * nu) <> 0 holds
( ((lambda / (1 - lambda)) * (mu / (1 - mu))) * (nu / (1 - nu)) = 1 iff ex A2 being Point of (TOP-REAL 2) st
( A,A1,A2 are_collinear & B,B1,A2 are_collinear & C,C1,A2 are_collinear ) )
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 & (1 - mu) + (lambda * mu) <> 0 & (1 - lambda) + (nu * lambda) <> 0 & (1 - nu) + (mu * nu) <> 0 implies ( ((lambda / (1 - lambda)) * (mu / (1 - mu))) * (nu / (1 - nu)) = 1 iff ex A2 being Point of (TOP-REAL 2) st
( A,A1,A2 are_collinear & B,B1,A2 are_collinear & C,C1,A2 are_collinear ) ) )
set q1 = (1 - mu) + (lambda * mu);
set q2 = (1 - lambda) + (nu * lambda);
set q3 = (1 - nu) + (mu * nu);
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
and
A6:
mu <> 1
and
A7:
nu <> 1
and
A8:
(1 - mu) + (lambda * mu) <> 0
and
A9:
(1 - lambda) + (nu * lambda) <> 0
and
A10:
(1 - nu) + (mu * nu) <> 0
; ( ((lambda / (1 - lambda)) * (mu / (1 - mu))) * (nu / (1 - nu)) = 1 iff ex A2 being Point of (TOP-REAL 2) st
( A,A1,A2 are_collinear & B,B1,A2 are_collinear & C,C1,A2 are_collinear ) )
A11:
C,A,B is_a_triangle
by A1;
A12:
B,C,A is_a_triangle
by A1;
consider C2 being Point of (TOP-REAL 2) such that
A13:
A,A1,C2 are_collinear
and
A14:
B,B1,C2 are_collinear
by Lm3, A1, A2, A3, A8;
consider B2 being Point of (TOP-REAL 2) such that
A15:
C,C1,B2 are_collinear
and
A16:
A,A1,B2 are_collinear
by Lm3, A11, A4, A2, A9;
consider A2 being Point of (TOP-REAL 2) such that
A17:
B,B1,A2 are_collinear
and
A18:
C,C1,A2 are_collinear
by Lm3, A12, A3, A4, A10;
A19:
A <> A1
by Th14, A1, A2;
C2,A,A1 are_collinear
by A13;
then A20:
C2 in Line (A,A1)
by A19, Th13;
B2,A,A1 are_collinear
by A16;
then A21:
B2 in Line (A,A1)
by A19, Th13;
A22:
A,A1,B2,C2 are_collinear
by A13, A16, A19, RLTOPSP1:81;
B,C,A is_a_triangle
by A1;
then
B <> B1
by Th14, A3;
then A23:
B,B1,A2,C2 are_collinear
by A14, A17, RLTOPSP1:81;
C,A,B is_a_triangle
by A1;
then
C <> C1
by Th14, A4;
then A24:
C,C1,A2,B2 are_collinear
by A15, A18, RLTOPSP1:81;
hereby ( ex A2 being Point of (TOP-REAL 2) st
( A,A1,A2 are_collinear & B,B1,A2 are_collinear & C,C1,A2 are_collinear ) implies ((lambda / (1 - lambda)) * (mu / (1 - mu))) * (nu / (1 - nu)) = 1 )
assume A25:
((lambda / (1 - lambda)) * (mu / (1 - mu))) * (nu / (1 - nu)) = 1
;
ex A2 being Point of (TOP-REAL 2) st
( A,A1,A2 are_collinear & B,B1,A2 are_collinear & C,C1,A2 are_collinear )per cases
( B2 <> C2 or B2 = C2 )
;
suppose A26:
B2 <> C2
;
ex A2 being Point of (TOP-REAL 2) st
( A,A1,A2 are_collinear & B,B1,A2 are_collinear & C,C1,A2 are_collinear )take A2 =
A2;
( A,A1,A2 are_collinear & B,B1,A2 are_collinear & C,C1,A2 are_collinear )
A2,
B2,
C2 are_collinear
by A25, Lm7, A1, A2, A3, A4, A5, A6, A7, A22, A23, A24;
then A27:
A2 in Line (
B2,
C2)
by Th13, A26;
Line (
B2,
C2)
c= Line (
A,
A1)
by A20, A21, EUCLID_4:42;
then
A2,
A,
A1 are_collinear
by Th13, A19, A27;
hence
A,
A1,
A2 are_collinear
;
( B,B1,A2 are_collinear & C,C1,A2 are_collinear )thus
(
B,
B1,
A2 are_collinear &
C,
C1,
A2 are_collinear )
by A17, A18;
verum end; suppose A28:
B2 = C2
;
ex B2 being Point of (TOP-REAL 2) st
( A,A1,B2 are_collinear & B,B1,B2 are_collinear & C,C1,B2 are_collinear )take B2 =
B2;
( A,A1,B2 are_collinear & B,B1,B2 are_collinear & C,C1,B2 are_collinear )thus
(
A,
A1,
B2 are_collinear &
B,
B1,
B2 are_collinear &
C,
C1,
B2 are_collinear )
by A28, A14, A15, A16;
verum end;
end;
given C3 being Point of (TOP-REAL 2) such that A29:
A,A1,C3 are_collinear
and
A30:
B,B1,C3 are_collinear
and
A31:
C,C1,C3 are_collinear
; ((lambda / (1 - lambda)) * (mu / (1 - mu))) * (nu / (1 - nu)) = 1
A32:
C3,B2,C2 are_collinear
proof
per cases
( B2 <> C2 or B2 = C2 )
;
suppose A33:
B2 <> C2
;
C3,B2,C2 are_collinear
C3,
A,
A1 are_collinear
by A29;
then A34:
C3 in Line (
A,
A1)
by Th13, A19;
Line (
A,
A1)
c= Line (
B2,
C2)
by A20, A21, A33, EUCLID_4:43;
hence
C3,
B2,
C2 are_collinear
by A33, Th13, A34;
verum end;
end;
C3 = A2
proof
assume A35:
C3 <> A2
;
contradiction
C,
A,
B is_a_triangle
by A1;
then A36:
C <> C1
by Th14, A4;
then A37:
Line (
C,
C1) is
being_line
;
B,
C,
A is_a_triangle
by A1;
then A38:
B <> B1
by Th14, A3;
then A39:
Line (
B,
B1) is
being_line
;
C3,
B,
B1 are_collinear
by A30;
then A40:
C3 in Line (
B,
B1)
by Th13, A38;
A2,
B,
B1 are_collinear
by A17;
then A41:
A2 in Line (
B,
B1)
by Th13, A38;
A2,
C,
C1 are_collinear
by A18;
then A42:
A2 in Line (
C,
C1)
by Th13, A36;
C3,
C,
C1 are_collinear
by A31;
then
C3 in Line (
C,
C1)
by Th13, A36;
then A43:
Line (
B,
B1)
= Line (
C,
C1)
by A40, A35, A41, A42, A39, A37, EUCLID_4:44;
A44:
1
- nu <> 0
by A7;
B in Line (
B,
B1)
by EUCLID_4:41;
then
B,
C,
C1 are_collinear
by Th13, A36, A43;
then
the_area_of_polygon3 (
B,
C,
C1)
= 0
by Th9;
then
the_area_of_polygon3 (
C1,
B,
C)
= 0
;
then
((1 - nu) * (the_area_of_polygon3 (A,B,C))) + (nu * (the_area_of_polygon3 (B,B,C))) = 0
by Th7, A4;
then
the_area_of_polygon3 (
A,
B,
C)
= 0
by A44;
hence
contradiction
by Th9, A1;
verum
end;
hence
((lambda / (1 - lambda)) * (mu / (1 - mu))) * (nu / (1 - nu)) = 1
by A32, Lm7, A1, A2, A3, A4, A5, A6, A7, A22, A23, A24; verum