:: Morley's Trisector Theorem
:: by Roland Coghetto
::
:: Received March 26, 2015
:: Copyright (c) 2015-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 NUMBERS, COMPLEX1, RELAT_1, CARD_1, ARYTM_1, ARYTM_3, PRE_TOPC,
EUCLID, SIN_COS, COMPLEX2, EUCLID_6, XXREAL_0, REAL_1, SQUARE_1,
ZFMISC_1, EUCLID_3, XXREAL_1, INT_1, NAT_1, PROJPL_1, XBOOLE_0, RLTOPSP1,
EUCLID10;
notations ORDINAL1,
RLTOPSP1, XCMPLX_0, PRE_TOPC, XXREAL_0, RLVECT_1, SIN_COS, EUCLID,
EUCLID_3, EUCLID_6, SQUARE_1, COMPLEX2, XREAL_0, RCOMP_1, ZFMISC_1,
SUBSET_1, EUCLID10, NUMBERS, SEQ_4, INT_1, NAT_1;
constructors MONOID_0, SIN_COS, EUCLID_3, EUCLID_6, SQUARE_1, COMPLEX2,
EUCLID10, INTEGRA1, SEQ_4;
registrations XREAL_0, EUCLID, SIN_COS, XCMPLX_0, ORDINAL1, SQUARE_1,
XXREAL_0, MONOID_0, INT_1;
requirements NUMERALS, SUBSET, ARITHM, REAL;
equalities EUCLID10, SQUARE_1, XCMPLX_0;
expansions ZFMISC_1;
theorems XCMPLX_1, EUCLID_3, EUCLID_6, XREAL_1, MENELAUS, SQUARE_1, SIN_COS,
COMPLEX2, XXREAL_1, COMPTRIG, XXREAL_0, TARSKI, SIN_COS6, EUCLID10,
XBOOLE_0, BORSUK_7, INT_1, NAT_1;
begin :: Preliminaries
reserve A,B,C,D,E,F,G for Point of TOP-REAL 2;
theorem Th1:
angle(A,B,A) = 0
proof
0 = angle(euc2cpx(A),euc2cpx(B),euc2cpx(A)) by COMPLEX2:79
.= angle(A,B,A) by EUCLID_3:def 4;
hence thesis;
end;
theorem Th2:
0 <= angle(A,B,C) < 2*PI
proof
angle(A,B,C) = angle(euc2cpx(A),euc2cpx(B),euc2cpx(C)) by EUCLID_3:def 4;
hence thesis by COMPLEX2:70;
end;
Lm1:
[. 0 , 2*PI .[ = [. 0 , PI .[ \/ { PI } \/ ]. PI , 2*PI .[
proof
[. 0, 2*PI .[ = [. 0 , PI.] \/ ].PI,2*PI.[ by COMPTRIG:5,XXREAL_1:169
.= ([.0,PI.[\/{PI})\/].PI,2*PI.[ by COMPTRIG:5,XXREAL_1:129;
hence thesis;
end;
theorem
0 <= angle(A,B,C) < PI or angle(A,B,C) = PI or PI < angle(A,B,C) < 2*PI
proof
set alpha = angle(A,B,C);
0 <= alpha < 2*PI by Th2;
then alpha in [. 0 , PI .[ \/ { PI } \/ ]. PI , 2*PI .[
by Lm1,XXREAL_1:3;
then alpha in [.0 , PI.[ \/ {PI} or alpha in ].PI,2*PI.[
by XBOOLE_0:def 3;
then alpha in [.0 , PI.[ or alpha in {PI} or alpha in ].PI,2*PI.[
by XBOOLE_0:def 3;
hence thesis by XXREAL_1:3,TARSKI:def 1,XXREAL_1:4;
end;
theorem Th3:
|.F-E.|^2 = |.A-E.|^2 + |.A-F.|^2 - 2 * |.A-E.| * |.A-F.| * cos angle(E,A,F)
proof
|.F-E.|^2 = |.E-A.|^2 + |.F-A.|^2 - 2*|.E-A.|*|.F-A.|*cos angle (E,A,F)
by EUCLID_6:7
.= |.A-E.|^2 + |.F-A.|^2 - 2*|.E-A.|*|.F-A.|*cos angle (E,A,F)
by EUCLID_6:43
.= |.A-E.|^2 + |.A-F.|^2 - 2*|.E-A.|*|.F-A.|*cos angle (E,A,F)
by EUCLID_6:43
.= |.A-E.|^2 + |.A-F.|^2 - 2*|.A-E.|*|.F-A.|*cos angle (E,A,F)
by EUCLID_6:43
.= |.A-E.|^2 + |.A-F.|^2 - 2*|.A-E.|*|.A-F.|*cos angle (E,A,F)
by EUCLID_6:43;
hence thesis;
end;
Lm2:
for i being Integer st i > 0 holds ex k being Nat st i = k
proof
let i be Integer;
assume
A1: i > 0;
i in INT by INT_1:def 2;
then consider k be Nat such that
A2: i = k or i = -k by INT_1:def 1;
0 <= k by NAT_1:2;
hence thesis by A1,A2;
end;
Lm3:
for i being Integer st i < 0 holds ex k being Nat st i = - k
proof
let i be Integer; assume
A1: i < 0;
i in INT by INT_1:def 2;
then consider k be Nat such that
A2: i = k or i = -k by INT_1:def 1;
thus thesis by A1,A2,NAT_1:2;
end;
Lm4:
for i being Integer st 3 * i <= 1 & 0 < 1 + 3 * i holds i = 0
proof
let i be Integer;
assume that
A1: 3 * i <=1 and
A2: 0 < 1 + 3 * i;
assume
A3: not i = 0;
then per cases;
suppose i < 0;
then consider k be Nat such that
A4: i = - k by Lm3;
0 + (3 * k) < 1 - 3 * k + (3 * k) by A2,A4,XREAL_1:8; then
A5: 3 * k / 3 < 1 / 3 by XREAL_1:74;
k <> 0 by A3,A4;
then consider j be Nat such that
A6: k = j + 1 by NAT_1:6;
j + 1 - 1 < 1/3 - 1 by A6,A5,XREAL_1:8;
then j + 0 < -2/3;
hence contradiction by NAT_1:2;
end;
suppose
A7: i > 0;
then consider k be Nat such that
A8: i = k by Lm2;
consider j be Nat such that
A9: k = j + 1 by A7,A8,NAT_1:6;
(k * 3) / 3 <= 1 / 3 by A1,A8,XREAL_1:72;
then j + 1 - 1 <= 1/3 - 1 by A9,XREAL_1:9;
then j + 0 <= -2/3;
hence contradiction by NAT_1:2;
end;
end;
theorem Th4:
A,B,C are_mutually_distinct & 0 < angle(A,B,C) < PI implies
0 < angle(B,C,A) < PI & 0 < angle(C,A,B) < PI
proof
assume that
A1: A,B,C are_mutually_distinct and
A2: 0 < angle(A,B,C) < PI;
set z1 = euc2cpx(A);
set z2 = euc2cpx(B);
set z3 = euc2cpx(C);
z1 <> z2 & z2 <> z3 & z1 <> z3 & 0 < angle(z1,z2,z3) < PI
by A1,A2,EUCLID_3:4,EUCLID_3:def 4; then
A3: 0 < angle(z2,z3,z1) & 0 < angle(z3,z1,z2) by COMPLEX2:84; then
A4: 0 < angle(B,C,A) & 0 < angle(C,A,B) by EUCLID_3:def 4;
A5: angle(A,B,C) + angle(B,C,A) + angle(C,A,B) = PI by A1,A2,EUCLID_3:47;
now
assume PI <= angle(B,C,A) or PI <= angle(C,A,B);
then per cases;
suppose PI <= angle(B,C,A);
then angle(A,B,C) + PI <= angle(A,B,C) + angle(B,C,A) by XREAL_1:6;
then
A6: angle(A,B,C) + PI + angle(C,A,B) <= PI by A5,XREAL_1:6;
0 + PI < angle(A,B,C) + PI by A2,XREAL_1:6;
hence contradiction by A4,XREAL_1:8,A6;
end;
suppose PI <= angle(C,A,B);
then angle(A,B,C) + PI <= angle(A,B,C) + angle(C,A,B) by XREAL_1:6;
then
A7: angle(A,B,C) + PI + angle(B,C,A) <=
angle(A,B,C) + angle(C,A,B) +angle(B,C,A) by XREAL_1:6;
0 + PI < angle(A,B,C) + PI by A2,XREAL_1:6;
hence contradiction by A7,A5,A4,XREAL_1:8;
end;
end;
hence thesis by A3,EUCLID_3:def 4;
end;
theorem
A,B,C are_mutually_distinct & angle(A,B,C) = 0 implies (angle(B,C,A) =0 &
angle(C,A,B) = PI) or (angle(B,C,A) = PI & angle(C,A,B) = 0) & angle(A,B,C)
+ angle(B,C,A) + angle(C,A,B) = PI
proof
assume that
A1: A,B,C are_mutually_distinct and
A2: angle(A,B,C) = 0;
set z1 = euc2cpx(A);
set z2 = euc2cpx(B);
set z3 = euc2cpx(C);
z1 <> z2 & z2 <> z3 & z1 <> z3 & angle(z1,z2,z3) = 0
by A1,A2,EUCLID_3:4,EUCLID_3:def 4;
then per cases by COMPLEX2:87;
suppose angle(z2,z3,z1) = 0 & angle(z3,z1,z2) = PI;
hence thesis by EUCLID_3:def 4;
end;
suppose angle(z2,z3,z1) = PI & angle(z3,z1,z2) = 0;
then angle(B,C,A) = PI & angle(C,A,B) = 0 by EUCLID_3:def 4;
hence thesis by A2;
end;
end;
theorem
A,B,C are_mutually_distinct & angle(A,B,C) = PI implies angle(B,C,A) = 0 &
angle(C,A,B) = 0 & angle(A,B,C) + angle(B,C,A) + angle(C,A,B) = PI
proof
assume that
A1: A,B,C are_mutually_distinct and
A2: angle(A,B,C) = PI;
set z1 = euc2cpx(A);
set z2 = euc2cpx(B);
set z3 = euc2cpx(C);
z1 <> z2 & z2 <> z3 & z1 <> z3 & angle(z1,z2,z3) = PI
by A1,A2,EUCLID_3:4,EUCLID_3:def 4;
then angle(z2,z3,z1) = 0 & angle(z3,z1,z2) = 0 by COMPLEX2:86;
hence angle(B,C,A) = 0 & angle(C,A,B) = 0 by EUCLID_3:def 4;
hence thesis by A2;
end;
theorem
A,B,C are_mutually_distinct & angle (A,B,C) > PI implies
angle (B,C,A) > PI & angle (C,A,B) > PI
proof
assume
A1: A,B,C are_mutually_distinct & angle (A,B,C) > PI;
set z1 = euc2cpx(A);
set z2 = euc2cpx(B);
set z3 = euc2cpx(C);
z1 <> z2 & z2 <> z3 & z1 <> z3 & angle (z1,z2,z3) > PI
by A1,EUCLID_3:4,EUCLID_3:def 4;
then angle (z2,z3,z1) > PI & angle (z3,z1,z2) > PI by COMPLEX2:85;
hence thesis by EUCLID_3:def 4;
end;
theorem
A,B,C are_mutually_distinct & angle(A,B,C) > PI implies
angle(A,B,C) + angle(B,C,A) + angle(C,A,B) = 5*PI
proof
assume that
A1: A,B,C are_mutually_distinct and
A2: angle(A,B,C) > PI;
angle(A,B,C) <> 0 & angle(B,C,A) <> 0 & angle(C,A,B) <> 0
by A1,A2,COMPTRIG:5,EUCLID_6:24;
then
A3: angle(A,B,C) = 2*PI - angle(C,B,A) & angle(B,C,A) = 2*PI - angle(A,C,B) &
angle(C,A,B) = 2*PI - angle(B,A,C) by EUCLID_3:38;
2*PI - angle(A,B,C) < 2*PI - PI by A2,XREAL_1:15;
then angle(C,B,A) + angle(B,A,C) + angle(A,C,B) = PI
by A1,A3,EUCLID_3:47;
hence thesis by A3;
end;
Lm5:
for a be Real holds sin (4*PI/3 - a) = - sin (PI/3 - a)
proof
let a be Real;
sin (4*PI/3 - a) = sin (PI+(PI/3 -a))
.= - sin (PI/3 - a) by SIN_COS:79;
hence thesis;
end;
theorem Th5:
angle(C,B,A) < PI implies 0 <= the_area_of_polygon3(A,B,C)
proof
assume angle(C,B,A) < PI;
then 2*PI*0 <= angle(C,B,A) < PI+2*PI*0 by Th2;
then
A1: sin angle(C,B,A) >=0 by SIN_COS6:16;
the_area_of_polygon3(A,B,C) = |.A-B.| * |.C-B.| * sin angle(C,B,A) /2
by EUCLID_6:5;
hence thesis by A1;
end;
theorem Th6:
angle(C,B,A) < PI implies 0 <= the_diameter_of_the_circumcircle(A,B,C)
proof
assume angle(C,B,A) < PI;
then 0 <= the_area_of_polygon3(A,B,C) by Th5;
hence thesis;
end;
begin :: Morley's Theorem
theorem Th7:
A,F,C is_a_triangle & angle (C,F,A) < PI &
angle (A,C,F) = angle (A,C,B)/3 & angle (F,A,C) = angle (B,A,C)/3 &
angle (A,C,B)/3 + angle(B,A,C)/3 + angle(C,B,A)/3 = PI/3
implies
|.A-F.| * sin (PI/3 - angle(C,B,A)/3) = |.A-C.| * sin (angle (A,C,B)/3)
proof
assume that
A1: A,F,C is_a_triangle and
A2: angle (C,F,A) < PI and
A3: angle (A,C,F) = angle (A,C,B)/3 and
A4: angle (F,A,C) = angle (B,A,C)/3 and
A5: angle (A,C,B)/3 + angle(B,A,C)/3 + angle(C,B,A)/3 = PI/3;
A6: angle (F,C,A) = 2*PI - angle(A,C,B)/3 by A1,A3,EUCLID10:31;
A7: angle(A,C,F) = 2*PI - angle(F,C,A) &
angle(F,A,C) = 2*PI - angle(C,A,F) by A1,EUCLID10:31;
A8: A,F,C are_mutually_distinct by A1,EUCLID_6:20;
F,A,C is_a_triangle & angle(C,F,A)<PI by A1,A2,MENELAUS:15;
then angle(C,A,F) + angle(A,F,C) + angle(F,C,A) = 5 * PI by EUCLID10:54;
then angle(A,F,C)=4*PI/3 - angle(C,B,A)/3 by A7,A3,A5,A4;
then
A9: sin angle(A,F,C) = - sin (PI/3 - angle(C,B,A)/3) by Lm5;
|.A-F.| * sin angle(A,F,C) = |.A-C.| * sin (2*PI - angle (A,C,B)/3)
by A8,A6,EUCLID_6:6;
then |.A-F.| * - sin (PI/3 - angle(C,B,A)/3)
= |.A-C.| * (-sin (angle (A,C,B)/3)) by A9,EUCLID10:3;
hence thesis;
end;
theorem Th8:
A,B,C is_a_triangle & A,F,C is_a_triangle & angle (C,F,A) < PI &
angle (A,C,F) = angle (A,C,B)/3 & angle (F,A,C) = angle (B,A,C)/3 &
angle (A,C,B)/3 + angle(B,A,C)/3 + angle(C,B,A)/3 = PI/3 &
sin (PI/3 - angle(C,B,A)/3)<>0 implies
|.A-F.| = 4 * the_diameter_of_the_circumcircle(A,B,C)
* sin (angle(C,B,A) / 3) * sin (PI/3 + angle(C,B,A)/3)
* sin (angle(A,C,B) / 3)
proof
assume that
A1: A,B,C is_a_triangle and
A2: A,F,C is_a_triangle and
A3: angle (C,F,A) < PI and
A4: angle (A,C,F) = angle (A,C,B)/3 and
A5: angle (F,A,C) = angle (B,A,C)/3 and
A6: angle (A,C,B)/3 + angle(B,A,C)/3 + angle(C,B,A)/3 = PI/3 and
A7: sin (PI/3 - angle(C,B,A)/3)<>0;
A8: |.A-F.| * sin (PI/3 - angle(C,B,A)/3) = |.A-C.| * sin (angle (A,C,B)/3)
by A3,A4,A5,A2,A6,Th7
.= |.C-A.| * sin (angle(A,C,B)/3) by EUCLID_6:43
.= the_diameter_of_the_circumcircle(A,B,C) * sin angle(C,B,A)
* sin (angle(A,C,B)/3) by A1,EUCLID10:50;
sin angle(C,B,A) = sin (3* (angle(C,B,A)/3))
.= 4 * sin (angle(C,B,A)/3) * sin (PI/3 + angle(C,B,A)/3)
* sin (PI/3 - angle(C,B,A)/3) by EUCLID10:29;
then |.A-F.| =
((the_diameter_of_the_circumcircle(A,B,C) * 4 * sin (angle(C,B,A)/3) *
sin (PI/3 + angle(C,B,A)/3) * sin (angle(A,C,B) /3)) *
sin (PI/3 - angle(C,B,A)/3)) / sin (PI/3 - angle(C,B,A)/3)
by A7,A8,XCMPLX_1:89;
then
A9: |.A-F.| =
(the_diameter_of_the_circumcircle(A,B,C) * 4 * sin (angle(C,B,A)/3) *
sin (PI/3 + angle(C,B,A)/3) * sin (angle(A,C,B) /3)) *
(sin (PI/3 - angle(C,B,A)/3) / sin (PI/3 - angle(C,B,A)/3));
sin (PI/3 - angle(C,B,A)/3) / sin (PI/3 - angle(C,B,A)/3) = 1
by A7,XCMPLX_1:60;
hence thesis by A9;
end;
theorem Th9:
C,A,B is_a_triangle & A,F,C is_a_triangle &
F,A,E is_a_triangle & E,A,B is_a_triangle &
angle(B,A,E) = angle(B,A,C) / 3 & angle(F,A,C) = angle(B,A,C) / 3
implies angle(E,A,F) = angle(B,A,C) / 3
proof
assume that
A1: C,A,B is_a_triangle and
A2: A,F,C is_a_triangle and
A3: F,A,E is_a_triangle and
A4: E,A,B is_a_triangle and
A5: angle (B,A,E) = angle (B,A,C) / 3 and
A6: angle (F,A,C) = angle (B,A,C) / 3;
A7: angle(C,A,B)=2*PI-angle(B,A,C) by A1,EUCLID10:31;
A8: angle(C,A,F) + angle(F,A,E) = angle(C,A,E) or
angle(C,A,F) + angle(F,A,E) = angle(C,A,E)+2*PI by EUCLID_6:4;
A9: angle(C,A,E)+angle(E,A,B)=angle(C,A,B) or
angle(C,A,E)+angle(E,A,B)=angle(C,A,B)+2*PI by EUCLID_6:4;
A10: angle(C,A,F) = 2*PI-angle(B,A,C)/3 by A2,A6,EUCLID10:31;
A11: angle(F,A,E)=2*PI-angle(E,A,F) by A3,EUCLID10:31;
A12: angle(E,A,B) = 2*PI - angle(B,A,C)/3 by A5,A4,EUCLID10:31;
A13: not angle(E,A,F) = 4*PI + angle(B,A,C)/3
proof
assume
A14: angle(E,A,F) = 4*PI + angle(B,A,C)/3;
now
0+ 2*PI < 2*PI + 2*PI by COMPTRIG:5,XREAL_1:8;
hence 2*PI < 4*PI;
0 <= angle(B,A,C) & angle(B,A,C) <> 0 by Th2,A1,EUCLID10:30;
hence 0 < angle(B,A,C)/3;
end;
then 2*PI + 0 < 4*PI + angle(B,A,C)/3 by XREAL_1:8;
hence contradiction by A14,Th2;
end;
not angle(E,A,F) = 2*PI + angle(B,A,C)/3
proof
assume
A15: angle(E,A,F) = 2*PI + angle(B,A,C)/3;
0 <= angle(B,A,C) & angle(B,A,C) <> 0 by Th2,A1,EUCLID10:30;
then 2*PI + 0 < 2*PI + angle(B,A,C)/3 by XREAL_1:8;
hence contradiction by A15,Th2;
end;
hence thesis by A12,A7,A8,A9,A10,A11,A13;
end;
theorem Th10:
C,A,B is_a_triangle & angle(A,C,B) < PI &
A,F,C is_a_triangle & F,A,E is_a_triangle & E,A,B is_a_triangle &
angle (B,A,E) = angle (B,A,C) / 3 & angle (F,A,C) = angle (B,A,C) / 3
implies
(PI/3 + angle(A,C,B)/3) + (PI/3 + angle(C,B,A)/3) + angle(E,A,F) = PI
proof
assume that
A1: C,A,B is_a_triangle and
A2: angle(A,C,B)<PI and
A3: A,F,C is_a_triangle and
A4: F,A,E is_a_triangle and
A5: E,A,B is_a_triangle and
A6: angle (B,A,E) = angle (B,A,C) / 3 and
A7: angle (F,A,C) = angle (B,A,C)/3;
set lambda = (PI/3 + angle(A,C,B)/3) + (PI/3 + angle(C,B,A)/3)
+ angle(E,A,F);
set theta = angle(A,C,B)/3 + angle(C,B,A)/3 + angle(B,A,C)/3;
A8: angle(E,A,F) = angle(B,A,C)/3 by A1,A3,A4,A5,A6,A7,Th9;
C,A,B are_mutually_distinct & angle(A,C,B) < PI by A1,A2,EUCLID_6:20;
then angle(A,C,B) + angle(C,B,A) + angle(B,A,C) = PI by EUCLID_3:47;
hence thesis by A8;
end;
theorem Th11:
A,C,B is_a_triangle implies sin (PI/3 - angle(A,C,B)/3)<>0
proof
assume
A1: A,C,B is_a_triangle;
assume sin (PI/3 - angle(A,C,B)/3)=0;
then consider i0 be Integer such that
A2: PI/3 - angle(A,C,B)/3 = PI * i0 by BORSUK_7:7;
0 + 3 * i0 * PI <= PI - 3 * i0 * PI + (3 * i0 * PI) &
PI - 3 * i0 *PI + (3 * i0 * PI) < 2 * PI + (3 * i0 * PI)
by A2,XREAL_1:6,Th2;
then 3 * i0 * PI <= PI & PI - PI < 2 * PI + 3 * i0 * PI - PI by XREAL_1:9;
then 3 * i0 * PI / PI <= PI / PI & 0 < (1 + 3 * i0) * PI
by COMPTRIG:5,XREAL_1:72;
then 3 * i0 * (PI / PI) <= PI / PI & 0 / PI < (1 + 3 * i0) * PI / PI
by COMPTRIG:5;
then 3 * i0 <= PI / PI & 0 / PI < (1 + 3 * i0) by XCMPLX_1:88,COMPTRIG:5;
then 3 * i0 <= 1 & 0 < (1 + 3 * i0) by XCMPLX_1:60;
then i0 = 0 by Lm4;
hence contradiction by A1,A2,EUCLID_6:20;
end;
theorem Th12:
A,B,C is_a_triangle & A,B,E is_a_triangle &
angle (E,B,A) = angle (C,B,A) / 3 & angle (B,A,E) = angle (B,A,C) / 3 &
A,F,C is_a_triangle &
angle (A,C,F) = angle (A,C,B)/3 & angle (F,A,C) = angle (B,A,C)/3 &
angle(A,C,B) < PI
implies
|.F-E.| = 4 * the_diameter_of_the_circumcircle(A,B,C)
* sin (angle(A,C,B)/3) * sin (angle(C,B,A) /3)
* sin (angle(B,A,C)/3)
proof
assume that
A1: A,B,C is_a_triangle and
A2: A,B,E is_a_triangle and
A3: angle (E,B,A) = angle (C,B,A) / 3 and
A4: angle (B,A,E) = angle (B,A,C) / 3 and
A5: A,F,C is_a_triangle and
A6: angle (A,C,F) = angle (A,C,B)/3 and
A7: angle (F,A,C) = angle (B,A,C)/3 and
A8: angle(A,C,B) < PI;
A9: A,C,B is_a_triangle by A1,MENELAUS:15;
then
A10: sin (PI/3 - angle(A,C,B)/3)<>0 by Th11;
C,B,A is_a_triangle by A1,MENELAUS:15;
then
A11: sin (PI/3 - angle(C,B,A)/3)<>0 by Th11;
A12: A,C,B are_mutually_distinct by A9,EUCLID_6:20;
then angle (A,C,B) + angle(C,B,A) + angle(B,A,C) = PI
by A8,EUCLID_3:47;
then
A13: angle (A,C,B)/3 + angle(B,A,C)/3 + angle(C,B,A)/3 = PI/3;
angle(A,C,B) <> 0 by A1,EUCLID10:30;
then
A14: 0 < angle(A,C,B) by Th2;
then
A15: angle (C,B,A) < PI by A12,A8,Th4;
angle(A,C,B) <> 0 by A1,EUCLID10:30;
then
A16: 0 < angle(A,C,B) < PI & A,C,B are_mutually_distinct
by A9,EUCLID_6:20,A8,Th2;
then angle(B,A,C) < PI by Th4;
then
A17: angle(B,A,C)/3 < PI/3 & PI/3 < PI
by XREAL_1:74,XREAL_1:221,COMPTRIG:5;
A18: E,A,B is_a_triangle &
B,A,E is_a_triangle & E,B,A is_a_triangle by A2,MENELAUS:15;
then
A19: B,A,E are_mutually_distinct & E,B,A are_mutually_distinct &
angle(E,B,A) <> 0 & angle(B,A,E) <> 0 by EUCLID_6:20,EUCLID10:30;
0 < angle(B,A,E) < PI by A17,A4,XXREAL_0:2,A19,Th2;
then
A20: angle(A,E,B) < PI by A19,Th4;
F,A,C is_a_triangle by A5,MENELAUS:15;
then
A21: F,A,C are_mutually_distinct & angle(F,A,C) <> 0
by EUCLID_6:20,EUCLID10:30;
then 0 < angle(F,A,C) < PI by A17,A7,XXREAL_0:2,Th2;
then
A22: angle(C,F,A) < PI by A21,Th4;
A23: F,A,E is_a_triangle
proof
now
E<>F
proof
assume
A24: E=F;
per cases by EUCLID_6:4;
suppose
A25: angle(B,A,E) + angle(E,A,C) = angle(B,A,C);
A26: 0 < angle(B,A,C) by A16,Th4;
then
A27: angle(B,A,C) / angle(B,A,C) = 1 by XCMPLX_1:60;
angle(B,A,C) / angle(B,A,C) = 2/3 * angle(B,A,C) / angle(B,A,C)
by A24,A7,A4,A25
.= 2/3 by A27;
hence contradiction by A26,XCMPLX_1:60;
end;
suppose
A28: angle(B,A,E)+angle(E,A,C) = angle(B,A,C) + 2*PI;
A29: 0 < angle(B,A,C) by A16,Th4;
2*PI = -1/3 * angle(B,A,C) by A24,A7,A4,A28;
hence contradiction by A29,COMPTRIG:5;
end;
end;
hence F,A,E are_mutually_distinct by A21,A19;
now
hereby
assume
A30: angle(F,A,E)=PI;
A31: angle(C,A,F)+angle(F,A,E)=angle(C,A,E) or
angle(C,A,F)+angle(F,A,E)=angle(C,A,E)+2*PI by EUCLID_6:4;
per cases by EUCLID_6:4;
suppose angle(C,A,E)+angle(E,A,B)=angle(C,A,B);
then per cases by A31,A30;
suppose
A32: angle(C,A,F) + PI + angle(E,A,B) = angle(C,A,B);
A33: 0 < angle(B,A,C) by A16,Th4;
A34: angle(C,A,F) + PI + angle(E,A,B) = 2*PI - angle(B,A,C)
by A32,A1,EUCLID10:31;
A35: angle(C,A,F) = 2*PI - angle(B,A,C)/3 by A7,A5,EUCLID10:31;
angle(E,A,B) = 2*PI - angle(B,A,E) = 2*PI - angle(B,A,C)/3
by A4,A2,EUCLID10:31;
then 3*PI = -1/3 * angle(B,A,C) by A34,A35;
hence contradiction by A33,COMPTRIG:5;
end;
suppose
A36: angle(C,A,F) - PI +angle(E,A,B)=angle(C,A,B);
A37: 0 < angle(B,A,C) by A16,Th4;
A38: angle(C,A,F) - PI + angle(E,A,B) = 2*PI - angle(B,A,C)
by A36,A1,EUCLID10:31;
A39: angle(C,A,F) = 2*PI - angle(F,A,C) = 2*PI - angle(B,A,C)/3
by A7,A5,EUCLID10:31;
angle(E,A,B) = 2*PI - angle(B,A,C)/3 by A4,A2,EUCLID10:31;
hence contradiction by A37,COMPTRIG:5,A38,A39;
end;
end;
suppose angle(C,A,E)+angle(E,A,B)=angle(C,A,B)+2*PI;
then per cases by A31,A30;
suppose
A40: angle(C,A,F)+ PI +angle(E,A,B)=angle(C,A,B)+2*PI;
A41: 0 < angle(B,A,C) by A16,Th4;
A42: angle(C,A,F) + PI + angle(E,A,B)
= 2*PI - angle(B,A,C) + 2*PI by A40,A1,EUCLID10:31;
A43: angle(C,A,F) = 2*PI - angle(B,A,C)/3 by A7,A5,EUCLID10:31;
angle(E,A,B) = 2*PI - angle(B,A,C)/3 by A4,A2,EUCLID10:31;
hence contradiction by A42,A43,A41,COMPTRIG:5;
end;
suppose
A44: angle(C,A,F)- PI +angle(E,A,B)=angle(C,A,B)+2*PI;
A45: angle(C,A,F) - PI + angle(E,A,B)
= 2*PI - angle(B,A,C) + 2*PI by A44,A1,EUCLID10:31;
A46: angle(C,A,F) = 2*PI - angle(B,A,C)/3 by A7,A5,EUCLID10:31;
angle(E,A,B) = 2*PI - angle(B,A,C)/3 by A4,A2,EUCLID10:31;
then 3 * PI = 3 * 1/3 * angle(B,A,C) & 2 * PI + 0 < 2 * PI + PI
by A45,A46,XREAL_1:6,COMPTRIG:5;
hence contradiction by Th2;
end;
end;
end;
hereby
assume angle(A,E,F)=PI;
then
A47: E in LSeg(A,F) & E<> A by A19,EUCLID_6:11;
A48: angle(C,A,F) + angle(F,A,B)=angle(C,A,B) or
angle(C,A,F) + angle(F,A,B)=angle(C,A,B) + 2*PI by EUCLID_6:4;
A49: angle(C,A,F) = 2*PI - angle(B,A,C)/3 by A7,A5,EUCLID10:31;
angle(F,A,B) = angle(E,A,B) by A47,EUCLID_6:9
.= 2*PI - angle(B,A,C)/3 by A4,A2,EUCLID10:31;
then per cases by A1,EUCLID10:31,A48,A49;
suppose
A50: 2*PI - angle(B,A,C)/3 + 2*PI -angle(B,A,C)/3
= 2*PI - angle(B,A,C);
0 < angle(B,A,C) by A16,Th4;
hence contradiction by A50,COMPTRIG:5;
end;
suppose 2*PI - angle(B,A,C)/3 + 2*PI -angle(B,A,C)/3 =
2*PI - angle(B,A,C) + 2*PI;
hence contradiction by A16,Th4;
end;
end;
hereby
assume angle(E,F,A)=PI;
then
A51: F in LSeg(E,A) & F <> A by A21,EUCLID_6:11;
A52: angle(C,A,F) + angle(F,A,B)=angle(C,A,B) or
angle(C,A,F) + angle(F,A,B)=angle(C,A,B) + 2*PI by EUCLID_6:4;
A53: angle(C,A,F) = 2*PI - angle(B,A,C)/3 by A5,A7,EUCLID10:31;
angle(F,A,B) = angle(E,A,B) by A51,EUCLID_6:9
.= 2*PI - angle(B,A,C)/3 by A4,A2,EUCLID10:31;
then per cases by A1,EUCLID10:31,A52,A53;
suppose
A54: 2*PI - angle(B,A,C)/3 + 2*PI -angle(B,A,C)/3
= 2*PI - angle(B,A,C);
0 < angle(B,A,C) by A16,Th4;
hence contradiction by A54,COMPTRIG:5;
end;
suppose
2*PI - angle(B,A,C)/3 + 2*PI -angle(B,A,C)/3
= 2*PI - angle(B,A,C) + 2*PI;
hence contradiction by A16,Th4;
end;
end;
end;
hence angle(F,A,E)<>PI & angle(A,E,F)<>PI & angle(E,F,A)<>PI;
end;
hence thesis by EUCLID_6:20;
end;
A55: - the_diameter_of_the_circumcircle(C,B,A)
= the_diameter_of_the_circumcircle(A,B,C) by A1,EUCLID10:49;
set lambda = (- the_diameter_of_the_circumcircle(C,B,A) * 4
* sin (angle(A,C,B)/3) * sin (angle(C,B,A) /3));
A56: |.A-E.| =
(- the_diameter_of_the_circumcircle(C,B,A) * 4 * sin (angle(A,C,B)/3) *
sin (PI/3 + angle(A,C,B)/3) * sin (angle(C,B,A) /3))
by A1,A2,A3,A4,A15,A20,A10,EUCLID10:56
.= lambda * sin(PI/3 + angle(A,C,B)/3);
A57: |.A-F.| =
(the_diameter_of_the_circumcircle(A,B,C) * 4 * sin (angle(C,B,A)/3) *
sin (PI/3 + angle(C,B,A)/3) * sin (angle(A,C,B) /3))
by A1,A5,A6,A7,A11,A13,A22,Th8
.= lambda * sin(PI/3 + angle(C,B,A)/3) by A55;
A58: C,A,B is_a_triangle by A1,MENELAUS:15;
then
A59: (PI/3 + angle(A,C,B)/3) + (PI/3 + angle(C,B,A)/3) + angle(E,A,F) = PI
by Th10,A5,A23,A18,A4,A7,A8;
A60: |.F-E.|^2 =
|.A-E.|^2 + |.A-F.|^2 - 2*|.A-E.|*|.A-F.|*cos angle (E,A,F) by Th3
.= lambda^2 * ((sin(PI/3 + angle(A,C,B)/3))^2
+ (sin(PI/3 + angle(C,B,A)/3))^2
- 2 * sin(PI/3 + angle(A,C,B)/3)
* sin(PI/3 + angle(C,B,A)/3) * cos angle(E,A,F))
by A56,A57
.= lambda^2 * (sin angle(E,A,F))^2 by A59,EUCLID10:25
.= lambda^2 * (sin (angle(B,A,C)/3))^2 by Th9,A58,A5,A23,A18,A4,A7
.= (lambda * sin(angle(B,A,C)/3))^2;
now
A61: lambda = (- the_diameter_of_the_circumcircle(C,B,A)) * 4
* sin (angle(A,C,B)/3) * sin (angle(C,B,A) /3)
.= the_diameter_of_the_circumcircle(A,B,C) * 4
* sin (angle(A,C,B)/3) * sin (angle(C,B,A) /3)
by A1,EUCLID10:49;
now
0 <= angle(C,B,A) < PI by A14,A12,A8,Th4;
then
A62: 0 <= angle(C,B,A)/3 < PI/3 by XREAL_1:74;
PI/3 < PI/1 by COMPTRIG:5,XREAL_1:76;
then 2*PI*0 <= angle(C,B,A)/3 < PI+2*PI*0 by A62,XXREAL_0:2;
hence sin (angle(C,B,A)/3) >=0 by SIN_COS6:16;
0 <= angle(A,C,B) < PI by A8,Th2;
then
A63: 0 <= angle(A,C,B)/3 < PI/3 by XREAL_1:74;
PI/3 < PI/1 by COMPTRIG:5,XREAL_1:76;
then 2*PI*0 <= angle(A,C,B)/3 < PI+2*PI*0 by A63,XXREAL_0:2;
hence 0 <= sin (angle(A,C,B)/3) by SIN_COS6:16;
thus 0 <= the_diameter_of_the_circumcircle(A,B,C) by A15,Th6;
end;
hence 0 <= lambda by A61;
now
A,C,B is_a_triangle by A1,MENELAUS:15;
hence A,C,B are_mutually_distinct by EUCLID_6:20;
angle(A,C,B) <> 0 by A1,EUCLID10:30;
hence 0 < angle(A,C,B) < PI by A8,Th2;
end;
then 0 <= angle(B,A,C) < PI by Th4;
then
A64: 0 <= angle(B,A,C)/3 < PI/3 by XREAL_1:74;
PI/3 < PI/1 by COMPTRIG:5,XREAL_1:76;
then 2*PI*0 <= angle(B,A,C)/3 < PI+2*PI*0 by A64,XXREAL_0:2;
hence 0 <= sin (angle(B,A,C)/3) by SIN_COS6:16;
end;
then
A65: sqrt ((lambda * sin(angle(B,A,C)/3))^2) = lambda
* sin(angle(B,A,C)/3) by SQUARE_1:22;
lambda = (- the_diameter_of_the_circumcircle(C,B,A)) * 4
* sin (angle(A,C,B)/3) * sin (angle(C,B,A) /3)
.= the_diameter_of_the_circumcircle(A,B,C) * 4 * sin (angle(A,C,B)/3)
* sin (angle(C,B,A) /3) by A1,EUCLID10:49;
hence thesis by A60,SQUARE_1:22,A65;
end;
theorem Th13:
A,B,C is_a_triangle & angle (E,B,A) = angle (C,B,A) / 3 &
angle (B,A,E) = angle (B,A,C) / 3 implies A,B,E is_a_triangle
proof
assume that
A1: A,B,C is_a_triangle and
A2: angle (E,B,A) = angle (C,B,A) / 3 and
A3: angle (B,A,E) = angle (B,A,C) / 3;
A4: A,B,C are_mutually_distinct by A1,EUCLID_6:20;
A5: angle(C,B,A) <> 0 & angle(B,A,C) <> 0 by A1,EUCLID10:30;
now
thus A,B,E are_mutually_distinct by A4,A2,Th1,A3,A5;
hereby
assume angle(A,B,E)=PI;
then B in LSeg(A,E) & B <> A by A4,EUCLID_6:11;
then angle(E,A,B) = angle(B,A,B) by EUCLID_6:9
.= 0 by Th1;
hence contradiction by A5,A3,EUCLID_3:36;
end;
hereby assume angle(B,E,A)=PI;
then E in LSeg(B,A) & E <> B by Th1,A3,A5,EUCLID_6:11;
then angle(A,B,E) = angle(E,B,E) by EUCLID_6:9
.= 0 by Th1;
hence contradiction by A5,A2,EUCLID_3:36;
end;
hereby
assume
A6: angle(E,A,B)=PI;
then
A7: angle(B,A,E) = 2*PI - angle(E,A,B) by COMPTRIG:5,EUCLID_3:37
.= PI by A6;
2*PI+0 < 2*PI+PI by XREAL_1:8,COMPTRIG:5;
hence contradiction by A7,A3,Th2;
end;
end;
hence thesis by EUCLID_6:20;
end;
theorem Th14:
A,B,C is_a_triangle & angle (A,C,F) = angle (A,C,B) / 3 &
angle (F,A,C) = angle (B,A,C) / 3 implies A,F,C is_a_triangle
proof
assume that
A1: A,B,C is_a_triangle and
A2: angle (A,C,F) = angle (A,C,B) / 3 and
A3: angle (F,A,C) = angle (B,A,C) / 3;
A4: A,B,C are_mutually_distinct by A1,EUCLID_6:20;
A5: angle(A,C,B) <> 0 & angle(B,A,C) <> 0 by A1,EUCLID10:30;
now
thus A,F,C are_mutually_distinct by A2,A3,A4,A5,Th1;
hereby
assume angle(A,F,C)=PI;
then F in LSeg(A,C) & F <> A by A2,A5,Th1,EUCLID_6:11;
then angle(C,A,F) = angle(F,A,F) by EUCLID_6:9
.= 0 by Th1;
hence contradiction by A5,A3,EUCLID_3:36;
end;
hereby
assume
A6: angle(C,A,F)=PI;
then
A7: angle(F,A,C) = 2*PI - angle(C,A,F) by COMPTRIG:5,EUCLID_3:37
.= PI by A6;
2*PI+0 < 2*PI+PI by XREAL_1:8,COMPTRIG:5;
hence contradiction by A3,A7,Th2;
end;
hereby
assume
A8: angle(F,C,A)=PI;
then
A9: angle(A,C,F) = 2*PI - angle(F,C,A) by COMPTRIG:5,EUCLID_3:37
.= PI by A8;
2*PI+0<2*PI+PI by COMPTRIG:5,XREAL_1:8;
hence contradiction by A9,A2,Th2;
end;
end;
hence thesis by EUCLID_6:20;
end;
theorem Th15:
A,B,C is_a_triangle & angle (C,B,G) = angle (C,B,A)/3 &
angle (G,C,B) = angle (A,C,B)/3 implies C,G,B is_a_triangle
proof
assume that
A1: A,B,C is_a_triangle and
A2: angle (C,B,G) = angle (C,B,A)/3 and
A3: angle (G,C,B) = angle (A,C,B)/3;
A4: A,B,C are_mutually_distinct by A1,EUCLID_6:20;
A5: angle(A,C,B) <> 0 & angle(C,B,A) <> 0 by A1,EUCLID10:30;
now
thus C,G,B are_mutually_distinct by A2,A3,A4,A5,Th1;
hereby
assume angle(C,G,B)=PI;
then G in LSeg(C,B) & G <> C by A2,A5,Th1,EUCLID_6:11;
then angle(G,C,B) = angle(B,C,B) by EUCLID_6:9
.= 0 by Th1;
hence contradiction by A3,A1,EUCLID10:30;
end;
hereby
assume angle(G,B,C)=PI;
then
A6: angle(C,B,G) = 2*PI - PI by COMPTRIG:5,EUCLID_3:37
.= PI;
2*PI+0 < 2*PI+PI by COMPTRIG:5,XREAL_1:8;
hence contradiction by A2,A6,Th2;
end;
hereby
assume angle(B,C,G)=PI;
then
A7: angle(G,C,B) = 2*PI - PI by COMPTRIG:5,EUCLID_3:37
.= PI;
2*PI+0 < 2*PI+PI by COMPTRIG:5,XREAL_1:8;
hence contradiction by A3,A7,Th2;
end;
end;
hence thesis by EUCLID_6:20;
end;
theorem Th16:
A,B,C is_a_triangle & angle(A,C,B) < PI &
angle (E,B,A) = angle (C,B,A) / 3 &
angle (B,A,E) = angle (B,A,C) / 3 &
angle (A,C,F) = angle (A,C,B) / 3 &
angle (F,A,C) = angle (B,A,C) / 3 &
angle (C,B,G) = angle (C,B,A) / 3 &
angle (G,C,B) = angle (A,C,B) / 3
implies
|.F-E.| = 4 * the_diameter_of_the_circumcircle(A,B,C)
* sin (angle(A,C,B)/3) * sin (angle(C,B,A) /3) * sin (angle(B,A,C)/3) &
|.G-F.| = 4 * the_diameter_of_the_circumcircle(C,A,B)
* sin (angle(C,B,A)/3) * sin (angle(B,A,C) /3) * sin (angle(A,C,B)/3) &
|.E-G.| = 4 * the_diameter_of_the_circumcircle(B,C,A)
* sin (angle(B,A,C)/3) * sin (angle(A,C,B) /3) * sin (angle(C,B,A)/3)
proof
assume
A1: A,B,C is_a_triangle & angle(A,C,B) < PI &
angle (E,B,A) = angle (C,B,A) / 3 &
angle (B,A,E) = angle (B,A,C) / 3 &
angle (A,C,F) = angle (A,C,B) / 3 &
angle (F,A,C) = angle (B,A,C) / 3 &
angle (C,B,G) = angle (C,B,A) / 3 &
angle (G,C,B) = angle (A,C,B) / 3;
then
A2: A,B,E is_a_triangle & A,F,C is_a_triangle &
C,G,B is_a_triangle by Th13,Th14,Th15;
now
thus
A3: C,A,B is_a_triangle & B,C,A is_a_triangle by A1,MENELAUS:15;
thus C,A,F is_a_triangle & B,C,G is_a_triangle & B,E,A is_a_triangle
by A2,MENELAUS:15;
angle(A,C,B) <> 0 by A1,EUCLID10:30;
then A,C,B are_mutually_distinct & 0 < angle(A,C,B) < PI
by A1,A3,EUCLID_6:20,Th2;
hence angle(C,B,A) < PI & angle(B,A,C) < PI by Th4;
end;
hence thesis by A1,A2,Th12;
end;
theorem Th17:
A,B,C is_a_triangle & angle(A,C,B) < PI &
angle(E,B,A) = angle(C,B,A) / 3 &
angle(B,A,E) = angle(B,A,C) / 3 &
angle(A,C,F) = angle(A,C,B) / 3 &
angle(F,A,C) = angle(B,A,C) / 3 &
angle(C,B,G) = angle(C,B,A) / 3 &
angle(G,C,B) = angle(A,C,B) / 3
implies
|.F-E.| = |.G-F.| & |.F-E.| = |.E-G.| & |.G-F.| = |.E-G.|
proof
assume A,B,C is_a_triangle & angle(A,C,B) < PI &
angle (E,B,A) = angle (C,B,A) / 3 &
angle (B,A,E) = angle (B,A,C) / 3 &
angle (A,C,F) = angle (A,C,B)/3 &
angle (F,A,C) = angle (B,A,C)/3 &
angle (C,B,G) = angle (C,B,A)/3 &
angle (G,C,B) = angle (A,C,B)/3;
then
A1: |.F-E.| = the_diameter_of_the_circumcircle(A,B,C) * 4
* sin (angle(A,C,B)/3) * sin (angle(C,B,A) /3) * sin (angle(B,A,C)/3) &
|.G-F.| = the_diameter_of_the_circumcircle(C,A,B) * 4
* sin (angle(C,B,A)/3) * sin (angle(B,A,C) /3) * sin (angle(A,C,B)/3) &
|.E-G.| = the_diameter_of_the_circumcircle(B,C,A) * 4
* sin (angle(B,A,C)/3) * sin (angle(A,C,B) /3) * sin (angle(C,B,A)/3)
by Th16;
the_diameter_of_the_circumcircle(A,B,C)
= the_diameter_of_the_circumcircle(C,A,B) &
the_diameter_of_the_circumcircle(A,B,C)
= the_diameter_of_the_circumcircle(B,C,A) by EUCLID10:46;
hence thesis by A1;
end;
::$N Morley's trisector theorem
::$L https://en.wikipedia.org/wiki/Morley's_trisector_theorem Morley's trisector theorem
theorem
A,B,C is_a_triangle & angle(A,B,C) < PI &
angle(E,C,A) = angle(B,C,A) / 3 &
angle(C,A,E) = angle(C,A,B) / 3 &
angle(A,B,F) = angle(A,B,C) / 3 &
angle(F,A,B) = angle(C,A,B) / 3 &
angle(B,C,G) = angle(B,C,A) / 3 &
angle(G,B,C) = angle(A,B,C) / 3
implies
|.F-E.| = |.G-F.| & |.F-E.| = |.E-G.| & |.G-F.| = |.E-G.|
proof
assume
A1: A,B,C is_a_triangle & angle(A,B,C) < PI &
angle(E,C,A) = angle(B,C,A) / 3 &
angle(C,A,E) = angle(C,A,B) / 3 &
angle(A,B,F) = angle(A,B,C) / 3 &
angle(F,A,B) = angle(C,A,B) / 3 &
angle(B,C,G) = angle(B,C,A) / 3 &
angle(G,B,C) = angle(A,B,C) / 3;
A,C,B is_a_triangle by A1,MENELAUS:15;
hence thesis by A1,Th17;
end;