let A, B, C, A1, B1, C1 be Point of (TOP-REAL 2); :: thesis: 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 & ( not (1 - mu) + (lambda * mu) <> 0 or not (1 - lambda) + (nu * lambda) <> 0 or not (1 - nu) + (mu * nu) <> 0 ) holds
( ((lambda / (1 - lambda)) * (mu / (1 - mu))) * (nu / (1 - nu)) = 1 iff ( Line (A,A1) is_parallel_to Line (B,B1) & Line (B,B1) is_parallel_to Line (C,C1) & Line (C,C1) is_parallel_to Line (A,A1) ) )
let lambda, mu, nu be Real; :: thesis: ( 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 & ( not (1 - mu) + (lambda * mu) <> 0 or not (1 - lambda) + (nu * lambda) <> 0 or not (1 - nu) + (mu * nu) <> 0 ) implies ( ((lambda / (1 - lambda)) * (mu / (1 - mu))) * (nu / (1 - nu)) = 1 iff ( Line (A,A1) is_parallel_to Line (B,B1) & Line (B,B1) is_parallel_to Line (C,C1) & Line (C,C1) is_parallel_to Line (A,A1) ) ) )
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: ( not (1 - mu) + (lambda * mu) <> 0 or not (1 - lambda) + (nu * lambda) <> 0 or not (1 - nu) + (mu * nu) <> 0 ) ; :: thesis: ( ((lambda / (1 - lambda)) * (mu / (1 - mu))) * (nu / (1 - nu)) = 1 iff ( Line (A,A1) is_parallel_to Line (B,B1) & Line (B,B1) is_parallel_to Line (C,C1) & Line (C,C1) is_parallel_to Line (A,A1) ) )
A9: B,C,A is_a_triangle by A1;
A10: C,A,B is_a_triangle by A1;
hereby :: thesis: ( Line (A,A1) is_parallel_to Line (B,B1) & Line (B,B1) is_parallel_to Line (C,C1) & Line (C,C1) is_parallel_to Line (A,A1) implies ((lambda / (1 - lambda)) * (mu / (1 - mu))) * (nu / (1 - nu)) = 1 )
assume ((lambda / (1 - lambda)) * (mu / (1 - mu))) * (nu / (1 - nu)) = 1 ; :: thesis: ( Line (A,A1) is_parallel_to Line (B,B1) & Line (B,B1) is_parallel_to Line (C,C1) & Line (C,C1) is_parallel_to Line (A,A1) )
then A11: 0 = ((lambda * mu) * nu) - (((1 - lambda) * (1 - mu)) * (1 - nu)) by Lm4, A5, A6, A7;
then A12: 0 = ((nu * lambda) * mu) - (((1 - nu) * (1 - lambda)) * (1 - mu)) ;
A13: 0 = ((mu * nu) * lambda) - (((1 - mu) * (1 - nu)) * (1 - lambda)) by A11;
( (1 - mu) + (lambda * mu) = 0 & (1 - nu) + (mu * nu) = 0 & (1 - lambda) + (nu * lambda) = 0 )
proof
per cases ( (1 - mu) + (lambda * mu) = 0 or (1 - lambda) + (nu * lambda) = 0 or (1 - nu) + (mu * nu) = 0 ) by A8;
suppose A14: (1 - mu) + (lambda * mu) = 0 ; :: thesis: ( (1 - mu) + (lambda * mu) = 0 & (1 - nu) + (mu * nu) = 0 & (1 - lambda) + (nu * lambda) = 0 )
then (1 - lambda) + (nu * lambda) = 0 by Lm5, A6, A11;
hence ( (1 - mu) + (lambda * mu) = 0 & (1 - nu) + (mu * nu) = 0 & (1 - lambda) + (nu * lambda) = 0 ) by Lm5, A5, A12, A14; :: thesis: verum
end;
suppose A15: (1 - lambda) + (nu * lambda) = 0 ; :: thesis: ( (1 - mu) + (lambda * mu) = 0 & (1 - nu) + (mu * nu) = 0 & (1 - lambda) + (nu * lambda) = 0 )
then (1 - nu) + (nu * mu) = 0 by Lm5, A5, A12;
hence ( (1 - mu) + (lambda * mu) = 0 & (1 - nu) + (mu * nu) = 0 & (1 - lambda) + (nu * lambda) = 0 ) by Lm5, A7, A13, A15; :: thesis: verum
end;
suppose A16: (1 - nu) + (mu * nu) = 0 ; :: thesis: ( (1 - mu) + (lambda * mu) = 0 & (1 - nu) + (mu * nu) = 0 & (1 - lambda) + (nu * lambda) = 0 )
then (1 - mu) + (lambda * mu) = 0 by Lm5, A7, A13;
hence ( (1 - mu) + (lambda * mu) = 0 & (1 - nu) + (mu * nu) = 0 & (1 - lambda) + (nu * lambda) = 0 ) by Lm5, A6, A11, A16; :: thesis: verum
end;
end;
end;
hence ( Line (A,A1) is_parallel_to Line (B,B1) & Line (B,B1) is_parallel_to Line (C,C1) & Line (C,C1) is_parallel_to Line (A,A1) ) by A1, A9, Th16, A2, A3, A4, A5, A6, A7, A10; :: thesis: verum
end;
assume ( Line (A,A1) is_parallel_to Line (B,B1) & Line (B,B1) is_parallel_to Line (C,C1) ) ; :: thesis: ( not Line (C,C1) is_parallel_to Line (A,A1) or ((lambda / (1 - lambda)) * (mu / (1 - mu))) * (nu / (1 - nu)) = 1 )
then A17: ( (1 - mu) + (lambda * mu) = 0 & (1 - nu) + (mu * nu) = 0 ) by A1, A9, Th16, A2, A3, A4, A6, A7;
then ((lambda * mu) * nu) - (((1 - lambda) * (1 - mu)) * (1 - nu)) = ((lambda * mu) * nu) - (((1 - lambda) * (1 - mu)) * (- (mu * nu)))
.= ((lambda + ((1 - lambda) * (1 - mu))) * mu) * nu
.= 0 by A17 ;
hence ( not Line (C,C1) is_parallel_to Line (A,A1) or ((lambda / (1 - lambda)) * (mu / (1 - mu))) * (nu / (1 - nu)) = 1 ) by Lm4, A5, A6, A7; :: thesis: verum