:: Routh's, {M}enelaus' and Generalized {C}eva's Theorems
:: by Boris A. Shminke
::
:: Received January 16, 2012
:: Copyright (c) 2012-2021 Association of Mizar Users


notation
let X, Y be Subset of (TOP-REAL 2);
synonym X is_parallel_to Y for X misses Y;
end;

definition
let X, Y, Z be Subset of (TOP-REAL 2);
pred X,Y,Z are_concurrent means :: MENELAUS:def 1
( ( X is_parallel_to Y & Y is_parallel_to Z & Z is_parallel_to X ) or ex A being Point of (TOP-REAL 2) st
( A in X & A in Y & A in Z ) );
end;

:: deftheorem defines are_concurrent MENELAUS:def 1 :
for X, Y, Z being Subset of (TOP-REAL 2) holds
( X,Y,Z are_concurrent iff ( ( X is_parallel_to Y & Y is_parallel_to Z & Z is_parallel_to X ) or ex A being Point of (TOP-REAL 2) st
( A in X & A in Y & A in Z ) ) );

theorem Th1: :: MENELAUS:1
for A, B being Point of (TOP-REAL 2) holds
( (A + B) `1 = (A `1) + (B `1) & (A + B) `2 = (A `2) + (B `2) )
proof end;

theorem Th2: :: MENELAUS:2
for A being Point of (TOP-REAL 2)
for lambda being Real holds
( (lambda * A) `1 = lambda * (A `1) & (lambda * A) `2 = lambda * (A `2) )
proof end;

theorem Th3: :: MENELAUS:3
for A being Point of (TOP-REAL 2) holds
( (- A) `1 = - (A `1) & (- A) `2 = - (A `2) )
proof end;

theorem Th4: :: MENELAUS:4
for A, B being Point of (TOP-REAL 2)
for lambda, mu being Real holds
( ((lambda * A) + (mu * B)) `1 = (lambda * (A `1)) + (mu * (B `1)) & ((lambda * A) + (mu * B)) `2 = (lambda * (A `2)) + (mu * (B `2)) )
proof end;

theorem :: MENELAUS:5
for A being Point of (TOP-REAL 2)
for lambda being Real holds
( ((- lambda) * A) `1 = - (lambda * (A `1)) & ((- lambda) * A) `2 = - (lambda * (A `2)) )
proof end;

theorem :: MENELAUS:6
for A, B being Point of (TOP-REAL 2)
for lambda, mu being Real holds
( ((lambda * A) - (mu * B)) `1 = (lambda * (A `1)) - (mu * (B `1)) & ((lambda * A) - (mu * B)) `2 = (lambda * (A `2)) - (mu * (B `2)) )
proof end;

theorem Th7: :: MENELAUS:7
for A, B, C, A1 being Point of (TOP-REAL 2)
for lambda being Real holds the_area_of_polygon3 ((((1 - lambda) * A) + (lambda * A1)),B,C) = ((1 - lambda) * (the_area_of_polygon3 (A,B,C))) + (lambda * (the_area_of_polygon3 (A1,B,C)))
proof end;

theorem Th8: :: MENELAUS:8
for A, B, C being Point of (TOP-REAL 2) st angle (A,B,C) = 0 & A,B,C are_mutually_distinct & not angle (B,C,A) = PI holds
angle (B,A,C) = PI
proof end;

theorem Th9: :: MENELAUS:9
for A, B, C being Point of (TOP-REAL 2) holds
( A,B,C are_collinear iff the_area_of_polygon3 (A,B,C) = 0 )
proof end;

theorem Th10: :: MENELAUS:10
for B, C being Point of (TOP-REAL 2) holds the_area_of_polygon3 ((0. (TOP-REAL 2)),B,C) = (((B `1) * (C `2)) - ((C `1) * (B `2))) / 2
proof end;

theorem :: MENELAUS:11
for A, B, C, A1 being Point of (TOP-REAL 2) holds the_area_of_polygon3 ((A + A1),B,C) = ((the_area_of_polygon3 (A,B,C)) + (the_area_of_polygon3 (A1,B,C))) - (the_area_of_polygon3 ((0. (TOP-REAL 2)),B,C))
proof end;

theorem Th12: :: MENELAUS:12
for A, B, C being Point of (TOP-REAL 2) st A in LSeg (B,C) holds
A in Line (B,C)
proof end;

theorem Th13: :: MENELAUS:13
for A, B, C being Point of (TOP-REAL 2) st B <> C holds
( A,B,C are_collinear iff A in Line (B,C) )
proof end;

Lm1: for A, B, C, A1, B1, C2 being Point of (TOP-REAL 2)
for lambda, mu, alpha being Real st A1 = ((1 - lambda) * B) + (lambda * C) & B1 = ((1 - mu) * C) + (mu * A) & C2 = ((1 - alpha) * A) + (alpha * A1) holds
the_area_of_polygon3 (B,B1,C2) = ((1 - mu) - (alpha * ((1 - mu) + (lambda * mu)))) * (the_area_of_polygon3 (A,B,C))
proof end;

theorem Th14: :: MENELAUS:14
for A, B, C, A1 being Point of (TOP-REAL 2)
for lambda being Real st A,B,C is_a_triangle & A1 = ((1 - lambda) * B) + (lambda * C) holds
A <> A1
proof end;

theorem :: MENELAUS:15
for A, B, C being Point of (TOP-REAL 2) st A,B,C is_a_triangle holds
( A,C,B is_a_triangle & B,A,C is_a_triangle & B,C,A is_a_triangle & C,A,B is_a_triangle & C,B,A is_a_triangle ) ;

Lm2: for A, B, C, A1, B1, C2 being Point of (TOP-REAL 2)
for lambda, mu being Real st A,B,C is_a_triangle & A1 = ((1 - lambda) * B) + (lambda * C) & B1 = ((1 - mu) * C) + (mu * A) & mu <> 1 & A,A1,C2 are_collinear & B,B1,C2 are_collinear holds
( (1 - mu) + (lambda * mu) <> 0 & ex alpha being Real st
( C2 = ((1 - alpha) * A) + (alpha * A1) & alpha = (1 - mu) / ((1 - mu) + (lambda * mu)) ) )
proof end;

Lm3: for A, B, C, A1, B1 being Point of (TOP-REAL 2)
for lambda, mu being Real st A,B,C is_a_triangle & A1 = ((1 - lambda) * B) + (lambda * C) & B1 = ((1 - mu) * C) + (mu * A) & (1 - mu) + (lambda * mu) <> 0 holds
ex C2 being Point of (TOP-REAL 2) st
( A,A1,C2 are_collinear & B,B1,C2 are_collinear )
proof end;

Lm4: for lambda, mu, nu being Real st lambda <> 1 & mu <> 1 & nu <> 1 holds
( 0 = ((lambda * mu) * nu) - (((1 - lambda) * (1 - mu)) * (1 - nu)) iff ((lambda / (1 - lambda)) * (mu / (1 - mu))) * (nu / (1 - nu)) = 1 )
proof end;

Lm5: for lambda, mu, nu being Real st mu <> 1 & 0 = ((lambda * mu) * nu) - (((1 - lambda) * (1 - mu)) * (1 - nu)) & (1 - mu) + (mu * lambda) = 0 holds
(1 - lambda) + (lambda * nu) = 0
proof end;

theorem Th16: :: MENELAUS:16
for A, B, C, A1, B1 being Point of (TOP-REAL 2)
for lambda, mu being Real st A,B,C is_a_triangle & A1 = ((1 - lambda) * B) + (lambda * C) & B1 = ((1 - mu) * C) + (mu * A) & mu <> 1 holds
( (1 - mu) + (lambda * mu) <> 0 iff not Line (A,A1) is_parallel_to Line (B,B1) )
proof end;

Lm6: for A, B, C, A1, B1, C1 being 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 & ( 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) ) )
proof end;

