:: Some Facts about Trigonometry and Euclidean Geometry
:: by Roland Coghetto
::
:: 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,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 () st O = & 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 () st O = & 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 () st O = & 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 () st O = & 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 ;

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 () 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 () 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 () 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 () 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 () 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 () 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 () 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 () 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 ()
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 ()
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 ()
for a, b, r being Real st A,B,C is_a_triangle & angle (C,B,A) in & angle (B,A,C) in & 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 ()
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 () 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 () 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 () 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 ();
::: 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 () 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 () 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 () 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 () 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 () st A,B,C is_a_triangle holds
the_diameter_of_the_circumcircle (A,B,C) = - ()
proof end;

theorem Thm32: :: EUCLID10:48
for A, B, C being Point of () st A,B,C is_a_triangle holds
the_diameter_of_the_circumcircle (A,B,C) = - ()
proof end;

theorem Thm33: :: EUCLID10:49
for A, B, C being Point of () st A,B,C is_a_triangle holds
the_diameter_of_the_circumcircle (A,B,C) = - ()
proof end;

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

proof end;

theorem Thm34: :: EUCLID10:50
for A, B, C being Point of () st A,B,C is_a_triangle holds
( |.(A - B).| = () * (sin (angle (A,C,B))) & |.(B - C).| = () * (sin (angle (B,A,C))) & |.(C - A).| = () * (sin (angle (C,B,A))) )
proof end;

theorem :: EUCLID10:51
for A, B, C being Point of () st A,B,C is_a_triangle holds
|.(A - B).| = (((() * 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 () 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 () 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 () 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 () 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 () 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 () 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 () 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).| = - ((((() * 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 () 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 ()
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 () st C = circle (a,b,r) holds
diameter C = 2 * r
proof end;