:: Morley's Trisector Theorem
:: by Roland Coghetto
::
:: Received March 26, 2015
:: Copyright (c) 2015-2021 Association of Mizar Users

theorem Th1: :: EUCLID11:1

for A, B being Point of (TOP-REAL 2) holds angle (A,B,A) = 0

proof end;

theorem Th2: :: EUCLID11:2

for A, B, C being Point of (TOP-REAL 2) holds
( 0 <= angle (A,B,C) & angle (A,B,C) < 2 * PI )

proof end;

Lm1: [.0,(2 * PI).[ = ([.0,PI.[ \/ {PI}) \/ ].PI,(2 * PI).[

proof end;

theorem :: EUCLID11:3

for A, B, C being Point of (TOP-REAL 2) 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 (TOP-REAL 2) 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 (TOP-REAL 2) 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 (TOP-REAL 2) 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 (TOP-REAL 2) 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 (TOP-REAL 2) 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 (TOP-REAL 2) 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 (TOP-REAL 2) 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 (TOP-REAL 2) 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 (TOP-REAL 2) 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 (TOP-REAL 2) 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 * (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 end;

theorem Th9: :: EUCLID11:14

for A, B, C, E, F being Point of (TOP-REAL 2) 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 (TOP-REAL 2) 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 (TOP-REAL 2) 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 (TOP-REAL 2) 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 * (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 end;

theorem Th13: :: EUCLID11:18

for A, B, C, E being Point of (TOP-REAL 2) 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 (TOP-REAL 2) 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 (TOP-REAL 2) 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 (TOP-REAL 2) 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 * (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 end;

theorem Th17: :: EUCLID11:22

for A, B, C, E, F, G being Point of (TOP-REAL 2) 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 (TOP-REAL 2) 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;