environ
vocabularies HIDDEN, 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 HIDDEN, 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;
definitions ;
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;
schemes ;
registrations XREAL_0, EUCLID, SIN_COS, XCMPLX_0, ORDINAL1, SQUARE_1, XXREAL_0, MONOID_0, INT_1;
constructors HIDDEN, MONOID_0, SIN_COS, EUCLID_3, EUCLID_6, SQUARE_1, COMPLEX2, EUCLID10, INTEGRA1, SEQ_4;
requirements HIDDEN, NUMERALS, SUBSET, ARITHM, REAL;
equalities EUCLID10, SQUARE_1, XCMPLX_0;
expansions ZFMISC_1;
Lm1:
[.0,(2 * PI).[ = ([.0,PI.[ \/ {PI}) \/ ].PI,(2 * PI).[
theorem
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 ) )
Lm2:
for i being Integer st i > 0 holds
ex k being Nat st i = k
Lm3:
for i being Integer st i < 0 holds
ex k being Nat st i = - k
Lm4:
for i being Integer st 3 * i <= 1 & 0 < 1 + (3 * i) holds
i = 0
theorem Th4:
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 )
theorem
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 )
theorem
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 )
theorem
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 )
theorem
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
Lm5:
for a being Real holds sin (((4 * PI) / 3) - a) = - (sin ((PI / 3) - a))
theorem Th7:
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))
theorem Th8:
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))
theorem Th9:
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
theorem Th10:
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
theorem Th12:
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))
theorem Th13:
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
theorem Th14:
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
theorem Th15:
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
theorem Th16:
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)) )
theorem Th17:
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).| )
theorem
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).| )