:: Some Facts about Trigonometry and Euclidean Geometry
:: by Roland Coghetto
::
:: Received November 29, 2014
:: Copyright (c) 2014-2026 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;
expansions ZFMISC_1, TARSKI, XBOOLE_0;
theorems XCMPLX_1, EUCLID, EUCLID_3, EUCLID_6, NEWTON, SIN_COS5, XREAL_1,
MENELAUS, SQUARE_1, SIN_COS, JGRAPH_1, COMPLEX2, XXREAL_1, COMPTRIG,
SIN_COS4, COMPLEX1, XXREAL_0, TOPREAL9, JGRAPH_6, TARSKI, RLTOPSP1,
SIN_COS6, METRIC_1, TBSP_1, SPPOL_1, SPPOL_2, JORDAN2C;
begin :: Values of the trigonometric functions for angles: PI / 3 and PI / 6
theorem Thm1:
for a be Real holds sin (PI-a) = sin a
proof
let a be Real;
sin (PI - a) = 0 * cos a - cos PI * sin a by SIN_COS:77,SIN_COS:82
.= sin a by SIN_COS:77;
hence thesis;
end;
theorem
for a be Real holds cos (PI-a) = - cos a
proof
let a be Real;
cos (PI - a) = cos PI * cos a + sin PI * sin a by SIN_COS:83
.= - cos a by SIN_COS:77;
hence thesis;
end;
theorem
for a be Real holds sin (2*PI-a) = - sin a
proof
let a be Real;
sin (2* PI - a) = 0 * cos a - cos (2*PI) * sin a by SIN_COS:77,SIN_COS:82
.= - sin a by SIN_COS:77;
hence thesis;
end;
theorem
for a be Real holds cos (2*PI-a) = cos a
proof
let a be Real;
cos (2* PI - a) = 1 * cos a + 0 * sin a by SIN_COS:77,SIN_COS:83
.= cos a;
hence thesis;
end;
theorem Thm2:
for a be Real holds sin(-2*PI+a) = sin a
proof
let a be Real;
sin(-2*PI + a ) = sin (a - 2*PI)
.=sin a * 1 - cos a * sin (2*PI) by SIN_COS:77,SIN_COS:82
.=sin a by SIN_COS:77;
hence thesis;
end;
theorem
for a be Real holds cos(-2*PI+a)=cos a
proof
let a be Real;
cos(-2*PI + a ) = cos (a - 2*PI)
.=cos a * 1 + sin a * sin (2*PI) by SIN_COS:77,SIN_COS:83
.=cos a by SIN_COS:77;
hence thesis;
end;
theorem Thm3:
for a be Real holds sin (3*PI/2 + a) = - cos a
proof
let a be Real;
sin (3*PI/2 + a) = sin (3*PI/2) * cos a + cos (3*PI/2) * sin a
by SIN_COS:75
.= - cos a by SIN_COS:77;
hence thesis;
end;
theorem Thm4:
for a be Real holds cos (3*PI/2 + a) = sin a
proof
let a be Real;
cos (3*PI/2 + a) = cos (3*PI/2) * cos a - sin (3*PI/2) * sin a
by SIN_COS:75
.= - (- sin a) by SIN_COS:77;
hence thesis;
end;
theorem
for a be Real holds sin (3*PI/2 + a) = - sin (PI/2 -a)
proof
let a be Real;
sin (3*PI/2 + a) = - cos a by Thm3
.= - sin (PI/2 - a) by SIN_COS:79;
hence thesis;
end;
theorem
for a be Real holds cos (3*PI/2 + a) = cos (PI/2 -a)
proof
let a be Real;
cos (3*PI/2 + a) = sin a by Thm4
.= cos (PI/2 - a) by SIN_COS:79;
hence thesis;
end;
theorem Thm5:
for a be Real holds sin (2*PI/3 - a) = sin (PI/3 +a)
proof
let a be Real;
sin (2*PI/3 - a) = sin (PI - (PI/3+a))
.= sin PI * cos (PI/3 + a) - cos PI * sin (PI/3+a) by SIN_COS:82
.= sin (PI/3 + a) by SIN_COS:77;
hence thesis;
end;
theorem Thm6:
for a be Real holds cos (2*PI/3 - a) = - cos (PI/3 + a)
proof
let a be Real;
cos (2*PI/3 - a) = cos (PI - (PI/3+a))
.= cos PI * cos (PI/3 + a) + sin PI * sin (PI/3 + a) by SIN_COS:83
.= - cos (PI/3 + a) by SIN_COS:77;
hence thesis;
end;
theorem Thm7:
for a be Real holds sin (2*PI/3 + a) = sin (PI/3 - a)
proof
let a be Real;
sin (2*PI/3 + a) = sin (PI - (PI/3 - a))
.= sin PI * cos (PI/3 - a) - cos PI * sin (PI/3 - a) by SIN_COS:82
.= sin (PI/3 - a) by SIN_COS:77;
hence thesis;
end;
Lm1:
angle(|[0,0]|,|[0,1]|,|[sqrt 3 /2,1/2]|) < PI
proof
set O=euc2cpx(|[0,0]|);
set A=euc2cpx(|[0,1]|);
set B=euc2cpx(|[sqrt 3 /2,1/2]|);
|[0,0]|`1=0 & |[0,0]|`2=0 & |[0,1]|`1=0 & |[0,1]|`2=1 &
|[sqrt 3 /2,1/2]|`1=sqrt 3 /2 & |[sqrt 3 /2,1/2]|`2=1/2 by EUCLID:52;
then
A1: O= 0 + 0 * <i> & A=0 + 1 * <i> & B=sqrt 3 /2 + 1/2 * <i>
by EUCLID_3:def 2;
A2: Arg( (-1) * <i>) =3/2 * PI by COMPTRIG:38;
B-A = sqrt 3 /2 + (-1/2) * <i> by A1; then
A3: Re (B-A)=sqrt 3 /2 & Im (B-A)= - 1/2 by COMPLEX1:12;
sqrt 3 > 0 by SQUARE_1:25;
then Arg(B-A) in ]. 3/2 * PI , 2 * PI.[ by A3,COMPTRIG:44;
then 3/2 * PI < Arg(B-A) & Arg(B-A) < 2 * PI by XXREAL_1:4; then
A4: 3/2 * PI - 3/2 * PI < Arg(B-A) - 3/2 * PI &
Arg(B-A) - 3/2 * PI < 2 * PI - 3/2 * PI by XREAL_1:14;
set th=Arg(B-A)-Arg(O-A);
PI in ]. 0, 4 .[ by SIN_COS:def 28; then
A5: 0 < PI by XXREAL_1:4;
th < 1/2 * PI & 1/2 * PI < PI by A1,A2,A4,A5,XREAL_1:157;
then
A6: not PI <= th by XXREAL_0:2;
angle(O,A,B)=th by A1,A2,A4,COMPLEX2:def 4;
hence thesis by A6,EUCLID_3:def 4;
end;
Lm2:
|.|[sqrt 3 /2,1/2]|.|=1
proof
set B=|[(sqrt 3)/2,1/2]|;
B`1=(sqrt 3)/2 & B`2=1/2 by EUCLID:52; then
A1: |.B.|=sqrt( (sqrt 3 /2)^2+(1/2)^2) by JGRAPH_1:30;
A2: (sqrt 3 /2)^2=(sqrt 3/2)*(sqrt 3/2) by SQUARE_1:def 1;
A3: (1/2)^2=(1/2)*(1/2) by SQUARE_1:def 1;
(sqrt 3)^2=3 by SQUARE_1:def 2;
then sqrt 3 * sqrt 3 /2 /2=3/2/2 by SQUARE_1:def 1;
hence thesis by A1,A2,A3;
end;
Lm3:
for O,A,B be 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
let O,A,B be Point of TOP-REAL 2 such that
A1: O=|[0,0]| and
A2: A=|[0,1]| and
A3: B=|[(sqrt 3)/2,1/2]|;
A4: A`1=0 & A`2=1 & O`1=0 & O`2=0 & B`1=(sqrt 3)/2 & B`2=1/2
by A1,A2,A3,EUCLID:52; then
A5: A-O=|[ 0 - 0 , 1 - 0 ]| by EUCLID:61;
0 ^2 = 0 * 0 & 1^2 = 1 * 1 by SQUARE_1:def 1; then
A6: |.A.|=sqrt( 0 * 0 + 1 * 1) by A4,JGRAPH_1:30;
A7: B-O=|[(sqrt 3)/2 - 0,1/2 - 0]| by A4,EUCLID:61
.=|[(sqrt 3)/2,1/2]|;
A-B=|[0-(sqrt 3)/2,1-1/2]| by A4,EUCLID:61;
then (A-B)`1=- sqrt 3 /2 & (A-B)`2=1/2 by EUCLID:52; then
A8: |.A-B.|=sqrt( (- sqrt 3 /2)^2+(1/2)^2) by JGRAPH_1:30;
A9: (- sqrt 3 /2)^2=(- sqrt 3/2)*(- sqrt 3/2) by SQUARE_1:def 1;
A10: (1/2)^2=(1/2)*(1/2) by SQUARE_1:def 1;
(sqrt 3)^2=3 by SQUARE_1:def 2; then
A11: sqrt 3 * sqrt 3 /2 /2=3/2/2 by SQUARE_1:def 1;
|.O - B.|=|.B - O.| by EUCLID_6:43;
hence thesis by EUCLID_6:43,A6,A5,A2,A9,A10,A8,A11,A7,Lm2;
end;
Lm4:
for O,A,B be 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
let O,A,B be Point of TOP-REAL 2 such that
A1: O=|[0,0]| and
A2: A=|[0,1]| and
A3: B=|[(sqrt 3)/2,1/2]|;
O<>A & A<>B & O<>B
proof
O`2=0 & B`2=1/2 by A1,A3,EUCLID:52;
hence thesis by A2,EUCLID:52;
end;
hence thesis;
end;
Lm5:
for O,A,B be 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
let O,A,B be Point of TOP-REAL 2 such that
A1: O=|[0,0]| and
A2: A=|[0,1]| and
A3: B=|[(sqrt 3)/2,1/2]|;
A4: |.O-A.|=|.O-B.| & |.O-A.|=|.A-B.| by A1,A2,A3,Lm3; then
A5: |.O-A.|=|.B-O.| & |.A-O.|=|.O-B.| &
|.O-A.|=|.B-A.| & |.A-O.|=|.A-B.| by EUCLID_6:43;
O<>A & A<>B & O<>B by A1,A2,A3,Lm4;
hence thesis by A4, A5, EUCLID_6:16;
end;
Lm6:
for O,A,B be 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
let O,A,B be Point of TOP-REAL 2 such that
A1: O=|[0,0]| and
A2: A=|[0,1]| and
A3: B=|[(sqrt 3)/2,1/2]| and
A4: angle(O,A,B)<PI;
A<>O & O <> B & B <>A by A1,A2,A3,Lm4; then
A5: angle(O,A,B)+angle(A,B,O)+angle(B,O,A)=PI by A4,EUCLID_3:47;
angle(B,O,A)=angle(O,A,B) & angle(O,A,B)=angle(A,B,O) by A1,A2,A3,Lm5;
hence thesis by A5;
end;
theorem Thm8:
cos(PI/3) = 1/2
proof
set O=|[0,0]|;
set A=|[0,1]|;
set B=|[sqrt 3 /2,1/2]|;
set a =|.B-O.|;
set b =|.A-O.|;
set c =|.A-B.|;
|.O-A.|=|.O-B.| & |.O-A.|=|.A-B.| & |.O-A.|=1 by Lm3; then
A1: b=1 & c =1 & a=1 by EUCLID_6:43;
1^2 = 1 * 1 by SQUARE_1:def 1
.=1;
then 1 = 1 + 1 - 2 * 1 * 1 * cos angle(B,O,A) by A1,EUCLID_6:7;
hence thesis by Lm1,Lm6;
end;
theorem Thm9:
sin(PI/3) = sqrt 3 /2
proof
A1: (sin(PI/3)) ^2 + (cos(PI/3)) ^2 =1 by SIN_COS:29;
A2: (cos(PI/3)) ^2 = cos(PI/3) * cos(PI/3) by SQUARE_1:def 1
.=1/4 by Thm8;
sin(PI/3) >=0
proof
A3: (PI/2-(PI/3)) in ]. 0 , PI/2 .[
proof
set n=PI/2-(PI/3);
PI/6 < PI/2 by COMPTRIG:5,XREAL_1:76;
hence thesis by COMPTRIG:5,XXREAL_1:4;
end;
sin(PI/3)=cos(PI/2-(PI/3)) by SIN_COS:79;
hence thesis by A3,SIN_COS:81;
end;
then sin(PI/3) = sqrt (3/4) by A1,A2,SQUARE_1:22;
hence thesis by SQUARE_1:20,SQUARE_1:30;
end;
theorem Thm10:
tan(PI/3) = sqrt 3
proof
tan(PI/3) =(sqrt(3)/2)/(1/2) by Thm8,Thm9,SIN_COS4:def 1
.=sqrt(3);
hence thesis;
end;
theorem Thm11:
sin(PI/6) = 1/2
proof
sin(PI/6)=sin(PI/2-PI/3)
.=1/2 by Thm8,SIN_COS:79;
hence thesis;
end;
theorem Thm12:
cos(PI/6) = sqrt 3 /2
proof
cos(PI/6)=cos(PI/2-PI/3)
.=sqrt(3)/2 by Thm9,SIN_COS:79;
hence thesis;
end;
theorem Thm13:
tan(PI/6) = sqrt 3 / 3
proof
tan(PI/6) = (1/2)/(sqrt(3)/2) by Thm11,Thm12,SIN_COS4:def 1
.=1/sqrt(3) by XCMPLX_1:55;
hence thesis by SQUARE_1:33;
end;
theorem
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
arcsin (1/2) = PI/6 & arcsin (sqrt 3 / 2) = PI/3
proof
PI/6 < PI/2 & PI/3 < PI/2 & -PI/2<= PI/6 & -PI/2<=PI/3
by XREAL_1:76,COMPTRIG:5;
hence thesis by Thm9,Thm11,SIN_COS6:69;
end;
theorem Thm14:
sin (2*PI/3) = sqrt(3)/2
proof
sin(2*PI/3) = sin(2*PI/3 - 0)
.=sin(PI/3 + 0 ) by Thm5
.=sin(PI/3);
hence thesis by Thm9;
end;
theorem Thm15:
cos(2*PI/3) = - 1/2
proof
cos(2*PI/3)=cos(2*PI/3 - 0)
.= - cos (PI/3 + 0) by Thm6
.= - cos (PI/3);
hence thesis by Thm8;
end;
begin :: Some trigonometric identities
theorem Thm16:
for x being Real holds (sin (-x))^2=(sin x)^2
proof
let x be Real;
(sin(-x))^2 = sin(-x) * sin(-x) by SQUARE_1:def 1
.= (- sin x) * sin (-x) by SIN_COS:31
.= (- sin x) * (- sin x) by SIN_COS:31
.= (sin x) * (sin x);
hence thesis by SQUARE_1:def 1;
end;
theorem Thm17:
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
let x,y,z be Real such that
A1: x + y + z = PI;
sin((x+y)-PI)=- sin(x+y) by COMPLEX2:5;
then - sin((x+y)-PI)= sin(x+y); then
A2: (sin(-((x+y)-PI)))^2=(sin(x+y))^2 by SIN_COS:31;
A3: (cos y)^2 + (sin y)^2 = 1 by SIN_COS:29;
A4: (cos x)^2 + (sin x)^2 = 1 by SIN_COS:29;
A5: (sin(x+y))^2 = (sin x * cos y + cos x * sin y)^2 by SIN_COS:75
.= (sin x * cos y)^2+ 2 * (sin x * cos y) * (cos x * sin y) +
(cos x * sin y)^2 by SQUARE_1:4
.= (sin x * cos y) * (sin x * cos y) +
2 * sin x * cos y * cos x * sin y + (cos x * sin y)^2 by SQUARE_1:def 1
.= (sin x * cos y) * (sin x * cos y) +
2 * sin x * cos y * cos x * sin y + (cos x * sin y) * (cos x * sin y)
by SQUARE_1:def 1
.= (sin x * sin x) * (cos y * cos y) +
2 * sin x * cos y * cos x * sin y + cos x * cos x * sin y * sin y
.= (sin x)^2 * (cos y * cos y) + 2 * sin x * cos y * cos x * sin y +
cos x * cos x * sin y * sin y by SQUARE_1:def 1
.= (sin x)^2 * (cos y)^2 + 2 * sin x * cos y * cos x * sin y +
(cos x * cos x) * sin y * sin y by SQUARE_1:def 1
.= (sin x)^2 * (cos y)^2 + 2 * sin x * cos y * cos x * sin y +
(cos x)^2 * sin y * sin y by SQUARE_1:def 1
.= (sin x)^2 * (cos y)^2 + 2 * sin x * cos y * cos x * sin y +
(cos x)^2 * (sin y * sin y)
.= (sin x)^2 * (cos y)^2 + 2 * sin x * cos y * cos x * sin y +
(cos x)^2 * (sin y)^2 by SQUARE_1:def 1;
(sin x)^2+(sin y)^2 - 2 * sin x * sin y * cos z
=(sin x)^2+(sin y)^2 - 2 * sin x * sin y * cos (- ((x+y)-PI) ) by A1
.=(sin x)^2+(sin y)^2 - 2 * sin x * sin y * cos ((x+y)-PI) by SIN_COS:31
.=(sin x)^2+(sin y)^2 - 2 * sin x * sin y * (- cos (x+y)) by COMPLEX2:5
.=(sin x)^2+(sin y)^2 + 2 * sin x * sin y * cos (x+y)
.=(sin x)^2+(sin y)^2 +
2 * sin x * sin y * (cos x * cos y - sin x * sin y) by SIN_COS:75
.=(sin x)^2+(sin y)^2 + 2 * sin x * sin y * cos x * cos y -
2 * (sin x * sin x) * sin y * sin y
.=(sin x)^2+(sin y)^2 + 2 * sin x * sin y * cos x * cos y -
2 * (sin x)^2 * sin y * sin y by SQUARE_1:def 1
.=(sin x)^2+(sin y)^2 + 2 * sin x * sin y * cos x * cos y -
2 * (sin x)^2 * (sin y * sin y)
.=(sin x)^2+(sin y)^2 + 2 * sin x * sin y * cos x * cos y -
2 * (sin x)^2 * (sin y)^2 by SQUARE_1:def 1
.=(sin x)^2 * (1 - (sin y)^2) +(sin y)^2 +
2 * sin x * sin y * cos x * cos y - (sin x)^2 * (sin y)^2
.=(sin x)^2 * (cos y)^2 +(sin y)^2 * ( 1 - (sin x)^2) +
2 * sin x * sin y * cos x * cos y by A3
.=(sin x)^2 * (cos y)^2 +(sin y)^2 * (cos x)^2 +
2 * sin x * sin y * cos x * cos y by A4;
hence thesis by A1,A2,A5;
end;
theorem
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
let x,y,z be Real;
assume x - y + z = PI; then
A1: x + (-y) + z = PI;
(sin x)^2 + (sin (-y))^2 - 2 * sin x * sin (-y) * cos z
=(sin x)^2 + (sin (-y))^2 - 2 * sin x * (- sin y) * cos z by SIN_COS:31
.=(sin x)^2 + (sin (-y))^2 + 2 * sin x * sin y * cos z
.=(sin x)^2 + (sin y)^2 + 2 * sin x * sin y * cos z by Thm16;
hence thesis by A1,Thm17;
end;
theorem
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
let x,y,z be Real;
assume x - (-2*PI + y) + z = PI; then
A1: x + (- (-2*PI + y)) + z = PI;
(sin x)^2 + (sin (-(-2*PI+y)))^2 - 2 * sin x * sin (-(-2*PI+y)) * cos z
=(sin x)^2 + (sin (-(-2*PI+y)))^2 - 2 * sin x * (- sin (-2*PI+y)) *
cos z by SIN_COS:31
.=(sin x)^2 + (sin (-(-2*PI+y)))^2 + 2 * sin x * sin (-2*PI+y) * cos z
.=(sin x)^2 + (sin (-2*PI+y))^2 + 2 * sin x * sin (-2*PI+y) * cos z
by Thm16
.=(sin x)^2 + (sin (y))^2 + 2 * sin x * sin (-2*PI+y) * cos z by Thm2
.=(sin x)^2 + (sin (y))^2 + 2 * sin x * sin y * cos z by Thm2;
hence thesis by A1,Thm17;
end;
theorem
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
let x,y,z be Real;
assume (PI - x) - (PI - y) + z = PI; then
A1: (PI - x) + (-(PI-y)) + z = PI;
(sin (PI - x))^2 + (sin (-(PI - y)))^2 - 2 * sin (PI - x) *
sin (-(PI-y)) * cos z
=(sin (PI -x))^2 + (sin (-(PI - y)))^2 - 2 * sin (PI - x) *
(- sin (PI- y)) * cos z by SIN_COS:31
.=(sin (PI-x))^2 + (sin (-(PI-y)))^2 + 2 * sin (PI - x) * sin (PI - y)
* cos z
.=(sin (PI-x))^2 + (sin (PI-y))^2 + 2 * sin (PI-x) * sin (PI-y) * cos z
by Thm16
.=(sin x)^2 + (sin (PI-y))^2 + 2 * sin (PI-x) * sin (PI-y) * cos z
by Thm1
.=(sin x)^2 + (sin y)^2 + 2 * sin (PI-x) * sin (PI-y) * cos z by Thm1
.=(sin x)^2 + (sin y)^2 + 2 * sin x * sin (PI-y) * cos z by Thm1
.=(sin x)^2 + (sin y)^2 + 2 * sin x * sin y * cos z by Thm1;
hence thesis by A1,Thm17;
end;
theorem Thm18:
for a be Real holds
sin (3 * a) = 4 * sin a * sin (PI/3 + a) * sin (PI/3 - a)
proof
let a be Real;
A1: (sqrt 3 /2)^2 = (sqrt 3 /2) * (sqrt 3 /2) by SQUARE_1:def 1
.= sqrt 3 * sqrt 3 /2/2
.= sqrt (3 * 3) /2/2 by SQUARE_1:29
.= sqrt (3^2) /2/2 by SQUARE_1:def 1
.= 3 /2/2 by SQUARE_1:22
.= 3/4;
sin( 3 * a ) =-4 * (sin(a)) |^3 + 3 * sin(a) by SIN_COS5:16
.=4*sin(a)*3/4 - 4* (sin(a)) |^ (2+1)
.=4*sin(a)*3/4 - 4 * ((sin(a)) |^2 * (sin(a))) by NEWTON:6
.=4*sin(a)*((sqrt 3/2)^2-(sin(a)) |^2) by A1
.=4*sin(a)*( (sin (PI/3))^2-(sin a )^2) by Thm9,NEWTON:81
.=4*sin(a)*(((sin (PI/3))-(sin a ))* (sin(PI/3) + sin a)) by SQUARE_1:8
.=4*sin(a)*( sin (PI/3) + sin a )* (sin (PI/3) - sin a)
.=4*sin(a)*( 2*(cos(((PI/3)-a)/2)*sin(((PI/3)+a)/2)))*
(sin (PI/3) - sin a) by SIN_COS4:15
.=4*sin(a)*( 2*(cos(((PI/3)-a)/2)*sin(((PI/3)+a)/2)))*
(2*(cos(((PI/3)+a)/2)*sin(((PI/3)-a)/2))) by SIN_COS4:16
.=4*sin(a)*(2*sin(((PI/3)-a)/2)*cos(((PI/3)-a)/2))*(2*sin(((PI/3)+a)/2)*
cos(((PI/3)+a)/2))
.=4*sin(a)*(sin(2*(((PI/3)-a)/2)))*(2*sin(((PI/3)+a)/2)*
cos(((PI/3)+a)/2)) by SIN_COS5:5
.=4*sin(a)*(sin(2*(((PI/3)-a)/2)))*(sin(2*(((PI/3)+a)/2))) by SIN_COS5:5
.=4*sin(a)*sin(((PI/3)-a))*sin(((PI/3)+a));
hence thesis;
end;
begin :: Trigonometric functions and right triangle
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
let A,B,C be Point of TOP-REAL 2;
assume
A1: A,B,C is_a_triangle; then
A2: A,B,C are_mutually_distinct by EUCLID_6:20;
now assume angle(A,B,C)=0;
then angle (B,C,A)=PI or angle (B,A,C)=PI by A2,MENELAUS:8;
then C in LSeg(B,A) or A in LSeg(B,C) by EUCLID_6:11;
hence contradiction by A1,TOPREAL9:67;
end;
hence thesis;
end;
theorem Thm19:
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
proof
let A,B,C be Point of TOP-REAL 2;
assume
A1: A,B,C is_a_triangle;
then B,C,A is_a_triangle & C,A,B is_a_triangle &
B,A,C is_a_triangle & A,C,B is_a_triangle & C,B,A is_a_triangle
by MENELAUS:15;
hence thesis by A1,Lm7;
end;
Lm9:
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(C,B,A) = 2*PI - angle(A,B,C)
proof
let A,B,C be Point of TOP-REAL 2;
assume A,B,C is_a_triangle;
then angle(A,B,C)<>0 by Thm19;
hence angle(A,B,C) = 2*PI - angle(C,B,A) by EUCLID_3:38;
hence thesis;
end;
theorem Thm20:
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)
proof
let A,B,C be Point of TOP-REAL 2;
assume A,B,C is_a_triangle; then
B,C,A is_a_triangle & C,A,B is_a_triangle &B,A,C is_a_triangle &
A,C,B is_a_triangle & C,B,A is_a_triangle by MENELAUS:15;
hence thesis by Lm9;
end;
theorem
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.|
proof
let A,B,C be Point of TOP-REAL 2 such that
A1: A,B,C is_a_triangle and
A2: |( B - A , C - A )| = 0;
A3: A,B,C are_mutually_distinct by A1,EUCLID_6:20; then
A4: |. C - B .| * sin (angle(C,B,A)) = |. C - A .| * sin (angle(B,A,C))
by EUCLID_6:6;
sin angle(B,A,C)=1 or sin angle(B,A,C) = -1
by A2,A3,SIN_COS:77,EUCLID_3:45;
hence thesis by A4,EUCLID_6:43;
end;
theorem
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
proof
let A,B,C be Point of TOP-REAL 2 such that
A1: A,B,C is_a_triangle and
A2: angle(B,A,C) = PI/2;
A3: A,B,C are_mutually_distinct by A1,EUCLID_6:20;
angle(B,A,C)+angle(A,C,B)+angle(C,B,A)=PI by A2,COMPTRIG:5,A3,EUCLID_3:47;
hence thesis by A2;
end;
theorem Thm21:
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.|
proof
let A,B,C be Point of TOP-REAL 2 such that
A1: A,B,C is_a_triangle and
A2: angle(B,A,C) = PI/2;
A3: A,B,C are_mutually_distinct by A1,EUCLID_6:20; then
A4: |. C - B .| * sin (angle(C,B,A)) = |. C - A .| *
sin (angle(B,A,C)) by EUCLID_6:6;
A5: |. B - A .| * sin angle(B,A,C)=|.B - C.| * sin angle(A,C,B)
by A3,EUCLID_6:6; thus
A6: |.C-B.| * sin angle (C,B,A)=|.A-C.| by A2,A4,SIN_COS:77,EUCLID_6:43;
|. A - B .| * sin angle(B,A,C)=|.B- C.| * sin angle(A,C,B)
by A5,EUCLID_6:43;
hence
A7: |.C-B.| * sin angle (A,C,B)=|.A-B.| by A2,SIN_COS:77,EUCLID_6:43;
angle(B,A,C)+angle(A,C,B)+angle(C,B,A)=PI by A2,A3,COMPTRIG:5,EUCLID_3:47;
then sin angle(A,C,B)=sin (PI/2-angle(C,B,A)) by A2;
hence |.C-B.| * cos angle (C,B,A)=|.A-B.| by A7,SIN_COS:79;
angle(B,A,C)+angle(A,C,B)+angle(C,B,A)=PI by A2,A3,COMPTRIG:5,EUCLID_3:47;
then sin angle(C,B,A)=sin (PI/2-angle(A,C,B)) by A2;
hence |.C-B.| * cos angle (A,C,B)=|.A-C.| by A6,SIN_COS:79;
end;
theorem
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.|
proof
let A,B,C be Point of TOP-REAL 2 such that
A1: A,B,C is_a_triangle and
A2: angle(B,A,C) = PI/2;
A3: A,B,C are_mutually_distinct by A1,EUCLID_6:20;
|.C-B.| * sin angle (A,C,B)=|.A-B.| &
|.C-B.| * cos angle (A,C,B)=|.A-C.| by A1,A2,Thm21;
then (|.C-B.|/|.C-B.|) * sin angle (A,C,B) / cos angle (A,C,B) =
|.A-B.|/|.A-C.| by XCMPLX_1:83; then
A4: 1 * sin angle (A,C,B) / cos angle (A,C,B) =
|.A-B.|/|.A-C.| by A3,EUCLID_6:42,XCMPLX_1:60;
hence tan angle(A,C,B) = |.A-B.| / |.A-C.| by SIN_COS4:def 1;
angle(B,A,C)+angle(A,C,B)+angle(C,B,A)=PI by A2,A3,COMPTRIG:5,EUCLID_3:47;
then tan angle(C,B,A)
=(sin (PI/2-angle(A,C,B))) / cos (PI/2-angle(A,C,B)) by A2,SIN_COS4:def 1
.=cos (angle(A,C,B)) / cos (PI/2-angle(A,C,B)) by SIN_COS:79
.=cos angle(A,C,B) / sin angle(A,C,B) by SIN_COS:79
.=1/(sin angle(A,C,B) / cos angle(A,C,B)) by XCMPLX_1:57
.=|.A-C.|/|.A-B.| by A4,XCMPLX_1:57;
hence thesis;
end;
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;
coherence
proof
circle(a,b,r)=Sphere(|[a,b]|,r) by TOPREAL9:52;
hence thesis;
end;
end;
theorem Thm23:
for a,b be Real holds circle(a,b,0) = { |[a,b]| }
proof
let a,b be Real;
now
hereby
let t be object;
assume t in {p where p is Point of TOP-REAL 2: |.p-|[a,b]|.|=0};
then consider p0 be Point of TOP-REAL 2 such that
A1: t=p0 and
A2: |.p0-|[a,b]|.|=0;
p0=|[a,b]| by A2,EUCLID_6:42;
hence t in { |[a,b]| } by A1,TARSKI:def 1;
end;
let t be object;
assume
A3: t in { |[a,b]| }; then
A4: t = |[a,b]| by TARSKI:def 1;
reconsider p0=t as Point of TOP-REAL 2 by A3,TARSKI:def 1;
|.p0-|[a,b]|.|=0 by A4,EUCLID_6:42;
hence t in {p where p is Point of TOP-REAL 2: |.p-|[a,b]|.|=0};
end;
then {p where p is Point of TOP-REAL 2: |.p-|[a,b]|.|=0} c= { |[a,b]| } &
{ |[a,b]| } c= {p where p is Point of TOP-REAL 2: |.p-|[a,b]|.|=0};
hence thesis by JGRAPH_6:def 5;
end;
registration
let a,b be Real;
cluster circle(a,b,0) -> trivial;
coherence
proof
circle(a,b,0)= { |[a,b]| } by Thm23;
hence thesis;
end;
end;
theorem Thm24:
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
proof
let A,B,C be Point of TOP-REAL 2, a,b,r be Real such that
A1: A,B,C is_a_triangle and
A2: A in circle(a,b,r) & B in circle(a,b,r);
A3: A,B,C are_mutually_distinct by A1,EUCLID_6:20;
assume not r is positive;
then per cases;
suppose r<0;
hence contradiction by A2;
end;
suppose r=0;
then A in { |[a,b]| } & B in { |[a,b]| } by A2,Thm23;
then A = |[a,b]| & B = |[a,b]| by TARSKI:def 1;
hence contradiction by A3;
end;
end;
theorem Thm25:
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]|
proof
let A be Point of TOP-REAL 2,a,b be Real,r be positive Real such that
A1: A in circle(a,b,r);
circle(a,b,r)={p where p is Point of TOP-REAL 2: |.p-|[a,b]|.|=r}
by JGRAPH_6:def 5;
then consider p0 be Point of TOP-REAL 2 such that
A2: A=p0 and
A3: |.p0-|[a,b]|.|=r by A1;
thus thesis by A2,A3,EUCLID_6:42;
end;
theorem
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
proof
let A,B,C be Point of TOP-REAL 2,
a,b,r be Real such that
A1: A,B,C is_a_triangle and
A2: angle(C,B,A) in ].0,PI.[ and
A3: angle(B,A,C) in].0,PI.[ and
A4: A in circle(a,b,r) & B in circle(a,b,r) & C in circle(a,b,r) and
A5: |[a,b]| in LSeg(A,C);
A6: A,B,C are_mutually_distinct by A1,EUCLID_6:20;
set O = |[a,b]|;
A7: angle(C,B,A) > 0 & angle(C,B,A) < PI by A2,XXREAL_1:4;
A8: angle(B,A,C) >0 & angle(B,A,C)<PI by A3,XXREAL_1:4;
A9: circle(a,b,r)={p where p is Point of TOP-REAL 2: |.p-|[a,b]|.|=r}
by JGRAPH_6:def 5;
consider JA be Point of TOP-REAL 2 such that
A10: A=JA and
A11: |.JA-|[a,b]|.|=r by A4,A9;
consider JB be Point of TOP-REAL 2 such that
A12: B=JB and
A13: |.JB-|[a,b]|.|=r by A4,A9;
consider JC be Point of TOP-REAL 2 such that
A14: C=JC and
A15: |.JC-|[a,b]|.|=r by A4,A9;
r is positive by A1,A4,Thm24; then
A16: O<>A & O<>C by A4,Thm25;
A17: angle(C,B,A)<PI by A2,XXREAL_1:4;
A18: |.B-O.|=|.O-C.| & B<>C by A12,A13,A14,A15,A6,EUCLID_6:43;
A19: angle(C,B,O)<PI
proof
assume angle(C,B,O)>=PI;
then angle(O,C,B)>=PI by A18,EUCLID_6:16; then
A20: angle(A,C,B)>=PI by A5,A16,EUCLID_6:9;
angle(C,B,A)+angle(B,A,C)+angle(A,C,B)=PI by A17,A6,EUCLID_3:47;
then
A21: angle(C,B,A)+angle(B,A,C)=PI - angle(A,C,B);
angle(B,A,C) <= 0
proof
assume
A22: angle(B,A,C)>0;
angle(C,B,A)>0 by A2,XXREAL_1:4;
hence contradiction by A21,A20,A22,XREAL_1:47;
end;
hence contradiction by A3,XXREAL_1:4;
end;
A23: A,O,B is_a_triangle & C,O,B is_a_triangle
proof
A23a: r is positive by A1,A4,Thm24; then
A24: O<>B & O<>A & O<>C by A4,Thm25;
not A in Line(O,B)
proof
assume
A25: A in Line(O,B);
B in Line(O,B) by RLTOPSP1:72;
then Line(A,B)=Line(O,B) by A6,A25,RLTOPSP1:75;
then O in Line(A,B) & A in Line(A,B) by RLTOPSP1:72; then
A26: Line(O,A)=Line(A,B) by A4,A23a,Thm25,RLTOPSP1:75;
O in Line(A,C) & A in Line(A,C) by A5,MENELAUS:12,RLTOPSP1:72; then
Line(O,A)=Line(A,C) by A4,A23a,Thm25,RLTOPSP1:75;
then A in Line(A,B) & B in Line(A,B) & C in Line(A,B)
by A26,RLTOPSP1:72;
hence contradiction by A1,RLTOPSP1:def 16;
end;
hence A,O,B is_a_triangle by A24,MENELAUS:13;
not C,O,B are_collinear
proof
assume
A28: C,O,B are_collinear;
then C in Line(O,B) & B in Line(O,B) by A24,MENELAUS:13,RLTOPSP1:72;
then
A29: Line(C,B) = Line (O,B) by A6,RLTOPSP1:75;
C in Line(O,B) & O in Line(O,B) & O<>C by A28,A24,MENELAUS:13,
RLTOPSP1:72; then
A30: Line(C,O)=Line(O,B) by RLTOPSP1:75;
A31: O in Line(A,C) & A in Line(A,C) & C in Line(C,A)
by A5,MENELAUS:12,RLTOPSP1:72;
then Line(C,O)=Line(A,C) by A4,A23a,Thm25,RLTOPSP1:75;
hence contradiction by A30,A31,A29,A1,A6,MENELAUS:13;
end;
hence C,O,B is_a_triangle;
end; then
A32: A,O,B are_mutually_distinct & C,O,B are_mutually_distinct
by EUCLID_6:20;
then angle(B,A,O)<PI by A8,A5,EUCLID_6:10; then
A33: angle(B,A,O)+angle(A,O,B)+angle(O,B,A)=PI by A32,EUCLID_3:47;
|.O-A.|=|.B-O.| by A10,A11,A12,A13,EUCLID_6:43; then
A34: angle(O,A,B)=angle(A,B,O) by A6,EUCLID_6:16;
|.O-B.|=|.C-O.| by A12,A13,A14,A15,EUCLID_6:43; then
A35: angle(O,B,C)=angle(B,C,O) by A6,EUCLID_6:16;
A36: angle(C,B,O)+angle(O,C,B) + angle (O,B,A)+angle(B,A,O)=PI or
angle(C,B,O)+angle(O,C,B) + angle (O,B,A)+angle(B,A,O)=-PI
proof
A37: angle(A,O,B)+angle(B,O,C)=PI or angle(A,O,B)+angle(B,O,C)=3*PI
by A32,A5,EUCLID_6:13;
angle(C,B,O)+angle(B,O,C)+angle(O,C,B)=PI by A19,A32,EUCLID_3:47;
hence thesis by A33,A37;
end;
angle(O,C,B)=angle(C,B,O) & angle (B,A,O)=angle(O,B,A)
proof
2*PI-angle(C,B,O)=angle(O,B,C) & 2*PI-angle(O,C,B)=angle(B,C,O)
by A23,Thm20;
hence angle(O,C,B)=angle(C,B,O) by A35;
2*PI-angle(O,B,A)=angle(A,B,O) & 2*PI-angle(O,A,B)=angle(B,A,O)
by A23,Thm20;
hence thesis by A34;
end;
then angle(C,B,O)+angle(O,B,A)=PI/2 or angle(C,B,O)+angle(O,B,A)=-PI/2
by A36;
then angle(C,B,A)=PI/2 or angle(C,B,A)+2*PI=PI/2 or
angle(C,B,A)=-PI/2 or angle(C,B,A)+2*PI=-PI/2 by EUCLID_6:4;
then angle(C,B,A)=PI/2 or angle(C,B,A)=-3*PI/2 or
angle(C,B,A)=-PI/2 or angle(C,B,A)=-5*PI/2;
hence thesis by A7;
end;
theorem Thm26:
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))
proof
let A,B,C be Point of TOP-REAL 2,r being positive Real;
assume angle(A,B,C) is non zero; then
angle(C,B,A)= 2 * PI - angle(A,B,C) by EUCLID_3:37;
then r * angle(C,B,A)= r * 2 * PI - r * angle(A,B,C);
hence thesis by SIN_COS:82;
end;
theorem
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)
proof
let A,B,C be Point of TOP-REAL 2;
assume angle(A,B,C) is non zero; then
sin (1/3 * angle(C,B,A))
= sin(2 * PI/3) * cos (1/3 * angle(A,B,C)) - cos ( 1/3 * 2 * PI) *
sin (1/3 * angle(A,B,C)) by Thm26
.=(sqrt 3 /2) * cos (angle(A,B,C)/3) + 1/2 * sin (angle(A,B,C)/3)
by Thm14,Thm15;
hence thesis;
end;
begin :: Diameter of the circumcircle of a triangle
theorem Thm27:
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)
proof
let A,B,C be Point of TOP-REAL 2;
A1: the_area_of_polygon3(A,B,C)= ((A`1*B`2-B`1*
A`2)+(B`1*C`2-C`1*B`2)+(C`1*A`2-A`1*C`2))/2 by EUCLID_6:def 1;
the_area_of_polygon3(B,C,A)= ((B`1*C`2-C`1*
B`2)+(C`1*A`2-A`1*C`2)+(A`1*B`2-B`1*A`2))/2 by EUCLID_6:def 1;
hence the_area_of_polygon3(A,B,C)=the_area_of_polygon3(B,C,A) by A1;
the_area_of_polygon3(C,A,B)= ((C`1*A`2-A`1*
C`2)+(A`1*B`2-B`1*A`2)+(B`1*C`2-C`1*B`2))/2 by EUCLID_6:def 1;
hence thesis by A1;
end;
theorem Thm28:
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)
proof
let A,B,C be Point of TOP-REAL 2;
A1: the_area_of_polygon3(A,B,C)= ((A`1*B`2-B`1*
A`2)+(B`1*C`2-C`1*B`2)+(C`1*A`2-A`1*C`2))/2 by EUCLID_6:def 1;
the_area_of_polygon3(B,A,C)= ((B`1*A`2-A`1*
B`2)+(A`1*C`2-C`1*A`2)+(C`1*B`2-B`1*C`2))/2 by EUCLID_6:def 1;
hence thesis by A1;
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
|.A-B.|*|.B-C.|*|.C-A.|/2/the_area_of_polygon3(A,B,C);
correctness;
end;
theorem Thm29:
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
let A,B,C be Point of TOP-REAL 2;
assume A,B,C is_a_triangle; then
A2: A,B,C are_mutually_distinct by EUCLID_6:20;
the_diameter_of_the_circumcircle(A,B,C)=
|.A-B.|*|.B-C.|*|.C-A.|/2/(|.A-B.|*|.C-B.|*sin angle (C,B,A)/2)
by EUCLID_6:5
.=(|.A-B.|*|.B-C.|*|.C-A.|/2)/(1/2*(|.A-B.|*|.C-B.|*sin(angle (C,B,A))))
.=((|.A-B.|*|.B-C.|*|.C-A.|/2)/(1/2))/(|.A-B.|*(|.C-B.| *
sin(angle (C,B,A)))) by XCMPLX_1:78
.=((|.A-B.|*|.B-C.|*|.C-A.|/2)/(1/2)/|.A-B.|)/(|.C-B.|*
sin(angle (C,B,A))) by XCMPLX_1:78
.=(|.A-B.|*(|.B-C.|*|.C-A.|)/|.A-B.|)/|.C-B.|/sin(angle (C,B,A))
by XCMPLX_1:78
.=(|.B-C.|*|.C-A.|)/|.C-B.|/sin(angle (C,B,A))
by XCMPLX_1:89,A2,EUCLID_6:42
.=((|.B-C.|*|.C-A.|)/|.B-C.|)/sin(angle (C,B,A)) by EUCLID_6:43
.=|.C-A.|/sin(angle (C,B,A)) by XCMPLX_1:89,A2,EUCLID_6:42;
hence thesis;
end;
theorem
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
let A,B,C be Point of TOP-REAL 2;
assume A,B,C is_a_triangle; then
the_diameter_of_the_circumcircle(A,B,C) = |.C-A.|/ sin angle (C,B,A)
by Thm29
.= |.C-A.| / (- sin angle(A,B,C)) by EUCLID_6:2
.= - |.C-A.| / sin angle(A,B,C) by XCMPLX_1:188;
hence thesis;
end;
theorem
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) by Thm27;
theorem Thm31:
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)
proof
let A,B,C be Point of TOP-REAL 2;
A3: |.B-A.|=|.A-B.| & |.A-C.|=|.C-A.| & |.C-B.|=|.B-C.| by EUCLID_6:43;
the_diameter_of_the_circumcircle(B,A,C)=
|.A-B.|*|.C-A.|*|.B-C.|/2/( - the_area_of_polygon3(A,B,C)) by A3,Thm28
.= - |.A-B.|*|.C-A.|*|.B-C.|/2/the_area_of_polygon3(A,B,C)
by XCMPLX_1:188;
hence thesis;
end;
theorem Thm32:
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)
proof
let A,B,C be Point of TOP-REAL 2;
assume A,B,C is_a_triangle; then
A2: A,C,B is_a_triangle & B,C,A is_a_triangle by MENELAUS:15;
the_diameter_of_the_circumcircle(A,B,C)
=the_diameter_of_the_circumcircle(B,C,A) by Thm27
.= - the_diameter_of_the_circumcircle(C,B,A) by A2,Thm31;
hence thesis by Thm27;
end;
theorem Thm33:
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)
proof
let A,B,C be Point of TOP-REAL 2;
assume A,B,C is_a_triangle; then
the_diameter_of_the_circumcircle(A,B,C)=
- the_diameter_of_the_circumcircle(A,C,B) by Thm32;
hence thesis by Thm27;
end;
begin :: Some identities of a triangle
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
let A,B,C be Point of TOP-REAL 2;
assume A,B,C is_a_triangle; then
A2: the_area_of_polygon3(A,B,C)<>0 by MENELAUS:9;
set k=|.A - B.|*|.B - C.|*|.C - A.|/(the_area_of_polygon3(B,C,A));
A3: the_area_of_polygon3(B,C,A)=|.B-C.|*|.A-C.|*sin angle (A,C,B)/2
by EUCLID_6:5;
the_area_of_polygon3(B,C,A)<>0 by A2,Thm27; then
A4: |.A-B.|=|.A-B.|*
the_area_of_polygon3(B,C,A)/the_area_of_polygon3(B,C,A) by XCMPLX_1:89;
A5: |.A-B.|= (|.A-B.|*|.B-C.|*|.A-C.|*sin angle (A,C,B)/2)/
the_area_of_polygon3(B,C,A) by A4,A3;
set abc=|.A-B.|*|.B-C.|*|.C-A.|;
set S=the_area_of_polygon3(B,C,A);
set an=sin angle (A,C,B);
A6: (abc*an/2)/S = (abc*an*1/2)*(1/S) by XCMPLX_1:99
.=(abc*(1/S))*1/2*an
.=k/2*an by XCMPLX_1:99;
k/2=|.A-B.|*|.B-C.|*|.C-A.|*(1/the_area_of_polygon3(B,C,A))/2
by XCMPLX_1:99
.=|.A-B.|*|.B-C.|*|.C-A.|/2*(1/the_area_of_polygon3(B,C,A))
.=|.A-B.|*|.B-C.|*|.C-A.|/2 *(1/the_area_of_polygon3(A,B,C)) by Thm27
.=|.A-B.|*|.B-C.|*|.C-A.|/2/the_area_of_polygon3(A,B,C) by XCMPLX_1:99;
hence thesis by A6,A5,EUCLID_6:43;
end;
theorem Thm34:
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)
proof
let A,B,C be Point of TOP-REAL 2;
assume
A1: A,B,C is_a_triangle; then
A2: B,C,A is_a_triangle & C,A,B is_a_triangle by MENELAUS:15;
A3: |.B-C.|=the_diameter_of_the_circumcircle(B,C,A)*sin angle (B,A,C)
by A2,Lm10;
thus|.A-B.|= the_diameter_of_the_circumcircle(A,B,C)*sin angle (A,C,B)
by A1,Lm10;
thus |.B-C.|=the_diameter_of_the_circumcircle(A,B,C)*sin angle (B,A,C)
by A3,Thm27;
|.C-A.|=the_diameter_of_the_circumcircle(C,A,B)*sin angle (C,B,A)
by A2,Lm10;
hence |.C-A.|=the_diameter_of_the_circumcircle(A,B,C)*sin angle (C,B,A)
by Thm27;
end;
theorem
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)
proof
let A,B,C be Point of TOP-REAL 2;
assume
A1: A,B,C is_a_triangle;
|.A-B.|=the_diameter_of_the_circumcircle(A,B,C)* sin (3*(angle(A,C,B)/3))
by A1,Lm10;
then |.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))) by Thm18;
hence thesis;
end;
theorem
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)
proof
let A,B,C,P be Point of TOP-REAL 2;
assume that
A1: A,B,P are_mutually_distinct and
A2: angle (P,B,A) = angle (C,B,A) /3 and
A3: angle (B,A,P) = angle (B,A,C) /3 and
A4: angle (A,P,B) < PI;
angle (A,P,B) + angle (P,B,A)+angle(B,A,P)=PI by A1,A4,EUCLID_3:47;
hence thesis by A1,A2,A3,EUCLID_6:6;
end;
Lm11:
for A,B,C be 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
let A,B,C be Point of TOP-REAL 2;
assume that
A1: A,B,C is_a_triangle and
A2: angle(C,B,A)<PI;
A3: A,B,C are_mutually_distinct by A1,EUCLID_6:20;
hence angle (C,B,A) + angle (B,A,C) + angle (A,C,B) = PI
by A2,EUCLID_3:47;
angle(C,B,A)=2*PI-angle(A,B,C) &
angle(B,A,C)=2*PI-angle(C,A,B) &
angle(A,C,B)=2*PI-angle(B,C,A) by A1,Thm20;
then angle (C,A,B) + angle (A,B,C) + angle (B,C,A)
= 6*PI - (angle(B,A,C) + angle(C,B,A) + angle(A,C,B))
.= 6*PI - PI by A2,A3,EUCLID_3:47
.= 5*PI;
hence thesis;
end;
Lm12:
for A,B,C be 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
let A,B,C be Point of TOP-REAL 2;
assume that
A1: A,B,C is_a_triangle and
A2: angle(C,B,A) <PI;
angle(C,B,A)+angle(B,A,C)+angle(A,C,B)=PI by A1,A2,Lm11;
hence thesis;
end;
theorem Thm35:
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)
proof
let A,B,C,P be Point of TOP-REAL 2;
assume that
A1: A,B,P are_mutually_distinct and
A2: angle (P,B,A) = angle (C,B,A) /3 and
A3: angle (B,A,P) = angle (B,A,C) /3 and
A4: angle (A,P,B) < PI and
A5: angle (C,B,A)/3 + angle (B,A,C)/3 + angle (A,C,B)/3 = PI/3;
angle (A,P,B) + angle (P,B,A)+angle(B,A,P)=PI by A1,A4,EUCLID_3:47;
hence thesis by A1,A2,A3 ,A5,EUCLID_6:6;
end;
theorem
for A,B,C be 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
let A,B,C be Point of TOP-REAL 2;
assume that
A1: A,B,C is_a_triangle and
A2: angle(C,A,B)<PI;
B,A,C is_a_triangle by A1,MENELAUS:15;
hence thesis by A2,Lm11;
end;
theorem
for A,B,C,P be 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
let A,B,C,P be Point of TOP-REAL 2;
assume that
A1: A,B,C is_a_triangle and
A2: angle(C,B,A)<PI and
A3: A,B,P are_mutually_distinct and
A4: angle (P,B,A) = angle (C,B,A) /3 and
A5: angle (B,A,P) = angle (B,A,C) /3 and
A6: angle (A,P,B) < PI;
A7: angle (C,B,A)/3 + angle (B,A,C)/3 + angle (A,C,B)/3 = PI/3
by A1,A2,Lm12;
A8: angle (A,P,B) + angle (P,B,A)+angle(B,A,P)=PI by A3,A6,EUCLID_3:47;
|.A-P.| * sin (PI - (angle (C,B,A)/3 + angle (B,A,C)/3)) =
|.A-B.| * sin (angle(C,B,A) /3) by A3,A4,EUCLID_6:6,A8,A5;
hence thesis by A7,Thm1;
end;
theorem
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
let A,B,C,P be Point of TOP-REAL 2;
assume that
A1: A,B,C is_a_triangle and
A2: A,B,P is_a_triangle and
A3: angle(C,B,A) < PI and
A4: angle (A,P,B) < PI and
A5: angle (P,B,A) = angle (C,B,A) /3 and
A6: angle (B,A,P) = angle (B,A,C) /3 and
A7: sin (PI/3 - angle(A,C,B)/3)<>0;
A8: angle (C,B,A)/3 + angle (B,A,C)/3 + angle (A,C,B)/3 = PI/3
by A1,A3,Lm12;
A,B,P are_mutually_distinct by A2,EUCLID_6:20; then
A9: |.A-P.| * sin (2*PI/3 +angle(A,C,B)/3) =
|.A-B.| * sin (angle(C,B,A) /3) by A5,A6,A4,A8,Thm35;
sin angle (A,C,B) = sin (3 * (angle(A,C,B)/3))
.= 4 * sin (angle(A,C,B)/3) * sin (PI/3 + angle(A,C,B)/3) *
sin (PI/3 - angle(A,C,B)/3) by Thm18; then
A10: |.A-P.| * sin (2*PI/3 + (angle(A,C,B)/3)) =
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)) *
sin (angle(C,B,A) /3) by A9,A1,Thm34;
|.A-P.| * sin (PI/3 - angle(A,C,B)/3) =
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)) *
sin (angle(C,B,A) /3) by A10,Thm7;
then |.A-P.| =
the_diameter_of_the_circumcircle(A,B,C) * 4 * sin (angle(A,C,B)/3) *
sin (PI/3 + angle(A,C,B)/3) * sin (angle(C,B,A) /3) *
sin (PI/3 - angle(A,C,B)/3) / sin (PI/3 - angle(A,C,B)/3)
by A7,XCMPLX_1:89; then
A11: |.A-P.| =
(the_diameter_of_the_circumcircle(A,B,C) * 4 * sin (angle(A,C,B)/3) *
sin (PI/3 + angle(A,C,B)/3) * sin (angle(C,B,A) /3)) *
(sin (PI/3 - angle(A,C,B)/3) / sin (PI/3 - angle(A,C,B)/3))
by XCMPLX_1:74;
sin (PI/3 - angle(A,C,B)/3) / sin (PI/3 - angle(A,C,B)/3) = 1
by A7,XCMPLX_1:60;
then |.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)
by A11,A1,Thm33;
hence thesis;
end;
begin :: Diameter of a circle
theorem Thm37:
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.|
proof
let A,B,C be Point of TOP-REAL 2 such that
A1: A,B,C are_mutually_distinct and
A2: C in LSeg(A,B);
|.B-A.|^2
=|.A-C.|^2+|.B-C.|^2 - 2 * |.A-C.| * |.B-C.| * (cos angle (A,C,B))
by EUCLID_6:7
.= |.A-C.|^2+|.B-C.|^2 - 2 * |.A-C.| * |.B-C.| * (-1)
by A1,A2,SIN_COS:77,EUCLID_6:8
.= |.A-C.|^2+ 2 * |.A-C.| * |.B-C.| + |.B-C.|^2
.= (|.A-C.|+|.B-C.|)^2 by SQUARE_1:4; then
A3: |.B-A.|=|.A-C.|+|.B-C.| or |.B-A.|=-(|.A-C.|+|.B-C.|) by SQUARE_1:40;
|. B - A .| >= 0 & |. A - C .| >= 0 & |. B - C .| >= 0 &
not |. B - A .| = 0 & not |. A - C .| = 0 & not |. B - C .| = 0
by A1,EUCLID_6:42;
then |.A-B.|=|.A-C.|+|.B-C.| by A3,EUCLID_6:43;
hence thesis by EUCLID_6:43;
end;
theorem Thm38:
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
proof
let A,B be Point of TOP-REAL 2, a,b be Real,r be positive Real such that
A1: A,B,|[a,b]| are_mutually_distinct and
A2: A in circle(a,b,r) & B in circle(a,b,r) and
A3: |[a,b]| in LSeg(A,B);
A4: circle(a,b,r)={p where p is Point of TOP-REAL 2: |.p-|[a,b]|.|=r}
by JGRAPH_6:def 5;
consider JA be Point of TOP-REAL 2 such that
A5: A=JA and
A6: |.JA-|[a,b]|.|=r by A2,A4;
consider JB be Point of TOP-REAL 2 such that
A7: B=JB and
A8: |.JB-|[a,b]|.|=r by A2,A4;
|.A-B.| = |.A-|[a,b]|.|+|.|[a,b]|-B.| by A1,A3,Thm37
.= r + r by A5,A6,A7,A8,EUCLID_6:43;
hence thesis;
end;
theorem
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
proof
let a,b be Real,r be positive Real, C be Subset of Euclid 2 such that
A1: C=circle(a,b,r);
A2: circle(a,b,r)={p where p is Point of TOP-REAL 2: |.p-|[a,b]|.|=r}
by JGRAPH_6:def 5;
A3: for x,y being Point of Euclid 2 st x in C & y in C holds dist(x,y) <= 2 * r
proof
let x,y be Point of Euclid 2 such that
A4: x in C and
A5: y in C;
consider JA be Point of TOP-REAL 2 such that
A6: x=JA and
A7: |.JA-|[a,b]|.|=r by A1,A4,A2;
consider JB be Point of TOP-REAL 2 such that
A8: y=JB and
A9: |.JB-|[a,b]|.|=r by A1,A5,A2;
reconsider KA=JA,KB=JB as Element of REAL 2 by EUCLID:22;
reconsider O=|[a,b]| as Element of REAL 2 by EUCLID:22;
reconsider O2=|[a,b]| as Point of Euclid 2 by EUCLID:67;
A10: dist(x,y)<=dist(x,O2)+dist(y,O2) by METRIC_1:4;
dist(y,O2)=|.KB-O.| by A8,SPPOL_1:5;
then
dist(x,y) <= |.KA-O.| + |.KB-O.| by A10,A6,SPPOL_1:5;
hence thesis by A7,A9;
end;
A12: C is bounded by A1,JORDAN2C:11;
for s be Real st (for x,y being Point of Euclid 2 st x in C & y in C holds
dist(x,y) <= s) holds 2 * r <= s
proof
let s be Real;
assume
A13: for x,y being Point of Euclid 2 st x in C & y in C holds
dist(x,y) <= s;
assume
A14: s < 2 * r;
set A1=|[a+r,b]|;
set B1=|[a-r,b]|;
A15: A1-|[a,b]|=|[a+r-a,b-b]| by EUCLID:62
.=|[r,0]|;
A16: B1-|[a,b]|=|[a-r-a,b-b]| by EUCLID:62
.=|[-r,0]|;
A17: r^2 + 0^2 =r^2 + 0 * 0 by SQUARE_1:def 1
.=r^2;
Re (r + 0 * <i>)=r & Im (r + 0 * <i>)=0 by COMPLEX1:12;
then |.cpx2euc(r + 0 * <i>).| = sqrt (r^2) by A17,EUCLID_3:24
.=r by SQUARE_1:22; then
A18: |.A1-|[a,b]|.|=r by A15,EUCLID_3:5; then
A19: A1 in circle(a,b,r) by A2;
A20: A1 in C by A18,A1,A2;
A21: (-r)^2 + 0^2 =(-r)^2 + 0 * 0 by SQUARE_1:def 1
.=r^2 by SQUARE_1:3;
Re (-r + 0 * <i>)=-r & Im (-r + 0 * <i>)=0 by COMPLEX1:12;
then |.cpx2euc(-r + 0 * <i>).| = sqrt (r^2) by A21,EUCLID_3:24
.=r by SQUARE_1:22; then
A22: |.|[-r,0]|.|=r by EUCLID_3:5; then
A23: B1 in circle(a,b,r) by A2,A16;
A24: B1 in C by A1,A2,A22,A16;
A25: |[a,b]| in LSeg(A1,B1)
proof
|[a+r,b]|+|[a-r,b]|=|[a+r+(a-r),b+b]| by EUCLID:56;
then 1/2*(A1+B1)=|[1/2*(2*a),1/2*(2*b)]| by EUCLID:58
.=|[a,b]|;
hence thesis by RLTOPSP1:69;
end;
A26: A1<>B1
proof
assume A1=B1;
then a+r=a-r & b=b by SPPOL_2:1;
then r=0;
hence contradiction;
end;
A27: A1<>|[a,b]|
proof
assume A1=|[a,b]|;
then a+r=a & b=b by SPPOL_2:1;
then r=0;
hence contradiction;
end;
A1,B1,|[a,b]| are_mutually_distinct
proof
B1<>|[a,b]|
proof
assume B1=|[a,b]|;
then a-r=a & b=b by SPPOL_2:1;
then -r=0;
hence contradiction;
end;
hence thesis by A26,A27;
end; then
A28: |.A1-B1.|=2 * r by A19,A23,A25,Thm38;
reconsider a1=A1,b1=B1 as Point of Euclid 2 by EUCLID:67;
reconsider A2=A1,B2=B1 as Element of REAL 2 by EUCLID:22;
Euclid 2=MetrStruct(#REAL 2,Pitag_dist 2#) by EUCLID:def 7;
then dist(a1,b1)=(Pitag_dist 2).(A1,B1) by METRIC_1:def 1
.=|. A2 - B2 .| by EUCLID:def 6
.= 2 * r by A28;
hence contradiction by A14,A20,A24,A13;
end;
hence thesis by A3,A12,A1,TBSP_1:def 8;
end;