:: Trigonometric Form of Complex Numbers
:: by Robert Milewski
::
:: Received July 21, 2000
:: Copyright (c) 2000-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, NAT_1, XBOOLE_0, ARYTM_3, CARD_1, SUBSET_1, XXREAL_0,
XCMPLX_0, COMPLEX1, ARYTM_1, RELAT_1, SQUARE_1, POWER, NEWTON, SIN_COS,
XXREAL_1, FUNCT_1, ORDINAL2, REAL_1, FDIFF_1, RCOMP_1, VALUED_0, TARSKI,
PARTFUN1, COMPTRIG;
notations TARSKI, XBOOLE_0, SUBSET_1, ORDINAL1, NUMBERS, XCMPLX_0, XREAL_0,
COMPLEX1, REAL_1, SQUARE_1, NAT_1, NEWTON, POWER, RELAT_1, FUNCT_1,
RFUNCT_2, FCONT_1, FDIFF_1, PARTFUN1, PARTFUN2, RCOMP_1, SIN_COS,
XXREAL_0;
constructors PARTFUN1, ARYTM_0, REAL_1, SQUARE_1, NAT_1, RCOMP_1, PARTFUN2,
RFUNCT_2, FCONT_1, FDIFF_1, COMSEQ_3, BINARITH, SIN_COS, BINOP_2, POWER,
RVSUM_1, RELSET_1, ABIAN;
registrations RELSET_1, XCMPLX_0, XXREAL_0, XREAL_0, NAT_1, MEMBERED, NEWTON,
SIN_COS, VALUED_0, FCONT_1, FUNCT_1, SQUARE_1, ORDINAL1, CARD_1;
requirements NUMERALS, SUBSET, REAL, ARITHM;
equalities SQUARE_1, COMPLEX1, XCMPLX_0;
theorems NAT_1, SQUARE_1, POWER, ABSVALUE, RELAT_1, FUNCT_1, RFUNCT_2,
PARTFUN1, FCONT_2, RCOMP_1, FDIFF_1, ROLLE, COMPLEX1, SIN_COS, SIN_COS2,
XBOOLE_0, XCMPLX_1, XREAL_1, XXREAL_0, NEWTON, XCMPLX_0, XXREAL_1,
XBOOLE_1, XREAL_0;
schemes NAT_1;
begin
reserve x for Real;
scheme
Regrwithout0 { P[Nat] } : P[1]
provided
A1: ex k be non zero Nat st P[k] and
A2: for k be non zero Nat st k <> 1 & P[k] ex n be non zero Nat st n <
k & P[n]
proof
consider t be non zero Nat such that
A3: P[t] by A1;
defpred R[Nat] means P[$1+1];
A4: now
let k be Nat;
assume that
A5: k <> 0 and
A6: R[k];
reconsider k1=k+1 as non zero Element of NAT;
k+1 > 0+1 by A5,XREAL_1:6;
then consider n be non zero Nat such that
A7: n < k1 and
A8: P[n] by A2,A6;
consider l be Nat such that
A9: n = l+1 by NAT_1:6;
take l;
thus l < k by A7,A9,XREAL_1:6;
thus R[l] by A8,A9;
end;
ex s be Nat st t = s+1 by NAT_1:6;
then
A10: ex k be Nat st R[k] by A3;
R[0] from NAT_1:sch 7(A10,A4);
hence thesis;
end;
theorem Th1:
for z be Complex holds Re z >= -|.z.|
proof
let z be Complex;
0 <= (Im z)^2 by XREAL_1:63;
then
A1: (Re z)^2+0 <= (Re z)^2 + (Im z)^2 by XREAL_1:7;
0 <= (Re z)^2 by XREAL_1:63;
then sqrt(Re z)^2 <= |.z.| by A1,SQUARE_1:26;
then -sqrt(Re z)^2 >= -|.z.| by XREAL_1:24;
then Re z >= -|.Re z.| & -|.Re z.| >= -|.z.| by ABSVALUE:4,COMPLEX1:72;
hence thesis by XXREAL_0:2;
end;
theorem
for z be Complex holds Im z >= -|.z.|
proof
let z be Complex;
0 <= (Re z)^2 by XREAL_1:63;
then
A1: (Im z)^2+0 <= (Re z)^2 + (Im z)^2 by XREAL_1:7;
0 <= (Im z)^2 by XREAL_1:63;
then sqrt(Im z)^2 <= |.z.| by A1,SQUARE_1:26;
then -sqrt(Im z)^2 >= -|.z.| by XREAL_1:24;
then Im z >= -|.Im z.| & -|.Im z.| >= -|.z.| by ABSVALUE:4,COMPLEX1:72;
hence thesis by XXREAL_0:2;
end;
theorem Th3:
for z be Complex holds |.z.|^2 = (Re z)^2 + (Im z)^2
proof
let z be Complex;
thus |.z.|^2 = |.z*z.| by COMPLEX1:65
.= (Re z)^2 + (Im z)^2 by COMPLEX1:68;
end;
theorem Th4:
for n be Nat st x >= 0 & n <> 0 holds (n-root x) |^ n = x
proof
let n be Nat;
assume that
A1: x >= 0 and
A2: n <> 0;
n >= 0+1 by A2,NAT_1:13;
hence thesis by A1,POWER:4;
end;
registration
cluster PI -> non negative;
coherence
proof
PI in ].0, 4.[ by SIN_COS:def 28;
hence thesis by XXREAL_1:4;
end;
end;
begin
PI in ].0, 4.[ by SIN_COS:def 28;
then
Lm1: 0 < PI by XXREAL_1:4;
then
Lm2: 0 + PI/2 < PI/2 + PI/2 by XREAL_1:6;
Lm3: 0 + PI < PI + PI by Lm1,XREAL_1:6;
Lm4: 0+PI/2 < PI+PI/2 by Lm1,XREAL_1:6;
Lm5: PI/2+PI/2 < PI+PI/2 by Lm2,XREAL_1:6;
3/2*PI+PI/2 = 2*PI;
then
Lm6: 3/2*PI < 2*PI by Lm5,XREAL_1:6;
Lm7: 0 < 3/2*PI by Lm1;
theorem
0 < PI/2 & PI/2 < PI & 0 < PI & -PI/2 < PI/2 & PI < 2*PI & PI/2 < 3/2*
PI & -PI/2 < 0 & 0 < 2*PI & PI < 3/2*PI & 3/2*PI < 2*PI & 0 < 3/2*PI by Lm2,Lm3
,Lm4,XREAL_1:6;
theorem Th6:
for a,b,c,x be Real st x in ].a,c.[ holds x in ].a,b.[ or
x = b or x in ].b,c.[
proof
let a,b,c,x be Real;
assume that
A1: x in ].a,c.[ and
A2: not x in ].a,b.[ and
A3: not x = b;
x <= a or x >= b by A2,XXREAL_1:4;
then
A4: x > b by A1,A3,XXREAL_0:1,XXREAL_1:4;
x < c by A1,XXREAL_1:4;
hence thesis by A4,XXREAL_1:4;
end;
theorem Th7:
x in ].0,PI.[ implies sin.x > 0
proof
assume
A1: x in ].0,PI.[;
per cases by A1,Th6;
suppose
A2: x in ].0,PI/2.[;
then x < PI/2 by XXREAL_1:4;
then -x > -PI/2 by XREAL_1:24;
then
A3: -x+PI/2 > -PI/2+PI/2 by XREAL_1:6;
0 < x by A2,XXREAL_1:4;
then -x+PI/2 < 0+PI/2 by XREAL_1:6;
then PI/2-x in ].0,PI/2.[ by A3,XXREAL_1:4;
then cos.(PI/2-x) > 0 by SIN_COS:80;
hence thesis by SIN_COS:78;
end;
suppose
x=PI/2;
hence thesis by SIN_COS:76;
end;
suppose
A4: x in ].PI/2,PI.[;
then x < PI by XXREAL_1:4;
then
A5: x-PI/2 < PI-PI/2 by XREAL_1:9;
PI/2 < x by A4,XXREAL_1:4;
then PI/2-PI/2 < x-PI/2 by XREAL_1:9;
then x-PI/2 in ].0,PI/2.[ by A5,XXREAL_1:4;
then cos.(-(PI/2-x)) > 0 by SIN_COS:80;
then cos.(PI/2-x) > 0 by SIN_COS:30;
hence thesis by SIN_COS:78;
end;
end;
theorem Th8:
x in [.0,PI.] implies sin.x >= 0
proof
assume
A1: x in [.0,PI.];
then x <= PI by XXREAL_1:1;
then x = 0 or x = PI or 0 < x & x < PI by A1,XXREAL_0:1,XXREAL_1:1;
then x = 0 or x = PI or x in ].0,PI.[ by XXREAL_1:4;
hence thesis by Th7,SIN_COS:30,76;
end;
theorem Th9:
x in ].PI,2*PI.[ implies sin.x < 0
proof
A1: sin.(x-PI) = sin.(-(PI-x)) .= -sin.(PI+-x) by SIN_COS:30
.= --sin.(-x) by SIN_COS:78
.= -sin.x by SIN_COS:30;
assume
A2: x in ].PI,2*PI.[;
then x < 2*PI by XXREAL_1:4;
then
A3: x-PI < 2*PI-PI by XREAL_1:9;
PI < x by A2,XXREAL_1:4;
then PI-PI < x-PI by XREAL_1:9;
then x-PI in ].0,PI.[ by A3,XXREAL_1:4;
hence thesis by A1,Th7;
end;
theorem Th10:
x in [.PI,2*PI.] implies sin.x <= 0
proof
assume x in [.PI,2*PI.];
then PI <= x & x <= 2*PI by XXREAL_1:1;
then x = PI or x = 2*PI or PI < x & x < 2*PI by XXREAL_0:1;
then x = PI or x = 2*PI or x in ].PI,2*PI.[ by XXREAL_1:4;
hence thesis by Th9,SIN_COS:76;
end;
theorem Th11:
x in ].-PI/2,PI/2.[ implies cos.x > 0
proof
A1: sin.(x+PI/2) = cos.x by SIN_COS:78;
assume
A2: x in ].-PI/2,PI/2.[;
then x < PI/2 by XXREAL_1:4;
then
A3: x+PI/2 < PI/2+PI/2 by XREAL_1:6;
-PI/2 < x by A2,XXREAL_1:4;
then -PI/2+PI/2 < x+PI/2 by XREAL_1:6;
then x+PI/2 in ].0,PI.[ by A3,XXREAL_1:4;
hence thesis by A1,Th7;
end;
theorem Th12:
x in [.-PI/2,PI/2.] implies cos.x >= 0
proof
assume x in [.-PI/2,PI/2.];
then -PI/2 <= x & x <= PI/2 by XXREAL_1:1;
then x = -PI/2 or x = PI/2 or -PI/2 < x & x < PI/2 by XXREAL_0:1;
then x = -PI/2 or x = PI/2 or x in ].-PI/2,PI/2.[ by XXREAL_1:4;
hence thesis by Th11,SIN_COS:30,76;
end;
theorem Th13:
x in ].PI/2,3/2*PI.[ implies cos.x < 0
proof
A1: sin.(x+PI/2) = cos.x by SIN_COS:78;
assume
A2: x in ].PI/2,3/2*PI.[;
then x < 3/2*PI by XXREAL_1:4;
then
A3: x+PI/2 < 3/2*PI+PI/2 by XREAL_1:6;
PI/2 < x by A2,XXREAL_1:4;
then PI/2+PI/2 < x+PI/2 by XREAL_1:6;
then x+PI/2 in ].PI,2*PI.[ by A3,XXREAL_1:4;
hence thesis by A1,Th9;
end;
theorem Th14:
x in [.PI/2,3/2*PI.] implies cos.x <= 0
proof
assume x in [.PI/2,3/2*PI.];
then PI/2 <= x & x <= 3/2*PI by XXREAL_1:1;
then x = PI/2 or x = 3/2*PI or PI/2 < x & x < 3/2*PI by XXREAL_0:1;
then x = PI/2 or x = 3/2*PI or x in ].PI/2,3/2*PI.[ by XXREAL_1:4;
hence thesis by Th13,SIN_COS:76;
end;
theorem Th15:
x in ].3/2*PI,2*PI.[ implies cos.x > 0
proof
A1: cos.(x-PI) = cos.(-(PI-x)) .= cos.(PI+-x) by SIN_COS:30
.= -cos.(-x) by SIN_COS:78
.= -cos.x by SIN_COS:30;
assume
A2: x in ].3/2*PI,2*PI.[;
then x < 2*PI by XXREAL_1:4;
then x-PI < 2*PI-PI by XREAL_1:9;
then
A3: x-PI < 3/2*PI by Lm5,XXREAL_0:2;
3/2*PI < x by A2,XXREAL_1:4;
then 3/2*PI-PI < x-PI by XREAL_1:9;
then x-PI in ].PI/2,3/2*PI.[ by A3,XXREAL_1:4;
hence thesis by A1,Th13;
end;
theorem Th16:
x in [.3/2*PI,2*PI.] implies cos.x >= 0
proof
assume x in [.3/2*PI,2*PI.];
then 3/2*PI <= x & x <= 2*PI by XXREAL_1:1;
then x = 3/2*PI or x = 2*PI or 3/2*PI < x & x < 2*PI by XXREAL_0:1;
then x = 3/2*PI or x = 2*PI or x in ].3/2*PI,2*PI.[ by XXREAL_1:4;
hence thesis by Th15,SIN_COS:76;
end;
theorem Th17:
0 <= x & x < 2*PI & sin x = 0 implies x = 0 or x = PI
proof
assume that
A1: 0 <= x & x < 2*PI and
A2: sin x = 0;
sin.x = 0 by A2,SIN_COS:def 17;
then ( not x in ].0,PI.[)& not x in ].PI,2*PI.[ by Th7,Th9;
then x = 0 or x >= PI & PI >= x by A1,XXREAL_1:4;
hence thesis by XXREAL_0:1;
end;
theorem Th18:
0 <= x & x < 2*PI & cos x = 0 implies x = PI/2 or x = 3/2*PI
proof
assume that
A1: 0 <= x and
A2: x < 2*PI and
A3: cos x = 0;
A4: cos.x = 0 by A3,SIN_COS:def 19;
then not x in ].PI/2,3/2*PI.[ by Th13;
then
A5: PI/2 >= x or x >= 3/2*PI by XXREAL_1:4;
not x in ].-PI/2,PI/2.[ by A4,Th11;
then -PI/2 >= x or x >= PI/2 by XXREAL_1:4;
then x = PI/2 or x = 3/2*PI or x > 3/2* PI by A1,A5,Lm1,XXREAL_0:1;
then x = PI/2 or x = 3/2*PI or x in ].3/2* PI,2*PI.[ by A2,XXREAL_1:4;
hence thesis by A4,Th15;
end;
theorem Th19:
sin|].-PI/2,PI/2.[ is increasing
proof
A1: for x st x in ].-PI/2,PI/2.[ holds diff(sin,x) > 0
proof
let x;
assume x in ].-PI/2,PI/2.[;
then 0 < cos.x by Th11;
hence thesis by SIN_COS:68;
end;
].-PI/2,PI/2.[ is open by RCOMP_1:7;
hence thesis by A1,FDIFF_1:26,ROLLE:9,SIN_COS:24,68;
end;
theorem Th20:
sin|].PI/2,3/2*PI.[ is decreasing
proof
A1: for x st x in ].PI/2,3/2*PI.[ holds diff(sin,x) < 0
proof
let x;
assume x in ].PI/2,3/2*PI.[;
then 0 > cos.x by Th13;
hence thesis by SIN_COS:68;
end;
].PI/2,3/2*PI.[ is open by RCOMP_1:7;
hence thesis by A1,FDIFF_1:26,ROLLE:10,SIN_COS:24,68;
end;
theorem Th21:
cos|].0,PI.[ is decreasing
proof
A1: for x st x in ].0,PI.[ holds diff(cos,x) < 0
proof
let x;
assume x in ].0,PI.[;
then 0 < sin.x by Th7;
then 0-sin.x < 0;
hence thesis by SIN_COS:67;
end;
].0,PI.[ is open by RCOMP_1:7;
hence thesis by A1,FDIFF_1:26,ROLLE:10,SIN_COS:24,67;
end;
theorem Th22:
cos|].PI,2*PI.[ is increasing
proof
A1: for x st x in ].PI,2*PI.[ holds diff(cos,x) > 0
proof
let x;
assume x in ].PI,2*PI.[;
then 0-sin.x > 0 by Th9,XREAL_1:50;
hence thesis by SIN_COS:67;
end;
].PI,2*PI.[ is open by RCOMP_1:7;
hence thesis by A1,FDIFF_1:26,ROLLE:9,SIN_COS:24,67;
end;
theorem
sin|[.-PI/2,PI/2.] is increasing
proof
now
let r1,r2 be Real;
assume that
A1: r1 in [.-PI/2,PI/2.] /\ dom sin and
A2: r2 in [.-PI/2,PI/2.] /\ dom sin and
A3: r1 < r2;
A4: r1 in dom sin by A1,XBOOLE_0:def 4;
set r3 = (r1+r2)/2;
r1 in [.-PI/2,PI/2.] by A1,XBOOLE_0:def 4;
then
A5: -PI/2 <= r1 by XXREAL_1:1;
|.sin r3.| <= 1 by SIN_COS:27;
then
A6: |.sin.r3.| <= 1 by SIN_COS:def 17;
then
A7: sin.r3 <= 1 by ABSVALUE:5;
r2 in [.-PI/2,PI/2.] by A2,XBOOLE_0:def 4;
then
A8: r2 <= PI/2 by XXREAL_1:1;
A9: r1 < r3 by A3,XREAL_1:226;
then
A10: -PI/2 < r3 by A5,XXREAL_0:2;
A11: r3 < r2 by A3,XREAL_1:226;
then r3 < PI/2 by A8,XXREAL_0:2;
then r3 in ].-PI/2,PI/2.[ by A10,XXREAL_1:4;
then
A12: r3 in ].-PI/2,PI/2.[ /\ dom sin by SIN_COS:24,XBOOLE_0:def 4;
|.sin r2.| <= 1 by SIN_COS:27;
then |.sin.r2.| <= 1 by SIN_COS:def 17;
then
A13: sin.r2 >= -1 by ABSVALUE:5;
A14: r2 in dom sin by A2,XBOOLE_0:def 4;
A15: sin.r3 >= -1 by A6,ABSVALUE:5;
now
per cases by A5,XXREAL_0:1;
suppose
A16: -PI/2 < r1;
then
A17: -PI/2 < r2 by A3,XXREAL_0:2;
now
per cases by A8,XXREAL_0:1;
suppose
A18: r2 < PI/2;
then r1 < PI/2 by A3,XXREAL_0:2;
then r1 in ].-PI/2,PI/2.[ by A16,XXREAL_1:4;
then
A19: r1 in ].-PI/2,PI/2.[ /\ dom sin by A4,XBOOLE_0:def 4;
r2 in ].-PI/2,PI/2.[ by A17,A18,XXREAL_1:4;
then r2 in ].-PI/2,PI/2.[ /\ dom sin by A14,XBOOLE_0:def 4;
hence sin.r2 > sin.r1 by A3,A19,Th19,RFUNCT_2:20;
end;
suppose
A20: r2 = PI/2;
then r1 in ].-PI/2,PI/2.[ by A3,A16,XXREAL_1:4;
then r1 in ].-PI/2,PI/2.[ /\ dom sin by A4,XBOOLE_0:def 4;
then
A21: sin.r3 > sin.r1 by A9,A12,Th19,RFUNCT_2:20;
assume sin.r2 <= sin.r1;
hence contradiction by A7,A20,A21,SIN_COS:76,XXREAL_0:2;
end;
end;
hence sin.r2 > sin.r1;
end;
suppose
A22: -PI/2 = r1;
now
per cases by A8,XXREAL_0:1;
suppose
r2 < PI/2;
then r2 in ].-PI/2,PI/2.[ by A3,A22,XXREAL_1:4;
then r2 in ].-PI/2,PI/2.[ /\ dom sin by A14,XBOOLE_0:def 4;
then
A23: sin.r2 > sin.r3 by A11,A12,Th19,RFUNCT_2:20;
assume sin.r2 <= sin.r1;
then sin.r2 <= -1 by A22,SIN_COS:30,76;
hence contradiction by A15,A13,A23,XXREAL_0:1;
end;
suppose
r2 = PI/2;
hence sin.r2 > sin.r1 by A22,SIN_COS:30,76;
end;
end;
hence sin.r2 > sin.r1;
end;
end;
hence sin.r2 > sin.r1;
end;
hence thesis by RFUNCT_2:20;
end;
theorem
sin|[.PI/2,3/2*PI.] is decreasing
proof
now
let r1,r2 be Real;
assume that
A1: r1 in [.PI/2,3/2*PI.] /\ dom sin and
A2: r2 in [.PI/2,3/2*PI.] /\ dom sin and
A3: r1 < r2;
A4: r1 in dom sin by A1,XBOOLE_0:def 4;
|.sin r2.| <= 1 by SIN_COS:27;
then |.sin.r2.| <= 1 by SIN_COS:def 17;
then
A5: sin.r2 <= 1 by ABSVALUE:5;
|.sin r1.| <= 1 by SIN_COS:27;
then |.sin.r1.| <= 1 by SIN_COS:def 17;
then
A6: sin.r1 >= -1 by ABSVALUE:5;
r2 in [.PI/2,3/2*PI.] by A2,XBOOLE_0:def 4;
then
A7: r2 <= 3/2*PI by XXREAL_1:1;
set r3 = (r1+r2)/2;
r1 in [.PI/2,3/2*PI.] by A1,XBOOLE_0:def 4;
then
A8: PI/2 <= r1 by XXREAL_1:1;
|.sin r3.| <= 1 by SIN_COS:27;
then
A9: |.sin.r3.| <= 1 by SIN_COS:def 17;
then
A10: sin.r3 <= 1 by ABSVALUE:5;
A11: r2 in dom sin by A2,XBOOLE_0:def 4;
A12: r1 < r3 by A3,XREAL_1:226;
then
A13: PI/2 < r3 by A8,XXREAL_0:2;
A14: r3 < r2 by A3,XREAL_1:226;
then r3 < 3/2*PI by A7,XXREAL_0:2;
then r3 in ].PI/2,3/2*PI.[ by A13,XXREAL_1:4;
then
A15: r3 in ].PI/2,3/2*PI.[ /\ dom sin by SIN_COS:24,XBOOLE_0:def 4;
A16: sin.r3 >= -1 by A9,ABSVALUE:5;
now
per cases by A8,XXREAL_0:1;
suppose
A17: PI/2 < r1;
then
A18: PI/2 < r2 by A3,XXREAL_0:2;
now
per cases by A7,XXREAL_0:1;
suppose
A19: r2 < 3/2*PI;
then r1 < 3/2*PI by A3,XXREAL_0:2;
then r1 in ].PI/2,3/2*PI.[ by A17,XXREAL_1:4;
then
A20: r1 in ].PI/2,3/2*PI.[ /\ dom sin by A4,XBOOLE_0:def 4;
r2 in ].PI/2,3/2*PI.[ by A18,A19,XXREAL_1:4;
then r2 in ].PI/2,3/2*PI.[ /\ dom sin by A11,XBOOLE_0:def 4;
hence sin.r2 < sin.r1 by A3,A20,Th20,RFUNCT_2:21;
end;
suppose
A21: r2 = 3/2*PI;
then r1 in ].PI/2,3/2*PI.[ by A3,A17,XXREAL_1:4;
then r1 in ].PI/2,3/2*PI.[ /\ dom sin by A4,XBOOLE_0:def 4;
then
A22: sin.r3 < sin.r1 by A12,A15,Th20,RFUNCT_2:21;
assume sin.r2 >= sin.r1;
hence contradiction by A6,A16,A21,A22,SIN_COS:76,XXREAL_0:1;
end;
end;
hence sin.r2 < sin.r1;
end;
suppose
A23: PI/2 = r1;
now
per cases by A7,XXREAL_0:1;
suppose
r2 < 3/2*PI;
then r2 in ].PI/2,3/2*PI.[ by A3,A23,XXREAL_1:4;
then r2 in ].PI/2,3/2*PI.[ /\ dom sin by A11,XBOOLE_0:def 4;
then
A24: sin.r2 < sin.r3 by A14,A15,Th20,RFUNCT_2:21;
assume sin.r2 >= sin.r1;
hence contradiction by A10,A5,A23,A24,SIN_COS:76,XXREAL_0:1;
end;
suppose
r2 = 3/2*PI;
hence sin.r2 < sin.r1 by A23,SIN_COS:76;
end;
end;
hence sin.r2 < sin.r1;
end;
end;
hence sin.r2 < sin.r1;
end;
hence thesis by RFUNCT_2:21;
end;
theorem Th25:
cos|[.0,PI.] is decreasing
proof
now
let r1,r2 be Real;
assume that
A1: r1 in [.0,PI.] /\ dom cos and
A2: r2 in [.0,PI.] /\ dom cos and
A3: r1 < r2;
A4: r1 in dom cos by A1,XBOOLE_0:def 4;
|.cos r2.| <= 1 by SIN_COS:27;
then |.cos.r2.| <= 1 by SIN_COS:def 19;
then
A5: cos.r2 <= 1 by ABSVALUE:5;
|.cos r1.| <= 1 by SIN_COS:27;
then |.cos.r1.| <= 1 by SIN_COS:def 19;
then
A6: cos.r1 >= -1 by ABSVALUE:5;
r2 in [.0,PI.] by A2,XBOOLE_0:def 4;
then
A7: r2 <= PI by XXREAL_1:1;
set r3 = (r1+r2)/2;
A8: r1 < r3 by A3,XREAL_1:226;
|.cos r3.| <= 1 by SIN_COS:27;
then
A9: |.cos.r3.| <= 1 by SIN_COS:def 19;
then
A10: cos.r3 <= 1 by ABSVALUE:5;
A11: r2 in dom cos by A2,XBOOLE_0:def 4;
A12: r1 in [.0,PI.] by A1,XBOOLE_0:def 4;
then
A13: 0 < r3 by A8,XXREAL_1:1;
A14: r3 < r2 by A3,XREAL_1:226;
then r3 < PI by A7,XXREAL_0:2;
then r3 in ].0,PI.[ by A13,XXREAL_1:4;
then
A15: r3 in ].0,PI.[ /\ dom cos by SIN_COS:24,XBOOLE_0:def 4;
A16: cos.r3 >= -1 by A9,ABSVALUE:5;
now
per cases by A12,XXREAL_1:1;
suppose
A17: 0 < r1;
now
per cases by A7,XXREAL_0:1;
suppose
A18: r2 < PI;
then r1 < PI by A3,XXREAL_0:2;
then r1 in ].0,PI.[ by A17,XXREAL_1:4;
then
A19: r1 in ].0,PI.[ /\ dom cos by A4,XBOOLE_0:def 4;
r2 in ].0,PI.[ by A3,A17,A18,XXREAL_1:4;
then r2 in ].0,PI.[ /\ dom cos by A11,XBOOLE_0:def 4;
hence cos.r2 < cos.r1 by A3,A19,Th21,RFUNCT_2:21;
end;
suppose
A20: r2 = PI;
then r1 in ].0,PI.[ by A3,A17,XXREAL_1:4;
then r1 in ].0,PI.[ /\ dom cos by A4,XBOOLE_0:def 4;
then
A21: cos.r3 < cos.r1 by A8,A15,Th21,RFUNCT_2:21;
assume cos.r2 >= cos.r1;
hence contradiction by A6,A16,A20,A21,SIN_COS:76,XXREAL_0:1;
end;
end;
hence cos.r2 < cos.r1;
end;
suppose
A22: 0 = r1;
now
per cases by A7,XXREAL_0:1;
suppose
r2 < PI;
then r2 in ].0,PI.[ by A3,A22,XXREAL_1:4;
then r2 in ].0,PI.[ /\ dom cos by A11,XBOOLE_0:def 4;
then
A23: cos.r2 < cos.r3 by A14,A15,Th21,RFUNCT_2:21;
assume cos.r2 >= cos.r1;
hence contradiction by A10,A5,A22,A23,SIN_COS:30,XXREAL_0:1;
end;
suppose
r2 = PI;
hence cos.r2 < cos.r1 by A22,SIN_COS:30,76;
end;
end;
hence cos.r2 < cos.r1;
end;
end;
hence cos.r2 < cos.r1;
end;
hence thesis by RFUNCT_2:21;
end;
theorem Th26:
cos|[.PI,2*PI.] is increasing
proof
now
let r1,r2 be Real;
assume that
A1: r1 in [.PI,2*PI.] /\ dom cos and
A2: r2 in [.PI,2*PI.] /\ dom cos and
A3: r1 < r2;
A4: r1 in dom cos by A1,XBOOLE_0:def 4;
set r3 = (r1+r2)/2;
r1 in [.PI,2*PI.] by A1,XBOOLE_0:def 4;
then
A5: PI <= r1 by XXREAL_1:1;
|.cos r3.| <= 1 by SIN_COS:27;
then
A6: |.cos.r3.| <= 1 by SIN_COS:def 19;
then
A7: cos.r3 <= 1 by ABSVALUE:5;
r2 in [.PI,2*PI.] by A2,XBOOLE_0:def 4;
then
A8: r2 <= 2*PI by XXREAL_1:1;
A9: r1 < r3 by A3,XREAL_1:226;
then
A10: PI < r3 by A5,XXREAL_0:2;
A11: r3 < r2 by A3,XREAL_1:226;
then r3 < 2*PI by A8,XXREAL_0:2;
then r3 in ].PI,2*PI.[ by A10,XXREAL_1:4;
then
A12: r3 in ].PI,2*PI.[ /\ dom cos by SIN_COS:24,XBOOLE_0:def 4;
|.cos r2.| <= 1 by SIN_COS:27;
then |.cos.r2.| <= 1 by SIN_COS:def 19;
then
A13: cos.r2 >= -1 by ABSVALUE:5;
A14: r2 in dom cos by A2,XBOOLE_0:def 4;
A15: cos.r3 >= -1 by A6,ABSVALUE:5;
now
per cases by A5,XXREAL_0:1;
suppose
A16: PI < r1;
then
A17: PI < r2 by A3,XXREAL_0:2;
now
per cases by A8,XXREAL_0:1;
suppose
A18: r2 < 2*PI;
then r1 < 2*PI by A3,XXREAL_0:2;
then r1 in ].PI,2*PI.[ by A16,XXREAL_1:4;
then
A19: r1 in ].PI,2*PI.[ /\ dom cos by A4,XBOOLE_0:def 4;
r2 in ].PI,2*PI.[ by A17,A18,XXREAL_1:4;
then r2 in ].PI,2*PI.[ /\ dom cos by A14,XBOOLE_0:def 4;
hence cos.r2 > cos.r1 by A3,A19,Th22,RFUNCT_2:20;
end;
suppose
A20: r2 = 2*PI;
then r1 in ].PI,2*PI.[ by A3,A16,XXREAL_1:4;
then r1 in ].PI,2*PI.[ /\ dom cos by A4,XBOOLE_0:def 4;
then
A21: cos.r3 > cos.r1 by A9,A12,Th22,RFUNCT_2:20;
assume cos.r2 <= cos.r1;
hence contradiction by A7,A20,A21,SIN_COS:76,XXREAL_0:2;
end;
end;
hence cos.r2 > cos.r1;
end;
suppose
A22: PI = r1;
now
per cases by A8,XXREAL_0:1;
suppose
r2 < 2*PI;
then r2 in ].PI,2*PI.[ by A3,A22,XXREAL_1:4;
then r2 in ].PI,2*PI.[ /\ dom cos by A14,XBOOLE_0:def 4;
then
A23: cos.r2 > cos.r3 by A11,A12,Th22,RFUNCT_2:20;
assume cos.r2 <= cos.r1;
hence contradiction by A15,A13,A22,A23,SIN_COS:76,XXREAL_0:1;
end;
suppose
r2 = 2*PI;
hence cos.r2 > cos.r1 by A22,SIN_COS:76;
end;
end;
hence cos.r2 > cos.r1;
end;
end;
hence cos.r2 > cos.r1;
end;
hence thesis by RFUNCT_2:20;
end;
theorem Th27:
sin.x in [.-1,1 .] & cos.x in [.-1,1 .]
proof
|.cos x.| <= 1 by SIN_COS:27;
then |.cos.x.| <= 1 by SIN_COS:def 19;
then
A1: -1 <= cos.x & cos.x <= 1 by ABSVALUE:5;
|.sin x.| <= 1 by SIN_COS:27;
then |.sin.x.| <= 1 by SIN_COS:def 17;
then -1 <= sin.x & sin.x <= 1 by ABSVALUE:5;
hence thesis by A1,XXREAL_1:1;
end;
theorem
rng sin = [.-1,1 .]
proof
now
let y be object;
thus y in [.-1,1 .] implies ex x be object st x in dom sin & y = sin.x
proof
assume
A1: y in [.-1,1 .];
then reconsider y1=y as Real;
y1 in [.-1,1 .] \/ [.1,sin.(-PI/2).] by A1,XBOOLE_0:def 3;
then
sin|[.-PI/2,PI/2.] is continuous & y1 in [.sin.(-PI/2),sin.(PI/2).]
\/ [.sin .(PI/2),sin.(-PI/2).] by SIN_COS:30,76;
then consider x be Real such that
x in [.-PI/2,PI/2 .] and
A2: y1 = sin.x by FCONT_2:15,SIN_COS:24;
take x;
x in REAL by XREAL_0:def 1;
hence thesis by A2,SIN_COS:24;
end;
thus (ex x be object st x in dom sin & y = sin.x) implies y in [.-1,1 .]
by Th27,SIN_COS:24;
end;
hence thesis by FUNCT_1:def 3;
end;
theorem
rng cos = [.-1,1 .]
proof
now
let y be object;
thus y in [.-1,1 .] implies ex x be object st x in dom cos & y = cos.x
proof
assume
A1: y in [.-1,1 .];
then reconsider y1=y as Real;
cos|[.0,PI.] is continuous & y1 in [.cos.0,cos.PI.] \/ [.cos.PI,cos.
0 .] by A1,SIN_COS:30,76,XBOOLE_0:def 3;
then consider x be Real such that
x in [.0,PI.] and
A2: y1 = cos.x by FCONT_2:15,SIN_COS:24;
take x;
x in REAL by XREAL_0:def 1;
hence thesis by A2,SIN_COS:24;
end;
thus (ex x be object st x in dom cos & y = cos.x) implies y in [.-1,1 .]
by
Th27,SIN_COS:24;
end;
hence thesis by FUNCT_1:def 3;
end;
theorem
rng (sin|[.-PI/2,PI/2.]) = [.-1,1 .]
proof
set sin1 = sin|[.-PI/2,PI/2.];
now
let y be object;
thus y in [.-1,1 .] implies
ex x be object st x in dom sin1 & y = sin1.x
proof
assume
A1: y in [.-1,1 .];
then reconsider y1=y as Real;
PI/2 in [.-PI/2,PI/2.] by XXREAL_1:1;
then
A2: sin1.(PI/2) = sin.(PI/2) by FUNCT_1:49;
-PI/2 in [.-PI/2,PI/2.] by XXREAL_1:1;
then sin1.(-PI/2) = sin.(-PI/2) by FUNCT_1:49;
then y1 in [.sin1.(-PI/2),sin1.(PI/2).] by A1,A2,SIN_COS:30,76;
then
A3: sin1|[.-PI/2,PI/2.] is continuous & y1 in [.sin1.(-PI/2),sin1.(PI/2
).]\/[. sin1.(PI/2),sin1.(-PI/2).] by XBOOLE_0:def 3;
dom sin1 = [.-PI/2,PI/2 .] /\ REAL by RELAT_1:61,SIN_COS:24
.= [.-PI/2,PI/2 .] by XBOOLE_1:28;
then consider x be Real such that
A4: x in [.-PI/2,PI/2 .] and
A5: y1 = sin1.x by A3,FCONT_2:15;
take x;
x in REAL /\ [.-PI/2,PI/2 .] by A4,XBOOLE_0:def 4;
hence thesis by A5,RELAT_1:61,SIN_COS:24;
end;
thus (ex x be object st x in dom sin1 & y = sin1.x)
implies y in [.-1,1 .]
proof
given x be object such that
A6: x in dom sin1 and
A7: y = sin1.x;
dom sin1 c= dom sin by RELAT_1:60;
then reconsider x1=x as Real by A6,SIN_COS:24;
y = sin.x1 by A6,A7,FUNCT_1:47;
hence thesis by Th27;
end;
end;
hence thesis by FUNCT_1:def 3;
end;
theorem
rng (sin|[.PI/2,3/2*PI.]) = [.-1,1 .]
proof
set sin1 = sin|[.PI/2,3/2*PI.];
now
let y be object;
thus y in [.-1,1 .] implies
ex x be object st x in dom sin1 & y = sin1.x
proof
3/2*PI in [.PI/2,3/2*PI.] by Lm4,XXREAL_1:1;
then
A1: sin1.(3/2*PI) = sin.(3/2*PI) by FUNCT_1:49;
assume
A2: y in [.-1,1 .];
then reconsider y1=y as Real;
A3: dom sin1 = [.PI/2,3/2*PI .] /\ REAL by RELAT_1:61,SIN_COS:24
.= [.PI/2,3/2*PI .] by XBOOLE_1:28;
PI/2 in [.PI/2,3/2*PI.] by Lm4,XXREAL_1:1;
then sin1.(PI/2) = sin.(PI/2) by FUNCT_1:49;
then
sin1|[.PI/2,3/2*PI.] is continuous & y1 in [.sin1.(PI/2),sin1.(3/2*
PI).] \/ [.sin1.(3/2*PI),sin1.(PI/2).] by A2,A1,SIN_COS:76,XBOOLE_0:def 3;
then consider x be Real such that
A4: x in [.PI/2,3/2*PI.] and
A5: y1 = sin1.x by A3,Lm4,FCONT_2:15;
take x;
x in REAL /\ [.PI/2,3/2*PI.] by A4,XBOOLE_0:def 4;
hence thesis by A5,RELAT_1:61,SIN_COS:24;
end;
thus (ex x be object st x in dom sin1 & y = sin1.x)
implies y in [.-1,1 .]
proof
given x be object such that
A6: x in dom sin1 and
A7: y = sin1.x;
dom sin1 c= dom sin by RELAT_1:60;
then reconsider x1=x as Real by A6,SIN_COS:24;
y = sin.x1 by A6,A7,FUNCT_1:47;
hence thesis by Th27;
end;
end;
hence thesis by FUNCT_1:def 3;
end;
theorem Th32:
rng (cos|[.0,PI.]) = [.-1,1 .]
proof
set cos1 = cos|[.0,PI.];
now
let y be object;
thus y in [.-1,1 .] implies
ex x be object st x in dom cos1 & y = cos1.x
proof
PI in [.0,PI.] by XXREAL_1:1;
then
A1: cos1.PI = cos.PI by FUNCT_1:49;
assume
A2: y in [.-1,1 .];
then reconsider y1=y as Real;
A3: dom cos1 = [.0,PI .] /\ REAL by RELAT_1:61,SIN_COS:24
.= [.0,PI .] by XBOOLE_1:28;
0 in [.0,PI.] by XXREAL_1:1;
then cos1.0 = cos.0 by FUNCT_1:49;
then
cos1|[.0,PI.] is continuous & y1 in [.cos1.0,cos1.PI.] \/ [.cos1.PI,
cos1.0 .] by A2,A1,SIN_COS:30,76,XBOOLE_0:def 3;
then consider x be Real such that
A4: x in [.0,PI.] and
A5: y1 = cos1.x by A3,FCONT_2:15;
take x;
x in REAL /\ [.0,PI.] by A4,XBOOLE_0:def 4;
hence thesis by A5,RELAT_1:61,SIN_COS:24;
end;
thus (ex x be object st x in dom cos1 & y = cos1.x)
implies y in [.-1,1 .]
proof
given x be object such that
A6: x in dom cos1 and
A7: y = cos1.x;
dom cos1 c= dom cos by RELAT_1:60;
then reconsider x1=x as Real by A6,SIN_COS:24;
y = cos.x1 by A6,A7,FUNCT_1:47;
hence thesis by Th27;
end;
end;
hence thesis by FUNCT_1:def 3;
end;
theorem Th33:
rng (cos|[.PI,2*PI.]) = [.-1,1 .]
proof
set cos1 = cos|[.PI,2*PI.];
now
let y be object;
thus y in [.-1,1 .] implies
ex x be object st x in dom cos1 & y = cos1.x
proof
2*PI in [.PI,2*PI.] by Lm3,XXREAL_1:1;
then
A1: cos1.(2*PI) = cos.(2*PI) by FUNCT_1:49;
assume
A2: y in [.-1,1 .];
then reconsider y1=y as Real;
A3: dom cos1 = [.PI,2*PI .] /\ REAL by RELAT_1:61,SIN_COS:24
.= [.PI,2*PI .] by XBOOLE_1:28;
PI in [.PI,2*PI.] by Lm3,XXREAL_1:1;
then cos1.PI = cos.PI by FUNCT_1:49;
then
cos1|[.PI,2*PI.] is continuous & y1 in [.cos1.PI,cos1.(2*PI).] \/ [.
cos1.(2* PI),cos1.PI.] by A2,A1,SIN_COS:76,XBOOLE_0:def 3;
then consider x be Real such that
A4: x in [.PI,2*PI.] and
A5: y1 = cos1.x by A3,Lm3,FCONT_2:15;
take x;
x in REAL /\ [.PI,2*PI.] by A4,XBOOLE_0:def 4;
hence thesis by A5,RELAT_1:61,SIN_COS:24;
end;
thus (ex x be object st x in dom cos1 & y = cos1.x)
implies y in [.-1,1 .]
proof
given x be object such that
A6: x in dom cos1 and
A7: y = cos1.x;
dom cos1 c= dom cos by RELAT_1:60;
then reconsider x1=x as Real by A6,SIN_COS:24;
y = cos.x1 by A6,A7,FUNCT_1:47;
hence thesis by Th27;
end;
end;
hence thesis by FUNCT_1:def 3;
end;
begin :: Argument of Complex Number
definition
let z be Complex;
func Arg z -> Real means
:Def1:
z = |.z.|*cos it + |.z.|*sin it * <i> & 0 <=
it & it < 2*PI if z <> 0 otherwise it = 0;
existence
proof
thus z <> 0 implies
ex r be Real st z = |.z.|*cos r + |.z.|*sin r * <i> &
0 <= r & r < 2*PI
proof
|.z.| >= 0 by COMPLEX1:46;
then
A1: Re z/|.z.| <= 1 by COMPLEX1:54,XREAL_1:185;
assume
A2: z <> 0;
then
A3: |.z.| <> 0 by COMPLEX1:45;
now
per cases;
suppose
A4: Im z >= 0;
set 0PI = [.0,PI.];
reconsider cos1 = cos|0PI as PartFunc of 0PI,REAL by PARTFUN1:10;
reconsider cos1 as one-to-one PartFunc of 0PI,REAL by Th25,
RFUNCT_2:50;
reconsider r = cos1".(Re z/|.z.|) as Real;
A5: |.z.|^2 = (Re z)^2 + (Im z)^2 by Th3;
take r;
Re z >= -|.z.| by Th1;
then -1 <= Re z/|.z.| by COMPLEX1:46,XREAL_1:193;
then
A6: Re z/|.z.| in rng cos1 by A1,Th32,XXREAL_1:1;
then Re z/|.z.| in dom (cos1") by FUNCT_1:33;
then r in rng (cos1") by FUNCT_1:def 3;
then r in dom cos1 by FUNCT_1:33;
then
A7: r in [.0,PI.] by RELAT_1:57;
then r <= PI by XXREAL_1:1;
then
A8: r = PI or r < PI by XXREAL_0:1;
A9: cos r = cos.r by SIN_COS:def 19
.= cos1.r by A7,FUNCT_1:49
.= Re z/|.z.| by A6,FUNCT_1:35;
0 = r or 0 < r by A7,XXREAL_1:1;
then r = 0 or r = PI or r in ].0,PI.[ by A8,XXREAL_1:4;
then
A10: sin.r >= 0 by Th7,SIN_COS:30,76;
(cos.r)^2 + (sin.r)^2 = 1 by SIN_COS:28;
then (sin.r)^2 = 1 - (cos.r)^2
.= 1 - (Re z/|.z.|)^2 by A9,SIN_COS:def 19
.= 1 - (Re z)^2/|.z.|^2 by XCMPLX_1:76
.= |.z.|^2/|.z.|^2 - (Re z)^2/|.z.|^2 by A3,XCMPLX_1:60
.= (|.z.|^2 - (Re z)^2)/|.z.|^2
.= ((Im z)/|.z.|)^2 by A5,XCMPLX_1:76;
then sin.r = sqrt((Im z)/|.z.|)^2 by A10,SQUARE_1:22
.= |.(Im z)/|.z.|.| by COMPLEX1:72
.= |.Im z.|/|.|.z.|.| by COMPLEX1:67
.= |.Im z.|/|.z.|;
then |.Im z.| = |.z.|*sin.r by A2,COMPLEX1:45,XCMPLX_1:87;
then
A11: Im z = |.z.|*sin.r by A4,ABSVALUE:def 1
.= |.z.|*sin r by SIN_COS:def 17;
Re z = |.z.|*cos r by A2,A9,COMPLEX1:45,XCMPLX_1:87;
hence z = |.z.|*cos r + |.z.|*sin r*<i> by A11,COMPLEX1:13;
thus 0 <= r by A7,XXREAL_1:1;
r <= PI by A7,XXREAL_1:1;
hence r < 2*PI by Lm3,XXREAL_0:2;
end;
suppose
A12: Im z < 0;
per cases;
suppose
A13: Re z <> |.z.|;
set 0PI = [.PI,2*PI.];
reconsider cos1 = cos|0PI as PartFunc of 0PI,REAL by PARTFUN1:10;
reconsider cos1 as one-to-one PartFunc of 0PI,REAL by Th26,
RFUNCT_2:50;
reconsider r = cos1".(Re z/|.z.|) as Real;
Re z >= -|.z.| by Th1;
then -1 <= Re z/|.z.| by COMPLEX1:46,XREAL_1:193;
then
A14: Re z/|.z.| in rng cos1 by A1,Th33,XXREAL_1:1;
then
A15: Re z/|.z.| in dom (cos1") by FUNCT_1:33;
then r in rng (cos1") by FUNCT_1:def 3;
then r in dom cos1 by FUNCT_1:33;
then
A16: r in [.PI,2*PI.] by RELAT_1:57;
then r <= 2*PI by XXREAL_1:1;
then
A17: r = 2*PI or r < 2*PI by XXREAL_0:1;
A18: Re z/|.z.| <> 1 by A13,XCMPLX_1:58;
A19: r <> 2*PI
proof
2*PI in [.PI,2*PI.] by Lm3,XXREAL_1:1;
then 2*PI in dom cos1 & cos1.(2*PI) = 1 by FUNCT_1:49
,RELAT_1:57,SIN_COS:24,76;
then
A20: cos1".1 = 2*PI by FUNCT_1:32;
1 in rng cos1 by Th33,XXREAL_1:1;
then
A21: 1 in dom (cos1") by FUNCT_1:33;
assume r = 2*PI;
hence contradiction by A18,A15,A21,A20,FUNCT_1:def 4;
end;
A22: cos r = cos.r by SIN_COS:def 19
.= cos1.r by A16,FUNCT_1:49
.= Re z/|.z.| by A14,FUNCT_1:35;
PI <= r by A16,XXREAL_1:1;
then PI = r or PI < r by XXREAL_0:1;
then r = PI or r = 2*PI or r in ].PI,2*PI.[ by A17,XXREAL_1:4;
then
A23: sin.r <= 0 by Th9,SIN_COS:76;
take r;
A24: |.z.|^2 = (Re z)^2 + (Im z)^2 by Th3;
(cos.r)^2 + (sin.r)^2 = 1 by SIN_COS:28;
then (sin.r)^2 = 1 - (cos.r)^2
.= 1 - (Re z/|.z.|)^2 by A22,SIN_COS:def 19
.= 1 - (Re z)^2/|.z.|^2 by XCMPLX_1:76
.= |.z.|^2/|.z.|^2 - (Re z)^2/|.z.|^2 by A3,XCMPLX_1:60
.= (|.z.|^2 - (Re z)^2)/|.z.|^2
.= ((Im z)/|.z.|)^2 by A24,XCMPLX_1:76;
then -sin.r = sqrt((Im z)/|.z.|)^2 by A23,SQUARE_1:23
.= |.(Im z)/|.z.|.| by COMPLEX1:72
.= |.Im z.|/|.|.z.|.| by COMPLEX1:67
.= |.Im z.|/|.z.|;
then sin.r = (-|.Im z.|)/|.z.|;
then -|.Im z.| = |.z.|*sin.r by A2,COMPLEX1:45,XCMPLX_1:87;
then
A25: --Im z = |.z.|*sin.r by A12,ABSVALUE:def 1
.= |.z.|*sin r by SIN_COS:def 17;
Re z = |.z.|*cos r by A2,A22,COMPLEX1:45,XCMPLX_1:87;
hence z = |.z.|*cos r + |.z.|*sin r*<i> by A25,COMPLEX1:13;
thus 0 <= r by A16,XXREAL_1:1;
r <= 2*PI by A16,XXREAL_1:1;
hence r < 2*PI by A19,XXREAL_0:1;
end;
suppose
A26: Re z = |.z.|;
reconsider r=0 as Real;
take r;
(Re z)^2 = (Re z)^2 + (Im z)^2 by A26,Th3;
then Im z = 0;
hence z = |.z.|*cos r+|.z.|*sin r*<i> by A26,COMPLEX1:13
,SIN_COS:31;
thus 0 <= r;
thus r < 2*PI by Lm1;
end;
end;
end;
hence thesis;
end;
thus thesis;
end;
uniqueness
proof
z <> 0 implies
for x,y be Real st z = |.z.|*cos x + |.z.|*sin x*<i> &
0 <= x & x < 2*PI & z = |.z.|*cos y + |.z.|*sin y*<i> & 0 <= y & y < 2*PI holds
x = y
proof
assume z <> 0;
then
A27: |.z.| <> 0 by COMPLEX1:45;
let x,y be Real;
assume that
A28: z = |.z.|*cos x + |.z.|*sin x*<i> and
A29: 0 <= x and
A30: x < 2*PI and
A31: z = |.z.|*cos y + |.z.|*sin y*<i> and
A32: 0 <= y and
A33: y < 2*PI;
|.z.|*cos x = |.z.|*cos y by A28,A31,COMPLEX1:77;
then cos x = cos y by A27,XCMPLX_1:5;
then cos x = cos.y by SIN_COS:def 19;
then
A34: cos.x = cos.y by SIN_COS:def 19;
|.z.|*sin x = |.z.|*sin y by A28,A31,COMPLEX1:77;
then sin x = sin y by A27,XCMPLX_1:5;
then
A35: sin x = sin.y by SIN_COS:def 17;
now
per cases;
suppose
A36: x <= PI & y <= PI;
then y in [.0,PI.] by A32,XXREAL_1:1;
then
A37: y in [.0,PI.] /\ dom cos by SIN_COS:24,XBOOLE_0:def 4;
assume x <> y;
then
A38: x < y or y < x by XXREAL_0:1;
x in [.0,PI.] by A29,A36,XXREAL_1:1;
then x in [.0,PI.] /\ dom cos by SIN_COS:24,XBOOLE_0:def 4;
hence contradiction by A34,A37,A38,Th25,RFUNCT_2:21;
end;
suppose
A39: x > PI & y > PI;
then y in [.PI,2*PI.] by A33,XXREAL_1:1;
then
A40: y in [.PI,2*PI.] /\ dom cos by SIN_COS:24,XBOOLE_0:def 4;
assume x <> y;
then
A41: x < y or y < x by XXREAL_0:1;
x in [.PI,2*PI.] by A30,A39,XXREAL_1:1;
then x in [.PI,2*PI.] /\ dom cos by SIN_COS:24,XBOOLE_0:def 4;
hence contradiction by A34,A40,A41,Th26,RFUNCT_2:20;
end;
suppose
A42: x <= PI & y > PI;
then y in ].PI,2*PI.[ by A33,XXREAL_1:4;
then
A43: sin.y < 0 by Th9;
x in [.0,PI.] by A29,A42,XXREAL_1:1;
then sin.x >= 0 by Th8;
hence thesis by A35,A43,SIN_COS:def 17;
end;
suppose
A44: y <= PI & x > PI;
then x in ].PI,2*PI.[ by A30,XXREAL_1:4;
then
A45: sin.x < 0 by Th9;
y in [.0,PI.] by A32,A44,XXREAL_1:1;
then sin.y >= 0 by Th8;
hence thesis by A35,A45,SIN_COS:def 17;
end;
end;
hence thesis;
end;
hence thesis;
end;
consistency;
end;
theorem Th34:
for z be Complex holds 0 <= Arg z & Arg z < 2*PI
proof
let z be Complex;
0 <= Arg z & Arg z < 2*PI or z = 0 by Def1;
hence thesis by Def1,Lm6,Lm7;
end;
theorem Th35:
for x be Real st x >= 0 holds Arg x = 0
proof
let x be Real;
A1: 0 <= Arg (x+0*<i>) & Arg (x+0*<i>) < 2*PI by Th34;
assume
A2: x >= 0;
per cases by A2;
suppose
A3: x > -0;
then
A4: (x+0*<i>) = |. (x+0*<i>) .|*cos Arg (x+0*<i>)+ |. (x+0*<i>) .|*sin Arg
(x+0*<i>)*<i> by Def1;
|. (x+0*<i>) .| <> 0 by A3,COMPLEX1:45;
then sin Arg (x+0*<i>) = 0 by A4,COMPLEX1:77;
then Arg (x+0*<i>) = 0 or |. (x+0*<i>) .|*-1 = x by A1,A4,Th17,SIN_COS:77;
then Arg (x+0*<i>) = 0 or |. (x+0*<i>) .| < 0 by A3;
hence thesis by COMPLEX1:46;
end;
suppose
x+0*<i> = 0;
hence thesis by Def1;
end;
end;
theorem Th36:
for x be Real st x < 0 holds Arg x = PI
proof
let x be Real;
A1: 0 <= Arg (x+0*<i>) & Arg (x+0*<i>) < 2*PI by Th34;
assume
A2: x < 0;
then
A3: (x+0*<i>) = |. (x+0*<i>) .|*cos Arg (x+0*<i>)+ |. (x+0*<i>) .|*sin Arg (
x+0*<i>)*<i> by Def1;
|. (x+0*<i>) .| <> 0 by A2,COMPLEX1:45;
then sin Arg (x+0*<i>) = 0 by A3,COMPLEX1:77;
then Arg (x+0*<i>) = PI or |. (x+0*<i>) .|*1 = x by A1,A3,Th17,SIN_COS:31;
hence thesis by A2,COMPLEX1:46;
end;
theorem Th37:
for x be Real st x > 0 holds Arg (x*<i>) = PI/2
proof
let x be Real;
A1: 0 <= Arg (0+x*<i>) & Arg (0+x*<i>) < 2*PI by Th34;
assume
A2: x > 0;
then
A3: 0+x*<i> <> 0;
then
A4: (0+x*<i>) = |. (0+x*<i>) .|*cos Arg (0+x*<i>)+ |. (0+x*<i>) .|*sin Arg (
0+x*<i>)*<i> by Def1;
|.0+x*<i>.| <> 0 by A3,COMPLEX1:45;
then cos Arg (0+x*<i>) = 0 by A4,COMPLEX1:77;
then Arg (0+x*<i>) = PI/2 or |. (0+x*<i>) .|*-1 = x by A1,A4,Th18,SIN_COS:77;
then Arg (0+x*<i>) = PI/2 or |. (0+x*<i>) .| < 0 by A2;
hence thesis by COMPLEX1:46;
end;
theorem Th38:
for x be Real st x < 0 holds Arg (x*<i>) = 3/2*PI
proof
let x be Real;
A1: 0 <= Arg (0+x*<i>) & Arg (0+x*<i>) < 2*PI by Th34;
assume
A2: x < 0;
then
A3: (0+x*<i>) <> 0;
then
A4: (0+x*<i>) = |. (0+x*<i>) .|*cos Arg (0+x*<i>)+ |. (0+x*<i>) .|*sin Arg (
0+x*<i>)*<i> by Def1;
|. (0+x*<i>) .| <> 0 by A3,COMPLEX1:45;
then cos Arg (0+x*<i>) = 0 by A4,COMPLEX1:77;
then Arg (0+x*<i>) = 3/2*PI or |. (0+x*<i>) .|*1 = x by A1,A4,Th18,SIN_COS:77
;
hence thesis by A2,COMPLEX1:46;
end;
theorem
Arg 1 = 0 by Th35;
theorem
Arg <i> = PI/2
proof
<i> = (0+1*<i>);
hence thesis by Th37;
end;
theorem Th41:
for z be Complex holds Arg z in ].0,PI/2.[ iff Re z > 0 & Im z > 0
proof
let z be Complex;
A1: Arg z < 2*PI by Th34;
thus Arg z in ].0,PI/2.[ implies Re z > 0 & Im z > 0
proof
assume
A2: Arg z in ].0,PI/2.[;
then
A3: Arg z > 0 by XXREAL_1:4;
then z <> 0 by Def1;
then
A4: z = |.z.|*cos Arg z+|.z.|*sin Arg z*<i> & |.z.| > 0 by Def1,COMPLEX1:47;
cos Arg z > 0 by A2,SIN_COS:81;
hence Re z > 0 by A4,COMPLEX1:12;
Arg z < PI/2 by A2,XXREAL_1:4;
then Arg z < PI by Lm2,XXREAL_0:2;
then Arg z in ].0,PI.[ by A3,XXREAL_1:4;
then sin.Arg z > 0 by Th7;
then sin Arg z > 0 by SIN_COS:def 17;
hence thesis by A4,COMPLEX1:12;
end;
assume that
A5: Re z > 0 and
A6: Im z > 0;
z = (Re z+Im z*<i>) by COMPLEX1:13;
then z <> 0+0*<i> by A5,COMPLEX1:77;
then
A7: |.z.| > 0 & z = |.z.|*cos Arg z+|.z.|*sin Arg z*<i> by Def1,COMPLEX1:47;
then sin Arg z > 0 by A6,COMPLEX1:12;
then
A8: sin.Arg z > 0 by SIN_COS:def 17;
cos Arg z > 0 by A5,A7,COMPLEX1:12;
then cos.Arg z > 0 by SIN_COS:def 19;
then
A9: not Arg z in [.PI/2,3/2*PI.] by Th14;
0 <= Arg z by Th34;
then
A10: Arg z > 0 by A8,SIN_COS:30;
not Arg z in [.PI,2*PI.] by A8,Th10;
then PI/2 > Arg z or PI > Arg z & 3/2*PI < Arg z by A1,A9,XXREAL_1:1;
hence thesis by A10,Lm5,XXREAL_0:2,XXREAL_1:4;
end;
theorem Th42:
for z be Complex holds Arg z in ].PI/2,PI.[ iff Re z < 0 & Im z > 0
proof
let z be Complex;
thus Arg z in ].PI/2,PI.[ implies Re z < 0 & Im z > 0
proof
assume
A1: Arg z in ].PI/2,PI.[;
then Arg z < PI by XXREAL_1:4;
then
A2: Arg z < 3/2*PI by Lm5,XXREAL_0:2;
A3: Arg z > PI/2 by A1,XXREAL_1:4;
then z <> 0 by Def1;
then
A4: z = |.z.|*cos Arg z+|.z.|*sin Arg z*<i> & |.z.| > 0 by Def1,COMPLEX1:47;
PI/2 < Arg z by A1,XXREAL_1:4;
then Arg z in ].PI/2,3/2*PI.[ by A2,XXREAL_1:4;
then cos.Arg z < 0 by Th13;
then cos Arg z < 0 by SIN_COS:def 19;
hence Re z < 0 by A4,COMPLEX1:12;
Arg z < PI by A1,XXREAL_1:4;
then Arg z in ].0,PI.[ by A3,XXREAL_1:4;
then sin.Arg z > 0 by Th7;
then sin Arg z > 0 by SIN_COS:def 17;
hence thesis by A4,COMPLEX1:12;
end;
assume that
A5: Re z < 0 and
A6: Im z > 0;
z = (Re z+Im z*<i>) by COMPLEX1:13;
then z <> 0+0*<i> by A5,COMPLEX1:77;
then
A7: |.z.| > 0 & z = |.z.|*cos Arg z+|.z.|*sin Arg z*<i> by Def1,COMPLEX1:47;
then sin Arg z > 0 by A6,COMPLEX1:12;
then sin.Arg z > 0 by SIN_COS:def 17;
then
A8: not Arg z in [.PI,2*PI.] by Th10;
cos Arg z < 0 by A5,A7,COMPLEX1:12;
then cos.Arg z < 0 by SIN_COS:def 19;
then not Arg z in [.-PI/2,PI/2.] by Th12;
then
A9: Arg z < -PI/2 or Arg z > PI/2 by XXREAL_1:1;
Arg z < 2*PI by Th34;
then Arg z < PI by A8,XXREAL_1:1;
hence thesis by A9,Th34,XXREAL_1:4;
end;
theorem Th43:
for z be Complex holds Arg z in ].PI,3/2*PI.[ iff Re z < 0 & Im z < 0
proof
let z be Complex;
thus Arg z in ].PI,3/2*PI.[ implies Re z < 0 & Im z < 0
proof
assume
A1: Arg z in ].PI,3/2*PI.[;
then PI < Arg z by XXREAL_1:4;
then
A2: PI/2 < Arg z by Lm2,XXREAL_0:2;
A3: Arg z > PI by A1,XXREAL_1:4;
then z <> 0 by Def1;
then
A4: z = |.z.|*cos Arg z+|.z.|*sin Arg z*<i> & |.z.| > 0 by Def1,COMPLEX1:47;
Arg z < 3/2*PI by A1,XXREAL_1:4;
then Arg z in ].PI/2,3/2*PI.[ by A2,XXREAL_1:4;
then cos.Arg z < 0 by Th13;
then cos Arg z < 0 by SIN_COS:def 19;
hence Re z < 0 by A4,COMPLEX1:12;
Arg z < 3/2*PI by A1,XXREAL_1:4;
then Arg z < 2*PI by Lm6,XXREAL_0:2;
then Arg z in ].PI,2*PI.[ by A3,XXREAL_1:4;
then sin.Arg z < 0 by Th9;
then sin Arg z < 0 by SIN_COS:def 17;
hence thesis by A4,COMPLEX1:12;
end;
assume that
A5: Re z < 0 and
A6: Im z < 0;
z = (Re z+Im z*<i>) by COMPLEX1:13;
then z <> 0+0*<i> by A5,COMPLEX1:77;
then
A7: |.z.| > 0 & z = |.z.|*cos Arg z+|.z.|*sin Arg z*<i> by Def1,COMPLEX1:47;
then cos Arg z < 0 by A5,COMPLEX1:12;
then cos.Arg z < 0 by SIN_COS:def 19;
then
A8: not Arg z in [.3/2*PI,2*PI.] by Th16;
sin Arg z < 0 by A6,A7,COMPLEX1:12;
then sin.Arg z < 0 by SIN_COS:def 17;
then
A9: not Arg z in [.0,PI.] by Th8;
Arg z < 2*PI by Th34;
then
A10: Arg z < 3/2*PI by A8,XXREAL_1:1;
0 <= Arg z by Th34;
then Arg z > PI by A9,XXREAL_1:1;
hence thesis by A10,XXREAL_1:4;
end;
theorem Th44:
for z be Complex holds Arg z in ].3/2*PI,2*PI.[ iff Re z
> 0 & Im z < 0
proof
let z be Complex;
thus Arg z in ].3/2*PI,2*PI.[ implies Re z > 0 & Im z < 0
proof
assume
A1: Arg z in ].3/2*PI,2*PI.[;
then
A2: Arg z < 2*PI by XXREAL_1:4;
A3: Arg z > 3/2*PI by A1,XXREAL_1:4;
then z <> 0 by Def1;
then
A4: z = |.z.|*cos Arg z+|.z.|*sin Arg z*<i> & |.z.| > 0 by Def1,COMPLEX1:47;
cos.Arg z > 0 by A1,Th15;
then cos Arg z > 0 by SIN_COS:def 19;
hence Re z > 0 by A4,COMPLEX1:12;
Arg z > PI by A3,Lm5,XXREAL_0:2;
then Arg z in ].PI,2*PI.[ by A2,XXREAL_1:4;
then sin.Arg z < 0 by Th9;
then sin Arg z < 0 by SIN_COS:def 17;
hence thesis by A4,COMPLEX1:12;
end;
assume that
A5: Re z > 0 and
A6: Im z < 0;
z = (Re z+Im z*<i>) by COMPLEX1:13;
then z <> 0+0*<i> by A5,COMPLEX1:77;
then
A7: |.z.| > 0 & z = |.z.|*cos Arg z+|.z.|*sin Arg z*<i> by Def1,COMPLEX1:47;
then sin Arg z < 0 by A6,COMPLEX1:12;
then sin.Arg z < 0 by SIN_COS:def 17;
then
A8: not Arg z in [.0,PI.] by Th8;
cos Arg z > 0 by A5,A7,COMPLEX1:12;
then cos.Arg z > 0 by SIN_COS:def 19;
then not Arg z in [.PI/2,3/2*PI.] by Th14;
then
A9: Arg z < PI/2 or Arg z > 3/2*PI by XXREAL_1:1;
0 <= Arg z by Th34;
then
A10: Arg z > PI by A8,XXREAL_1:1;
Arg z < 2*PI by Th34;
hence thesis by A10,A9,Lm2,XXREAL_0:2,XXREAL_1:4;
end;
theorem Th45:
for z be Complex st Im z > 0 holds sin Arg z > 0
proof
let z be Complex;
Re z < 0 or Re z = 0 or Re z > 0;
then
A1: Re z < 0 or Re z > 0 or z = (0+Im z*<i>) by COMPLEX1:13;
assume Im z > 0;
then Arg z in ].PI/2,PI.[ or Arg z in ].0,PI/2.[ or Arg z = PI/2 by A1,Th37
,Th41,Th42;
then
A2: PI/2 < Arg z & Arg z < PI or 0 < Arg z & Arg z < PI/2 or Arg z = PI/2 by
XXREAL_1:4;
then Arg z < PI by Lm2,XXREAL_0:2;
then Arg z in ].0,PI.[ by A2,XXREAL_1:4;
then sin.Arg z > 0 by Th7;
hence thesis by SIN_COS:def 17;
end;
theorem Th46:
for z be Complex st Im z < 0 holds sin Arg z < 0
proof
let z be Complex;
Re z < 0 or Re z = 0 or Re z > 0;
then
A1: Re z < 0 or Re z > 0 or z = (0+Im z*<i>) by COMPLEX1:13;
assume Im z < 0;
then
Arg z in ].PI,3/2*PI.[ or Arg z in ].3/2*PI,2*PI.[ or Arg z = 3/2*PI by A1
,Th38,Th43,Th44;
then
PI < Arg z & Arg z < 3/2*PI or 3/2*PI < Arg z & Arg z < 2*PI or Arg z =
3/2*PI by XXREAL_1:4;
then PI < Arg z & Arg z < 2*PI by Lm5,Lm6,XXREAL_0:2;
then Arg z in ].PI,2*PI.[ by XXREAL_1:4;
then sin.Arg z < 0 by Th9;
hence thesis by SIN_COS:def 17;
end;
theorem
for z be Complex st Im z >= 0 holds sin Arg z >= 0
proof
let z be Complex;
assume Im z >= 0;
then Im z > 0 or Im z = 0;
then sin Arg z > 0 or z = (Re z+0*<i>) & (Re z >= 0 or Re z < 0) by Th45,
COMPLEX1:13;
hence thesis by Th35,Th36,SIN_COS:31,77;
end;
theorem
for z be Complex st Im z <= 0 holds sin Arg z <= 0
proof
let z be Complex;
assume Im z <= 0;
then Im z < 0 or Im z = 0;
then sin Arg z < 0 or z = (Re z+0*<i>) & (Re z >= 0 or Re z < 0) by Th46,
COMPLEX1:13;
hence thesis by Th35,Th36,SIN_COS:31,77;
end;
theorem Th49:
for z be Complex st Re z > 0 holds cos Arg z > 0
proof
let z be Complex;
Im z < 0 or Im z = 0 or Im z > 0;
then
A1: Im z < 0 or Im z > 0 or z = (Re z+0*<i>) by COMPLEX1:13;
assume Re z > 0;
then Arg z in ].0,PI/2.[ or Arg z in ].3/2*PI,2*PI.[ or Arg z = 0 by A1,Th35
,Th41,Th44;
then cos.Arg z > 0 by Th15,SIN_COS:30,80;
hence thesis by SIN_COS:def 19;
end;
theorem Th50:
for z be Complex st Re z < 0 holds cos Arg z < 0
proof
let z be Complex;
Im z < 0 or Im z = 0 or Im z > 0;
then
A1: Im z < 0 or Im z > 0 or z = (Re z+0*<i>) by COMPLEX1:13;
assume Re z < 0;
then Arg z in ].PI/2,PI.[ or Arg z in ].PI,3/2*PI.[ or Arg z = PI by A1,Th36
,Th42,Th43;
then PI/2 < Arg z & Arg z < PI or PI < Arg z & Arg z < 3/2*PI or Arg z = PI
by XXREAL_1:4;
then PI/2 < Arg z & Arg z < 3/2*PI by Lm2,Lm5,XXREAL_0:2;
then Arg z in ].PI/2,3/2*PI.[ by XXREAL_1:4;
then cos.Arg z < 0 by Th13;
hence thesis by SIN_COS:def 19;
end;
theorem
for z be Complex st Re z >= 0 holds cos Arg z >= 0
proof
let z be Complex;
assume Re z >= 0;
then Re z > 0 or Re z = 0;
then
cos Arg z > 0 or z = (0+Im z*<i>) & (Im z > 0 or Im z < 0 or Im z = 0 )
by Th49,COMPLEX1:13;
hence thesis by Def1,Th37,Th38,SIN_COS:31,77;
end;
theorem
for z be Complex st Re z <= 0 & z <> 0 holds cos Arg z <= 0
proof
let z be Complex;
assume that
A1: Re z <= 0 and
A2: z <> 0;
A3: 0 = 0+0*<i>;
Re z < 0 or Re z = 0 by A1;
then cos Arg z < 0 or z = 0+Im z*<i> & (Im z >= 0 or Im z < 0) by Th50,
COMPLEX1:13;
then cos Arg z < 0 or z = 0+Im z*<i> & (Im z > 0 or Im z < 0) by A2,A3;
hence thesis by Th37,Th38,SIN_COS:77;
end;
theorem Th53:
for x be Real, n be Nat holds (cos x+(sin x)*<i>)|^n =
cos (n*x)+sin (n*x)*<i>
proof
let x be Real;
defpred P[Nat] means (cos x+(sin x)*<i>)|^$1 = cos ($1*x)+sin ($1*x)*<i>;
A1: now
let n be Nat;
assume P[n];
then
(cos x+(sin x)*<i>)|^(n+1) = (cos (n*x)+sin (n*x)*<i>)*(cos x+(sin x)*
<i>) by NEWTON:6
.= cos(n*x)*cos x - sin(n*x)*sin x +cos(n*x)*(sin x)*<i>+cos x*sin(n*x
)*<i>
.= cos(n*x+x)+cos(n*x)*(sin x)*<i>+cos x*sin(n*x)*<i> by SIN_COS:75
.= cos(n*x+x)+(cos(n*x)*sin x+cos x*sin(n*x))*<i>
.= cos ((n+1)*x)+sin ((n+1)*x)*<i> by SIN_COS:75;
hence P[n+1];
end;
A2: P[0] by NEWTON:4,SIN_COS:31;
thus for n being Nat holds P[n] from NAT_1:sch 2(A2,A1);
end;
theorem
for z be Element of COMPLEX for n be Nat st z <> 0 or n <> 0 holds z|^
n = (|.z.| |^ n)*cos (n*Arg z)+(|.z.| |^ n)*sin (n*Arg z)*<i>
proof
let z be Element of COMPLEX;
let n be Nat;
assume
A1: z <> 0 or n <> 0;
per cases by A1;
suppose
z <> 0;
hence z|^n = (|.z.|*cos Arg z+|.z.|*sin Arg z*<i>)|^n by Def1
.= ((|.z.|+0*<i>)*(cos Arg z+(sin Arg z)*<i>))|^n
.= ((|.z.|+0*<i>)|^n)* ((cos Arg z+(sin Arg z)*<i>))|^n by NEWTON:7
.= (|.z.| |^ n+0*<i>)*(cos (n*Arg z)+sin (n*Arg z)*<i>) by Th53
.= (|.z.| |^ n)*cos(n*Arg z)+ (|.z.| |^ n)*sin(n*Arg z)*<i>;
end;
suppose
A2: z = 0 & n > 0;
then
A3: n >= 1+0 by NAT_1:13;
hence z|^n = 0*cos(n*Arg z)+0*sin(n*Arg z)*<i> by A2,NEWTON:11
.= 0*cos(n*Arg z)+(|.z.| |^ n)*sin(n*Arg z)*<i> by A2,A3,COMPLEX1:44
,NEWTON:11
.= (|.z.| |^ n)*cos(n*Arg z)+(|.z.| |^ n)*sin(n*Arg z)*<i> by A2,A3,
COMPLEX1:44,NEWTON:11;
end;
end;
theorem Th55:
for x be Real, n,k be Nat st n <> 0 holds (cos((x+2*PI*k)/n)+sin
((x+2*PI*k)/n)*<i>)|^n = (cos x+(sin x)*<i>)
proof
let x be Real;
let n,k be Nat;
assume
A1: n <> 0;
thus (cos((x+2*PI*k)/n)+sin((x+2*PI*k)/n)*<i>)|^n = cos(n*((x+2*PI*k)/n))+
sin(n*((x+2*PI*k)/n))*<i> by Th53
.= cos(x+2*PI*k)+sin(n*((x+2*PI*k)/n))*<i> by A1,XCMPLX_1:87
.= cos(x+2*PI*k)+sin(x+2*PI*k)*<i> by A1,XCMPLX_1:87
.= cos.(x+2*PI*k)+sin(x+2*PI*k)*<i> by SIN_COS:def 19
.= cos.(x+2*PI*k)+sin.(x+2*PI*k)*<i> by SIN_COS:def 17
.= cos.(x+2*PI*k)+sin.x*<i> by SIN_COS2:10
.= cos.x+sin.x*<i> by SIN_COS2:11
.= cos.x+sin x*<i> by SIN_COS:def 17
.= (cos x+(sin x)*<i>) by SIN_COS:def 19;
end;
theorem Th56:
for z be Complex for n,k be Nat st n <> 0 holds z = ((n
-root |.z.|)*cos((Arg z+2*PI*k)/n)+ (n-root |.z.|)*sin((Arg z+2*PI*k)/n)*<i>)|^
n
proof
let z be Complex;
let n,k be Nat;
assume
A1: n <> 0;
then
A2: n >= 0+1 by NAT_1:13;
per cases;
suppose
A3: z <> 0;
thus ((n-root |.z.|)*cos((Arg z+2*PI*k)/n)+ (n-root |.z.|)*sin((Arg z+2*PI
*k)/n)*<i>)|^n = ((n-root |.z.|+0*<i>)* (cos((Arg z+2*PI*k)/n)+sin((Arg z+2*PI*
k)/n)*<i>))|^n
.= ((n-root |.z.|+0*<i>))|^n* (cos((Arg z+2*PI*k)/n)+sin((Arg z+2*PI*k
)/n)*<i>)|^n by NEWTON:7
.= (n-root |.z.|+0*<i>)|^n*(cos Arg z+(sin Arg z)*<i>) by A1,Th55
.= (|.z.|+0*<i>)*(cos Arg z+(sin Arg z)*<i>) by A1,Th4,COMPLEX1:46
.= |.z.|*cos Arg z-0*sin Arg z+(|.z.|*sin Arg z+0*cos Arg z)*<i>
.= z by A3,Def1;
end;
suppose
A4: z = 0;
hence
((n-root |.z.|)*cos((Arg z+2*PI*k)/n)+ (n-root |.z.|)*sin((Arg z+2*PI
*k)/n)*<i>)|^n = (0*cos((Arg z+2*PI*k)/n)+ (n-root 0)*sin((Arg z+2*PI*k)/n)*<i>
)|^n by A2,COMPLEX1:44,POWER:5
.= (0+0*sin((Arg z+2*PI*k)/n)*<i>)|^n by A2,POWER:5
.= z by A2,A4,NEWTON:11;
end;
end;
definition
let x be Complex;
let n be non zero Nat;
mode CRoot of n,x -> Complex means
:Def2:
it|^n = x;
existence
proof
reconsider z=(n-root |. x .|)*cos((Arg x+2*PI*0)/n)+ (n-root |. x .|)*sin(
(Arg x+2*PI*0)/n)*<i> as Element of COMPLEX by XCMPLX_0:def 2;
take z;
thus thesis by Th56;
end;
end;
theorem
for x be Element of COMPLEX for n be non zero Nat for k be Nat holds
(n-root |. x .|)*cos((Arg x+2*PI*k)/n)+ (n-root |. x .|)*sin((Arg x+2*PI*k)/n)*
<i> is CRoot of n,x
proof
let x be Element of COMPLEX;
let n be non zero Nat;
let k be Nat;
reconsider z = (n-root |. x .|)*cos((Arg x+2*PI*k)/n)+ (n-root |. x .|)*sin(
(Arg x+2*PI*k)/n)*<i> as Element of COMPLEX by XCMPLX_0:def 2;
z|^n = x by Th56;
hence thesis by Def2;
end;
theorem
for x be Element of COMPLEX for v be CRoot of 1,x holds v = x
proof
let x be Element of COMPLEX;
let v be CRoot of 1,x;
v|^1 = x by Def2;
hence thesis;
end;
theorem
for n be non zero Nat for v be CRoot of n,0 holds v = 0
proof
let n be non zero Nat;
let v be CRoot of n,0;
defpred P[Nat] means v|^$1 = 0;
assume
A1: v <> 0;
A2: now
let k be non zero Nat;
assume that
A3: k <> 1 and
A4: P[k];
consider t be Nat such that
A5: k = t+1 by NAT_1:6;
reconsider t as non zero Nat by A3,A5;
take t;
thus t < k by A5,NAT_1:13;
v|^k = v|^t*v by A5,NEWTON:6;
hence P[t] by A1,A4;
end;
A6: ex n be non zero Nat st P[n]
proof
take n;
thus thesis by Def2;
end;
P[1] from Regrwithout0(A6,A2);
hence thesis by A1;
end;
theorem
for n be non zero Nat for x be Element of COMPLEX for v be CRoot of n
,x st v = 0 holds x = 0
proof
let n be non zero Nat;
let x be Element of COMPLEX;
let v be CRoot of n,x;
assume v = 0;
then n >= 0+1 & 0|^n = x by Def2,NAT_1:13;
hence thesis by NEWTON:11;
end;
theorem
for a being Real st 0 <= a & a < 2*PI & cos(a) = 1 holds a = 0
proof
let a be Real such that
A1: 0 <= a & a < 2*PI and
A2: cos(a) = 1;
1*1+(sin a)*(sin a) = 1 by A2,SIN_COS:29;
then sin a = 0;
hence thesis by A1,A2,Th17,SIN_COS:77;
end;
theorem
for z being Complex holds z = |.z.|*cos Arg z + |.z.|*sin Arg z * <i>
proof
let z be Complex;
per cases;
suppose
z = 0;
hence thesis by COMPLEX1:44;
end;
suppose
z <> 0;
hence thesis by Def1;
end;
end;