:: Some Facts about Trigonometry and Euclidean Geometry
:: by Roland Coghetto
::
:: Received November 29, 2014
:: Copyright (c) 2014-2021 Association of Mizar Users

theorem Thm1: :: EUCLID10:1

for a being Real holds sin (PI - a) = sin a

proof end;

theorem :: EUCLID10:2

for a being Real holds cos (PI - a) = - (cos a)

proof end;

theorem :: EUCLID10:3

for a being Real holds sin ((2 * PI) - a) = - (sin a)

proof end;

theorem :: EUCLID10:4

for a being Real holds cos ((2 * PI) - a) = cos a

proof end;

theorem Thm2: :: EUCLID10:5

for a being Real holds sin ((- (2 * PI)) + a) = sin a

proof end;

theorem :: EUCLID10:6

for a being Real holds cos ((- (2 * PI)) + a) = cos a

proof end;

theorem Thm3: :: EUCLID10:7

for a being Real holds sin (((3 * PI) / 2) + a) = - (cos a)

proof end;

theorem Thm4: :: EUCLID10:8

for a being Real holds cos (((3 * PI) / 2) + a) = sin a

proof end;

theorem :: EUCLID10:9

for a being Real holds sin (((3 * PI) / 2) + a) = - (sin ((PI / 2) - a))

proof end;

theorem :: EUCLID10:10

for a being Real holds cos (((3 * PI) / 2) + a) = cos ((PI / 2) - a)

proof end;

theorem Thm5: :: EUCLID10:11

for a being Real holds sin (((2 * PI) / 3) - a) = sin ((PI / 3) + a)

proof end;

theorem Thm6: :: EUCLID10:12

for a being Real holds cos (((2 * PI) / 3) - a) = - (cos ((PI / 3) + a))

proof end;

theorem Thm7: :: EUCLID10:13

for a being Real holds sin (((2 * PI) / 3) + a) = sin ((PI / 3) - a)

proof end;

Lm1: angle (|[0,0]|,|[0,1]|,|[((sqrt 3) / 2),(1 / 2)]|) < PI

proof end;

Lm2: |.|[((sqrt 3) / 2),(1 / 2)]|.| = 1

proof end;

Lm3: for O, A, B being Point of (TOP-REAL 2) st O = |[0,0]| & A = |[0,1]| & B = |[((sqrt 3) / 2),(1 / 2)]| holds
( |.(O - A).| = |.(O - B).| & |.(O - A).| = |.(A - B).| & |.(O - A).| = 1 )

proof end;

Lm4: for O, A, B being Point of (TOP-REAL 2) st O = |[0,0]| & A = |[0,1]| & B = |[((sqrt 3) / 2),(1 / 2)]| holds
( O <> A & A <> B & O <> B & A <> O & B <> A & B <> O )

proof end;

Lm5: for O, A, B being Point of (TOP-REAL 2) st O = |[0,0]| & A = |[0,1]| & B = |[((sqrt 3) / 2),(1 / 2)]| holds
( angle (B,O,A) = angle (O,A,B) & angle (O,A,B) = angle (A,B,O) )

proof end;

Lm6: for O, A, B being Point of (TOP-REAL 2) st O = |[0,0]| & A = |[0,1]| & B = |[((sqrt 3) / 2),(1 / 2)]| & angle (O,A,B) < PI holds
angle (B,O,A) = PI / 3

proof end;

theorem Thm8: :: EUCLID10:14

cos (PI / 3) = 1 / 2

proof end;

theorem Thm9: :: EUCLID10:15

sin (PI / 3) = (sqrt 3) / 2

proof end;

theorem Thm10: :: EUCLID10:16

tan (PI / 3) = sqrt 3

proof end;

theorem Thm11: :: EUCLID10:17

sin (PI / 6) = 1 / 2

proof end;

theorem Thm12: :: EUCLID10:18

cos (PI / 6) = (sqrt 3) / 2

proof end;

theorem Thm13: :: EUCLID10:19

tan (PI / 6) = (sqrt 3) / 3

proof end;

theorem :: EUCLID10:20

( sin (- (PI / 6)) = - (1 / 2) & cos (- (PI / 6)) = (sqrt 3) / 2 & tan (- (PI / 6)) = - ((sqrt 3) / 3) & sin (- (PI / 3)) = - ((sqrt 3) / 2) & cos (- (PI / 3)) = 1 / 2 & tan (- (PI / 3)) = - (sqrt 3) ) by SIN_COS:31, SIN_COS4:1, Thm8, Thm9, Thm11, Thm12, Thm10, Thm13;

theorem :: EUCLID10:21

( arcsin (1 / 2) = PI / 6 & arcsin ((sqrt 3) / 2) = PI / 3 )

proof end;

theorem Thm14: :: EUCLID10:22

