:: Morley's Trisector Theorem
:: by Roland Coghetto
::
:: Copyright (c) 2015-2018 Association of Mizar Users

theorem Th1: :: EUCLID11:1
for A, B being Point of () holds angle (A,B,A) = 0
proof end;

theorem Th2: :: EUCLID11:2
for A, B, C being Point of () holds
( 0 <= angle (A,B,C) & angle (A,B,C) < 2 * PI )
proof end;

Lm1: [.0,(2 * PI).[ = () \/ ].PI,(2 * PI).[
proof end;

theorem :: EUCLID11:3
for A, B, C being Point of () holds
( ( 0 <= angle (A,B,C) & angle (A,B,C) < PI ) or angle (A,B,C) = PI or ( PI < angle (A,B,C) & angle (A,B,C) < 2 * PI ) )
proof end;

theorem Th3: :: EUCLID11:4
for A, E, F being Point of () holds |.(F - E).| ^2 = ((|.(A - E).| ^2) + (|.(A - F).| ^2)) - (((2 * |.(A - E).|) * |.(A - F).|) * (cos (angle (E,A,F))))
proof end;

Lm2: for i being Integer st i > 0 holds
ex k being Nat st i = k

proof end;

Lm3: for i being Integer st i < 0 holds
ex k being Nat st i = - k

proof end;

Lm4: for i being Integer st 3 * i <= 1 & 0 < 1 + (3 * i) holds
i = 0

proof end;

theorem Th4: :: EUCLID11:5
for A, B, C being Point of () st A,B,C are_mutually_distinct & 0 < angle (A,B,C) & angle (A,B,C) < PI holds
( 0 < angle (B,C,A) & angle (B,C,A) < PI & 0 < angle (C,A,B) & angle (C,A,B) < PI )
proof end;

theorem :: EUCLID11:6
for A, B, C being Point of () st A,B,C are_mutually_distinct & angle (A,B,C) = 0 & not ( angle (B,C,A) = 0 & angle (C,A,B) = PI ) holds
( angle (B,C,A) = PI & angle (C,A,B) = 0 & ((angle (A,B,C)) + (angle (B,C,A))) + (angle (C,A,B)) = PI )
proof end;

theorem :: EUCLID11:7
for A, B, C being Point of () st A,B,C are_mutually_distinct & angle (A,B,C) = PI holds
( angle (B,C,A) = 0 & angle (C,A,B) = 0 & ((angle (A,B,C)) + (angle (B,C,A))) + (angle (C,A,B)) = PI )
proof end;

theorem :: EUCLID11:8
for A, B, C being Point of () st A,B,C are_mutually_distinct & angle (A,B,C) > PI holds
( angle (B,C,A) > PI & angle (C,A,B) > PI )
proof end;

theorem :: EUCLID11:9
for A, B, C being Point of () st A,B,C are_mutually_distinct & angle (A,B,C) > PI holds
((angle (A,B,C)) + (angle (B,C,A))) + (angle (C,A,B)) = 5 * PI
proof end;

Lm5: for a being Real holds sin (((4 * PI) / 3) - a) = - (sin ((PI / 3) - a))
proof end;

theorem Th5: :: EUCLID11:10
for A, B, C being Point of () st angle (C,B,A) < PI holds
0 <= the_area_of_polygon3 (A,B,C)
proof end;

theorem Th6: :: EUCLID11:11
for A, B, C being Point of () st angle (C,B,A) < PI holds
0 <= the_diameter_of_the_circumcircle (A,B,C)
proof end;

theorem Th7: :: EUCLID11:12
for A, B, C, F being Point of () st 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 holds
|.(A - F).| * (sin ((PI / 3) - ((angle (C,B,A)) / 3))) = |.(A - C).| * (sin ((angle (A,C,B)) / 3))
proof end;

theorem Th8: :: EUCLID11:13
for A, B, C, F being Point of () st 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 holds
|.(A - F).| = (((4 * ()) * (sin ((angle (C,B,A)) / 3))) * (sin ((PI / 3) + ((angle (C,B,A)) / 3)))) * (sin ((angle (A,C,B)) / 3))
proof end;

theorem Th9: :: EUCLID11:14
for A, B, C, E, F being Point of () st 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 holds
angle (E,A,F) = (angle (B,A,C)) / 3
proof end;

theorem Th10: :: EUCLID11:15
for A, B, C, E, F being Point of () st 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 holds
(((PI / 3) + ((angle (A,C,B)) / 3)) + ((PI / 3) + ((angle (C,B,A)) / 3))) + (angle (E,A,F)) = PI
proof end;

theorem Th11: :: EUCLID11:16
for A, B, C being Point of () st A,C,B is_a_triangle holds
sin ((PI / 3) - ((angle (A,C,B)) / 3)) <> 0
proof end;

theorem Th12: :: EUCLID11:17
for A, B, C, E, F being Point of () st 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 holds
|.(F - E).| = (((4 * ()) * (sin ((angle (A,C,B)) / 3))) * (sin ((angle (C,B,A)) / 3))) * (sin ((angle (B,A,C)) / 3))
proof end;

theorem Th13: :: EUCLID11:18
for A, B, C, E being Point of () st A,B,C is_a_triangle & angle (E,B,A) = (angle (C,B,A)) / 3 & angle (B,A,E) = (angle (B,A,C)) / 3 holds
A,B,E is_a_triangle
proof end;

theorem Th14: :: EUCLID11:19
for A, B, C, F being Point of () st A,B,C is_a_triangle & angle (A,C,F) = (angle (A,C,B)) / 3 & angle (F,A,C) = (angle (B,A,C)) / 3 holds
A,F,C is_a_triangle
proof end;

theorem Th15: :: EUCLID11:20
for A, B, C, G being Point of () st A,B,C is_a_triangle & angle (C,B,G) = (angle (C,B,A)) / 3 & angle (G,C,B) = (angle (A,C,B)) / 3 holds
C,G,B is_a_triangle
proof end;

theorem Th16: :: EUCLID11:21
for A, B, C, E, F, G being Point of () st 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 holds
( |.(F - E).| = (((4 * ()) * (sin ((angle (A,C,B)) / 3))) * (sin ((angle (C,B,A)) / 3))) * (sin ((angle (B,A,C)) / 3)) & |.(G - F).| = (((4 * ()) * (sin ((angle (C,B,A)) / 3))) * (sin ((angle (B,A,C)) / 3))) * (sin ((angle (A,C,B)) / 3)) & |.(E - G).| = (((4 * ()) * (sin ((angle (B,A,C)) / 3))) * (sin ((angle (A,C,B)) / 3))) * (sin ((angle (C,B,A)) / 3)) )
proof end;

theorem Th17: :: EUCLID11:22
for A, B, C, E, F, G being Point of () st 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 holds
( |.(F - E).| = |.(G - F).| & |.(F - E).| = |.(E - G).| & |.(G - F).| = |.(E - G).| )
proof end;

:: Morley's trisector theorem
theorem :: EUCLID11:23
for A, B, C, E, F, G being Point of () st 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 holds
( |.(F - E).| = |.(G - F).| & |.(F - E).| = |.(E - G).| & |.(G - F).| = |.(E - G).| )
proof end;