:: WP: Pre-Routh's Theorem
theorem Th17: :: MENELAUS:17
for A, B, C, A1, B1, C1 being Point of (TOP-REAL 2)
for lambda, mu, nu being Real st A1 = ((1 - lambda) * B) + (lambda * C) & B1 = ((1 - mu) * C) + (mu * A) & C1 = ((1 - nu) * A) + (nu * B) holds
the_area_of_polygon3 (A1,B1,C1) = ((((1 - lambda) * (1 - mu)) * (1 - nu)) + ((lambda * mu) * nu)) * (the_area_of_polygon3 (A,B,C))
proof end;

:: WP: Menelaus' Theorem
theorem :: MENELAUS:18
for A, B, C, A1, B1, C1 being 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 )
proof end;

:: WP: Routh's Theorem
theorem Th19: :: MENELAUS:19
for A, B, C, A1, B1, C1, A2, B2, C2 being 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 & A,A1,B2,C2 are_collinear & B,B1,A2,C2 are_collinear & C,C1,A2,B2 are_collinear holds
( (((1 - mu) + (lambda * mu)) * ((1 - lambda) + (nu * lambda))) * ((1 - nu) + (mu * nu)) <> 0 & the_area_of_polygon3 (A2,B2,C2) = (((((mu * nu) * lambda) - (((1 - mu) * (1 - nu)) * (1 - lambda))) ^2) / ((((1 - mu) + (lambda * mu)) * ((1 - lambda) + (nu * lambda))) * ((1 - nu) + (mu * nu)))) * (the_area_of_polygon3 (A,B,C)) )
proof end;

:: WP: Feynman's (one-seventh area) Triangle
theorem :: MENELAUS:20
for A, B, C, A1, B1, C1, A2, B2, C2 being Point of (TOP-REAL 2) st A,B,C is_a_triangle & A1 = ((2 / 3) * B) + ((1 / 3) * C) & B1 = ((2 / 3) * C) + ((1 / 3) * A) & C1 = ((2 / 3) * A) + ((1 / 3) * B) & A,A1,B2,C2 are_collinear & B,B1,A2,C2 are_collinear & C,C1,A2,B2 are_collinear holds
the_area_of_polygon3 (A2,B2,C2) = (the_area_of_polygon3 (A,B,C)) / 7
proof end;

Lm7: for A, B, C, A1, B1, C1, A2, B2, C2 being 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 & A,A1,B2,C2 are_collinear & B,B1,A2,C2 are_collinear & C,C1,A2,B2 are_collinear holds
( ((lambda / (1 - lambda)) * (mu / (1 - mu))) * (nu / (1 - nu)) = 1 iff A2,B2,C2 are_collinear )
proof end;

:: WP: Ceva's Theorem
theorem Th21: :: MENELAUS:21
for A, B, C, A1, B1, C1 being 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 ) )
proof end;

:: WP: Generalized Ceva's Theorem
theorem :: MENELAUS:22
for A, B, C, A1, B1, C1 being 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
( ((lambda / (1 - lambda)) * (mu / (1 - mu))) * (nu / (1 - nu)) = 1 iff Line (A,A1), Line (B,B1), Line (C,C1) are_concurrent )
proof end;