:: Some Facts about Trigonometry and Euclidean Geometry
:: by Roland Coghetto
::
:: Received November 29, 2014
:: Copyright (c) 2014-2021 Association of Mizar Users
:: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.
environ
vocabularies RVSUM_1, NUMBERS, COMPLEX1, RELAT_1, CARD_1, ARYTM_1, ARYTM_3,
PRE_TOPC, EUCLID, SIN_COS, COMPLEX2, EUCLID_6, NEWTON, XXREAL_0, REAL_1,
SQUARE_1, XCMPLX_0, ZFMISC_1, RLTOPSP1, MCART_1, EUCLID_3, XXREAL_1,
COMPTRIG, PROJPL_1, JGRAPH_6, PENCIL_1, XBOOLE_0, TARSKI, METRIC_1,
INCSP_1, SIN_COS6, SUBSET_1, FUNCT_1, XXREAL_2, MEASURE5, EUCLID10;
notations RVSUM_1, XCMPLX_0, PRE_TOPC, XXREAL_0, RLVECT_1, SIN_COS, EUCLID,
EUCLID_3, EUCLID_6, NEWTON, ORDINAL1, SQUARE_1, COMPLEX2, XREAL_0,
RCOMP_1, COMPTRIG, COMPLEX1, ZFMISC_1, RLTOPSP1, JGRAPH_6, XBOOLE_0,
TARSKI, SIN_COS4, TOPREAL9, SIN_COS6, SUBSET_1, BINOP_1, STRUCT_0,
COMPTS_1, METRIC_1, TBSP_1;
constructors MONOID_0, RCOMP_1, SIN_COS, EUCLID_3, EUCLID_6, SQUARE_1,
COMPLEX2, COMSEQ_3, COMPTRIG, JGRAPH_6, SIN_COS4, TOPREAL9, SIN_COS6,
COMPTS_1, TBSP_1;
registrations XREAL_0, EUCLID, SIN_COS, NEWTON, XCMPLX_0, ORDINAL1, SQUARE_1,
XXREAL_0, RLTOPSP1, TOPREAL9, NAT_1, CARD_1, XBOOLE_0, RELSET_1,
JGRAPH_6, JORDAN2C, MONOID_0, VALUED_0;
requirements NUMERALS, SUBSET, ARITHM, REAL, BOOLE;
begin :: Values of the trigonometric functions for angles: PI / 3 and PI / 6
theorem :: EUCLID10:1
for a be Real holds sin (PI-a) = sin a;
theorem :: EUCLID10:2
for a be Real holds cos (PI-a) = - cos a;
theorem :: EUCLID10:3
for a be Real holds sin (2*PI-a) = - sin a;
theorem :: EUCLID10:4
for a be Real holds cos (2*PI-a) = cos a;
theorem :: EUCLID10:5
for a be Real holds sin(-2*PI+a) = sin a;
theorem :: EUCLID10:6
for a be Real holds cos(-2*PI+a)=cos a;
theorem :: EUCLID10:7
for a be Real holds sin (3*PI/2 + a) = - cos a;
theorem :: EUCLID10:8
for a be Real holds cos (3*PI/2 + a) = sin a;
theorem :: EUCLID10:9
for a be Real holds sin (3*PI/2 + a) = - sin (PI/2 -a);
theorem :: EUCLID10:10
for a be Real holds cos (3*PI/2 + a) = cos (PI/2 -a);
theorem :: EUCLID10:11
for a be Real holds sin (2*PI/3 - a) = sin (PI/3 +a);
theorem :: EUCLID10:12
for a be Real holds cos (2*PI/3 - a) = - cos (PI/3 + a);
theorem :: EUCLID10:13
for a be Real holds sin (2*PI/3 + a) = sin (PI/3 - a);
theorem :: EUCLID10:14
cos(PI/3) = 1/2;
theorem :: EUCLID10:15
sin(PI/3) = sqrt 3 /2;
theorem :: EUCLID10:16
tan(PI/3) = sqrt 3;
theorem :: EUCLID10:17
sin(PI/6) = 1/2;
theorem :: EUCLID10:18
cos(PI/6) = sqrt 3 /2;
theorem :: EUCLID10:19
tan(PI/6) = sqrt 3 / 3;
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;
theorem :: EUCLID10:21
arcsin (1/2) = PI/6 & arcsin (sqrt 3 / 2) = PI/3;
theorem :: EUCLID10:22
sin (2*PI/3) = sqrt(3)/2;
theorem :: EUCLID10:23
cos(2*PI/3) = - 1/2;
begin :: Some trigonometric identities
theorem :: EUCLID10:24
for x being Real holds (sin (-x))^2=(sin x)^2;
theorem :: 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;
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;
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;
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;
theorem :: EUCLID10:29
for a be Real holds
sin (3 * a) = 4 * sin a * sin (PI/3 + a) * sin (PI/3 - a);
begin
theorem :: EUCLID10:30
for A,B,C being Point of TOP-REAL 2 st A,B,C is_a_triangle holds
angle(A,B,C) is non zero & angle(B,C,A) is non zero &
angle(C,A,B) is non zero & angle(A,C,B) is non zero &
angle(C,B,A) is non zero & angle(B,A,C) is non zero;
theorem :: EUCLID10:31
for A,B,C be 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);
theorem :: EUCLID10:32
for A,B,C be Point of TOP-REAL 2 st
A,B,C is_a_triangle & |( B - A , C - A )| = 0
holds |.C-B.| * sin angle (C,B,A)=|.A-C.| or
|.C-B.| * (- sin angle (C,B,A))= |.A-C.|;
theorem :: EUCLID10:33
for A,B,C be 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;
theorem :: EUCLID10:34
for A,B,C be 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.|;
theorem :: EUCLID10:35
for A,B,C be 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.|;
begin :: Triangle inscribed in a semicircle is a right triangle
registration
let a,b be Real,
r be negative Real;
cluster circle(a,b,r) -> empty;
end;
theorem :: EUCLID10:36
for a,b be Real holds circle(a,b,0) = { |[a,b]| };
registration
let a,b be Real;
cluster circle(a,b,0) -> trivial;
end;
theorem :: EUCLID10:37
for A,B,C being Point of TOP-REAL 2,
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;
theorem :: EUCLID10:38
for A being Point of TOP-REAL 2,a,b be Real, r be positive Real st
A in circle(a,b,r) holds A <> |[a,b]|;
theorem :: EUCLID10:39
for A,B,C being Point of TOP-REAL 2,
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;
theorem :: EUCLID10:40
for A,B,C be Point of TOP-REAL 2, r being positive Real st
angle(A,B,C) is non 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));
theorem :: EUCLID10:41
for A,B,C be Point of TOP-REAL 2 st angle(A,B,C) is non 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);
begin :: Diameter of the circumcircle of a triangle
theorem :: EUCLID10:42
for A,B,C be 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);
theorem :: EUCLID10:43
for A,B,C be Point of TOP-REAL 2 holds
the_area_of_polygon3(A,B,C)= - the_area_of_polygon3(B,A,C);
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);
end;
theorem :: 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));
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));
theorem :: EUCLID10:46
for A,B,C be Point of TOP-REAL 2 holds
the_diameter_of_the_circumcircle(A,B,C)=
the_diameter_of_the_circumcircle(B,C,A);
theorem :: EUCLID10:47
for A,B,C be 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);
theorem :: EUCLID10:48
for A,B,C be 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);
theorem :: EUCLID10:49
for A,B,C be 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);
begin
theorem :: EUCLID10:50
for A,B,C be 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);
theorem :: EUCLID10:51
for A,B,C be 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);
theorem :: EUCLID10:52
for A,B,C,P be 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);
theorem :: EUCLID10:53
for A,B,C,P be 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);
theorem :: EUCLID10:54
for A,B,C be Point of TOP-REAL 2 st
A,B,C is_a_triangle & angle(C,A,B)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));
begin :: Diameter of a circle
theorem :: EUCLID10:57
for A,B,C be Point of TOP-REAL 2 st A,B,C are_mutually_distinct &
C in LSeg(A,B) holds |.A-B.| = |.A-C.| + |.C-B.|;
theorem :: EUCLID10:58
for A,B being Point of TOP-REAL 2,
a,b being Real, 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;
theorem :: EUCLID10:59
for a,b being Real,r being positive Real, C be Subset of Euclid 2 st
C = circle(a,b,r) holds diameter C = 2 * r;