sin ((2 * PI) / 3) = (sqrt 3) / 2

proof end;

theorem Thm15: :: EUCLID10:23

cos ((2 * PI) / 3) = - (1 / 2)

proof end;

theorem Thm16: :: EUCLID10:24

for x being Real holds (sin (- x)) ^2 = (sin x) ^2

proof end;

theorem Thm17: :: EUCLID10:25

for x, y, z being Real st (x + y) + z = PI holds
(((sin x) ^2) + ((sin y) ^2)) - (((2 * (sin x)) * (sin y)) * (cos z)) = (sin z) ^2

proof end;

theorem :: EUCLID10:26

for x, y, z being Real st (x - y) + z = PI holds
(((sin x) ^2) + ((sin y) ^2)) + (((2 * (sin x)) * (sin y)) * (cos z)) = (sin z) ^2

proof end;

theorem :: EUCLID10:27

for x, y, z being Real st (x - ((- (2 * PI)) + y)) + z = PI holds
(((sin x) ^2) + ((sin y) ^2)) + (((2 * (sin x)) * (sin y)) * (cos z)) = (sin z) ^2

proof end;

theorem :: EUCLID10:28

for x, y, z being Real st ((PI - x) - (PI - y)) + z = PI holds
(((sin x) ^2) + ((sin y) ^2)) + (((2 * (sin x)) * (sin y)) * (cos z)) = (sin z) ^2

proof end;

theorem Thm18: :: EUCLID10:29

for a being Real holds sin (3 * a) = ((4 * (sin a)) * (sin ((PI / 3) + a))) * (sin ((PI / 3) - a))

proof end;

Lm7: for A, B, C being Point of (TOP-REAL 2) st A,B,C is_a_triangle holds
angle (A,B,C) <> 0

proof end;

theorem Thm19: :: EUCLID10:30

for A, B, C being Point of (TOP-REAL 2) st A,B,C is_a_triangle holds
( not angle (A,B,C) is zero & not angle (B,C,A) is zero & not angle (C,A,B) is zero & not angle (A,C,B) is zero & not angle (C,B,A) is zero & not angle (B,A,C) is zero )

proof end;

Lm9: for A, B, C being Point of (TOP-REAL 2) st A,B,C is_a_triangle holds
( angle (A,B,C) = (2 * PI) - (angle (C,B,A)) & angle (C,B,A) = (2 * PI) - (angle (A,B,C)) )

proof end;

theorem Thm20: :: EUCLID10:31

for A, B, C being Point of (TOP-REAL 2) st A,B,C is_a_triangle holds
( 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)) & angle (B,A,C) = (2 * PI) - (angle (C,A,B)) & angle (A,C,B) = (2 * PI) - (angle (B,C,A)) & angle (C,B,A) = (2 * PI) - (angle (A,B,C)) )

proof end;

theorem :: EUCLID10:32

for A, B, C being Point of (TOP-REAL 2) st A,B,C is_a_triangle & |((B - A),(C - A))| = 0 & not |.(C - B).| * (sin (angle (C,B,A))) = |.(A - C).| holds
|.(C - B).| * (- (sin (angle (C,B,A)))) = |.(A - C).|

proof end;

theorem :: EUCLID10:33

for A, B, C being Point of (TOP-REAL 2) st A,B,C is_a_triangle & angle (B,A,C) = PI / 2 holds
(angle (C,B,A)) + (angle (A,C,B)) = PI / 2

proof end;

theorem Thm21: :: EUCLID10:34

for A, B, C being Point of (TOP-REAL 2) st A,B,C is_a_triangle & angle (B,A,C) = PI / 2 holds
( |.(C - B).| * (sin (angle (C,B,A))) = |.(A - C).| & |.(C - B).| * (sin (angle (A,C,B))) = |.(A - B).| & |.(C - B).| * (cos (angle (C,B,A))) = |.(A - B).| & |.(C - B).| * (cos (angle (A,C,B))) = |.(A - C).| )

proof end;

theorem :: EUCLID10:35

for A, B, C being Point of (TOP-REAL 2) st A,B,C is_a_triangle & angle (B,A,C) = PI / 2 holds
( tan (angle (A,C,B)) = |.(A - B).| / |.(A - C).| & tan (angle (C,B,A)) = |.(A - C).| / |.(A - B).| )

proof end;

registration

let a, b be Real;
let r be negative Real;

cluster circle (a,b,r) -> empty ;

coherence
circle (a,b,r) is empty

proof end;

end;

theorem Thm23: :: EUCLID10:36

for a, b being Real holds circle (a,b,0) = {|[a,b]|}

proof end;

registration

let a, b be Real;

cluster circle (a,b,0) -> trivial ;

coherence
circle (a,b,0) is trivial

proof end;

end;

theorem Thm24: :: EUCLID10:37

