:: Routh's, {M}enelaus' and Generalized {C}eva's Theorems :: by Boris A. Shminke :: :: Received January 16, 2012 :: Copyright (c) 2012 Association of Mizar Users begin 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); predX,Y,Z are_concurrent means :def2: :: 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 def2 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) ) proofend; 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) ) proofend; theorem Th3: :: MENELAUS:3 for A being Point of (TOP-REAL 2) holds ( (- A) `1 = - (A `1) & (- A) `2 = - (A `2) ) proofend; 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)) ) proofend; 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)) ) proofend; 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)) ) proofend; theorem Th7: :: MENELAUS:7 for A, A1, B, C 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))) proofend; 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_different & not angle (B,C,A) = PI holds angle (B,A,C) = PI proofend; theorem Th9: :: MENELAUS:9 for A, B, C being Point of (TOP-REAL 2) holds ( A,B,C is_collinear iff the_area_of_polygon3 (A,B,C) = 0 ) proofend; theorem Th21: :: 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 proofend; theorem :: MENELAUS:11 for A, A1, B, C 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)) proofend; 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) proofend; theorem Th13: :: MENELAUS:13 for B, C, A being Point of (TOP-REAL 2) st B <> C holds ( A,B,C is_collinear iff A in Line (B,C) ) proofend; Lm1: for A1, B, C, B1, A, 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)) proofend; 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 proofend; theorem Th15: :: 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 ) proofend; 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 is_collinear & B,B1,C2 is_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)) ) ) proofend; 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 is_collinear & B,B1,C2 is_collinear ) proofend; 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 ) proofend; Lm6: for mu, lambda, 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 proofend; theorem Th18: :: 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) ) proofend; Lm7: 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) ) ) proofend; begin :: Pre-Routh's Theorem theorem Th10: :: MENELAUS:17 for A1, B, C, B1, A, 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)) proofend; :: 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 is_collinear iff ((lambda / (1 - lambda)) * (mu / (1 - mu))) * (nu / (1 - nu)) = - 1 ) proofend; :: Routh's Theorem theorem Th16: :: MENELAUS:19 for A, B, C, A1, B1, C1, C2, A2, B2 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,C2 is_collinear & B,B1,C2 is_collinear & B,B1,A2 is_collinear & C,C1,A2 is_collinear & A,A1,B2 is_collinear & C,C1,B2 is_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)) ) proofend; :: Feynman's (one-seventh area) Triangle theorem :: MENELAUS:20 for A, B, C, A1, B1, C1, C2, A2, B2 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,C2 is_collinear & B,B1,C2 is_collinear & B,B1,A2 is_collinear & C,C1,A2 is_collinear & A,A1,B2 is_collinear & C,C1,B2 is_collinear holds the_area_of_polygon3 (A2,B2,C2) = (the_area_of_polygon3 (A,B,C)) / 7 proofend; Lm5: for A, B, C, A1, B1, C1, C2, A2, B2 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,C2 is_collinear & B,B1,C2 is_collinear & B,B1,A2 is_collinear & C,C1,A2 is_collinear & A,A1,B2 is_collinear & C,C1,B2 is_collinear holds ( ((lambda / (1 - lambda)) * (mu / (1 - mu))) * (nu / (1 - nu)) = 1 iff A2,B2,C2 is_collinear ) proofend; :: Ceva's Theorem theorem Th19: :: 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 is_collinear & B,B1,A2 is_collinear & C,C1,A2 is_collinear ) ) proofend; :: 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 ) proofend;