:: 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;