for A, B, C being Point of (TOP-REAL 2)
for a, b, r being Real st A,B,C is_a_triangle & A in circle (a,b,r) & B in circle (a,b,r) holds
r is positive

proof end;

theorem Thm25: :: EUCLID10:38

for A being Point of (TOP-REAL 2)
for a, b being Real
for r being positive Real st A in circle (a,b,r) holds
A <> |[a,b]|

proof end;

theorem :: EUCLID10:39

for A, B, C being Point of (TOP-REAL 2)
for a, b, r being Real st A,B,C is_a_triangle & angle (C,B,A) in ].0,PI.[ & angle (B,A,C) in ].0,PI.[ & A in circle (a,b,r) & B in circle (a,b,r) & C in circle (a,b,r) & |[a,b]| in LSeg (A,C) holds
angle (C,B,A) = PI / 2

proof end;

theorem Thm26: :: EUCLID10:40

for A, B, C being Point of (TOP-REAL 2)
for r being positive Real st not angle (A,B,C) is zero holds
sin (r * (angle (C,B,A))) = ((sin ((r * 2) * PI)) * (cos (r * (angle (A,B,C))))) - ((cos ((r * 2) * PI)) * (sin (r * (angle (A,B,C)))))

proof end;

theorem :: EUCLID10:41

for A, B, C being Point of (TOP-REAL 2) st not angle (A,B,C) is zero holds
sin ((angle (C,B,A)) / 3) = (((sqrt 3) / 2) * (cos ((angle (A,B,C)) / 3))) + ((1 / 2) * (sin ((angle (A,B,C)) / 3)))

proof end;

theorem Thm27: :: EUCLID10:42

for A, B, C being Point of (TOP-REAL 2) holds
( the_area_of_polygon3 (A,B,C) = the_area_of_polygon3 (B,C,A) & the_area_of_polygon3 (A,B,C) = the_area_of_polygon3 (C,A,B) )

proof end;

theorem Thm28: :: EUCLID10:43

for A, B, C being Point of (TOP-REAL 2) holds the_area_of_polygon3 (A,B,C) = - (the_area_of_polygon3 (B,A,C))

proof end;

definition

let A, B, C be Point of (TOP-REAL 2);

::: assume A,B,C is_a_triangle;

func the_diameter_of_the_circumcircle (A,B,C) -> Real equals :: EUCLID10:def 1
(((|.(A - B).| * |.(B - C).|) * |.(C - A).|) / 2) / (the_area_of_polygon3 (A,B,C));

correctness
coherence
(((|.(A - B).| * |.(B - C).|) * |.(C - A).|) / 2) / (the_area_of_polygon3 (A,B,C)) is Real;
;

end;

:: deftheorem defines the_diameter_of_the_circumcircle EUCLID10:def 1 :
for A, B, C being Point of (TOP-REAL 2) holds the_diameter_of_the_circumcircle (A,B,C) = (((|.(A - B).| * |.(B - C).|) * |.(C - A).|) / 2) / (the_area_of_polygon3 (A,B,C));

theorem Thm29: :: EUCLID10:44

for A, B, C being Point of (TOP-REAL 2) st A,B,C is_a_triangle holds
the_diameter_of_the_circumcircle (A,B,C) = |.(C - A).| / (sin (angle (C,B,A)))

proof end;

theorem :: EUCLID10:45

for A, B, C being Point of (TOP-REAL 2) st A,B,C is_a_triangle holds
the_diameter_of_the_circumcircle (A,B,C) = - (|.(C - A).| / (sin (angle (A,B,C))))

proof end;

theorem :: EUCLID10:46

for A, B, C being Point of (TOP-REAL 2) holds the_diameter_of_the_circumcircle (A,B,C) = the_diameter_of_the_circumcircle (B,C,A) by Thm27;

theorem Thm31: :: EUCLID10:47

for A, B, C being Point of (TOP-REAL 2) st A,B,C is_a_triangle holds
the_diameter_of_the_circumcircle (A,B,C) = - (the_diameter_of_the_circumcircle (B,A,C))

proof end;

theorem Thm32: :: EUCLID10:48

for A, B, C being Point of (TOP-REAL 2) st A,B,C is_a_triangle holds
the_diameter_of_the_circumcircle (A,B,C) = - (the_diameter_of_the_circumcircle (A,C,B))

proof end;

theorem Thm33: :: EUCLID10:49

for A, B, C being Point of (TOP-REAL 2) st A,B,C is_a_triangle holds
the_diameter_of_the_circumcircle (A,B,C) = - (the_diameter_of_the_circumcircle (C,B,A))

proof end;

Lm10: for A, B, C being Point of (TOP-REAL 2) st A,B,C is_a_triangle holds
|.(A - B).| = (the_diameter_of_the_circumcircle (A,B,C)) * (sin (angle (A,C,B)))

proof end;

theorem Thm34: :: EUCLID10:50

for A, B, C being Point of (TOP-REAL 2) st A,B,C is_a_triangle holds
( |.(A - B).| = (the_diameter_of_the_circumcircle (A,B,C)) * (sin (angle (A,C,B))) & |.(B - C).| = (the_diameter_of_the_circumcircle (A,B,C)) * (sin (angle (B,A,C))) & |.(C - A).| = (the_diameter_of_the_circumcircle (A,B,C)) * (sin (angle (C,B,A))) )

proof end;

theorem :: EUCLID10:51

for A, B, C being Point of (TOP-REAL 2) st A,B,C is_a_triangle holds
|.(A - B).| = ((((the_diameter_of_the_circumcircle (A,B,C)) * 4) * (sin ((angle (A,C,B)) / 3))) * (sin ((PI / 3) + ((angle (A,C,B)) / 3)))) * (sin ((PI / 3) - ((angle (A,C,B)) / 3)))

proof end;

theorem :: EUCLID10:52

for A, B, C, P being Point of (TOP-REAL 2) st A,B,P are_mutually_distinct & angle (P,B,A) = (angle (C,B,A)) / 3 & angle (B,A,P) = (angle (B,A,C)) / 3 & angle (A,P,B) < PI holds
|.(A - P).| * (sin (PI - (((angle (C,B,A)) / 3) + ((angle (B,A,C)) / 3)))) = |.(A - B).| * (sin ((angle (C,B,A)) / 3))

proof end;

Lm11: for A, B, C being Point of (TOP-REAL 2) st A,B,C is_a_triangle & angle (C,B,A) < PI holds
( ((angle (C,B,A)) + (angle (B,A,C))) + (angle (A,C,B)) = PI & ((angle (C,A,B)) + (angle (A,B,C))) + (angle (B,C,A)) = 5 * PI )

proof end;

Lm12: for A, B, C being Point of (TOP-REAL 2) st A,B,C is_a_triangle & angle (C,B,A) < PI holds
(((angle (C,B,A)) / 3) + ((angle (B,A,C)) / 3)) + ((angle (A,C,B)) / 3) = PI / 3

proof end;

theorem Thm35: :: EUCLID10:53

for A, B, C, P being Point of (TOP-REAL 2) st A,B,P are_mutually_distinct & angle (P,B,A) = (angle (C,B,A)) / 3 & angle (B,A,P) = (angle (B,A,C)) / 3 & angle (A,P,B) < PI & (((angle (C,B,A)) / 3) + ((angle (B,A,C)) / 3)) + ((angle (A,C,B)) / 3) = PI / 3 holds
|.(A - P).| * (sin (((2 * PI) / 3) + ((angle (A,C,B)) / 3))) = |.(A - B).| * (sin ((angle (C,B,A)) / 3))

proof end;

theorem :: EUCLID10:54

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

proof end;

theorem :: EUCLID10:55

for A, B, C, P being Point of (TOP-REAL 2) st A,B,C is_a_triangle & angle (C,B,A) < PI & A,B,P are_mutually_distinct & angle (P,B,A) = (angle (C,B,A)) / 3 & angle (B,A,P) = (angle (B,A,C)) / 3 & angle (A,P,B) < PI holds
|.(A - P).| * (sin ((PI / 3) - ((angle (A,C,B)) / 3))) = |.(A - B).| * (sin ((angle (C,B,A)) / 3))

proof end;

theorem :: EUCLID10:56

for A, B, C, P being Point of (TOP-REAL 2) st A,B,C is_a_triangle & A,B,P is_a_triangle & angle (C,B,A) < PI & angle (A,P,B) < PI & angle (P,B,A) = (angle (C,B,A)) / 3 & angle (B,A,P) = (angle (B,A,C)) / 3 & sin ((PI / 3) - ((angle (A,C,B)) / 3)) <> 0 holds
|.(A - P).| = - (((((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)))

proof end;

theorem Thm37: :: EUCLID10:57

for A, B, C being Point of (TOP-REAL 2) st A,B,C are_mutually_distinct & C in LSeg (A,B) holds
|.(A - B).| = |.(A - C).| + |.(C - B).|

proof end;

theorem Thm38: :: EUCLID10:58

for A, B being Point of (TOP-REAL 2)
for a, b being Real
for r being positive Real st A,B,|[a,b]| are_mutually_distinct & A in circle (a,b,r) & B in circle (a,b,r) & |[a,b]| in LSeg (A,B) holds
|.(A - B).| = 2 * r

proof end;

theorem :: EUCLID10:59

for a, b being Real
for r being positive Real
for C being Subset of (Euclid 2) st C = circle (a,b,r) holds
diameter C = 2 * r

proof end;