:: Inverse Trigonometric Functions Arcsin and Arccos
:: by Artur Korni{\l}owicz and Yasunari Shidama
::
:: Received September 25, 2004
:: Copyright (c) 2004-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 NUMBERS, XREAL_0, INT_1, CARD_1, XXREAL_0, ARYTM_3, ARYTM_1,
FUNCT_1, RELAT_1, TARSKI, XBOOLE_0, SIN_COS, XXREAL_1, SQUARE_1, REAL_1,
ORDINAL2, VALUED_0, PARTFUN1, FDIFF_1, SIN_COS6, ORDINAL1;
notations TARSKI, XBOOLE_0, SUBSET_1, ORDINAL1, NUMBERS, XCMPLX_0, XXREAL_0,
XREAL_0, REAL_1, INT_1, SQUARE_1, RCOMP_1, RELAT_1, FUNCT_1, PARTFUN1,
RELSET_1, PARTFUN2, RFUNCT_2, FCONT_1, FDIFF_1, SIN_COS;
constructors PARTFUN1, ARYTM_0, REAL_1, SQUARE_1, RCOMP_1, PARTFUN2, RFUNCT_2,
FCONT_1, FDIFF_1, COMSEQ_3, SIN_COS, RVSUM_1, RELSET_1;
registrations FUNCT_1, RELSET_1, XCMPLX_0, XXREAL_0, XREAL_0, SQUARE_1, INT_1,
RCOMP_1, RFUNCT_2, SIN_COS, VALUED_0, ORDINAL1;
requirements SUBSET, NUMERALS, ARITHM, REAL;
definitions TARSKI, XBOOLE_0, FUNCT_1, XXREAL_0;
equalities SQUARE_1;
expansions FUNCT_1;
theorems RELAT_1, SIN_COS, FUNCT_1, COMPTRIG, FDIFF_1, FDIFF_2, RFUNCT_2,
XCMPLX_1, INT_1, XBOOLE_0, SQUARE_1, COMPLEX2, FCONT_3, FCONT_1, XREAL_1,
XXREAL_0, XXREAL_1, XBOOLE_1;
schemes INT_1;
begin :: Preliminaries
reserve r,r1,r2, s,x for Real,
i for Integer;
theorem Th1:
0 <= r & r < s implies [\ r/s /] = 0
proof
assume
A1: 0 <= r & r < s;
then r/s < s/s by XREAL_1:74;
then r/s-1 < s/s-1 by XREAL_1:9;
then r/s-1 < 1-1 by A1,XCMPLX_1:60;
hence thesis by A1,INT_1:def 6;
end;
theorem Th2:
for f being Function, X, Y being set st f|X is one-to-one & Y c=
X holds f|Y is one-to-one
proof
let f be Function, X, Y be set such that
A1: f|X is one-to-one and
A2: Y c= X;
let x, y be object;
A3: dom (f|Y) = dom f /\ Y by RELAT_1:61;
assume
A4: x in dom (f|Y);
then
A5: x in Y by A3,XBOOLE_0:def 4;
x in dom f by A3,A4,XBOOLE_0:def 4;
then x in dom f /\ X by A2,A5,XBOOLE_0:def 4;
then
A6: x in dom (f|X) by RELAT_1:61;
assume
A7: y in dom (f|Y);
then
A8: y in Y by A3,XBOOLE_0:def 4;
y in dom f by A3,A7,XBOOLE_0:def 4;
then y in dom f /\ X by A2,A8,XBOOLE_0:def 4;
then
A9: y in dom (f|X) by RELAT_1:61;
assume
A10: (f|Y).x = (f|Y).y;
(f|X).x = f.x by A2,A5,FUNCT_1:49
.= (f|Y).x by A5,FUNCT_1:49
.= f.y by A8,A10,FUNCT_1:49
.= (f|X).y by A2,A8,FUNCT_1:49;
hence thesis by A1,A6,A9;
end;
begin :: sine and cosine
theorem Th3:
-1 <= sin r
proof
sin.r in [.-1,1.] by COMPTRIG:27;
then sin r in [.-1,1.] by SIN_COS:def 17;
hence thesis by XXREAL_1:1;
end;
theorem Th4:
sin r <= 1
proof
sin.r in [.-1,1.] by COMPTRIG:27;
then sin r in [.-1,1.] by SIN_COS:def 17;
hence thesis by XXREAL_1:1;
end;
theorem Th5:
-1 <= cos r
proof
cos.r in [.-1,1.] by COMPTRIG:27;
then cos r in [.-1,1.] by SIN_COS:def 19;
hence thesis by XXREAL_1:1;
end;
theorem Th6:
cos r <= 1
proof
cos.r in [.-1,1.] by COMPTRIG:27;
then cos r in [.-1,1.] by SIN_COS:def 19;
hence thesis by XXREAL_1:1;
end;
deffunc T(Integer) = 2*PI*$1;
Lm1: [.-PI/2+T(0),PI/2+T(0).] = [.-PI/2,PI/2.];
Lm2: [.PI/2+T(0),3/2*PI+T(0).] = [.PI/2,3/2*PI.];
Lm3: [.T(0),PI+T(0).] = [.0,PI.];
Lm4: [.PI+T(0),2*PI+T(0).] = [.PI,2*PI.];
Lm5: r^2 + s^2 = 1 implies -1 <= r & r <= 1
proof
s^2 >= 0 by XREAL_1:63;
then -s^2 <= -0;
then r^2 - (r^2 + s^2) <= 0;
hence thesis by SQUARE_1:43;
end;
registration
cluster PI -> positive;
coherence
proof
PI in ]. 0, 4 .[ by SIN_COS:def 28;
hence PI > 0 by XXREAL_1:4;
end;
end;
Lm6: PI/2 < PI/1 by XREAL_1:76;
Lm7: 1*PI < 3/2*PI by XREAL_1:68;
Lm8: 0+T(1) < PI/2+T(1) by XREAL_1:6;
Lm9: 3/2*PI < 2*PI by XREAL_1:68;
Lm10: 1*PI < 2*PI by XREAL_1:68;
theorem Th7:
sin(-PI/2) = -1 & sin.-PI/2 = -1
proof
sin.(-PI/2) = sin.(-PI/2+2*PI) by SIN_COS:78
.= -1 by SIN_COS:76;
hence thesis by SIN_COS:def 17;
end;
theorem Th8:
sin.r = sin.(r+2*PI*i)
proof
thus sin.r = sin r by SIN_COS:def 17
.= sin(r+2*PI*i) by COMPLEX2:8
.= sin.(r+2*PI*i) by SIN_COS:def 17;
end;
theorem Th9:
cos(-PI/2) = 0 & cos.-PI/2 = 0
proof
cos.(-PI/2) = cos.(-PI/2+2*PI) by SIN_COS:78
.= 0 by SIN_COS:76;
hence thesis by SIN_COS:def 19;
end;
theorem Th10:
cos.r = cos.(r+2*PI*i)
proof
thus cos.r = cos r by SIN_COS:def 19
.= cos(r+2*PI*i) by COMPLEX2:9
.= cos.(r+2*PI*i) by SIN_COS:def 19;
end;
theorem Th11:
2*PI*i < r & r < PI+2*PI*i implies sin r > 0
proof
assume T(i) < r & r < PI+T(i);
then T(i)-T(i) < r-T(i) & r-T(i) < PI+T(i)-T(i) by XREAL_1:9;
then r-T(i) in ].0,PI.[ by XXREAL_1:4;
then sin.(r+T(-i)) > 0 by COMPTRIG:7;
then sin.r > 0 by Th8;
hence thesis by SIN_COS:def 17;
end;
theorem Th12:
PI+2*PI*i < r & r < 2*PI+2*PI*i implies sin r < 0
proof
assume PI+T(i) < r & r < 2*PI+T(i);
then PI+T(i)-T(i) < r-T(i) & r-T(i) < 2*PI+T(i)-T(i) by XREAL_1:9;
then r-T(i) in ].PI,2*PI.[ by XXREAL_1:4;
then sin.(r+T(-i)) < 0 by COMPTRIG:9;
then sin.r < 0 by Th8;
hence thesis by SIN_COS:def 17;
end;
theorem Th13:
-PI/2+2*PI*i < r & r < PI/2+2*PI*i implies cos r > 0
proof
assume that
A1: -PI/2+T(i) < r and
A2: r < PI/2+T(i);
r+PI/2 < PI/2+T(i)+PI/2 by A2,XREAL_1:6;
then
A3: r+PI/2 < PI+T(i);
A4: sin(r+PI/2) = cos r by SIN_COS:79;
-PI/2+T(i)+PI/2 < r+PI/2 by A1,XREAL_1:6;
hence thesis by A3,A4,Th11;
end;
theorem Th14:
PI/2+2*PI*i < r & r < 3/2*PI+2*PI*i implies cos r < 0
proof
assume that
A1: PI/2+T(i) < r and
A2: r < 3/2*PI+T(i);
PI/2+T(i)+PI/2 < r+PI/2 by A1,XREAL_1:6;
then
A3: PI+T(i) < r+PI/2;
r+PI/2 < 3/2*PI+T(i)+PI/2 by A2,XREAL_1:6;
then
A4: r+PI/2 < 2*PI+T(i);
sin(r+PI/2) = cos r by SIN_COS:79;
hence thesis by A3,A4,Th12;
end;
theorem Th15:
3/2*PI+2*PI*i < r & r < 2*PI+2*PI*i implies cos r > 0
proof
assume that
A1: 3/2*PI+T(i) < r and
A2: r < 2*PI+T(i);
3/2*PI+T(i)-PI < r-PI by A1,XREAL_1:9;
then
A3: PI/2+T(i) < r-PI;
PI+T(i) < 3/2*PI+T(i) & r-PI < 2*PI+T(i)-PI by A2,COMPTRIG:5,XREAL_1:6,9;
then
A4: r-PI < 3/2*PI+T(i) by XXREAL_0:2;
cos(r-PI) = cos(-(PI-r)) .= cos(PI+-r) by SIN_COS:31
.= -cos(-r) by SIN_COS:79
.= -cos r by SIN_COS:31;
hence thesis by A3,A4,Th14;
end;
theorem
2*PI*i <= r & r <= PI+2*PI*i implies sin r >= 0
proof
assume
A1: 2*PI*i <= r & r <= PI+2*PI*i;
per cases by A1,XXREAL_0:1;
suppose
2*PI*i < r & r < PI+2*PI*i;
hence thesis by Th11;
end;
suppose
A2: 2*PI*i = r;
sin(0+2*PI*i) = sin 0 by COMPLEX2:8;
hence thesis by A2,SIN_COS:31;
end;
suppose
r = PI+2*PI*i;
hence thesis by COMPLEX2:8,SIN_COS:77;
end;
end;
theorem
PI+2*PI*i <= r & r <= 2*PI+2*PI*i implies sin r <= 0
proof
assume PI+2*PI*i <= r & r <= 2*PI+2*PI*i;
then PI+2*PI*i < r & r < 2*PI+2*PI*i or PI+2*PI*i = r or r = 2*PI+2*PI*i by
XXREAL_0:1;
hence thesis by Th12,COMPLEX2:8,SIN_COS:77;
end;
theorem
-PI/2+2*PI*i <= r & r <= PI/2+2*PI*i implies cos r >= 0
proof
assume -PI/2+2*PI*i <= r & r <= PI/2+2*PI*i;
then
-PI/2+2*PI*i < r & r < PI/2+2*PI*i or -PI/2+2*PI*i = r or r = PI/2+2*PI*
i by XXREAL_0:1;
hence thesis by Th9,Th13,COMPLEX2:9,SIN_COS:77;
end;
theorem
PI/2+2*PI*i <= r & r <= 3/2*PI+2*PI*i implies cos r <= 0
proof
assume PI/2+2*PI*i <= r & r <= 3/2*PI+2*PI*i;
then
PI/2+2*PI*i < r & r < 3/2*PI+2*PI*i or PI/2+2*PI*i = r or r = 3/2*PI+2*
PI*i by XXREAL_0:1;
hence thesis by Th14,COMPLEX2:9,SIN_COS:77;
end;
theorem
3/2*PI+2*PI*i <= r & r <= 2*PI+2*PI*i implies cos r >= 0
proof
assume
A1: 3/2*PI+2*PI*i <= r & r <= 2*PI+2*PI*i;
per cases by A1,XXREAL_0:1;
suppose
3/2*PI+2*PI*i < r & r < 2*PI+2*PI*i;
hence thesis by Th15;
end;
suppose
3/2*PI+2*PI*i = r;
hence thesis by COMPLEX2:9,SIN_COS:77;
end;
suppose
r = 2*PI+2*PI*i;
hence thesis by COMPLEX2:9,SIN_COS:77;
end;
end;
theorem Th21:
2*PI*i <= r & r < 2*PI+2*PI*i & sin r = 0 implies r = 2*PI*i or r = PI+2*PI*i
proof
assume
A1: T(i) <= r & r < 2*PI+T(i);
assume
A2: sin r = 0;
then
A3: r <= PI+T(i) or 2*PI+T(i) <= r by Th12;
r <= T(i) or r >= PI+T(i) by A2,Th11;
hence thesis by A1,A3,XXREAL_0:1;
end;
theorem Th22:
2*PI*i <= r & r < 2*PI+2*PI*i & cos r = 0 implies r = PI/2+2*PI*
i or r = 3/2*PI+2*PI*i
proof
assume that
A1: T(i) <= r and
A2: r < 2*PI+T(i);
A3: -PI/2+T(i) < 0+T(i) by XREAL_1:6;
assume
A4: cos r = 0;
then
A5: PI/2+T(i) >= r or r >= 3/2*PI+T(i) by Th14;
-PI/2+T(i) >= r or r >= PI/2+T(i) by A4,Th13;
then r = PI/2+T(i) or r = 3/2*PI+T(i) or r > 3/2*PI+T(i) by A1,A5,A3,
XXREAL_0:1,2;
hence thesis by A2,A4,Th15;
end;
theorem Th23:
sin r = -1 implies r = 3/2*PI + 2*PI*[\r/(2*PI)/]
proof
set i = [\r/(2*PI)/];
consider w being Real such that
A1: w = (2*PI)*-i+r and
A2: 0 <= w & w < 2*PI by COMPLEX2:1;
assume
A3: sin r = -1;
then (cos r)*(cos r)+(-1)*(-1) = 1 by SIN_COS:29;
then
A4: cos r = 0;
0+T(i) <= w+T(i) & w+T(i) < 2*PI+T(i) by A2,XREAL_1:6;
then r = PI/2+T(i) or r = 3/2*PI+T(i) by A1,A4,Th22;
hence thesis by A3,COMPLEX2:8,SIN_COS:77;
end;
theorem Th24:
sin r = 1 implies r = PI/2 + 2*PI*[\r/(2*PI)/]
proof
set i = [\r/(2*PI)/];
consider w being Real such that
A1: w = (2*PI)*-i+r and
A2: 0 <= w & w < 2*PI by COMPLEX2:1;
assume
A3: sin r = 1;
then (cos r)*(cos r)+1*1 = 1 by SIN_COS:29;
then
A4: cos r = 0;
0+T(i) <= w+T(i) & w+T(i) < 2*PI+T(i) by A2,XREAL_1:6;
then r = PI/2+T(i) or r = 3/2*PI+T(i) by A1,A4,Th22;
hence thesis by A3,COMPLEX2:8,SIN_COS:77;
end;
theorem Th25:
cos r = -1 implies r = PI + 2*PI*[\r/(2*PI)/]
proof
set i = [\r/(2*PI)/];
consider w being Real such that
A1: w = (2*PI)*-i+r and
A2: 0 <= w & w < 2*PI by COMPLEX2:1;
assume
A3: cos r = -1;
then (sin r)*(sin r)+(-1)*(-1) = 1 by SIN_COS:29;
then
A4: sin r = 0;
0+T(i) <= w+T(i) & w+T(i) < 2*PI+T(i) by A2,XREAL_1:6;
then r = 0+T(i) or r = PI+T(i) by A1,A4,Th21;
hence thesis by A3,COMPLEX2:9,SIN_COS:31;
end;
theorem Th26:
cos r = 1 implies r = 2*PI*[\r/(2*PI)/]
proof
set i = [\r/(2*PI)/];
consider w being Real such that
A1: w = (2*PI)*-i+r and
A2: 0 <= w & w < 2*PI by COMPLEX2:1;
assume
A3: cos r = 1;
then (sin r)*(sin r)+1*1 = 1 by SIN_COS:29;
then
A4: sin r = 0;
0+T(i) <= w+T(i) & w+T(i) < 2*PI+T(i) by A2,XREAL_1:6;
then r = 0+T(i) or r = PI+T(i) by A1,A4,Th21;
hence thesis by A3,COMPLEX2:9,SIN_COS:77;
end;
theorem Th27:
0 <= r & r <= 2*PI & sin r = -1 implies r = 3/2*PI
proof
assume that
A1: 0 <= r and
A2: r <= 2*PI and
A3: sin r = -1;
A4: r = 2*PI or r < 2*PI by A2,XXREAL_0:1;
thus r = 3/2*PI + 2*PI*[\r/(2*PI)/] by A3,Th23
.= 3/2*PI + 2*PI*0 by A1,A3,A4,Th1,SIN_COS:77
.= 3/2*PI;
end;
theorem Th28:
0 <= r & r <= 2*PI & sin r = 1 implies r = PI/2
proof
assume that
A1: 0 <= r and
A2: r <= 2*PI and
A3: sin r = 1;
A4: r = 2*PI or r < 2*PI by A2,XXREAL_0:1;
thus r = PI/2 + 2*PI*[\r/(2*PI)/] by A3,Th24
.= PI/2 + 2*PI*0 by A1,A3,A4,Th1,SIN_COS:77
.= PI/2;
end;
:: case cos(r) = 1 has been proved as UNIROOTS:17, COMPTRIG:79
theorem Th29:
0 <= r & r <= 2*PI & cos r = -1 implies r = PI
proof
assume that
A1: 0 <= r and
A2: r <= 2*PI and
A3: cos r = -1;
A4: r = 2*PI or r < 2*PI by A2,XXREAL_0:1;
thus r = PI + 2*PI*[\r/(2*PI)/] by A3,Th25
.= PI + 2*PI*0 by A1,A3,A4,Th1,SIN_COS:77
.= PI;
end;
theorem Th30:
0 <= r & r < PI/2 implies sin r < 1
proof
assume that
A1: 0 <= r and
A2: r < PI/2 and
A3: sin r >= 1;
A4: sin r <= 1 by Th4;
1/2*PI <= 2*PI by XREAL_1:64;
then r < 2*PI by A2,XXREAL_0:2;
hence thesis by A1,A2,A3,A4,Th28,XXREAL_0:1;
end;
theorem Th31:
0 <= r & r < 3/2*PI implies sin r > -1
proof
assume that
A1: 0 <= r and
A2: r < 3/2*PI and
A3: sin r <= -1;
A4: sin r >= -1 by Th3;
r <= 2*PI by A2,Lm9,XXREAL_0:2;
hence thesis by A1,A2,A3,A4,Th27,XXREAL_0:1;
end;
theorem Th32:
3/2*PI < r & r <= 2*PI implies sin r > -1
proof
assume
A1: 3/2*PI < r & r <= 2*PI & sin r <= -1;
sin r >= -1 by Th3;
hence thesis by A1,Th27,XXREAL_0:1;
end;
theorem Th33:
PI/2 < r & r <= 2*PI implies sin r < 1
proof
assume
A1: PI/2 < r & r <= 2*PI & sin r >= 1;
sin r <= 1 by Th4;
hence thesis by A1,Th28,XXREAL_0:1;
end;
theorem Th34:
0 < r & r < 2*PI implies cos r < 1
proof
assume 0 < r & r < 2*PI;
then
A1: cos r <> 1 by COMPTRIG:61;
cos r <= 1 by Th6;
hence thesis by A1,XXREAL_0:1;
end;
theorem Th35:
0 <= r & r < PI implies cos r > -1
proof
assume that
A1: 0 <= r and
A2: r < PI;
A3: cos r >= -1 by Th5;
r <= 2*PI by A2,Lm10,XXREAL_0:2;
hence thesis by A1,A2,A3,Th29,XXREAL_0:1;
end;
theorem Th36:
PI < r & r <= 2*PI implies cos r > -1
proof
assume
A1: PI < r & r <= 2*PI;
cos r >= -1 by Th5;
hence thesis by A1,Th29,XXREAL_0:1;
end;
theorem
2*PI*i <= r & r < PI/2+2*PI*i implies sin r < 1
proof
assume that
A1: T(i) <= r & r < PI/2+T(i) and
A2: sin r >= 1;
A3: T(i)-T(i) <= r-T(i) & r-T(i) < PI/2+T(i)-T(i) by A1,XREAL_1:9;
A4: sin r <= 1 by Th4;
sin(r-T(i)) = sin(r+T(-i)) .= sin r by COMPLEX2:8
.= 1 by A2,A4,XXREAL_0:1;
hence thesis by A3,Th30;
end;
theorem
2*PI*i <= r & r < 3/2*PI+2*PI*i implies sin r > -1
proof
assume that
A1: T(i) <= r & r < 3/2*PI+T(i) and
A2: sin r <= -1;
A3: T(i)-T(i) <= r-T(i) & r-T(i) < 3/2*PI+T(i)-T(i) by A1,XREAL_1:9;
A4: sin r >= -1 by Th3;
sin(r-T(i)) = sin(r+T(-i)) .= sin r by COMPLEX2:8
.= -1 by A2,A4,XXREAL_0:1;
hence thesis by A3,Th31;
end;
theorem
3/2*PI+2*PI*i < r & r <= 2*PI+2*PI*i implies sin r > -1
proof
assume that
A1: 3/2*PI+T(i) < r & r <= 2*PI+T(i) and
A2: sin r <= -1;
A3: 3/2*PI+T(i)-T(i) < r-T(i) & r-T(i) <= 2*PI+T(i)-T(i) by A1,XREAL_1:9;
A4: sin r >= -1 by Th3;
sin(r-T(i)) = sin(r+T(-i)) .= sin r by COMPLEX2:8
.= -1 by A2,A4,XXREAL_0:1;
hence thesis by A3,Th32;
end;
theorem
PI/2+2*PI*i < r & r <= 2*PI+2*PI*i implies sin r < 1
proof
assume that
A1: PI/2+T(i) < r & r <= 2*PI+T(i) and
A2: sin r >= 1;
A3: PI/2+T(i)-T(i) < r-T(i) & r-T(i) <= 2*PI+T(i)-T(i) by A1,XREAL_1:9;
A4: sin r <= 1 by Th4;
sin(r-T(i)) = sin(r+T(-i)) .= sin r by COMPLEX2:8
.= 1 by A2,A4,XXREAL_0:1;
hence thesis by A3,Th33;
end;
theorem
2*PI*i < r & r < 2*PI+2*PI*i implies cos r < 1
proof
assume that
A1: T(i) < r & r < 2*PI+T(i) and
A2: cos r >= 1;
A3: T(i)-T(i) < r-T(i) & r-T(i) < 2*PI+T(i)-T(i) by A1,XREAL_1:9;
A4: cos r <= 1 by Th6;
cos(r-T(i)) = cos(r+T(-i)) .= cos r by COMPLEX2:9
.= 1 by A2,A4,XXREAL_0:1;
hence thesis by A3,Th34;
end;
theorem
2*PI*i <= r & r < PI+2*PI*i implies cos r > -1
proof
assume that
A1: T(i) <= r & r < PI+T(i) and
A2: cos r <= -1;
A3: T(i)-T(i) <= r-T(i) & r-T(i) < PI+T(i)-T(i) by A1,XREAL_1:9;
A4: cos r >= -1 by Th5;
cos(r-T(i)) = cos(r+T(-i)) .= cos r by COMPLEX2:9
.= -1 by A2,A4,XXREAL_0:1;
hence thesis by A3,Th35;
end;
theorem
PI+2*PI*i < r & r <= 2*PI+2*PI*i implies cos r > -1
proof
assume that
A1: PI+T(i) < r & r <= 2*PI+T(i) and
A2: cos r <= -1;
A3: PI+T(i)-T(i) < r-T(i) & r-T(i) <= 2*PI+T(i)-T(i) by A1,XREAL_1:9;
A4: cos r >= -1 by Th5;
cos(r-T(i)) = cos(r+T(-i)) .= cos r by COMPLEX2:9
.= -1 by A2,A4,XXREAL_0:1;
hence thesis by A3,Th36;
end;
theorem
cos(2*PI*r) = 1 implies r in INT
proof
reconsider d = 2 as positive Real;
assume
A1: cos(2*PI*r) = 1;
assume not r in INT;
then r is not integer by INT_1:def 2;
then reconsider t = frac r as positive Real by INT_1:46;
set s = [\r/];
A2: r = s+t & d*PI*t < d*PI*1 by INT_1:42,43,XREAL_1:68;
cos(2*PI*(s+t)) = cos(2*PI*s+2*PI*t) .= cos(2*PI*t) by COMPLEX2:9;
hence contradiction by A1,A2,Th34;
end;
theorem Th45:
sin.:[.-PI/2,PI/2.] = [.-1,1.] by COMPTRIG:30,RELAT_1:115;
theorem Th46:
sin.:].-PI/2,PI/2.[ = ].-1,1.[
proof
sin|].-PI/2,PI/2.[ c= sin|[.-PI/2,PI/2.] by RELAT_1:75,XXREAL_1:25;
then
A1: rng (sin|].-PI/2,PI/2.[) c= rng (sin|[.-PI/2,PI/2.]) by RELAT_1:11;
A2: rng (sin|].-PI/2,PI/2.[) = sin.:].-PI/2,PI/2.[ by RELAT_1:115;
thus sin.:].-PI/2,PI/2.[ c= ].-1,1.[
proof
let x be object;
assume
A3: x in sin.:].-PI/2,PI/2.[;
then consider a being object such that
A4: a in dom sin and
A5: a in ].-PI/2,PI/2.[ and
A6: sin.a = x by FUNCT_1:def 6;
reconsider a, x as Real by A4,A6;
set i = [\a/(2*PI)/];
A7: T(i)/(2*PI*1) = i/1 by XCMPLX_1:91;
A8: sin.a = sin a by SIN_COS:def 17;
A9: now
assume x = 1;
then
A10: a = PI/2+T(i) by A6,A8,Th24;
then PI/2+T(i) < PI/2 by A5,XXREAL_1:4;
then PI/2+T(i)-PI/2 < PI/2-PI/2 by XREAL_1:9;
then i < 0;
then
A11: i <= -1 by INT_1:8;
-PI/2 < PI/2+T(i) by A5,A10,XXREAL_1:4;
then -PI/2-PI/2 < PI/2+T(i)-PI/2 by XREAL_1:9;
then ((-1)*PI)/(2*PI) < i by A7,XREAL_1:74;
then (-1)/2 < i by XCMPLX_1:91;
hence contradiction by A11,XXREAL_0:2;
end;
A12: now
assume x = -1;
then
A13: a = 3/2*PI+T(i) by A6,A8,Th23;
then -PI/2 < 3/2*PI+T(i) by A5,XXREAL_1:4;
then -PI/2-3/2*PI < 3/2*PI+T(i)-3/2*PI by XREAL_1:9;
then (-2*PI)/(2*PI) < i by A7,XREAL_1:74;
then -((2*PI)/(2*PI)) < i by XCMPLX_1:187;
then -1 < i by XCMPLX_1:60;
then
A14: -1+1 <= i by INT_1:7;
3/2*PI+T(i) < PI/2 by A5,A13,XXREAL_1:4;
then 3/2*PI+T(i)-3/2*PI < PI/2-3/2*PI by XREAL_1:9;
then i < (-PI)/(2*PI) by A7,XREAL_1:74;
hence contradiction by A14,XCMPLX_1:91;
end;
x <= 1 by A1,A2,A3,COMPTRIG:30,XXREAL_1:1;
then
A15: x < 1 by A9,XXREAL_0:1;
-1 <= x by A1,A2,A3,COMPTRIG:30,XXREAL_1:1;
then -1 < x by A12,XXREAL_0:1;
hence thesis by A15,XXREAL_1:4;
end;
let a be object;
assume
A16: a in ].-1,1.[;
then reconsider a as Real;
-1 < a & a < 1 by A16,XXREAL_1:4;
then a in rng (sin|[.-PI/2,PI/2.]) by COMPTRIG:30,XXREAL_1:1;
then consider x being object such that
A17: x in dom (sin|[.-PI/2,PI/2.]) and
A18: (sin|[.-PI/2,PI/2.]).x = a by FUNCT_1:def 3;
reconsider x as Real by A17;
A19: sin.x = a by A17,A18,FUNCT_1:47;
dom (sin|[.-PI/2,PI/2.]) = [.-PI/2,PI/2.] by RELAT_1:62,SIN_COS:24;
then -PI/2 <= x & x <= PI/2 by A17,XXREAL_1:1;
then -PI/2 < x & x < PI/2 or -PI/2 = x or PI/2 = x by XXREAL_0:1;
then x in ].-PI/2,PI/2.[ by A16,A19,Th7,SIN_COS:76,XXREAL_1:4;
hence thesis by A19,FUNCT_1:def 6,SIN_COS:24;
end;
theorem
sin.:[.PI/2,3/2*PI.] = [.-1,1.] by COMPTRIG:31,RELAT_1:115;
theorem
sin.:].PI/2,3/2*PI.[ = ].-1,1.[
proof
sin|].PI/2,3/2*PI.[ c= sin|[.PI/2,3/2*PI.] by RELAT_1:75,XXREAL_1:25;
then
A1: rng (sin|].PI/2,3/2*PI.[) c= rng (sin|[.PI/2,3/2*PI.]) by RELAT_1:11;
A2: rng (sin|].PI/2,3/2*PI.[) = sin.:].PI/2,3/2*PI.[ by RELAT_1:115;
thus sin.:].PI/2,3/2*PI.[ c= ].-1,1.[
proof
let x be object;
assume
A3: x in sin.:].PI/2,3/2*PI.[;
then consider a being object such that
A4: a in dom sin and
A5: a in ].PI/2,3/2*PI.[ and
A6: sin.a = x by FUNCT_1:def 6;
reconsider a, x as Real by A4,A6;
set i = [\a/(2*PI)/];
A7: T(i)/(2*PI*1) = i/1 by XCMPLX_1:91;
A8: sin.a = sin a by SIN_COS:def 17;
A9: now
assume x = 1;
then
A10: a = PI/2+T(i) by A6,A8,Th24;
then PI/2 < PI/2+T(i) by A5,XXREAL_1:4;
then PI/2-PI/2 < PI/2+T(i)-PI/2 by XREAL_1:9;
then 0 < i;
then
A11: 0+1 <= i by INT_1:7;
PI/2+T(i) < 3/2*PI by A5,A10,XXREAL_1:4;
then PI/2+T(i)-PI/2 < 3/2*PI-PI/2 by XREAL_1:9;
then i < (1*PI)/(2*PI) by A7,XREAL_1:74;
then i < 1/2 by XCMPLX_1:91;
hence contradiction by A11,XXREAL_0:2;
end;
A12: now
assume x = -1;
then
A13: a = 3/2*PI+T(i) by A6,A8,Th23;
then 3/2*PI+T(i) < 3/2*PI by A5,XXREAL_1:4;
then 3/2*PI+T(i)-3/2*PI < 3/2*PI-3/2*PI by XREAL_1:9;
then i < 0;
then
A14: i <= -1 by INT_1:8;
PI/2 < 3/2*PI+T(i) by A5,A13,XXREAL_1:4;
then PI/2-3/2*PI < 3/2*PI+T(i)-3/2*PI by XREAL_1:9;
then ((-1)*PI)/(2*PI) < i by A7,XREAL_1:74;
then (-1)/2 < i by XCMPLX_1:91;
hence contradiction by A14,XXREAL_0:2;
end;
x <= 1 by A1,A2,A3,COMPTRIG:31,XXREAL_1:1;
then
A15: x < 1 by A9,XXREAL_0:1;
-1 <= x by A1,A2,A3,COMPTRIG:31,XXREAL_1:1;
then -1 < x by A12,XXREAL_0:1;
hence thesis by A15,XXREAL_1:4;
end;
let a be object;
assume
A16: a in ].-1,1.[;
then reconsider a as Real;
-1 < a & a < 1 by A16,XXREAL_1:4;
then a in rng (sin|[.PI/2,3/2*PI.]) by COMPTRIG:31,XXREAL_1:1;
then consider x being object such that
A17: x in dom (sin|[.PI/2,3/2*PI.]) and
A18: (sin|[.PI/2,3/2*PI.]).x = a by FUNCT_1:def 3;
reconsider x as Real by A17;
A19: sin.x = a by A17,A18,FUNCT_1:47;
dom (sin|[.PI/2,3/2*PI.]) = [.PI/2,3/2*PI.] by RELAT_1:62,SIN_COS:24;
then PI/2 <= x & x <= 3/2*PI by A17,XXREAL_1:1;
then PI/2 < x & x < 3/2*PI or PI/2 = x or 3/2*PI = x by XXREAL_0:1;
then x in ].PI/2,3/2*PI.[ by A16,A19,SIN_COS:76,XXREAL_1:4;
hence thesis by A19,FUNCT_1:def 6,SIN_COS:24;
end;
theorem Th49:
cos.:[.0,PI.] = [.-1,1.] by COMPTRIG:32,RELAT_1:115;
theorem Th50:
cos.:].0,PI.[ = ].-1,1.[
proof
cos|].0,PI.[ c= cos|[.0,PI.] by RELAT_1:75,XXREAL_1:25;
then
A1: rng (cos|].0,PI.[) c= rng (cos|[.0,PI.]) by RELAT_1:11;
A2: rng (cos|].0,PI.[) = cos.:].0,PI.[ by RELAT_1:115;
thus cos.:].0,PI.[ c= ].-1,1.[
proof
let x be object;
assume
A3: x in cos.:].0,PI.[;
then consider a being object such that
A4: a in dom cos and
A5: a in ].0,PI.[ and
A6: cos.a = x by FUNCT_1:def 6;
reconsider a, x as Real by A4,A6;
set i = [\a/(2*PI)/];
A7: T(i)/(2*PI*1) = i/1 by XCMPLX_1:91;
A8: cos.a = cos a by SIN_COS:def 19;
A9: now
assume x = 1;
then
A10: a = T(i) by A6,A8,Th26;
then T(i) < PI by A5,XXREAL_1:4;
then i < (1*PI)/(2*PI) by A7,XREAL_1:74;
then
A11: i < 1/2 by XCMPLX_1:91;
0 < i by A5,A10,XXREAL_1:4;
then 0+1 <= i by INT_1:7;
hence contradiction by A11,XXREAL_0:2;
end;
A12: now
assume x = -1;
then
A13: a = PI+T(i) by A6,A8,Th25;
then 0 < PI+T(i) by A5,XXREAL_1:4;
then 0-PI < PI+T(i)-PI by XREAL_1:9;
then (-PI)/(2*PI) < T(i)/(2*PI) by XREAL_1:74;
then -(1*PI)/(2*PI) < i by A7,XCMPLX_1:187;
then
A14: -1/2 < i by XCMPLX_1:91;
PI+T(i) < PI by A5,A13,XXREAL_1:4;
then PI+T(i)-PI < PI-PI by XREAL_1:9;
then i < 0;
then i <= -1 by INT_1:8;
hence contradiction by A14,XXREAL_0:2;
end;
x <= 1 by A1,A2,A3,COMPTRIG:32,XXREAL_1:1;
then
A15: x < 1 by A9,XXREAL_0:1;
-1 <= x by A1,A2,A3,COMPTRIG:32,XXREAL_1:1;
then -1 < x by A12,XXREAL_0:1;
hence thesis by A15,XXREAL_1:4;
end;
let a be object;
assume
A16: a in ].-1,1.[;
then reconsider a as Real;
-1 < a & a < 1 by A16,XXREAL_1:4;
then a in rng (cos|[.0,PI.]) by COMPTRIG:32,XXREAL_1:1;
then consider x being object such that
A17: x in dom (cos|[.0,PI.]) and
A18: (cos|[.0,PI.]).x = a by FUNCT_1:def 3;
reconsider x as Real by A17;
A19: cos.x = a by A17,A18,FUNCT_1:47;
A20: dom (cos|[.0,PI.]) = [.0,PI.] by RELAT_1:62,SIN_COS:24;
then x <= PI by A17,XXREAL_1:1;
then 0 < x & x < PI or 0 = x or PI = x by A17,A20,XXREAL_0:1,XXREAL_1:1;
then x in ].0,PI.[ by A16,A19,SIN_COS:30,76,XXREAL_1:4;
hence thesis by A19,FUNCT_1:def 6,SIN_COS:24;
end;
theorem
cos.:[.PI,2*PI.] = [.-1,1.] by COMPTRIG:33,RELAT_1:115;
theorem
cos.:].PI,2*PI.[ = ].-1,1.[
proof
cos|].PI,2*PI.[ c= cos|[.PI,2*PI.] by RELAT_1:75,XXREAL_1:25;
then
A1: rng (cos|].PI,2*PI.[) c= rng (cos|[.PI,2*PI.]) by RELAT_1:11;
A2: rng (cos|].PI,2*PI.[) = cos.:].PI,2*PI.[ by RELAT_1:115;
thus cos.:].PI,2*PI.[ c= ].-1,1.[
proof
let x be object;
assume
A3: x in cos.:].PI,2*PI.[;
then consider a being object such that
A4: a in dom cos and
A5: a in ].PI,2*PI.[ and
A6: cos.a = x by FUNCT_1:def 6;
reconsider a, x as Real by A4,A6;
set i = [\a/(2*PI)/];
A7: T(i)/(2*PI*1) = i/1 by XCMPLX_1:91;
A8: cos.a = cos a by SIN_COS:def 19;
A9: now
assume x = 1;
then
A10: a = T(i) by A6,A8,Th26;
then T(i) < 2*PI by A5,XXREAL_1:4;
then i < 2*PI/(2*PI) by A7,XREAL_1:74;
then
A11: i < 1+0 by XCMPLX_1:60;
PI < T(i) by A5,A10,XXREAL_1:4;
hence contradiction by A7,A11,INT_1:7;
end;
A12: now
assume x = -1;
then
A13: a = PI+T(i) by A6,A8,Th25;
then PI < PI+T(i) by A5,XXREAL_1:4;
then PI-PI < PI+T(i)-PI by XREAL_1:9;
then 0/(2*PI) < i;
then
A14: 0+1 <= i by INT_1:7;
PI+T(i) < 2*PI by A5,A13,XXREAL_1:4;
then PI+T(i)-PI < 2*PI-PI by XREAL_1:9;
then i < (1*PI)/(2*PI) by A7,XREAL_1:74;
then i <= 1/2 by XCMPLX_1:91;
hence contradiction by A14,XXREAL_0:2;
end;
x <= 1 by A1,A2,A3,COMPTRIG:33,XXREAL_1:1;
then
A15: x < 1 by A9,XXREAL_0:1;
-1 <= x by A1,A2,A3,COMPTRIG:33,XXREAL_1:1;
then -1 < x by A12,XXREAL_0:1;
hence thesis by A15,XXREAL_1:4;
end;
let a be object;
assume
A16: a in ].-1,1.[;
then reconsider a as Real;
-1 < a & a < 1 by A16,XXREAL_1:4;
then a in rng (cos|[.PI,2*PI.]) by COMPTRIG:33,XXREAL_1:1;
then consider x being object such that
A17: x in dom (cos|[.PI,2*PI.]) and
A18: (cos|[.PI,2*PI.]).x = a by FUNCT_1:def 3;
reconsider x as Real by A17;
A19: cos.x = a by A17,A18,FUNCT_1:47;
dom (cos|[.PI,2*PI.]) = [.PI,2*PI.] by RELAT_1:62,SIN_COS:24;
then PI <= x & x <= 2*PI by A17,XXREAL_1:1;
then PI < x & x < 2*PI or PI = x or 2*PI = x by XXREAL_0:1;
then x in ].PI,2*PI.[ by A16,A19,SIN_COS:76,XXREAL_1:4;
hence thesis by A19,FUNCT_1:def 6,SIN_COS:24;
end;
Lm11: now
let i, r;
let p1, p2 be Real;
assume
A1: r in [.p1+T(i),p2+T(i).];
then r <= p2+T(i) by XXREAL_1:1;
then
A2: r+2*PI <= p2+T(i)+2*PI by XREAL_1:6;
p1+T(i) <= r by A1,XXREAL_1:1;
then p1+T(i)+2*PI <= r+2*PI by XREAL_1:6;
hence r+2*PI in [.p1+T(i+1),p2+T(i+1).] by A2,XXREAL_1:1;
end;
Lm12: now
let i, r;
let p1, p2 be Real;
assume r in [.p1+T(i),p2+T(i).] /\ REAL;
then r in [.p1+T(i),p2+T(i).] by XBOOLE_0:def 4;
then r+2*PI in [.p1+T(i+1),p2+T(i+1).] by Lm11;
hence r+2*PI in [.p1+T(i+1),p2+T(i+1).] /\ REAL by XBOOLE_0:def 4;
end;
Lm13: now
let i, r;
let p1, p2 be Real;
assume
A1: r in [.p1+T(i),p2+T(i).];
then r <= p2+T(i) by XXREAL_1:1;
then
A2: r-2*PI <= p2+T(i)-2*PI by XREAL_1:9;
p1+T(i) <= r by A1,XXREAL_1:1;
then p1+T(i)-2*PI <= r-2*PI by XREAL_1:9;
hence r-2*PI in [.p1+T(i-1),p2+T(i-1).] by A2,XXREAL_1:1;
end;
Lm14: now
let i, r;
let p1, p2 be Real;
assume r in [.p1+T(i),p2+T(i).] /\ REAL;
then r in [.p1+T(i),p2+T(i).] by XBOOLE_0:def 4;
then r-2*PI in [.p1+T(i-1),p2+T(i-1).] by Lm13;
hence r-2*PI in [.p1+T(i-1),p2+T(i-1).] /\ REAL by XBOOLE_0:def 4;
end;
theorem Th53:
sin|[.-PI/2+2*PI*i,PI/2+2*PI*i.] is increasing
proof
defpred P[Integer] means sin|[.-PI/2+T($1),PI/2+T($1).] is increasing;
A1: for i holds P[i] implies P[i-1] & P[i+1]
proof
let i such that
A2: P[i];
set Z = [.-PI/2+T(i-1+1),PI/2+T(i-1+1).];
thus P[i-1]
proof
set Y = [.-PI/2+T(i-1),PI/2+T(i-1).];
now
let r1,r2;
assume r1 in Y /\ dom sin & r2 in Y /\ dom sin;
then
A3: r1+2*PI in Z /\ dom sin & r2+2*PI in Z /\ dom sin by Lm12,SIN_COS:24;
assume r1 < r2;
then r1+2*PI < r2+2*PI by XREAL_1:6;
then sin.(r1+2*PI) < sin.(r2+2*PI*1) by A2,A3,RFUNCT_2:20;
then sin.(r1+2*PI*1) < sin.r2 by Th8;
hence sin.r1 < sin.r2 by Th8;
end;
hence thesis by RFUNCT_2:20;
end;
set Y = [.-PI/2+T(i+1),PI/2+T(i+1).];
A4: Z = [.-PI/2+T(i+1-1),PI/2+T(i+1-1).];
now
let r1, r2;
assume r1 in Y /\ dom sin & r2 in Y /\ dom sin;
then
A5: r1-2*PI in Z /\ dom sin & r2-2*PI in Z /\ dom sin by A4,Lm14,SIN_COS:24;
assume r1 < r2;
then r1-2*PI < r2-2*PI by XREAL_1:9;
then sin.(r1-2*PI) < sin.(r2+2*PI*(-1)) by A2,A5,RFUNCT_2:20;
then sin.(r1+2*PI*(-1)) < sin.r2 by Th8;
hence sin.r1 < sin.r2 by Th8;
end;
hence thesis by RFUNCT_2:20;
end;
A6: P[0] by COMPTRIG:23;
for i holds P[i] from INT_1:sch 4(A6,A1);
hence thesis;
end;
theorem Th54:
sin|[.PI/2+2*PI*i,3/2*PI+2*PI*i.] is decreasing
proof
defpred P[Integer] means sin|[.PI/2+T($1),3/2*PI+T($1).] is decreasing;
A1: for i holds P[i] implies P[i-1] & P[i+1]
proof
let i such that
A2: P[i];
set Z = [.PI/2+T(i-1+1),3/2*PI+T(i-1+1).];
thus P[i-1]
proof
set Y = [.PI/2+T(i-1),3/2*PI+T(i-1).];
now
let r1, r2;
assume r1 in Y /\ dom sin & r2 in Y /\ dom sin;
then
A3: r1+2*PI in Z /\ dom sin & r2+2*PI in Z /\ dom sin by Lm12,SIN_COS:24;
assume r1 < r2;
then r1+2*PI < r2+2*PI by XREAL_1:6;
then sin.(r1+2*PI) > sin.(r2+2*PI*1) by A2,A3,RFUNCT_2:21;
then sin.(r1+2*PI*1) > sin.r2 by Th8;
hence sin.r1 > sin.r2 by Th8;
end;
hence thesis by RFUNCT_2:21;
end;
set Y = [.PI/2+T(i+1),3/2*PI+T(i+1).];
A4: Z = [.PI/2+T(i+1-1),3/2*PI+T(i+1-1).];
now
let r1, r2;
assume r1 in Y /\ dom sin & r2 in Y /\ dom sin;
then
A5: r1-2*PI in Z /\ dom sin & r2-2*PI in Z /\ dom sin by A4,Lm14,SIN_COS:24;
assume r1 < r2;
then r1-2*PI < r2-2*PI by XREAL_1:9;
then sin.(r1-2*PI) > sin.(r2+2*PI*(-1)) by A2,A5,RFUNCT_2:21;
then sin.(r1+2*PI*(-1)) > sin.r2 by Th8;
hence sin.r1 > sin.r2 by Th8;
end;
hence thesis by RFUNCT_2:21;
end;
A6: P[0] by COMPTRIG:24;
for i holds P[i] from INT_1:sch 4(A6,A1);
hence thesis;
end;
theorem Th55:
cos|[.2*PI*i,PI+2*PI*i.] is decreasing
proof
defpred P[Integer] means cos|[.T($1),PI+T($1).] is decreasing;
A1: for i holds P[i] implies P[i-1] & P[i+1]
proof
let i such that
A2: P[i];
set Z = [.0+T(i-1+1),PI+T(i-1+1).];
thus P[i-1]
proof
set Y = [.T(i-1),PI+T(i-1).];
A3: Y = [.0+T(i-1),PI+T(i-1).];
now
let r1, r2;
assume r1 in Y /\ dom cos & r2 in Y /\ dom cos;
then
A4: r1+2*PI in Z /\ dom cos & r2+2*PI in Z /\ dom cos by A3,Lm12,SIN_COS:24
;
assume r1 < r2;
then r1+2*PI < r2+2*PI by XREAL_1:6;
then cos.(r1+2*PI) > cos.(r2+2*PI*1) by A2,A4,RFUNCT_2:21;
then cos.(r1+2*PI*1) > cos.r2 by Th10;
hence cos.r1 > cos.r2 by Th10;
end;
hence thesis by RFUNCT_2:21;
end;
set Y = [.T(i+1),PI+T(i+1).];
A5: Y = [.0+T(i+1),PI+T(i+1).] & Z = [.T(i+1-1),PI+T(i+1-1).];
now
let r1, r2;
assume r1 in Y /\ dom cos & r2 in Y /\ dom cos;
then
A6: r1-2*PI in Z /\ dom cos & r2-2*PI in Z /\ dom cos by A5,Lm14,SIN_COS:24;
assume r1 < r2;
then r1-2*PI < r2-2*PI by XREAL_1:9;
then cos.(r1-2*PI) > cos.(r2+2*PI*(-1)) by A2,A6,RFUNCT_2:21;
then cos.(r1+2*PI*(-1)) > cos.r2 by Th10;
hence cos.r1 > cos.r2 by Th10;
end;
hence thesis by RFUNCT_2:21;
end;
A7: P[0] by COMPTRIG:25;
for i holds P[i] from INT_1:sch 4(A7,A1);
hence thesis;
end;
theorem Th56:
cos|[.PI+2*PI*i,2*PI+2*PI*i.] is increasing
proof
defpred P[Integer] means cos|[.PI+T($1),2*PI+T($1).] is increasing;
A1: for i holds P[i] implies P[i-1] & P[i+1]
proof
let i such that
A2: P[i];
set Z = [.PI+T(i-1+1),2*PI+T(i-1+1).];
thus P[i-1]
proof
set Y = [.PI+T(i-1),2*PI+T(i-1).];
now
let r1, r2;
assume r1 in Y /\ dom cos & r2 in Y /\ dom cos;
then
A3: r1+2*PI in Z /\ dom cos & r2+2*PI in Z /\ dom cos by Lm12,SIN_COS:24;
assume r1 < r2;
then r1+2*PI < r2+2*PI by XREAL_1:6;
then cos.(r1+2*PI) < cos.(r2+2*PI*1) by A2,A3,RFUNCT_2:20;
then cos.(r1+2*PI*1) < cos.r2 by Th10;
hence cos.r1 < cos.r2 by Th10;
end;
hence thesis by RFUNCT_2:20;
end;
set Y = [.PI+T(i+1),2*PI+T(i+1).];
A4: Z = [.PI+T(i+1-1),2*PI+T(i+1-1).];
now
let r1, r2;
assume r1 in Y /\ dom cos & r2 in Y /\ dom cos;
then
A5: r1-2*PI in Z /\ dom cos & r2-2*PI in Z /\ dom cos by A4,Lm14,SIN_COS:24;
assume r1 < r2;
then r1-2*PI < r2-2*PI by XREAL_1:9;
then cos.(r1-2*PI) < cos.(r2+2*PI*(-1)) by A2,A5,RFUNCT_2:20;
then cos.(r1+2*PI*(-1)) < cos.r2 by Th10;
hence cos.r1 < cos.r2 by Th10;
end;
hence thesis by RFUNCT_2:20;
end;
A6: P[0] by COMPTRIG:26;
for i holds P[i] from INT_1:sch 4(A6,A1);
hence thesis;
end;
theorem Th57:
sin | [.-PI/2+2*PI*i,PI/2+2*PI*i.] is one-to-one
proof
set Q = [.-PI/2+2*PI*i,PI/2+2*PI*i.];
sin|Q is increasing by Th53;
hence thesis by FCONT_3:8;
end;
theorem Th58:
sin | [.PI/2+2*PI*i,3/2*PI+2*PI*i.] is one-to-one
proof
set Q = [.PI/2+2*PI*i,3/2*PI+2*PI*i.];
sin|Q is decreasing by Th54;
hence thesis by FCONT_3:8;
end;
registration
cluster sin | [.-PI/2,PI/2.] -> one-to-one;
coherence by Lm1,Th57;
cluster sin | [.PI/2,3/2*PI.] -> one-to-one;
coherence by Lm2,Th58;
end;
registration
cluster sin | [.-PI/2,0 .] -> one-to-one;
coherence
proof
sin | [.-PI/2,PI/2.] is one-to-one;
hence thesis by Th2,XXREAL_1:34;
end;
cluster sin | [.0,PI/2.] -> one-to-one;
coherence
proof
sin | [.-PI/2,PI/2.] is one-to-one;
hence thesis by Th2,XXREAL_1:34;
end;
cluster sin | [.PI/2,PI.] -> one-to-one;
coherence
proof
sin | [.PI/2,3/2*PI.] is one-to-one;
hence thesis by Lm7,Th2,XXREAL_1:34;
end;
cluster sin | [.PI,3/2*PI.] -> one-to-one;
coherence
proof
sin | [.PI/2,3/2*PI.] is one-to-one;
hence thesis by Lm6,Th2,XXREAL_1:34;
end;
cluster sin | [.3/2*PI,2*PI.] -> one-to-one;
coherence
proof
sin | [.-PI/2+T(1),PI/2+T(1).] is one-to-one by Th57;
hence thesis by Lm8,Th2,XXREAL_1:34;
end;
end;
registration
cluster sin | ].-PI/2,PI/2.[ -> one-to-one;
coherence
proof
sin | [.-PI/2,PI/2.] is one-to-one;
hence thesis by Th2,XXREAL_1:25;
end;
cluster sin | ].PI/2,3/2*PI.[ -> one-to-one;
coherence
proof
sin | [.PI/2,3/2*PI.] is one-to-one;
hence thesis by Th2,XXREAL_1:25;
end;
cluster sin | ].-PI/2,0 .[ -> one-to-one;
coherence
proof
sin | [.-PI/2,0 .] is one-to-one;
hence thesis by Th2,XXREAL_1:25;
end;
cluster sin | ].0,PI/2.[ -> one-to-one;
coherence
proof
sin | [.0,PI/2.] is one-to-one;
hence thesis by Th2,XXREAL_1:25;
end;
cluster sin | ].PI/2,PI.[ -> one-to-one;
coherence
proof
sin | [.PI/2,PI.] is one-to-one;
hence thesis by Th2,XXREAL_1:25;
end;
cluster sin | ].PI,3/2*PI.[ -> one-to-one;
coherence
proof
sin | [.PI,3/2*PI.] is one-to-one;
hence thesis by Th2,XXREAL_1:25;
end;
cluster sin | ].3/2*PI,2*PI.[ -> one-to-one;
coherence
proof
sin | [.3/2*PI,2*PI.] is one-to-one;
hence thesis by Th2,XXREAL_1:25;
end;
end;
theorem Th59:
cos | [.2*PI*i,PI+2*PI*i.] is one-to-one
proof
set Q1 = [.2*PI*i,PI+2*PI*i.];
cos|Q1 is decreasing by Th55;
hence thesis by FCONT_3:8;
end;
theorem Th60:
cos | [.PI+2*PI*i,2*PI+2*PI*i.] is one-to-one
proof
set Q1 = [.PI+2*PI*i,2*PI+2*PI*i.];
cos|Q1 is increasing by Th56;
hence thesis by FCONT_3:8;
end;
registration
cluster cos | [.0,PI.] -> one-to-one;
coherence by Lm3,Th59;
cluster cos | [.PI,2*PI.] -> one-to-one;
coherence by Lm4,Th60;
end;
registration
cluster cos | [.0,PI/2.] -> one-to-one;
coherence
proof
cos | [.0,PI.] is one-to-one;
hence thesis by Lm6,Th2,XXREAL_1:34;
end;
cluster cos | [.PI/2,PI.] -> one-to-one;
coherence
proof
cos | [.0,PI.] is one-to-one;
hence thesis by Th2,XXREAL_1:34;
end;
cluster cos | [.PI,3/2*PI.] -> one-to-one;
coherence
proof
cos | [.PI,2*PI.] is one-to-one;
hence thesis by Lm9,Th2,XXREAL_1:34;
end;
cluster cos | [.3/2*PI,2*PI.] -> one-to-one;
coherence
proof
cos | [.PI,2*PI.] is one-to-one;
hence thesis by Lm7,Th2,XXREAL_1:34;
end;
end;
registration
cluster cos | ].0,PI.[ -> one-to-one;
coherence
proof
cos | [.0,PI.] is one-to-one;
hence thesis by Th2,XXREAL_1:25;
end;
cluster cos | ].PI,2*PI.[ -> one-to-one;
coherence
proof
cos | [.PI,2*PI.] is one-to-one;
hence thesis by Th2,XXREAL_1:25;
end;
cluster cos | ].0,PI/2.[ -> one-to-one;
coherence
proof
cos | [.0,PI/2.] is one-to-one;
hence thesis by Th2,XXREAL_1:25;
end;
cluster cos | ].PI/2,PI.[ -> one-to-one;
coherence
proof
cos | [.PI/2,PI.] is one-to-one;
hence thesis by Th2,XXREAL_1:25;
end;
cluster cos | ].PI,3/2*PI.[ -> one-to-one;
coherence
proof
cos | [.PI,3/2*PI.] is one-to-one;
hence thesis by Th2,XXREAL_1:25;
end;
cluster cos | ].3/2*PI,2*PI.[ -> one-to-one;
coherence
proof
cos | [.3/2*PI,2*PI.] is one-to-one;
hence thesis by Th2,XXREAL_1:25;
end;
end;
theorem
2*PI*i <= r & r < 2*PI+2*PI*i & 2*PI*i <= s & s < 2*PI+2*PI*i & sin r
= sin s & cos r = cos s implies r = s
proof
assume that
A1: 2*PI*i <= r and
A2: r < 2*PI+2*PI*i & 2*PI*i <= s and
A3: s < 2*PI+2*PI*i and
A4: sin r = sin s & cos r = cos s;
A5: cos(r-s) = (cos r)*(cos s)+(sin r)*(sin s) by COMPLEX2:3
.= 1 by A4,SIN_COS:29;
A6: sin(r-s) = (sin r)*(cos s)-(cos r)*(sin s) by COMPLEX2:3
.= 0 by A4;
A7: cos (s-r) = (cos r)*(cos s)+(sin r)*(sin s) by COMPLEX2:3
.= 1 by A4,SIN_COS:29;
A8: sin (s-r) = (sin s)*(cos r)-(cos s)*(sin r) by COMPLEX2:3
.= 0 by A4;
per cases by XXREAL_0:1;
suppose
A9: r > s;
r+2*PI*i < 2*PI+2*PI*i+s by A2,XREAL_1:8;
then r+2*PI*i-2*PI*i < 2*PI+2*PI*i+s-2*PI*i by XREAL_1:9;
then r < 2*PI+s;
then
A10: r-s < 2*PI by XREAL_1:19;
r > s+0 by A9;
then 0 <= r-s by XREAL_1:20;
then r-s = 0 or r-s = PI by A6,A10,COMPTRIG:17;
hence thesis by A5,SIN_COS:77;
end;
suppose
A11: r < s;
s+2*PI*i < 2*PI+2*PI*i+r by A1,A3,XREAL_1:8;
then s+2*PI*i-2*PI*i < 2*PI+2*PI*i+r-2*PI*i by XREAL_1:9;
then s < 2*PI+r;
then
A12: s-r < 2*PI by XREAL_1:19;
s > r+0 by A11;
then 0 <= s-r by XREAL_1:20;
then s-r = 0 or s-r = PI by A8,A12,COMPTRIG:17;
hence thesis by A7,SIN_COS:77;
end;
suppose
r = s;
hence thesis;
end;
end;
begin :: arcsin
definition
func arcsin -> PartFunc of REAL, REAL equals
(sin | [.-PI/2,PI/2.])";
coherence;
end;
definition
let r be object;
func arcsin r -> number equals
arcsin.r;
coherence;
end;
registration
let r be object;
cluster arcsin r -> real;
coherence;
end;
Lm15: arcsin qua Function" = sin | [.-PI/2,PI/2.] by FUNCT_1:43;
theorem Th62:
rng arcsin = [.-PI/2,PI/2.]
proof
dom (sin|[.-PI/2,PI/2.]) = [.-PI/2,PI/2.] by RELAT_1:62,SIN_COS:24;
hence thesis by FUNCT_1:33;
end;
registration
cluster arcsin -> one-to-one;
coherence;
end;
theorem Th63:
dom arcsin = [.-1,1.] by COMPTRIG:30,FUNCT_1:33;
theorem Th64:
(sin | [.-PI/2,PI/2.]) qua Function * arcsin = id [.-1,1.] by COMPTRIG:30
,FUNCT_1:39;
theorem
arcsin * (sin | [.-PI/2,PI/2.]) = id [.-1,1.] by COMPTRIG:30,FUNCT_1:39;
theorem Th66:
(sin | [.-PI/2,PI/2.]) * arcsin = id [.-PI/2,PI/2.] by Lm15,Th62,FUNCT_1:39;
theorem
arcsin qua Function * (sin | [.-PI/2,PI/2.]) = id [.-PI/2,PI/2.] by Lm15,Th62
,FUNCT_1:39;
theorem Th68:
-1 <= r & r <= 1 implies sin arcsin r = r
proof
assume -1 <= r & r <= 1;
then
A1: r in [.-1,1.] by XXREAL_1:1;
then
A2: (arcsin.r) in [.-PI/2,PI/2.] by Th62,Th63,FUNCT_1:def 3;
thus sin arcsin r = sin.(arcsin.r) by SIN_COS:def 17
.= ((sin|[.-PI/2,PI/2.]) qua Function).(arcsin.r) by A2,FUNCT_1:49
.= (id [.-1,1.]).r by A1,Th63,Th64,FUNCT_1:13
.= r by A1,FUNCT_1:18;
end;
theorem Th69:
-PI/2 <= r & r <= PI/2 implies arcsin sin r = r
proof
A1: dom (sin|[.-PI/2,PI/2.]) = [.-PI/2,PI/2.] by RELAT_1:62,SIN_COS:24;
assume -PI/2 <= r & r <= PI/2;
then
A2: r in [.-PI/2,PI/2.] by XXREAL_1:1;
thus arcsin sin r = arcsin.(sin.r) by SIN_COS:def 17
.= arcsin.((sin|[.-PI/2,PI/2.]).r) by A2,FUNCT_1:49
.= (id [.-PI/2,PI/2.]).r by A2,A1,Th66,FUNCT_1:13
.= r by A2,FUNCT_1:18;
end;
theorem
arcsin (-1) = -PI/2 by Th7,Th69;
theorem
arcsin 0 = 0 by Th69,SIN_COS:31;
theorem
arcsin 1 = PI/2 by Th69,SIN_COS:77;
theorem
-1 <= r & r <= 1 & arcsin r = -PI/2 implies r = -1 by Th7,Th68;
theorem
-1 <= r & r <= 1 & arcsin r = 0 implies r = 0 by Th68,SIN_COS:31;
theorem
-1 <= r & r <= 1 & arcsin r = PI/2 implies r = 1 by Th68,SIN_COS:77;
theorem Th76:
-1 <= r & r <= 1 implies -PI/2 <= arcsin r & arcsin r <= PI/2
proof
assume -1 <= r & r <= 1;
then r in [.-1,1.] by XXREAL_1:1;
then arcsin.r in rng arcsin by Th63,FUNCT_1:def 3;
hence thesis by Th62,XXREAL_1:1;
end;
theorem Th77:
-1 < r & r < 1 implies -PI/2 < arcsin r & arcsin r < PI/2
proof
assume
A1: -1 < r & r < 1;
then -PI/2 <= arcsin r & arcsin r <= PI/2 by Th76;
then
-PI/2 < arcsin r & arcsin r < PI/2 or -PI/2 = arcsin r or arcsin r = PI/
2 by XXREAL_0:1;
hence thesis by A1,Th7,Th68,SIN_COS:77;
end;
theorem Th78:
-1 <= r & r <= 1 implies arcsin r = -arcsin(-r)
proof
assume -1 <= r & r <= 1;
then
A1: --1 >= -r & -r >= -1 by XREAL_1:24;
then arcsin(-r) <= PI/2 by Th76;
then
A2: -PI/2 <= -arcsin(-r) by XREAL_1:24;
-PI/2 <= arcsin(-r) by A1,Th76;
then
A3: -arcsin(-r) <= --PI/2 by XREAL_1:24;
r = 0-1*(-r)
.= sin 0 * cos arcsin(-r) - cos 0 * sin arcsin(-r) by A1,Th68,SIN_COS:31
.= sin(0-arcsin(-r)) by COMPLEX2:3;
hence thesis by A2,A3,Th69;
end;
theorem Th79:
0 <= s & r^2 + s^2 = 1 implies cos arcsin r = s
proof
set x = arcsin r;
assume that
A1: 0 <= s and
A2: r^2 + s^2 = 1;
A3: -1 <= r & r <= 1 by A2,Lm5;
then -PI/2 <= x & x <= PI/2 by Th76;
then
A4: x in [.-PI/2,PI/2.] by XXREAL_1:1;
(sin.x)^2 + (cos.x)^2 = 1 by SIN_COS:28;
then (cos.x)^2 = 1 - (sin.x)^2 .= 1 - (sin x)^2 by SIN_COS:def 17
.= 1 - r^2 by A3,Th68;
then
A5: cos.x = s or cos.x = -s by A2,SQUARE_1:40;
---s < 0 or s = 0 by A1;
hence thesis by A5,A4,COMPTRIG:12,SIN_COS:def 19;
end;
theorem
s <= 0 & r^2 + s^2 = 1 implies cos arcsin r = -s
proof
set x = arcsin r;
assume that
A1: s <= 0 and
A2: r^2 + s^2 = 1;
A3: -1 <= r & r <= 1 by A2,Lm5;
then -PI/2 <= x & x <= PI/2 by Th76;
then
A4: x in [.-PI/2,PI/2.] by XXREAL_1:1;
(sin.x)^2 + (cos.x)^2 = 1 by SIN_COS:28;
then (cos.x)^2 = 1 - (sin.x)^2 .= 1 - (sin x)^2 by SIN_COS:def 17
.= 1 - r^2 by A3,Th68;
then
A5: cos.x = s or cos.x = -s by A2,SQUARE_1:40;
0 > s or s = 0 by A1;
hence thesis by A5,A4,COMPTRIG:12,SIN_COS:def 19;
end;
theorem Th81:
-1 <= r & r <= 1 implies cos arcsin r = sqrt(1-r^2)
proof
set s = sqrt(1-r^2);
assume -1 <= r & r <= 1;
then r^2+0 <= 1^2 by SQUARE_1:49;
then 0 <= 1-r^2 by XREAL_1:19;
then 0 <= s & r^2 + s^2 = r^2 + (1-r^2) by SQUARE_1:def 2;
hence thesis by Th79;
end;
theorem
arcsin|[.-1,1.] is increasing
proof
set f = sin | [.-PI/2,PI/2.];
f.:[.-PI/2,PI/2.] = [.-1,1.] & (f|[.-PI/2,PI/2.])"|(f.:[.-PI/2,PI/2.])
is increasing by Th45,COMPTRIG:23,FCONT_3:9,RELAT_1:129;
hence thesis by RELAT_1:72;
end;
theorem
arcsin is_differentiable_on ].-1,1.[ & (-1 < r & r < 1 implies diff(
arcsin,r) = 1 / sqrt(1-r^2))
proof
set g = arcsin|].-1,1.[;
set h = sin|[.-PI/2,PI/2.];
set f = sin|].-PI/2,PI/2.[;
A1: dom f = ].-PI/2,PI/2.[ /\ REAL by RELAT_1:61,SIN_COS:24
.= ].-PI/2,PI/2.[ by XBOOLE_1:28;
set x = arcsin.r;
set s = sqrt(1-r^2);
A2: ].-1,1.[ c= dom arcsin by Th63,XXREAL_1:25;
A3: sin is_differentiable_on ].-PI/2,PI/2.[ by FDIFF_1:26,SIN_COS:68;
then
A4: f is_differentiable_on ].-PI/2,PI/2.[ by FDIFF_2:16;
A5: now
let x0 be Real such that
A6: x0 in ].-PI/2,PI/2.[;
diff(f,x0) = (f`|].-PI/2,PI/2.[).x0 by A4,A6,FDIFF_1:def 7
.= (sin`|].-PI/2,PI/2.[).x0 by A3,FDIFF_2:16
.= diff(sin,x0) by A3,A6,FDIFF_1:def 7
.= cos.x0 by SIN_COS:68;
hence 0 < diff(f,x0) by A6,COMPTRIG:11;
end;
A7: f" = (h|].-PI/2,PI/2.[)" by RELAT_1:74,XXREAL_1:25
.= h"|(h.:].-PI/2,PI/2.[) by RFUNCT_2:17
.= g by Th46,RELAT_1:129,XXREAL_1:25;
then
A8: f|].-PI/2,PI/2.[ = f & dom (f") = ].-1,1.[ by Th63,RELAT_1:62,72
,XXREAL_1:25;
then
A9: g is_differentiable_on ].-1,1.[ by A7,A4,A1,A5,FDIFF_2:48;
then for x st x in ].-1,1.[ holds g is_differentiable_in x by
FDIFF_1:9;
hence
A10: arcsin is_differentiable_on ].-1,1.[ by A2,FDIFF_1:def 6;
assume
A11: -1 < r & r < 1;
then
A12: r in ].-1,1.[ by XXREAL_1:4;
then
A13: g.r = x by FUNCT_1:49;
x = arcsin r;
then -PI/2 < x & x < PI/2 by A11,Th77;
then
A14: x in ].-PI/2,PI/2.[ by XXREAL_1:4;
then
A15: diff(f,x) = (f`|].-PI/2,PI/2.[).x by A4,FDIFF_1:def 7
.= (sin`|].-PI/2,PI/2.[).x by A3,FDIFF_2:16
.= diff(sin,x) by A3,A14,FDIFF_1:def 7
.= cos.x by SIN_COS:68
.= cos arcsin r by SIN_COS:def 19
.= s by A11,Th81;
thus diff(arcsin,r) = (arcsin`|].-1,1.[).r by A10,A12,FDIFF_1:def 7
.= (g`|].-1,1.[).r by A10,FDIFF_2:16
.= diff(g,r) by A9,A12,FDIFF_1:def 7
.= 1 / s by A7,A8,A4,A1,A5,A12,A13,A15,FDIFF_2:48;
end;
theorem
arcsin|[.-1,1.] is continuous
proof
set f = sin | [.-PI/2,PI/2.];
dom f = [.-PI/2,PI/2.] by RELAT_1:62,SIN_COS:24;
then f|[.-PI/2,PI/2.] = f & (f|[.-PI/2,PI/2.])"|(f.:[.-PI/2,PI/2.]) is
continuous by COMPTRIG:23,FCONT_1:47,RELAT_1:73;
hence thesis by COMPTRIG:30,RELAT_1:115;
end;
begin :: arccos
definition
func arccos -> PartFunc of REAL, REAL equals
(cos | [.0,PI.])";
coherence;
end;
definition
let r be object;
func arccos r -> number equals
arccos.r;
coherence;
end;
registration
let r be object;
cluster arccos r -> real;
coherence;
end;
Lm16: arccos qua Function" = cos | [.0,PI.] by FUNCT_1:43;
theorem Th85:
rng arccos = [.0,PI.]
proof
dom (cos|[.0,PI.]) = [.0,PI.] by RELAT_1:62,SIN_COS:24;
hence thesis by FUNCT_1:33;
end;
registration
cluster arccos -> one-to-one;
coherence;
end;
theorem Th86:
dom arccos = [.-1,1.] by COMPTRIG:32,FUNCT_1:33;
theorem Th87:
(cos | [.0,PI.]) qua Function * arccos = id [.-1,1.] by COMPTRIG:32
,FUNCT_1:39;
theorem
arccos * (cos | [.0,PI.]) = id [.-1,1.] by COMPTRIG:32,FUNCT_1:39;
theorem Th89:
(cos | [.0,PI.]) * arccos = id [.0,PI.] by Lm16,Th85,FUNCT_1:39;
theorem
arccos qua Function * (cos | [.0,PI.]) = id [.0,PI.] by Lm16,Th85,FUNCT_1:39;
theorem Th91:
-1 <= r & r <= 1 implies cos arccos r = r
proof
assume -1 <= r & r <= 1;
then
A1: r in [.-1,1.] by XXREAL_1:1;
then
A2: arccos.r in [.0,PI.] by Th85,Th86,FUNCT_1:def 3;
thus cos arccos r = cos.(arccos.r) by SIN_COS:def 19
.= ((cos|[.0,PI.]) qua Function).(arccos.r) by A2,FUNCT_1:49
.= (id [.-1,1.]).r by A1,Th86,Th87,FUNCT_1:13
.= r by A1,FUNCT_1:18;
end;
theorem Th92:
0 <= r & r <= PI implies arccos cos r = r
proof
A1: dom (cos|[.0,PI.]) = [.0,PI.] by RELAT_1:62,SIN_COS:24;
assume 0 <= r & r <= PI;
then
A2: r in [.0,PI.] by XXREAL_1:1;
thus arccos cos r = arccos.(cos.r) by SIN_COS:def 19
.= arccos.((cos|[.0,PI.]).r) by A2,FUNCT_1:49
.= (id [.0,PI.]).r by A2,A1,Th89,FUNCT_1:13
.= r by A2,FUNCT_1:18;
end;
theorem
arccos (-1) = PI by Th92,SIN_COS:77;
theorem
arccos 0 = PI/2 by Lm6,Th92,SIN_COS:77;
theorem
arccos 1 = 0 by Th92,SIN_COS:31;
theorem
-1 <= r & r <= 1 & arccos r = 0 implies r = 1 by Th91,SIN_COS:31;
theorem
-1 <= r & r <= 1 & arccos r = PI/2 implies r = 0 by Th91,SIN_COS:77;
theorem
-1 <= r & r <= 1 & arccos r = PI implies r = -1 by Th91,SIN_COS:77;
theorem Th99:
-1 <= r & r <= 1 implies 0 <= arccos r & arccos r <= PI
proof
assume -1 <= r & r <= 1;
then r in [.-1,1.] by XXREAL_1:1;
then arccos.r in rng arccos by Th86,FUNCT_1:def 3;
hence thesis by Th85,XXREAL_1:1;
end;
theorem Th100:
-1 < r & r < 1 implies 0 < arccos r & arccos r < PI
proof
assume
A1: -1 < r & r < 1;
then arccos r <= PI by Th99;
then 0 < arccos r & arccos r < PI or 0 = arccos r or arccos r = PI by A1,Th99
,XXREAL_0:1;
hence thesis by A1,Th91,SIN_COS:31,77;
end;
theorem Th101:
-1 <= r & r <= 1 implies arccos r = PI - arccos(-r)
proof
assume -1 <= r & r <= 1;
then
A1: --1 >= -r & -r >= -1 by XREAL_1:24;
then 0+arccos(-r) <= PI by Th99;
then
A2: 0 <= PI-arccos(-r) by XREAL_1:19;
0 <= arccos(-r) by A1,Th99;
then PI+0 <= PI+arccos(-r) by XREAL_1:6;
then
A3: PI-arccos(-r) <= PI by XREAL_1:20;
r = (-1)*(-r)
.= cos PI * cos arccos(-r) + sin PI * sin arccos(-r) by A1,Th91,SIN_COS:77
.= cos(PI-arccos(-r)) by COMPLEX2:3;
hence thesis by A2,A3,Th92;
end;
theorem Th102:
0 <= s & r^2 + s^2 = 1 implies sin arccos r = s
proof
set x = arccos r;
assume that
A1: 0 <= s and
A2: r^2 + s^2 = 1;
A3: -1 <= r & r <= 1 by A2,Lm5;
then 0 <= x & x <= PI by Th99;
then
A4: x in [.0,PI.] by XXREAL_1:1;
(sin.x)^2 + (cos.x)^2 = 1 by SIN_COS:28;
then (sin.x)^2 = 1 - (cos.x)^2 .= 1 - (cos x)^2 by SIN_COS:def 19
.= 1 - r^2 by A3,Th91;
then
A5: sin.x = s or sin.x = -s by A2,SQUARE_1:40;
---s < 0 or s = 0 by A1;
hence thesis by A5,A4,COMPTRIG:8,SIN_COS:def 17;
end;
theorem
s <= 0 & r^2 + s^2 = 1 implies sin arccos r = -s
proof
set x = arccos r;
assume that
A1: s <= 0 and
A2: r^2 + s^2 = 1;
A3: -1 <= r & r <= 1 by A2,Lm5;
then 0 <= x & x <= PI by Th99;
then
A4: x in [.0,PI.] by XXREAL_1:1;
(sin.x)^2 + (cos.x)^2 = 1 by SIN_COS:28;
then (sin.x)^2 = 1 - (cos.x)^2 .= 1 - (cos x)^2 by SIN_COS:def 19
.= 1 - r^2 by A3,Th91;
then
A5: sin.x = s or sin.x = -s by A2,SQUARE_1:40;
0 > s or s = 0 by A1;
hence thesis by A5,A4,COMPTRIG:8,SIN_COS:def 17;
end;
theorem Th104:
-1 <= r & r <= 1 implies sin arccos r = sqrt(1-r^2)
proof
set s = sqrt(1-r^2);
assume -1 <= r & r <= 1;
then r^2+0 <= 1^2 by SQUARE_1:49;
then 0 <= 1-r^2 by XREAL_1:19;
then 0 <= s & r^2 + s^2 = r^2 + (1-r^2) by SQUARE_1:def 2;
hence thesis by Th102;
end;
theorem
arccos|[.-1,1.] is decreasing
proof
set f = cos | [.0,PI.];
f.:[.0,PI.] = [.-1,1.] & (f|[.0,PI.])"|(f.:[.0,PI.]) is decreasing by Th49,
COMPTRIG:25,FCONT_3:10,RELAT_1:129;
hence thesis by RELAT_1:72;
end;
theorem
arccos is_differentiable_on ].-1,1.[ & (-1 < r & r < 1 implies diff(
arccos,r) = -1 / sqrt(1-r^2))
proof
set g = arccos|].-1,1.[;
set h = cos|[.0,PI.];
set f = cos|].0,PI.[;
A1: dom f = ].0,PI.[ /\ REAL by RELAT_1:61,SIN_COS:24
.= ].0,PI.[ by XBOOLE_1:28;
set x = arccos.r;
set s = sqrt(1-r^2);
A2: ].-1,1.[ c= dom arccos by Th86,XXREAL_1:25;
A3: cos is_differentiable_on ].0,PI.[ by FDIFF_1:26,SIN_COS:67;
then
A4: f is_differentiable_on ].0,PI.[ by FDIFF_2:16;
A5: now
let x0 be Real such that
A6: x0 in ].0,PI.[;
A7: --sin.x0 > 0 by A6,COMPTRIG:7;
diff(f,x0) = (f`|].0,PI.[).x0 by A4,A6,FDIFF_1:def 7
.= (cos`|].0,PI.[).x0 by A3,FDIFF_2:16
.= diff(cos,x0) by A3,A6,FDIFF_1:def 7
.= -sin.x0 by SIN_COS:67;
hence 0 > diff(f,x0) by A7;
end;
A8: f" = (h|].0,PI.[)" by RELAT_1:74,XXREAL_1:25
.= h"|(h.:].0,PI.[) by RFUNCT_2:17
.= g by Th50,RELAT_1:129,XXREAL_1:25;
then
A9: f|].0,PI.[ = f & dom (f") = ].-1,1.[ by Th86,RELAT_1:62,72,XXREAL_1:25;
then
A10: g is_differentiable_on ].-1,1.[ by A8,A4,A1,A5,FDIFF_2:48;
then for x st x in ].-1,1.[ holds g is_differentiable_in x by
FDIFF_1:9;
hence
A11: arccos is_differentiable_on ].-1,1.[ by A2,FDIFF_1:def 6;
assume
A12: -1 < r & r < 1;
then
A13: r in ].-1,1.[ by XXREAL_1:4;
then
A14: g.r = x by FUNCT_1:49;
x = arccos r;
then 0 < x & x < PI by A12,Th100;
then
A15: x in ].0,PI.[ by XXREAL_1:4;
then
A16: diff(f,x) = (f`|].0,PI.[).x by A4,FDIFF_1:def 7
.= (cos`|].0,PI.[).x by A3,FDIFF_2:16
.= diff(cos,x) by A3,A15,FDIFF_1:def 7
.= -sin.x by SIN_COS:67
.= -sin arccos r by SIN_COS:def 17
.= -s by A12,Th104;
thus diff(arccos,r) = (arccos`|].-1,1.[).r by A11,A13,FDIFF_1:def 7
.= (g`|].-1,1.[).r by A11,FDIFF_2:16
.= diff(g,r) by A10,A13,FDIFF_1:def 7
.= 1 / -s by A8,A9,A4,A1,A5,A13,A14,A16,FDIFF_2:48
.= (-1)/s by XCMPLX_1:192
.= -1/s by XCMPLX_1:187;
end;
theorem
arccos|[.-1,1.] is continuous
proof
set f = cos | [.0,PI.];
dom f = [.0,PI.] by RELAT_1:62,SIN_COS:24;
then f|[.0,PI.] = f & (f|[.0,PI.])"|(f.:[.0,PI.]) is continuous by
COMPTRIG:25,FCONT_1:47,RELAT_1:73;
hence thesis by COMPTRIG:32,RELAT_1:115;
end;
:: Correspondence between arcsin and arccos
theorem Th108:
-1 <= r & r <= 1 implies arcsin r + arccos r = PI/2
proof
assume
A1: -1 <= r & r <= 1;
then -PI/2+PI/2 <= arccos r by Th99;
then -PI/2 <= arccos r-PI/2 by XREAL_1:19;
then
A2: --PI/2 >= -(arccos r-PI/2) by XREAL_1:24;
arccos r <= PI/2+PI/2 by A1,Th99;
then arccos r-PI/2 <= PI/2 by XREAL_1:20;
then
A3: -(arccos r-PI/2) >= -PI/2 by XREAL_1:24;
r = sin(PI/2)*cos arccos r - cos(PI/2)*sin arccos r by A1,Th91,SIN_COS:77
.= sin(PI/2-arccos r) by COMPLEX2:3;
then arcsin r = PI/2 - arccos r by A2,A3,Th69;
hence thesis;
end;
theorem
-1 <= r & r <= 1 implies arccos(-r) - arcsin r = PI/2
proof
assume
A1: -1 <= r & r <= 1;
then
A2: arcsin r + arccos r = PI/2 + 0 by Th108;
--1 >= -r & -r >= -1 by A1,XREAL_1:24;
then arccos(-r) = PI - arccos(--r) by Th101
.= arcsin r + PI/2 by A2;
hence thesis;
end;
theorem
-1 <= r & r <= 1 implies arccos r - arcsin(-r) = PI/2
proof
assume
A1: -1 <= r & r <= 1;
then
A2: arcsin r + arccos r = PI/2 + 0 by Th108;
--1 >= -r & -r >= -1 by A1,XREAL_1:24;
then arcsin(-r) = -arcsin(--r) by Th78
.= arccos r - PI/2 by A2;
hence thesis;
end;