:: Routh's, {M}enelaus' and Generalized {C}eva's Theorems
:: by Boris A. Shminke
::
:: Received January 16, 2012
:: Copyright (c) 2012-2026 Association of Mizar Users
:: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.
environ
vocabularies PRE_TOPC, EUCLID, REAL_1, EUCLID_6, ARYTM_1, CARD_1, ARYTM_3,
MCART_1, RELAT_1, RLTOPSP1, XXREAL_0, COMPLEX1, SIN_COS, COMPLEX2,
ZFMISC_1, EUCLID_3, PROJPL_1, INCSP_1, TARSKI, SQUARE_1, AFF_1, SUBSET_1,
PROJRED2, RUSUB_5, SUPINF_2, XBOOLE_0, PENCIL_1;
notations XBOOLE_0, XXREAL_0, XCMPLX_0, PRE_TOPC, REAL_1, EUCLID_6, ORDINAL1,
NUMBERS, RLVECT_1, RLTOPSP1, SIN_COS, EUCLID_3, EUCLID, ZFMISC_1,
COMPLEX2, TARSKI, SQUARE_1, XREAL_0, SUBSET_1, EUCLID_4, STRUCT_0;
constructors XXREAL_0, PRE_TOPC, REAL_1, EUCLID_6, BINOP_2, NUMBERS, RLVECT_1,
RLTOPSP1, SIN_COS, EUCLID_3, EUCLID, MONOID_0, ZFMISC_1, COMPLEX2,
TARSKI, SQUARE_1, XREAL_0, ORDINAL1, SUBSET_1, EUCLID_4, STRUCT_0,
COMPLEX1;
registrations XREAL_0, MEMBERED, MONOID_0, EUCLID, XCMPLX_0, SQUARE_1,
SIN_COS, ORDINAL1;
requirements SUBSET, NUMERALS, ARITHM;
equalities EUCLID_6, RLTOPSP1, EUCLID_3, SQUARE_1;
expansions RLTOPSP1, EUCLID_4;
theorems EUCLID, EUCLID_6, ZFMISC_1, COMPLEX2, SIN_COS6, EUCLID_3, XCMPLX_1,
EUCLID_4, XBOOLE_0, RLVECT_1, TOPREAL9, RLTOPSP1;
begin :: Some Properties of the Area of Triangle
reserve A, B, C, A1, B1, C1, A2, B2, C2, C3 for Point of TOP-REAL 2,
lambda, mu, nu, alpha, beta, gamma for Real,
X, Y, Z for Subset of TOP-REAL 2;
notation
let X,Y;
synonym X is_parallel_to Y for X misses Y;
end;
definition
let X, Y, Z;
pred X, Y, Z are_concurrent means
((X is_parallel_to Y & Y is_parallel_to Z & Z is_parallel_to X) or
ex A st (A in X & A in Y & A in Z));
end;
theorem
Th1: (A + B) `1 = A `1 + B `1 & (A + B) `2 = A `2 + B `2
proof
A + B = |[((A `1) + (B `1)), ((A `2) + (B `2))]| by EUCLID:55;
hence thesis by EUCLID:52;
end;
theorem
Th2: (lambda * A) `1 = lambda * A `1 & (lambda * A) `2 = lambda * A `2
proof
lambda * A = |[lambda * A `1, lambda * A `2]| by EUCLID:57;
hence thesis by EUCLID:52;
end;
theorem
Th3: (- A) `1 = - A `1 & (- A) `2 = - A `2
proof
- A = |[- A `1, - A `2]| by EUCLID:59;
hence thesis by EUCLID:52;
end;
theorem
Th4: (lambda * A + mu * B) `1 = lambda * A `1 + mu * B `1 &
(lambda * A + mu * B) `2 = lambda * A `2 + mu * B `2
proof
(lambda * A + mu * B) `1 = (lambda * A) `1 + (mu * B) `1 by Th1
.= lambda * A `1 + (mu * B) `1 by Th2;
hence (lambda * A + mu * B) `1 = lambda * A `1 + mu * B `1 by Th2;
(lambda * A + mu * B) `2 = (lambda * A) `2 + (mu * B) `2 by Th1
.= lambda * A `2 + (mu * B) `2 by Th2;
hence thesis by Th2;
end;
theorem
((- lambda) * A) `1 = - lambda * A `1 &
((- lambda) * A) `2 = - lambda * A `2
proof
((- lambda) * A) `1 = (- (lambda * A)) `1 by RLVECT_1:79
.= - (lambda * A) `1 by Th3;
hence ((- lambda) * A) `1 = - lambda * A `1 by Th2;
((- lambda) * A) `2 = (- (lambda * A)) `2 by RLVECT_1:79
.= - (lambda * A) `2 by Th3;
hence thesis by Th2;
end;
theorem
(lambda * A - mu * B) `1 = lambda * A `1 - mu * B `1 &
(lambda * A - mu * B) `2 = lambda * A `2 - mu * B `2
proof
(lambda * A - mu * B) `1 = (lambda * A) `1 - (mu * B) `1 by EUCLID_6:41
.= lambda * A `1 - (mu * B) `1 by Th2;
hence (lambda * A - mu * B) `1 = lambda * A `1 - mu * B `1 by Th2;
(lambda * A - mu * B) `2 = (lambda * A) `2 - (mu * B) `2 by EUCLID_6:41
.= lambda * A `2 - (mu * B) `2 by Th2;
hence thesis by Th2;
end;
theorem
Th7: 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
the_area_of_polygon3((1 - lambda) * A + lambda * A1, B, C) =
((((1- lambda) * A `1 + lambda * A1 `1) * B `2
- B `1 * ((1- lambda) * A + lambda * A1) `2)
+ (B `1 * C `2 - C `1 * B `2) + (C `1 * ((1- lambda) * A + lambda * A1) `2
- ((1- lambda) * A + lambda * A1) `1 * C `2)) / 2 by Th4
.= ((((1- lambda) * A `1 + lambda * A1 `1) * B `2 -
B `1 * ((1- lambda) * A `2 + lambda * A1 `2)) + (B `1 * C `2 - C `1 * B `2)
+ (C `1 * ((1- lambda) * A + lambda * A1) `2
- ((1- lambda) * A + lambda * A1) `1 * C `2)) / 2 by Th4
.= ((((1- lambda) * A `1 + lambda * A1 `1) * B `2 -
B `1 * ((1- lambda) * A `2 + lambda * A1 `2)) + (B `1 * C `2 - C `1 * B `2)
+ (C `1 * ((1- lambda) * A `2 + lambda * A1 `2)
- ((1- lambda) * A + lambda * A1) `1 * C `2)) / 2 by Th4
.= ((((1- lambda) * A `1 + lambda * A1 `1) * B `2 -
B `1 * ((1- lambda) * A `2 + lambda * A1 `2)) + (B `1 * C `2 - C `1 * B `2)
+ (C `1 * ((1- lambda) * A `2 + lambda * A1 `2)
- ((1- lambda) * A `1 + lambda * A1 `1) * C `2)) / 2 by Th4;
hence thesis;
end;
theorem
Th8: (angle(A, B, C) = 0 & A, B, C are_mutually_distinct) implies
(angle(B, C, A) = PI or angle(B, A, C) = PI)
proof
set z1 = (euc2cpx A);
set z2 = (euc2cpx B);
set z3 = (euc2cpx C);
assume that A1: angle(A, B, C) = 0 and A2: A, B, C are_mutually_distinct;
A <> B & A <> C & B <> C by A2,ZFMISC_1:def 5;
then A3: z1 <> z2 & z1 <> z3 & z2 <> z3 by EUCLID_3:4;
per cases;
suppose angle (z2, z3, z1) = 0 & angle (z3, z1, z2) = PI;
hence thesis by COMPLEX2:82;
end;
suppose not (angle (z2, z3, z1) = 0 & angle (z3, z1, z2) = PI);
hence thesis by A3,A1,COMPLEX2:87;
end;
end;
theorem
Th9: A, B, C are_collinear iff the_area_of_polygon3(A, B, C) = 0
proof
hereby
assume A, B, C are_collinear;
then per cases by TOPREAL9:67;
suppose A in LSeg(B, C);
then consider lambda such that
A1: A = (1 - lambda) * B + lambda * C & 0 <= lambda & lambda <= 1;
the_area_of_polygon3(A, B, C) =
(1 - lambda) * the_area_of_polygon3(B, B, C)
+ lambda * the_area_of_polygon3(C, B, C) by Th7,A1;
hence the_area_of_polygon3(A, B, C) = 0;
end;
suppose B in LSeg(C, A);
then consider lambda such that
A2: B = (1 - lambda) * C + lambda * A & 0 <= lambda & lambda <= 1;
the_area_of_polygon3(A, B, C) =
- the_area_of_polygon3((1 - lambda) * C + lambda * A, A, C) by A2
.= - (1 - lambda) * the_area_of_polygon3(C, A, C)
- lambda * the_area_of_polygon3(A, A, C) by Th7;
hence the_area_of_polygon3(A, B, C) = 0;
end;
suppose C in LSeg(A, B);
then consider lambda such that
A3: C = (1 - lambda) * A + lambda * B & 0 <= lambda & lambda <= 1;
the_area_of_polygon3(A, B, C) =
- the_area_of_polygon3((1 - lambda) * A + lambda * B, B, A) by A3
.= - (1 - lambda) * the_area_of_polygon3(A, B, A)
- lambda * the_area_of_polygon3(B, B, A) by Th7;
hence the_area_of_polygon3(A, B, C) = 0;
end;
end;
assume the_area_of_polygon3(A, B, C) = 0;
then |.A - B.| * |.C - B.| * sin angle (C, B, A) / 2 = 0 by EUCLID_6:5;
then per cases;
suppose |.(A - B).| = 0;
then A = B by EUCLID_6:42;
then not A, B, C are_mutually_distinct by ZFMISC_1:def 5;
hence A, B, C are_collinear by EUCLID_6:20;
end;
suppose |.(C - B).| = 0;
then C = B by EUCLID_6:42;
then not A, B, C are_mutually_distinct by ZFMISC_1:def 5;
hence A, B, C are_collinear by EUCLID_6:20;
end;
suppose A4: sin (angle (C, B, A)) = 0;
2 * PI * 0 <= angle(C, B, A) & angle(C, B, A) < 2 * PI + 2 * PI * 0
by COMPLEX2:70;
then angle(C, B, A) = 2 * PI * 0 or angle(C, B, A) = PI + 2 * PI * 0
by A4,SIN_COS6:21;
then per cases;
suppose angle(C, B, A) = 0;
then angle(B, C, A) = PI or angle(B, A, C) = PI
or not C, B, A are_mutually_distinct by Th8;
then C in LSeg(B, A) or A in LSeg(B, C)
or not (C <> B & C <> A & B <> A) by EUCLID_6:11,ZFMISC_1:def 5;
then C in LSeg(B, A) or A in LSeg(B, C)
or not A, B, C are_mutually_distinct by ZFMISC_1:def 5;
hence thesis by EUCLID_6:20,TOPREAL9:67;
end;
suppose angle(C, B, A) = PI;
then B in LSeg(C, A) by EUCLID_6:11;
hence thesis by TOPREAL9:67;
end;
end;
end;
theorem
Th10: the_area_of_polygon3(0. (TOP-REAL 2), B, C) =
(B `1 * C `2 - C `1 * B `2) / 2
proof
the_area_of_polygon3(0. (TOP-REAL 2), B, C) = ((0 * B `2 - B `1 *
(|[0,0]|) `2) + (B `1 * C `2 - C `1 * B `2) + (C `1 * (|[0,0]|) `2 -
(|[0,0]|) `1 * C `2)) / 2 by EUCLID:52,54
.= ((0 - B `1 * 0) + (B `1 * C `2 - C `1 * B `2) + (C `1 * (|[0,0]|) `2 -
(|[0,0]|) `1 * C `2)) / 2 by EUCLID:52
.= ((B `1 * C `2 - C `1 * B `2) + (C `1 * 0 - (|[0,0]|) `1 * C `2)) / 2
by EUCLID:52
.= ((B `1 * C `2 - C `1 * B `2) + (0 - 0 * C `2)) / 2 by EUCLID:52;
hence thesis;
end;
theorem
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
the_area_of_polygon3(A + A1, B, C) = (((A `1 + A1 `1) * B `2 - B `1 * (A +
A1) `2) + (B `1 * C `2 - C `1 * B `2) + (C `1 * (A + A1) `2 - (A + A1) `1 *
C `2)) / 2 by Th1
.= (((A `1 + A1 `1) * B `2 - B `1 * (A `2 + A1 `2)) + (B `1 * C `2 - C `1 *
B `2) + (C `1 * (A + A1) `2 - (A + A1) `1 * C `2)) / 2 by Th1
.= (((A `1 + A1 `1) * B `2 - B `1 * (A `2 + A1 `2)) + (B `1 * C `2 - C `1 *
B `2) + (C `1 * (A `2 + A1 `2) - (A + A1) `1 * C `2)) / 2 by Th1
.= (((A `1 + A1 `1) * B `2 - B `1 * (A `2 + A1 `2)) + (B `1 * C `2 - C `1 *
B `2) + (C `1 * (A `2 + A1 `2) - (A `1 + A1 `1) * C `2)) / 2 by Th1
.= (((A `1 + A1 `1) * B `2 - B `1 * (A `2 + A1 `2)) + 2 * (B `1 * C `2 -
C `1 * B `2) + (C `1 * (A `2 + A1 `2) - (A `1 + A1 `1) * C `2)) / 2 - (B `1
* C `2 - C `1 * B `2) / 2;
hence thesis by Th10;
end;
theorem
Th12: A in LSeg(B, C) implies A in Line(B, C)
proof
assume A in LSeg(B, C);
then consider lambda such that
A1: A = (1 - lambda) * B + lambda * C & 0 <= lambda & lambda <=1;
thus thesis by A1;
end;
theorem
Th13: B <> C implies (A, B, C are_collinear iff A in Line(B, C))
proof
assume A1: B <> C;
hereby
assume A, B, C are_collinear;
then per cases by TOPREAL9:67;
suppose A in LSeg(B, C);
hence A in Line(B, C) by Th12;
end;
suppose B in LSeg(C, A);
then A2: B in Line(C, A) by Th12;
A3: C in Line(C, A) & A in Line(C, A) by EUCLID_4:41;
then Line(C, A) c= Line(B, C) by A2,A1,EUCLID_4:43;
hence A in Line(B, C) by A3;
end;
suppose C in LSeg(A, B);
then A4: C in Line(A, B) by Th12;
A5: A in Line(A, B) & B in Line(A, B) by EUCLID_4:41;
then Line(A, B) c= Line(B, C) by A4,A1,EUCLID_4:43;
hence A in Line(B, C) by A5;
end;
end;
assume A in Line(B, C);
then consider lambda such that
A6: A = (1 - lambda) * B + lambda * C;
the_area_of_polygon3(A, B, C) =
(1 - lambda) * the_area_of_polygon3(B, B, C) +
lambda * the_area_of_polygon3(C, B, C) by Th7,A6;
hence thesis by Th9;
end;
Lm1:
(A1 = (1 - lambda) * B + lambda * C & B1 = (1 - mu) * C + mu * A & C2 = (1 -
alpha) * A + alpha * A1) implies the_area_of_polygon3(B, B1, C2) = ((1 - mu)
- alpha * (1 - mu + lambda * mu)) * the_area_of_polygon3(A, B, C)
proof
assume that A1: A1 = (1 - lambda) * B + lambda * C and A2
: B1 = (1 - mu) * C +
mu * A and A3: C2 = (1 - alpha) * A + alpha * A1;
the_area_of_polygon3(B, B1, C2)
= the_area_of_polygon3((1 - alpha) * A + alpha * A1, B, B1) by A3
.= (1 - alpha) * the_area_of_polygon3(A, B, B1) + alpha *
the_area_of_polygon3(A1, B, B1) by Th7
.= (1 - alpha) * the_area_of_polygon3(B1, A, B) + alpha * ((1 - lambda) *
the_area_of_polygon3(B, B, B1) + lambda * the_area_of_polygon3(C, B, B1))
by Th7,A1
.= (1 - alpha) * ((1 - mu) * the_area_of_polygon3(C, A, B) + mu *
the_area_of_polygon3(A, A, B)) + alpha * lambda *
the_area_of_polygon3(B1, C, B) by Th7,A2
.= (1 - alpha) * (1 - mu) * the_area_of_polygon3(C, A, B) + alpha * lambda *
((1 - mu) * the_area_of_polygon3(C, C, B) + mu *
the_area_of_polygon3(A, C, B)) by Th7,A2
.= (1 - alpha) * (1 - mu) * the_area_of_polygon3(A, B, C) - alpha * lambda *
mu * the_area_of_polygon3(A, B, C);
hence thesis;
end;
theorem
Th14: A, B, C is_a_triangle & A1 = (1 - lambda) * B + lambda * C implies
A <> A1
proof
assume that A1: A, B, C is_a_triangle and A2: A1 = (1 - lambda) * B + lambda
* C;
A, B, C are_mutually_distinct by A1,EUCLID_6:20;
then A3: A <> B & A <> C & B <> C by ZFMISC_1:def 5;
hereby
assume A = A1;
then A in Line(B, C) by A2;
hence contradiction by A3,Th13,A1;
end;
end;
theorem
A, B, C is_a_triangle implies 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:
(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)
implies ((1 - mu) + lambda * mu) <> 0 & (ex alpha st (C2 = (1 - alpha) * A +
alpha * A1 & alpha = (1 - mu) / ((1 - mu) + lambda * mu)))
proof
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: mu <> 1 and A5: A, A1, C2
are_collinear and A6: B, B1, C2 are_collinear;
A7: A <> A1 by Th14,A1,A2;
A8: the_area_of_polygon3(A, B, C) <> 0 by A1,Th9;
C2, A, A1 are_collinear by A5;
then C2 in Line(A, A1) by A7,Th13;
then consider alpha such that A9: C2 = (1 - alpha) * A + alpha * A1;
0 = the_area_of_polygon3(B, B1, C2) by A6,Th9
.= ((1 - mu) - ((1 - mu) + lambda * mu) * alpha) *
the_area_of_polygon3(A, B, C) by Lm1,A9,A2,A3;
then A10: (1 - mu) - ((1 - mu) + lambda * mu) * alpha = 0 & 1 - mu <> 0 by A8
,A4;
then ((1 - mu) + lambda * mu) <> 0;
hence thesis by A9,A10,XCMPLX_1:89;
end;
Lm3:
(A, B, C is_a_triangle & A1 = (1 - lambda) * B + lambda * C &
B1 = (1 - mu) * C + mu * A & ((1 - mu) + lambda * mu) <> 0) implies
(ex C2 st A, A1, C2 are_collinear & B, B1, C2 are_collinear)
proof
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: ((1 - mu) + lambda * mu) <> 0;
A5: A <> A1 by Th14,A1,A2;
consider alpha such that A6: alpha = (1 - mu) / ((1 - mu) + lambda * mu);
consider C2 such that A7: C2 = (1 - alpha) * A + alpha * A1;
take C2;
C2 in Line(A, A1) by A7;
then C2, A, A1 are_collinear by A5,Th13;
hence A, A1, C2 are_collinear;
the_area_of_polygon3(B, B1, C2)
= ((1 - mu) - ((1 - mu) / ((1 - mu) + lambda * mu)) * (1 - mu + lambda *
mu)) * the_area_of_polygon3(A, B, C) by A6,Lm1,A2,A3,A7
.= ((1 - mu) - (1 - mu)) * the_area_of_polygon3(A, B, C) by A4,XCMPLX_1:87;
hence B, B1, C2 are_collinear by Th9;
end;
Lm4:
(lambda <> 1 & mu <> 1 & nu <> 1) implies (
0 = lambda * mu * nu - (1 - lambda) * (1 - mu) * (1 - nu) iff
(lambda / (1 - lambda)) * (mu / (1 - mu)) * (nu / (1 - nu)) = 1)
proof
set q = ((1 - lambda) * (1 - mu) * (1 - nu));
assume lambda <> 1 & mu <> 1 & nu <> 1;
then A1: (1 - lambda) <> 0 & (1 - mu) <> 0 & (1 - nu) <> 0;
0 = lambda * mu * nu - q iff 0 = q * 1 + (- mu * nu * lambda);
then 0 = lambda * mu * nu - q iff q * (1 + (- lambda * mu * nu) / q) = 0
by A1,XCMPLX_1:235;
then 0 = lambda * mu * nu - q iff 1 + (- (lambda * mu * nu)) / q = 0 by A1;
then 0 = lambda * mu * nu - q iff 1 + (- ((lambda * mu * nu) / q)) = 0
by XCMPLX_1:187;
then 0 = lambda * mu * nu - q iff 1 = (lambda * (mu * nu)) /
((1 - lambda) * ((1 - mu) * (1 - nu)));
then 0 = lambda * mu * nu - q iff 1 = ((lambda / (1 - lambda)) * (mu * nu))
/ ((1 - mu) * (1 - nu)) by XCMPLX_1:83;
then 0 = lambda * mu * nu - q iff 1 = (lambda / (1 - lambda)) * ((mu * nu)
/ ((1 - mu) * (1 - nu))) by XCMPLX_1:74;
then 0 = lambda * mu * nu - q iff 1 = (lambda / (1 - lambda)) * (((mu / (1
- mu)) * nu) / (1 - nu)) by XCMPLX_1:83;
then 0 = lambda * mu * nu - q iff 1 = (lambda / (1 - lambda)) * ((mu / (1 -
mu)) * (nu / (1 - nu))) by XCMPLX_1:74;
hence thesis;
end;
Lm5:
(mu <> 1 & 0 = lambda * mu * nu - (1 - lambda) * (1 - mu) * (1 - nu))
implies (1 - mu + mu * lambda = 0 implies 1 - lambda + lambda * nu = 0)
proof
assume that A1: mu <> 1 and A2
: 0 = lambda * mu * nu - (1 - lambda) * (1 - mu)
* (1 - nu) and A3: 1 - mu + mu * lambda = 0;
A4: 1 - mu <> 0 by A1;
0 = (- (1 - mu)) * nu - (1 - lambda) * (1 - mu) * (1 - nu) by A2,A3;
then 0 = (1 - mu) * (nu + (1 - lambda) * (1 - nu));
hence thesis by A4;
end;
theorem
Th16: (A, B, C is_a_triangle & A1 = (1 - lambda) * B + lambda * C &
B1 = (1 - mu) * C + mu * A & mu <> 1) implies ((1 - mu) + lambda * mu <> 0
iff not Line(A, A1) is_parallel_to Line(B, B1))
proof
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: mu <> 1;
A5: A <> A1 by A1,A2,Th14;
B, C, A is_a_triangle by A1;
then A6: B <> B1 by A3,Th14;
hereby
assume (1 - mu) + lambda * mu <> 0;
then consider C2 such that
A7: A, A1, C2 are_collinear & B, B1, C2 are_collinear by Lm3,A1,A2,A3;
C2, A, A1 are_collinear & C2, B, B1 are_collinear by A7;
then C2 in Line(A, A1) & C2 in Line(B, B1) by A5,A6,Th13;
hence not Line(A, A1) is_parallel_to Line(B, B1) by XBOOLE_0:3;
end;
assume not Line(A, A1) is_parallel_to Line(B, B1);
then consider C2 being object such that
A8: C2 in Line(A, A1) & C2 in Line(B, B1)
by XBOOLE_0:3;
reconsider C2 as Point of TOP-REAL 2 by A8;
C2, A, A1 are_collinear & C2, B, B1 are_collinear by A8,A5,A6,Th13;
then A, A1, C2 are_collinear & B, B1, C2 are_collinear;
hence thesis by Lm2,A1,A2,A3,A4;
end;
Lm6:
(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 & ((1 - lambda) + nu * lambda) <> 0 &
((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)))
proof
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 & ((1 - lambda) + nu * lambda) <> 0 & ((1 - nu)
+ mu * nu) <> 0);
A9: B, C, A is_a_triangle by A1;
A10: C, A, B is_a_triangle by A1;
hereby
assume (lambda / (1 - lambda)) * (mu / (1 - mu)) * (nu / (1 - nu)) = 1;
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 by A8;
suppose A14: 1 - mu + lambda * mu = 0;
then 1 - lambda + nu * lambda = 0 by Lm5,A6,A11;
hence thesis by Lm5,A5,A12,A14;
end;
suppose A15: 1 - lambda + nu * lambda = 0;
then 1 - nu + nu * mu = 0 by Lm5,A5,A12;
hence thesis by Lm5,A7,A13,A15;
end;
suppose A16: 1 - nu + mu * nu = 0;
then 1 - mu + lambda * mu = 0 by Lm5,A7,A13;
hence thesis by Lm5,A6,A11,A16;
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;
end;
assume Line(A, A1) is_parallel_to Line(B, B1) &
Line(B, B1) is_parallel_to Line(C, C1);
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 thesis by Lm4,A5,A6,A7;
end;
begin :: Ceva's Theorem and Others
::$N Pre-Routh's Theorem
theorem
Th17: (A1 = (1 - lambda) * B + lambda * C &
B1 = (1 - mu) * C + mu * A & C1 = (1 - nu) * A + nu * B) implies
the_area_of_polygon3(A1, B1, C1) = ((1 - lambda) * (1 - mu) * (1 - nu) +
lambda * mu * nu) * the_area_of_polygon3(A, B, C)
proof
assume that A1: A1 = (1 - lambda) * B + lambda * C
and A2: B1 = (1 - mu) * C + mu * A and A3: C1 = (1 - nu) * A + nu * B;
the_area_of_polygon3(A1, B1, C1) =
(1 - lambda) * the_area_of_polygon3(B, B1, C1) +
lambda * the_area_of_polygon3(C, B1, C1) by Th7,A1
.= - (1 - lambda) * the_area_of_polygon3((1 - mu) * C + mu * A, B, C1) -
lambda * the_area_of_polygon3((1 - mu) * C + mu * A, C, C1) by A2
.= - (1 - lambda) * ((1 - mu) * the_area_of_polygon3(C, B, C1) +
mu * the_area_of_polygon3(A, B, C1)) -
lambda * the_area_of_polygon3((1 - mu) * C + mu * A, C, C1) by Th7
.= - (1 - lambda) * ((1 - mu) * the_area_of_polygon3(C, B, C1) +
mu * the_area_of_polygon3(A, B, C1)) -
lambda * ((1 - mu) * the_area_of_polygon3(C, C, C1) +
mu * the_area_of_polygon3(A, C, C1)) by Th7
.= (1 - lambda) * (1 - mu) * the_area_of_polygon3((1 - nu) * A + nu * B, B,
C) + (1 - lambda) * mu * the_area_of_polygon3((1 - nu) * A +
nu * B, B, A) + lambda * mu * the_area_of_polygon3((1 - nu) * A +
nu * B, C, A) by A3
.= (1 - lambda) * (1 - mu) * ((1 - nu) * the_area_of_polygon3(A, B, C) +
nu * the_area_of_polygon3(B, B, C))
+ (1 - lambda) * mu * the_area_of_polygon3((1 - nu) * A +
nu * B, B, A) + lambda * mu * the_area_of_polygon3((1 - nu) * A +
nu * B, C, A) by Th7
.= (1 - lambda) * (1 - mu) * (1 - nu) * the_area_of_polygon3(A, B, C)
+ (1 - lambda) * mu * ((1 - nu) * the_area_of_polygon3(A, B, A)
+ nu * the_area_of_polygon3(B, B, A)) +
lambda * mu * the_area_of_polygon3((1 - nu) * A + nu * B, C, A) by Th7
.= (1 - lambda) * (1 - mu) * (1 - nu) * the_area_of_polygon3(A, B, C) +
lambda * mu * ((1 - nu) * the_area_of_polygon3(A, C, A) +
nu * the_area_of_polygon3(B, C, A)) by Th7;
hence thesis;
end;
::$N Menelaus' Theorem
::$L https://en.wikipedia.org/wiki/Menelaus's_theorem Menelaus' Theorem
theorem
(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)
proof
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;
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
(q + lambda * mu * nu) * the_area_of_polygon3(A, B, C) = 0
by Th17,A2,A3,A4;
then A1, B1, C1 are_collinear iff 1 * q + (lambda * mu * nu) = 0 by A6;
then A1, B1, C1 are_collinear iff q * (1 + (lambda * mu * nu) / q) = 0
by A7,XCMPLX_1:235;
then A1, B1, C1 are_collinear iff 1 + (lambda * mu * nu) / q = 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 thesis;
end;
::$N Routh's Theorem
::$L https://en.wikipedia.org/wiki/Routh's_theorem Routh's Theorem
theorem
Th19: (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)
implies (((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
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: A, A1, B2, C2 are_collinear and
A9: B, B1, A2, C2 are_collinear and
A10: C, C1, A2, B2 are_collinear;
A11: A, A1, C2 are_collinear by A8;
A12: B, B1, C2 are_collinear by A9;
A13: B, B1, A2 are_collinear by A9;
A14: C, C1, A2 are_collinear by A10;
A15: A, A1, B2 are_collinear by A8;
A16: C, C1, B2 are_collinear by A10;
A17: C, A, B is_a_triangle by A1;
A18: B, C, A is_a_triangle by A1;
set q1 = ((1 - mu) + lambda * mu);
set q2 = ((1 - lambda) + nu * lambda);
set q3 = ((1 - nu) + mu * nu);
consider alpha such that A19: C2 = (1 - alpha) * A + alpha * A1 and
A20: alpha = (1 - mu) / q1 by Lm2,A1,A2,A3,A6,A11,A12;
A21: q1 <> 0 by Lm2,A1,A2,A3,A6,A11,A12;
consider beta such that A22: B2 = (1 - beta) * C + beta * C1 and
A23: beta = (1 - lambda) / q2 by Lm2,A17,A4,A2,A5,A16,A15;
A24: q2 <> 0 by Lm2,A17,A4,A2,A5,A16,A15;
consider gamma such that A25: A2 = (1 - gamma) * B + gamma * B1 and
A26: gamma = (1 - nu) / q3 by Lm2,A18,A3,A4,A7,A13,A14;
A27: q3 <> 0 by Lm2,A18,A3,A4,A7,A13,A14;
1 - alpha = (1 * q1 - (1 - mu)) /q1 by A20,A21,XCMPLX_1:127;
then A28: 1 - alpha = lambda * mu * (1 / q1) by XCMPLX_1:99;
1 - beta = (1 * q2 - (1 - lambda)) /q2 by A23,A24,XCMPLX_1:127;
then A29: 1 - beta = nu * lambda * (1 / q2) by XCMPLX_1:99;
1 - gamma = (1 * q3 - (1 - nu)) /q3 by A26,A27,XCMPLX_1:127;
then A30: 1 - gamma = mu * nu * (1 / q3) by XCMPLX_1:99;
A31: alpha = (1 - mu) * (1 / q1) by A20,XCMPLX_1:99;
A32: beta = (1 - lambda) * (1 / q2) by A23,XCMPLX_1:99;
A33: gamma = (1 - nu) * (1 / q3) by A26,XCMPLX_1:99;
thus (q1 * q2 * q3) <> 0 by A21,A24,A27;
set S = the_area_of_polygon3(A, B, C);
the_area_of_polygon3(A2, B2, C2)
= (1 - gamma) * the_area_of_polygon3(B, B2, C2) +
gamma * the_area_of_polygon3((1 - mu) * C + mu * A, B2, C2) by A3,Th7,A25
.= (1 - gamma) * the_area_of_polygon3(B, B2, C2) + gamma * ((1 - mu) *
the_area_of_polygon3(C, B2, C2) + mu * the_area_of_polygon3(A, B2, C2))
by Th7
.= - (1 - gamma) * the_area_of_polygon3(C2, B2, B) - gamma * ((1 - mu) *
the_area_of_polygon3((1 - beta) * C + beta * C1, C, C2) + mu *
the_area_of_polygon3(C2, B2, A)) by A22
.= - (1 - gamma) * the_area_of_polygon3(C2, B2, B) - gamma * ((1 - mu) *
((1 - beta) * the_area_of_polygon3(C, C, C2) + beta *
the_area_of_polygon3(C1, C, C2)) + mu * the_area_of_polygon3(C2, B2, A))
by Th7
.= - (1 - gamma) * the_area_of_polygon3((1 - alpha) * A + alpha * A1, B2,
B) - gamma * (1 - mu) * beta * the_area_of_polygon3(C1, C, C2) - gamma *
mu * the_area_of_polygon3(C2, B2, A) by A19
.= - (1 - gamma) * ((1 - alpha) * the_area_of_polygon3(A, B2, B) + alpha *
the_area_of_polygon3((1 - lambda) * B + lambda * C, B2, B)) - gamma *
(1 - mu) * beta * the_area_of_polygon3(C1, C, C2) - gamma * mu *
the_area_of_polygon3(C2, B2, A) by A2,Th7
.= - (1 - gamma) * ((1 - alpha) * the_area_of_polygon3(A, B2, B) + alpha *
((1 - lambda) * the_area_of_polygon3(B, B2, B) + lambda *
the_area_of_polygon3(C, B2, B))) - gamma * (1 - mu) * beta *
the_area_of_polygon3(C1, C, C2) - gamma * mu *
the_area_of_polygon3(C2, B2, A) by Th7
.= - (1 - gamma) * ((1 - alpha) * the_area_of_polygon3(A, B2, B) - alpha *
lambda * the_area_of_polygon3((1 - beta) * C + beta * C1, C, B)) - gamma *
(1 - mu) * beta * the_area_of_polygon3(C1, C, C2) - gamma * mu *
the_area_of_polygon3(C2, B2, A) by A22
.= - (1 - gamma) * ((1 - alpha) * the_area_of_polygon3(A, B2, B) -
alpha * lambda * ((1 - beta) * the_area_of_polygon3(C, C, B) +
beta * the_area_of_polygon3(C1, C, B)))
- gamma * (1 - mu) * beta * the_area_of_polygon3(C1, C, C2)
- gamma * mu * the_area_of_polygon3(C2, B2, A) by Th7
.= - (1 - gamma) * ((1 - alpha) * the_area_of_polygon3(A, B2, B) -
alpha * lambda * beta * the_area_of_polygon3((1 - nu) * A + nu * B, C, B))
- gamma * (1 - mu) * beta * the_area_of_polygon3(C1, C, C2)
- gamma * mu * the_area_of_polygon3(C2, B2, A) by A4
.= - (1 - gamma) * ((1 - alpha) * the_area_of_polygon3(A, B2, B) -
alpha * lambda * beta * ((1 - nu) * the_area_of_polygon3(A, C, B) +
nu * the_area_of_polygon3(B, C, B)))
- gamma * (1 - mu) * beta * the_area_of_polygon3(C1, C, C2)
- gamma * mu * the_area_of_polygon3(C2, B2, A) by Th7
.= (1 - gamma) * ((1 - alpha) * the_area_of_polygon3((1 - beta) * C +
beta * C1, A, B) - alpha * lambda * beta * (1 - nu) * S)
- gamma * (1 - mu) * beta * the_area_of_polygon3(C1, C, C2)
- gamma * mu * the_area_of_polygon3(C2, B2, A) by A22
.= (1 - gamma) * ((1 - alpha) * ((1 - beta) * the_area_of_polygon3(C, A, B)
+ beta * the_area_of_polygon3(C1, A, B)) - alpha * lambda * beta * (1 - nu)
* S) - gamma * (1 - mu) * beta * the_area_of_polygon3(C1, C, C2) - gamma *
mu * the_area_of_polygon3(C2, B2, A) by Th7
.= (1 - gamma) * ((1 - alpha) * ((1 - beta) * S
+ beta * ((1 - nu) * the_area_of_polygon3(A, A, B) +
nu * the_area_of_polygon3(B, A, B))) -
alpha * lambda * beta * (1 - nu) * S)
- gamma * (1 - mu) * beta * the_area_of_polygon3(C1, C, C2)
- gamma * mu * the_area_of_polygon3(C2, B2, A) by Th7,A4
.= ((1 - gamma) * (1 - alpha) * (1 - beta) * S -
(1 - gamma) * alpha * lambda * beta * (1 - nu) * S)
- gamma * (1 - mu) * beta * ((1 - nu) * the_area_of_polygon3(A, C, C2) +
nu * the_area_of_polygon3(B, C, C2))
- gamma * mu * the_area_of_polygon3(C2, B2, A) by Th7,A4
.= ((1 - gamma) * (1 - alpha) * (1 - beta) * S -
(1 - gamma) * alpha * lambda * beta * (1 - nu) * S)
- gamma * (1 - mu) * beta * ((1 - nu) * the_area_of_polygon3((1 - alpha) *
A + alpha * A1, A, C) + nu * the_area_of_polygon3(C2, B, C))
- gamma * mu * the_area_of_polygon3(C2, B2, A) by A19
.= ((1 - gamma) * (1 - alpha) * (1 - beta) * S -
(1 - gamma) * alpha * lambda * beta * (1 - nu) * S)
- gamma * (1 - mu) * beta * ((1 - nu) * ((1 - alpha) *
the_area_of_polygon3(A, A, C) + alpha * the_area_of_polygon3(A1, A, C)) +
nu * the_area_of_polygon3(C2, B, C))
- gamma * mu * the_area_of_polygon3(C2, B2, A) by Th7
.= ((1 - gamma) * (1 - alpha) * (1 - beta) * S -
(1 - gamma) * alpha * lambda * beta * (1 - nu) * S)
- gamma * (1 - mu) * beta * ((1 - nu) * alpha *
the_area_of_polygon3((1 - lambda) * B + lambda * C, A, C) +
nu * the_area_of_polygon3(C2, B, C))
- gamma * mu * the_area_of_polygon3(C2, B2, A) by A2
.= ((1 - gamma) * (1 - alpha) * (1 - beta) * S -
(1 - gamma) * alpha * lambda * beta * (1 - nu) * S)
- gamma * (1 - mu) * beta * ((1 - nu) * alpha * (
(1 - lambda) * the_area_of_polygon3(B, A, C) +
lambda * the_area_of_polygon3(C, A, C)) +
nu * the_area_of_polygon3(C2, B, C))
- gamma * mu * the_area_of_polygon3(C2, B2, A) by Th7
.= ((1 - gamma) * (1 - alpha) * (1 - beta) * S -
(1 - gamma) * alpha * lambda * beta * (1 - nu) * S)
- gamma * (1 - mu) * beta * (- (1 - nu) * alpha * (1 - lambda) * S +
nu * ((1 - alpha) * S +
alpha * the_area_of_polygon3((1 - lambda) * B + lambda * C, B, C)))
- gamma * mu * the_area_of_polygon3(C2, B2, A) by A2,Th7,A19
.= ((1 - gamma) * (1 - alpha) * (1 - beta) * S -
(1 - gamma) * alpha * lambda * beta * (1 - nu) * S)
- gamma * (1 - mu) * beta * (- (1 - nu) * alpha * (1 - lambda) * S +
nu * ((1 - alpha) * S +
alpha * ((1 - lambda) * the_area_of_polygon3(B, B, C) +
lambda * the_area_of_polygon3(C, B, C))))
- gamma * mu * the_area_of_polygon3(C2, B2, A) by Th7
.= ((1 - gamma) * (1 - alpha) * (1 - beta) * S -
(1 - gamma) * alpha * lambda * beta * (1 - nu) * S)
+ (gamma * (1 - mu) * beta * (1 - nu) * alpha * (1 - lambda) * S -
gamma * (1 - mu) * beta * nu * (1 - alpha) * S) - gamma * mu * (
(1 - alpha) * the_area_of_polygon3(A, B2, A) +
alpha * the_area_of_polygon3(A1, B2, A)) by Th7,A19
.= ((1 - gamma) * (1 - alpha) * (1 - beta) * S -
(1 - gamma) * alpha * lambda * beta * (1 - nu) * S)
+ (gamma * (1 - mu) * beta * (1 - nu) * alpha * (1 - lambda) * S -
gamma * (1 - mu) * beta * nu * (1 - alpha) * S) - gamma * mu * alpha *
the_area_of_polygon3((1 - lambda) * B + lambda * C, B2, A) by A2
.= ((1 - gamma) * (1 - alpha) * (1 - beta) * S -
(1 - gamma) * alpha * lambda * beta * (1 - nu) * S)
+ (gamma * (1 - mu) * beta * (1 - nu) * alpha * (1 - lambda) * S -
gamma * (1 - mu) * beta * nu * (1 - alpha) * S) - gamma * mu * alpha * (
(1 - lambda) * the_area_of_polygon3(B, B2, A) + lambda *
the_area_of_polygon3(C, B2, A)) by Th7
.= ((1 - gamma) * (1 - alpha) * (1 - beta) * S -
(1 - gamma) * alpha * lambda * beta * (1 - nu) * S)
+ (gamma * (1 - mu) * beta * (1 - nu) * alpha * (1 - lambda) * S -
gamma * (1 - mu) * beta * nu * (1 - alpha) * S) - gamma * mu * alpha * (
(1 - lambda) * the_area_of_polygon3((1 - beta) * C + beta * C1, A, B)
+ lambda * the_area_of_polygon3(B2, A, C)) by A22
.= ((1 - gamma) * (1 - alpha) * (1 - beta) * S -
(1 - gamma) * alpha * lambda * beta * (1 - nu) * S)
+ (gamma * (1 - mu) * beta * (1 - nu) * alpha * (1 - lambda) * S -
gamma * (1 - mu) * beta * nu * (1 - alpha) * S) - gamma * mu * alpha * (
(1 - lambda) * ((1 - beta) * the_area_of_polygon3(C, A, B) +
beta * the_area_of_polygon3(C1, A, B))
+ lambda * the_area_of_polygon3(B2, A, C)) by Th7
.= ((1 - gamma) * (1 - alpha) * (1 - beta) * S -
(1 - gamma) * alpha * lambda * beta * (1 - nu) * S)
+ (gamma * (1 - mu) * beta * (1 - nu) * alpha * (1 - lambda) * S -
gamma * (1 - mu) * beta * nu * (1 - alpha) * S) - gamma * mu * alpha * (
(1 - lambda) * ((1 - beta) * S + beta * ((1 - nu) *
the_area_of_polygon3(A, A, B) + nu * the_area_of_polygon3(B, A, B))) +
lambda * the_area_of_polygon3(B2, A, C)) by Th7,A4
.= ((1 - gamma) * (1 - alpha) * (1 - beta) * S - (1 - gamma) * alpha *
lambda * beta * (1 - nu) * S) + (gamma * (1 - mu) * beta * (1 - nu) * alpha
* (1 - lambda) * S - gamma * (1 - mu) * beta * nu * (1 - alpha) * S) -
gamma * mu * alpha * ((1 - lambda) * (1 - beta) * S + lambda * (
(1 - beta) * the_area_of_polygon3(C, A, C) + beta *
the_area_of_polygon3(C1, A, C))) by Th7,A22
.= ((1 - gamma) * (1 - alpha) * (1 - beta) * S - (1 - gamma) * alpha *
lambda * beta * (1 - nu) * S) + (gamma * (1 - mu) * beta * (1 - nu) * alpha
* (1 - lambda) * S - gamma * (1 - mu) * beta * nu * (1 - alpha) * S) -
gamma * mu * alpha * ((1 - lambda) * (1 - beta) * S + lambda * beta * (
the_area_of_polygon3((1 - nu) * A + nu * B, A, C))) by A4
.= ((1 - gamma) * (1 - alpha) * (1 - beta) * S - (1 - gamma) * alpha *
lambda * beta * (1 - nu) * S) + (gamma * (1 - mu) * beta * (1 - nu) * alpha
* (1 - lambda) * S - gamma * (1 - mu) * beta * nu * (1 - alpha) * S) -
gamma * mu * alpha * ((1 - lambda) * (1 - beta) * S + lambda * beta * ((1 -
nu) * the_area_of_polygon3(A, A, C) + nu * the_area_of_polygon3(B, A, C)))
by Th7
.= (((1 - gamma) * (1 - alpha) * (1 - beta) - (1 - gamma) * alpha * lambda
* beta * (1 - nu)) + (gamma * (1 - mu) * beta * (1 - nu) * alpha * (1 -
lambda) - gamma * (1 - mu) * beta * nu * (1 - alpha)) + (gamma * mu * alpha
* lambda * beta * nu - gamma * mu * alpha * (1 - lambda) * (1 - beta))) *
S
.= (((mu * nu * (1 / q3)) * (lambda * mu * (1 / q1)) * (nu * lambda * (1 /
q2)) - (mu * nu * (1 / q3)) * ((1 - mu) * (1 / q1)) * lambda * ((1 - lambda
) * (1 / q2)) * (1 - nu)) + (((1 - nu) * (1 / q3)) * (1 - mu) * ((1 -
lambda) * (1 / q2)) * (1 - nu) * ((1 - mu) * (1 / q1)) * (1 - lambda) - ((1
- nu) * (1 / q3)) * (1 - mu) * ((1 - lambda) * (1 / q2)) * nu * (lambda *
mu * (1 / q1))) + (((1 - nu) * (1 / q3)) * mu * ((1 - mu) * (1 / q1)) *
lambda * ((1 - lambda) * (1 / q2)) * nu - ((1 - nu) * (1 / q3)) * mu * ((1
- mu) * (1 / q1)) * (1 - lambda) * (nu * lambda * (1 / q2)))) * S
by A28,A31,A29,A32,A30,A33
.= (mu * nu * lambda - (1 - mu) * (1 - nu) * (1 - lambda)) ^2 *
((1 / q1) * (1 / q2) * (1 / q3)) * S
.= (mu * nu * lambda - (1 - mu) * (1 - nu) * (1 - lambda)) ^2 *
((1 / (q1 * q2)) * (1 / q3)) * S by XCMPLX_1:102
.= (mu * nu * lambda - (1 - mu) * (1 - nu) * (1 - lambda)) ^2 *
(1 / (q1 * q2 * q3)) * S by XCMPLX_1:102;
hence thesis by XCMPLX_1:99;
end;
::$N Feynman's (one-seventh area) Triangle
::$L https://en.wikipedia.org/wiki/One-seventh_area_triangle One-seventh area triangle
theorem
(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)
implies the_area_of_polygon3(A2, B2, C2) = the_area_of_polygon3(A, B, C) / 7
proof
assume that A1: A, B, C is_a_triangle and
A2: A1 = (2 / 3) * B + (1 / 3) * C & B1 = (2 / 3) * C + (1 / 3) * A &
C1 = (2 / 3) * A + (1 / 3) * B and
A3: A, A1, B2, C2 are_collinear & B, B1, A2, C2 are_collinear &::
C, C1, A2, B2 are_collinear;
consider lambda, mu, nu such that
A4: lambda = (1 / 3) & mu = (1 / 3) & nu = (1 / 3);
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 - lambda = 2 / 3 & 1 - mu = 2 / 3 & 1 - nu = 2 / 3 by A2,A4;
then the_area_of_polygon3(A2, B2, C2) = ((1 / 3) * (1 / 3) * (1 / 3) -
(2 / 3) * (2 / 3) * (2 / 3)) ^2 / (((2 / 3) + (1 / 3) * (1 / 3)) * ((2 / 3)
+ (1 / 3) * (1 / 3)) * ((2 / 3) + (1 / 3) * (1 / 3))) *
the_area_of_polygon3(A, B, C) by Th19,A1,A3;
hence thesis;
end;
Lm7:
(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)
implies ((lambda / (1 - lambda)) * (mu / (1 - mu))
* (nu / (1 - nu)) = 1 iff A2, B2, C2 are_collinear)
proof
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: A, A1, B2, C2 are_collinear and
A9: B, B1, A2, C2 are_collinear and
A10: C, C1, A2, B2 are_collinear;
set q = ((1 - lambda) * (1 - mu) * (1 - nu));
A11: 0 = lambda * mu * nu - q iff (lambda / (1 - lambda)) * (mu / (1 - mu)) *
(nu / (1 - nu)) = 1 by Lm4,A5,A6,A7;
A12: (((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) by Th19,A1,A2,A3,A4,A5,A6,A7,A8,A9,A10;
the_area_of_polygon3(A, B, C) <> 0 by Th9,A1;
hence thesis by A12,Th9,A11;
end;
::$N Ceva's Theorem
::$L https://en.wikipedia.org/wiki/Ceva's_theorem Ceva's Theorem
theorem
Th21: (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 st A, A1, A2 are_collinear & B, B1, A2
are_collinear & C, C1, A2 are_collinear))
proof
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: q1 <> 0
and A9: q2 <> 0 and A10: q3 <> 0;
A11: C, A, B is_a_triangle by A1;
A12: B, C, A is_a_triangle by A1;
consider C2 such that A13: A, A1, C2 are_collinear and A14: B, B1, C2
are_collinear by Lm3,A1,A2,A3,A8;
consider B2 such that A15: C, C1, B2 are_collinear and A16: A, A1, B2
are_collinear by Lm3,A11,A4,A2,A9;
consider A2 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
assume
A25: (lambda / (1 - lambda)) * (mu / (1 - mu)) * (nu / (1 - nu)) = 1;
per cases;
suppose A26: B2 <> C2;
take A2;
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;
thus B, B1, A2 are_collinear & C, C1, A2 are_collinear by A17,A18;
end;
suppose A28: B2 = C2;
take B2;
thus A, A1, B2 are_collinear & B, B1, B2 are_collinear & C, C1, B2
are_collinear by A28,A14,A15,A16;
end;
end;
given C3 such that A29: A, A1, C3 are_collinear and A30: B, B1, C3
are_collinear and A31: C, C1, C3 are_collinear;
A32: C3, B2, C2 are_collinear
proof
per cases;
suppose A33: B2 <> C2;
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 thesis by A33,Th13,A34;
end;
suppose B2 = C2;
then not C3, B2, C2 are_mutually_distinct by ZFMISC_1:def 5;
hence thesis by EUCLID_6:20;
end;
end;
C3 = A2
proof
assume A35: C3 <> A2;
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;
end;
hence thesis by A32,Lm7,A1,A2,A3,A4,A5,A6,A7,A22,A23,A24;
end;
::$N Generalized Ceva's Theorem
theorem
(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 ((lambda / (1 - lambda)) * (mu / (1 - mu)) * (nu / (1 - nu)) = 1 iff
Line(A, A1), Line(B, B1), Line(C, C1) are_concurrent)
proof
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;
A8: A <> A1 by Th14,A1,A2;
A9: B, C, A is_a_triangle by A1;
then A10: B <> B1 by Th14,A3;
A11: C, A, B is_a_triangle by A1;
then A12: C <> C1 by Th14,A4;
hereby
assume A13:
(lambda / (1 - lambda)) * (mu / (1 - mu)) * (nu / (1 - nu)) = 1;
per cases;
suppose 1 - mu + lambda * mu <> 0 & 1 - lambda + nu * lambda <> 0 &
1 - nu + mu * nu <> 0;
then consider A2 such that A14: A, A1, A2 are_collinear & B, B1, A2
are_collinear & C, C1, A2 are_collinear by A13,Th21,A1,A2,A3,A4,A5,A6,A7;
A2, A, A1 are_collinear & A2, B, B1 are_collinear & A2, C, C1
are_collinear by A14;
then A2 in Line(A, A1) & A2 in Line(B, B1) & A2 in Line(C, C1) by Th13,A8
,A10,A12;
hence Line(A, A1), Line(B, B1), Line(C, C1) are_concurrent;
end;
suppose not (1 - mu + lambda * mu <> 0 & 1 - lambda + nu * lambda <> 0 &
1 - nu + mu * nu <> 0);
then 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 A13,Lm6,A1,A2,A3,A4,A5,A6,A7;
hence Line(A, A1), Line(B, B1), Line(C, C1) are_concurrent;
end;
end;
assume Line(A, A1), Line(B, B1), Line(C, C1) are_concurrent;
then per cases;
suppose A15: 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 1 - mu + lambda * mu = 0 & 1 - nu + mu * nu = 0 & 1 - lambda + nu *
lambda = 0 by Th16,A1,A9,A11,A2,A3,A4,A5,A6,A7;
hence thesis by Lm6,A15,A1,A2,A3,A4,A5,A6,A7;
end;
suppose ex C2 st (C2 in Line(A, A1) & C2 in Line(B, B1) &
C2 in Line(C, C1));
then consider C2 such that A16: C2 in Line(A, A1) & C2 in Line(B, B1) &
C2 in Line(C, C1);
not Line(A, A1) is_parallel_to Line(B, B1) & not Line(B, B1)
is_parallel_to Line(C, C1) & not Line(C, C1) is_parallel_to Line(A, A1)
by A16,XBOOLE_0:3;
then A17: 1 - mu + lambda * mu <> 0 & 1 - nu + mu * nu <> 0 & 1 - lambda +
nu * lambda <> 0 by Th16,A1,A2,A3,A4,A5,A6,A7,A9,A11;
C2, A, A1 are_collinear & C2, B, B1 are_collinear & C2, C, C1 are_collinear
by A16,Th13,A8,A10,A12;
then A, A1, C2 are_collinear & B, B1, C2 are_collinear & C, C1, C2
are_collinear;
hence thesis by A17,Th21,A1,A2,A3,A4,A5,A6,A7;
end;
end;