Copyright (c) 2000 Association of Mizar Users
environ
vocabulary RLVECT_1, VECTSP_1, COMPLEX1, ARYTM_1, SQUARE_1, ABSVALUE,
COMPLFLD, HAHNBAN1, GROUP_1, FUNCT_1, BINOP_1, POWER, RAT_1, PREPOWER,
RCOMP_1, SIN_COS, ARYTM_3, RFUNCT_2, FDIFF_1, PRE_TOPC, BOOLE, RELAT_1,
FCONT_1, PARTFUN1, COMPTRIG, ARYTM;
notation TARSKI, XBOOLE_0, SUBSET_1, STRUCT_0, ORDINAL1, NUMBERS, ARYTM_0,
XREAL_0, REAL_1, SQUARE_1, NAT_1, RAT_1, ABSVALUE, PREPOWER, POWER,
RLVECT_1, VECTSP_1, BINOP_1, RELAT_1, FUNCT_1, RFUNCT_2, FCONT_1,
FDIFF_1, SEQ_1, PARTFUN1, PARTFUN2, COMPLEX1, BINARITH, RCOMP_1, GROUP_1,
SIN_COS, COMPLFLD, HAHNBAN1;
constructors REAL_1, BINOP_1, TRIANG_1, SQUARE_1, PREPOWER, POWER, SEQ_1,
RFUNCT_1, RFUNCT_2, FCONT_1, BINARITH, COMSEQ_3, GROUP_1, ALGSTR_2,
RCOMP_1, VECTSP_2, FDIFF_1, PARTFUN2, COMPLSP1, SIN_COS, HAHNBAN1,
COMPLEX1, MEMBERED, ARYTM_0, ARYTM_3, FUNCT_4;
clusters XREAL_0, STRUCT_0, RELSET_1, PARTFUN2, BINARITH, GROUP_1, GCD_1,
COMPLFLD, POLYNOM2, MONOID_0, NAT_1, MEMBERED, NUMBERS, ORDINAL2;
requirements NUMERALS, BOOLE, SUBSET, REAL, ARITHM;
definitions RFUNCT_2;
theorems AXIOMS, XREAL_0, REAL_1, REAL_2, NAT_1, SQUARE_1, PREPOWER, POWER,
BINARITH, ABSVALUE, RELAT_1, FUNCT_1, RFUNCT_2, PARTFUN1, FCONT_1,
FCONT_2, CARD_1, TOPREAL3, RLVECT_1, VECTSP_1, GROUP_1, RCOMP_1, FDIFF_1,
ROLLE, COMPLEX1, SIN_COS, SIN_COS2, COMPLFLD, HAHNBAN1, POLYNOM2,
TOPREAL5, JORDAN6, XBOOLE_0, XCMPLX_0, XCMPLX_1, ARYTM_0;
schemes NAT_1;
begin
scheme Regr_without_0 { P[Nat] } :
P[1]
provided
A1: ex k be non empty Nat st P[k] and
A2: for k be non empty Nat st k <> 1 & P[k]
ex n be non empty Nat st n < k & P[n]
proof
defpred R[Nat] means P[$1+1];
consider t be non empty Nat such that
A3: P[t] by A1;
consider s be Nat such that
A4: t = s+1 by NAT_1:22;
A5: ex k be Nat st R[k] by A3,A4;
A6: now let k be Nat;
assume that
A7: k <> 0 and
A8: R[k];
reconsider k1=k+1 as non empty Nat;
k > 0 by A7,NAT_1:19;
then k+1 > 0+1 by REAL_1:53;
then consider n be non empty Nat such that
A9: n < k1 and
A10: P[n] by A2,A8;
consider l be Nat such that
A11: n = l+1 by NAT_1:22;
take l;
thus l < k by A9,A11,AXIOMS:24;
thus R[l] by A10,A11;
end;
R[0] from Regr(A5,A6);
hence thesis;
end;
canceled 2;
theorem Th3:
for z be Element of COMPLEX holds
Re z >= -|.z.|
proof
let z be Element of COMPLEX;
0 <= (Im z)^2 by SQUARE_1:72;
then (Re z)^2+0 <= (Re z)^2 + (Im z)^2 by REAL_1:55;
then 0 <= (Re z)^2 & (Re z)^2 <= (Re z)^2 + (Im z)^2 by SQUARE_1:72;
then sqrt(Re z)^2 <= sqrt((Re z)^2 + (Im z)^2) by SQUARE_1:94;
then sqrt(Re z)^2 <= |.z.| by COMPLEX1:def 16;
then -sqrt(Re z)^2 >= -|.z.| by REAL_1:50;
then Re z >= -abs(Re z) & -abs(Re z) >= -|.z.| by ABSVALUE:11,SQUARE_1:91;
hence thesis by AXIOMS:22;
end;
theorem Th4:
for z be Element of COMPLEX holds
Im z >= -|.z.|
proof
let z be Element of COMPLEX;
0 <= (Re z)^2 by SQUARE_1:72;
then (Im z)^2+0 <= (Re z)^2 + (Im z)^2 by REAL_1:55;
then 0 <= (Im z)^2 & (Im z)^2 <= (Re z)^2 + (Im z)^2 by SQUARE_1:72;
then sqrt(Im z)^2 <= sqrt((Re z)^2 + (Im z)^2) by SQUARE_1:94;
then sqrt(Im z)^2 <= |.z.| by COMPLEX1:def 16;
then -sqrt(Im z)^2 >= -|.z.| by REAL_1:50;
then Im z >= -abs(Im z) & -abs(Im z) >= -|.z.| by ABSVALUE:11,SQUARE_1:91;
hence thesis by AXIOMS:22;
end;
theorem Th5:
for z be Element of F_Complex holds
Re z >= -|.z.|
proof
let z be Element of F_Complex;
consider z1 be Element of COMPLEX such that
A1: z = z1 and
A2: Re z = Re z1 by HAHNBAN1:def 3;
consider z2 be Element of COMPLEX such that
A3: z = z2 and
A4: |.z.| = |.z2.| by COMPLFLD:def 3;
thus thesis by A1,A2,A3,A4,Th3;
end;
theorem
for z be Element of F_Complex holds
Im z >= -|.z.|
proof
let z be Element of F_Complex;
consider z1 be Element of COMPLEX such that
A1: z = z1 and
A2: Im z = Im z1 by HAHNBAN1:def 4;
consider z2 be Element of COMPLEX such that
A3: z = z2 and
A4: |.z.| = |.z2.| by COMPLFLD:def 3;
thus thesis by A1,A2,A3,A4,Th4;
end;
theorem Th7:
for z be Element of F_Complex holds
|.z.|^2 = (Re z)^2 + (Im z)^2
proof
let z be Element of F_Complex;
consider z1 be Element of COMPLEX such that
A1: z = z1 and
A2: Re z = Re z1 by HAHNBAN1:def 3;
consider z2 be Element of COMPLEX such that
A3: z = z2 and
A4: Im z = Im z2 by HAHNBAN1:def 4;
consider z3 be Element of COMPLEX such that
A5: z = z3 and
A6: |.z.| = |.z3.| by COMPLFLD:def 3;
thus |.z.|^2 = |.z.|*|.z.| by SQUARE_1:def 3
.= |.z3*z3.| by A6,COMPLEX1:151
.= (Re z)^2 + (Im z)^2 by A1,A2,A3,A4,A5,COMPLEX1:154;
end;
theorem Th8:
for x1,x2,y1,y2 be Real holds
[**x1,x2**] = [**y1,y2**] implies x1 = y1 & x2 = y2
proof
let x1,x2,y1,y2 be Real;
assume [**x1,x2**] = [**y1,y2**];
then [*x1,x2*] = [**y1,y2**] by HAHNBAN1:def 1
.= [*y1,y2*] by HAHNBAN1:def 1;
hence thesis by ARYTM_0:12;
end;
theorem Th9:
for z be Element of F_Complex holds
z = [**Re z,Im z**]
proof
let z be Element of F_Complex;
reconsider z1=z as Element of COMPLEX by COMPLFLD:def 1;
thus z = [*Re z1,Im z1*] by COMPLEX1:8
.= [**Re z1,Im z1**] by HAHNBAN1:def 1
.= [**Re z,Im z1**] by HAHNBAN1:def 3
.= [**Re z,Im z**] by HAHNBAN1:def 4;
end;
L0: 0c = [*0,0*] by ARYTM_0:def 7,COMPLEX1:def 6;
L1: 1r = [*1,0*] by ARYTM_0:def 7,COMPLEX1:def 7;
theorem Th10:
0.F_Complex = [**0,0**] by L0,COMPLFLD:9,HAHNBAN1:def 1;
Lm1:
0.F_Complex = the Zero of F_Complex by RLVECT_1:def 2;
canceled;
theorem Th12:
for L be unital (non empty HGrStr)
for x be Element of L holds
(power L).(x,1) = x
proof
let L be unital (non empty HGrStr);
let x be Element of L;
0+1 = 1;
hence (power L).(x,1) = (power L).(x,0) * x by GROUP_1:def 7
.= 1.L * x by GROUP_1:def 7
.= x by GROUP_1:def 4;
end;
theorem
for L be unital (non empty HGrStr)
for x be Element of L holds
(power L).(x,2) = x*x
proof
let L be unital (non empty HGrStr);
let x be Element of L;
1+1 = 2;
hence (power L).(x,2) = (power L).(x,1) * x by GROUP_1:def 7
.= x * x by Th12;
end;
theorem Th14:
for L be add-associative right_zeroed right_complementable
right-distributive unital (non empty doubleLoopStr)
for n be Nat st n > 0 holds
(power L).(0.L,n) = 0.L
proof
let L be add-associative right_zeroed right_complementable
right-distributive unital (non empty doubleLoopStr);
let n be Nat;
assume n > 0;
then n >= 0+1 by NAT_1:38;
then A1: n-1 >= 0 by REAL_1:84;
n = n+-1+1 by XCMPLX_1:139
.= n-1+1 by XCMPLX_0:def 8
.= n-'1+1 by A1,BINARITH:def 3;
hence (power L).(0.L,n) = (power L).(0.L,n-'1)*0.L by GROUP_1:def 7
.= 0.L by VECTSP_1:36;
end;
theorem Th15:
for L be associative commutative unital (non empty HGrStr)
for x,y be Element of L
for n be Nat holds
(power L).(x*y,n) = (power L).(x,n) * (power L).(y,n)
proof
let L be associative commutative unital (non empty HGrStr);
let x,y be Element of L;
defpred P[Nat] means
(power L).(x*y,$1) = (power L).(x,$1) * (power L).(y,$1);
(power L).(x*y,0) = 1.L by GROUP_1:def 7
.= 1.L * 1.L by GROUP_1:def 4
.= (power L).(x,0) * 1.L by GROUP_1:def 7
.= (power L).(x,0) * (power L).(y,0) by GROUP_1:def 7;
then
A1: P[0];
A2: now let n be Nat;
assume P[n];
then (power L).(x*y,n+1) = (power L).(x,n) * (power L).(y,n) * (x*y) by
GROUP_1:def 7
.= (power L).(x,n) * ((power L).(y,n) * (x*y)) by VECTSP_1:def 16
.= (power L).(x,n) * (x*((power L).(y,n)*y)) by VECTSP_1:def 16
.= (power L).(x,n) * (x*(power L).(y,n+1)) by GROUP_1:def 7
.= (power L).(x,n)*x * (power L).(y,n+1) by VECTSP_1:def 16
.= (power L).(x,n+1) * (power L).(y,n+1) by GROUP_1:def 7;
hence P[n+1];
end;
thus for n be Nat holds P[n] from Ind(A1,A2);
end;
theorem Th16:
for x be Real st x > 0
for n be Nat holds
(power F_Complex).([**x,0**],n) = [**x to_power n,0**]
proof
let x be Real;
assume A1: x > 0;
defpred P[Nat] means
(power F_Complex).([**x,0**],$1) = [**x to_power $1,0**];
(power F_Complex).([**x,0**],0) = 1.F_Complex by GROUP_1:def 7
.= [*1,0*] by COMPLFLD:10,POLYNOM2:3,L1
.= [**1,0**] by HAHNBAN1:def 1
.= [**x to_power 0,0**] by POWER:29;
then
A2: P[0];
A3: now let n be Nat;
assume P[n];
then (power F_Complex).([**x,0**],n+1) = [**x to_power n,0**]*[**x,0**]
by GROUP_1:def 7
.= [**(x to_power n)*x-0*0,(x to_power n)*0+0*x**] by HAHNBAN1:11
.= [**(x to_power n)*(x to_power 1),0**] by POWER:30
.= [**x to_power (n+1),0**] by A1,POWER:32;
hence P[n+1];
end;
thus for n be Nat holds P[n] from Ind(A2,A3);
end;
theorem Th17:
for x be real number
for n be Nat st x >= 0 & n <> 0 holds
(n-root x) to_power n = x
proof
let x be real number;
let n be Nat;
assume that
A1: x >= 0 and
A2: n <> 0;
A3: n > 0 by A2,NAT_1:19;
then A4: n >= 0+1 by NAT_1:38;
reconsider n1=n as Rational;
per cases by A1;
suppose A5: x > 0;
n-root x = n -Root x by A1,A4,POWER:def 1;
then A6: n-root x > 0 by A4,A5,PREPOWER:def 3;
hence (n-root x) to_power n = (n-root x) #R n by POWER:def 2
.= (n-root x) #Q n1 by A6,PREPOWER:88
.= (n-root x) |^ n by A6,PREPOWER:60
.= x by A1,A4,POWER:5;
suppose A7: x = 0;
hence (n-root x) to_power n = 0 to_power n by A4,POWER:6
.= x by A3,A7,POWER:def 2;
end;
begin
canceled 2;
theorem Th20:
PI+PI/2 = 3/2*PI & 3/2*PI+PI/2 = 2*PI & 3/2*PI - PI = PI/2
proof
thus PI+PI/2 = (2/2)*PI + 1*(PI/2)
.= (2*PI)/2 + 1*(PI/2) by XCMPLX_1:75
.= 2*(PI/2) + 1*(PI/2) by XCMPLX_1:75
.= (2 + 1)*(PI/2) by XCMPLX_1:8
.= (3*PI)/2 by XCMPLX_1:75
.= 3/2*PI by XCMPLX_1:75;
thus 3/2*PI + PI/2 = 3*PI/2 + 1*PI/2 by XCMPLX_1:75
.= (3*PI+1*PI)/2 by XCMPLX_1:63
.= ((3+1)*PI)/2 by XCMPLX_1:8
.= 4/2*PI by XCMPLX_1:75
.= 2*PI;
thus 3/2*PI - PI = 3/2*PI - 2/2*PI
.= (3/2 - 2/2)*PI by XCMPLX_1:40
.= (3-2)/2*PI
.= 1*PI/2 by XCMPLX_1:75
.= PI/2;
end;
theorem Th21:
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
proof
thus A1: 0 < PI/2
proof
PI in ].0, 4.[ by SIN_COS:def 30;
then 0 < PI & PI < 4 by JORDAN6:45;
then 0/2 < PI/2 by REAL_1:73;
hence 0 < PI/2;
end;
thus A2: PI/2 < PI
proof
0 + PI/2 < PI/2 + PI/2 by A1,REAL_1:53;
hence PI/2 < PI by XCMPLX_1:66;
end;
hence A3: 0 < PI by A1,AXIOMS:22;
then A4: 0-PI/2 < PI-PI/2 by REAL_1:54;
PI/2 + PI/2 = PI by XCMPLX_1:66;
then PI - PI/2 = PI/2 by XCMPLX_1:26;
hence -PI/2 < PI/2 by A4,XCMPLX_1:150;
0 + PI < PI + PI by A3,REAL_1:53;
hence A5: PI < 2*PI by XCMPLX_1:11;
0+PI/2 < PI+PI/2 by A3,REAL_1:53;
hence PI/2 < 3/2*PI by Th20;
0 = -0;
hence -PI/2 < 0 by A1,REAL_1:50;
thus 0 < 2*PI by A1,A2,A5,AXIOMS:22;
PI/2+PI/2 < PI+PI/2 by A2,REAL_1:53;
hence A6: PI < 3/2*PI by Th20,XCMPLX_1:66;
hence 3/2*PI < 2*PI by Th20,REAL_1:53;
thus 0 < 3/2*PI by A1,A2,A6,AXIOMS:22;
end;
theorem Th22:
for a,b,c,x be real number 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 number;
assume that
A1: x in ].a,c.[ and
A2: not x in ].a,b.[ and
A3: not x = b;
A4: a < x & x < c by A1,JORDAN6:45;
x <= a or x >= b by A2,JORDAN6:45;
then x > b by A1,A3,JORDAN6:45,REAL_1:def 5;
hence x in ].b,c.[ by A4,JORDAN6:45;
end;
theorem Th23:
for x be Real st x in ].0,PI.[ holds sin.x > 0
proof
let x be Real;
assume A1: x in ].0,PI.[;
PI/2 + PI/2 = PI by XCMPLX_1:66;
then A2: PI - PI/2 = PI/2 by XCMPLX_1:26;
per cases by A1,Th22;
suppose x in ].0,PI/2.[;
then 0 < x & x < PI/2 by JORDAN6:45;
then 0-x < 0 & -x > -PI/2 by REAL_1:50,REAL_2:105;
then -x < 0 & -x > -PI/2 by XCMPLX_1:150;
then -x+PI/2 < 0+PI/2 & -x+PI/2 > -PI/2+PI/2 by REAL_1:53;
then PI/2-x < PI/2 & PI/2+ -x > PI/2-PI/2 by XCMPLX_0:def 8;
then PI/2-x < PI/2 & PI/2-x > PI/2-PI/2 by XCMPLX_0:def 8;
then 0 < PI/2-x & PI/2-x < PI/2 by XCMPLX_1:14;
then PI/2-x in ].0,PI/2.[ by JORDAN6:45;
then cos.(PI/2-x) > 0 by SIN_COS:85;
hence sin.x > 0 by SIN_COS:83;
suppose x=PI/2;
hence sin.x > 0 by SIN_COS:81;
suppose x in ].PI/2,PI.[;
then PI/2 < x & x < PI by JORDAN6:45;
then PI/2-PI/2 < x-PI/2 & x-PI/2 < PI-PI/2 by REAL_1:54;
then 0 < x-PI/2 & x-PI/2 < PI-PI/2 by XCMPLX_1:14;
then x-PI/2 in ].0,PI/2.[ by A2,JORDAN6:45;
then cos.(x-PI/2) > 0 by SIN_COS:85;
then cos.(-(PI/2-x)) > 0 by XCMPLX_1:143;
then cos.(PI/2-x) > 0 by SIN_COS:33;
hence sin.x > 0 by SIN_COS:83;
end;
theorem Th24:
for x be real number st x in [.0,PI.] holds sin.x >= 0
proof
let x be real number;
assume x in [.0,PI.];
then 0 <= x & x <= PI by TOPREAL5:1;
then x = 0 or x = PI or (0 < x & x < PI) by REAL_1:def 5;
then x = 0 or x = PI or x in ].0,PI.[ by JORDAN6:45;
hence sin.x >= 0 by Th23,SIN_COS:33,81;
end;
theorem Th25:
for x be Real st x in ].PI,2*PI.[ holds sin.x < 0
proof
let x be Real;
assume x in ].PI,2*PI.[;
then PI < x & x < 2*PI by JORDAN6:45;
then PI-PI < x-PI & x-PI < 2*PI-PI by REAL_1:54;
then 0 < x-PI & x-PI < 2*PI+-PI by XCMPLX_0:def 8,XCMPLX_1:14;
then 0 < x-PI & x-PI < PI by XCMPLX_1:184;
then A1: x-PI in ].0,PI.[ by JORDAN6:45;
sin.(x-PI) = sin.(-(PI-x)) by XCMPLX_1:143
.= -sin.(PI-x) by SIN_COS:33
.= -sin.(PI+-x) by XCMPLX_0:def 8
.= --sin.(-x) by SIN_COS:83
.= -sin.x by SIN_COS:33;
then -sin.x > 0 by A1,Th23;
hence sin.x < 0 by REAL_1:66;
end;
theorem Th26:
for x be real number st x in [.PI,2*PI.] holds sin.x <= 0
proof
let x be real number;
assume x in [.PI,2*PI.];
then PI <= x & x <= 2*PI by TOPREAL5:1;
then x = PI or x = 2*PI or (PI < x & x < 2*PI) by REAL_1:def 5;
then x = PI or x = 2*PI or x in ].PI,2*PI.[ by JORDAN6:45;
hence sin.x <= 0 by Th25,SIN_COS:81;
end;
reserve x for Real;
theorem Th27:
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 JORDAN6:45;
then -PI/2+PI/2 < x+PI/2 & x+PI/2 < PI/2+PI/2 by REAL_1:53;
then 0 < x+PI/2 & x+PI/2 < PI by XCMPLX_0:def 6,XCMPLX_1:66;
then A1: x+PI/2 in ].0,PI.[ by JORDAN6:45;
sin.(x+PI/2) = cos.x by SIN_COS:83;
hence cos.x > 0 by A1,Th23;
end;
theorem Th28:
for x be real number st x in [.-PI/2,PI/2.] holds cos.x >= 0
proof
let x be real number;
assume x in [.-PI/2,PI/2.];
then -PI/2 <= x & x <= PI/2 by TOPREAL5:1;
then x = -PI/2 or x = PI/2 or (-PI/2 < x & x < PI/2) by REAL_1:def 5;
then x = -PI/2 or x = PI/2 or x in ].-PI/2,PI/2.[ by JORDAN6:45;
hence cos.x >= 0 by Th27,SIN_COS:33,81;
end;
theorem Th29:
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 JORDAN6:45;
then PI/2+PI/2 < x+PI/2 & x+PI/2 < 3/2*PI+PI/2 by REAL_1:53;
then PI < x+PI/2 & x+PI/2 < 3/2*PI+PI/2 by XCMPLX_1:66;
then A1: x+PI/2 in ].PI,2*PI.[ by Th20,JORDAN6:45;
sin.(x+PI/2) = cos.x by SIN_COS:83;
hence cos.x < 0 by A1,Th25;
end;
theorem Th30:
for x be real number st x in [.PI/2,3/2*PI.] holds cos.x <= 0
proof
let x be real number;
assume x in [.PI/2,3/2*PI.];
then PI/2 <= x & x <= 3/2*PI by TOPREAL5:1;
then x = PI/2 or x = 3/2*PI or (PI/2 < x & x < 3/2*PI) by REAL_1:def 5;
then x = PI/2 or x = 3/2*PI or x in ].PI/2,3/2*PI.[ by JORDAN6:45;
hence cos.x <= 0 by Th20,Th29,SIN_COS:81;
end;
theorem Th31:
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 JORDAN6:45;
then 3/2*PI-PI < x-PI & x-PI < 2*PI-PI by REAL_1:54;
then PI/2 < x-PI & x-PI < 2*PI+-PI by Th20,XCMPLX_0:def 8;
then PI/2 < x-PI & x-PI < PI by XCMPLX_1:184;
then PI/2 < x-PI & x-PI < 3/2*PI by Th21,AXIOMS:22;
then A1: x-PI in ].PI/2,3/2*PI.[ by JORDAN6:45;
cos.(x-PI) = cos.(-(PI-x)) by XCMPLX_1:143
.= cos.(PI-x) by SIN_COS:33
.= cos.(PI+-x) by XCMPLX_0:def 8
.= -cos.(-x) by SIN_COS:83
.= -cos.x by SIN_COS:33;
then -cos.x < -0 by A1,Th29;
hence cos.x > 0 by REAL_1:50;
end;
theorem Th32:
for x be real number st x in [.3/2*PI,2*PI.] holds cos.x >= 0
proof
let x be real number;
assume x in [.3/2*PI,2*PI.];
then 3/2*PI <= x & x <= 2*PI by TOPREAL5:1;
then x = 3/2*PI or x = 2*PI or (3/2*PI < x & x < 2*PI)
by REAL_1:def 5;
then x = 3/2*PI or x = 2*PI or x in ].3/2*PI,2*PI.[ by JORDAN6:45;
hence cos.x >= 0 by Th20,Th31,SIN_COS:81;
end;
theorem Th33:
for x be real number st 0 <= x & x < 2*PI & sin x = 0 holds
x = 0 or x = PI
proof
let x be real number;
assume that
A1: 0 <= x and
A2: x < 2*PI and
A3: sin x = 0;
sin.x = 0 by A3,SIN_COS:def 21;
then not x in ].0,PI.[ & not x in ].PI,2*PI.[ by Th23,Th25;
then x = 0 or x >= PI & PI >= x by A1,A2,JORDAN6:45;
hence x = 0 or x = PI by AXIOMS:21;
end;
theorem Th34:
for x be real number st 0 <= x & x < 2*PI & cos x = 0 holds
x = PI/2 or x = 3/2*PI
proof
let x be real number;
assume that
A1: 0 <= x and
A2: x < 2*PI and
A3: cos x = 0;
A4: cos.x = 0 by A3,SIN_COS:def 23;
then not x in ].-PI/2,PI/2.[ & not x in ].PI/2,3/2*PI.[ by Th27,Th29;
then (-PI/2 >= x or x >= PI/2) & (PI/2 >= x or x >= 3/2*PI) by JORDAN6:45;
then x = PI/2 or x = 3/2*PI or x > 3/2* PI
by A1,Th21,REAL_1:def 5;
then x = PI/2 or x = 3/2*PI or x in ].3/2* PI,2*PI.[ by A2,JORDAN6:45;
hence x = PI/2 or x = 3/2*PI by A4,Th31;
end;
theorem Th35:
sin is_increasing_on ].-PI/2,PI/2.[
proof
A1: sin is_differentiable_on ].-PI/2,PI/2.[
proof
].-PI/2,PI/2.[ is open by RCOMP_1:25;
hence sin is_differentiable_on ].-PI/2,PI/2.[ by FDIFF_1:34,SIN_COS:73;
end;
for x be Real st x in ].-PI/2,PI/2.[ holds diff(sin,x) > 0
proof
let x be Real;
assume x in ].-PI/2,PI/2.[;
then 0 < cos.x by Th27;
hence diff(sin,x) > 0 by SIN_COS:73;
end;
hence thesis by A1,Th21,ROLLE:9;
end;
theorem Th36:
sin is_decreasing_on ].PI/2,3/2*PI.[
proof
A1: sin is_differentiable_on ].PI/2,3/2*PI.[
proof
].PI/2,3/2*PI.[ is open by RCOMP_1:25;
hence sin is_differentiable_on ].PI/2,3/2*PI.[ by FDIFF_1:34,SIN_COS:73;
end;
for x be Real st x in ].PI/2,3/2*PI.[ holds diff(sin,x) < 0
proof
let x be Real;
assume x in ].PI/2,3/2*PI.[;
then 0 > cos.x by Th29;
hence diff(sin,x) < 0 by SIN_COS:73;
end;
hence thesis by A1,Th21,ROLLE:10;
end;
theorem Th37:
cos is_decreasing_on ].0,PI.[
proof
A1: cos is_differentiable_on ].0,PI.[
proof
].0,PI.[ is open by RCOMP_1:25;
hence cos is_differentiable_on ].0,PI.[ by FDIFF_1:34,SIN_COS:72;
end;
for x be Real st x in ].0,PI.[ holds diff(cos,x) < 0
proof
let x be Real;
assume A2: x in ].0,PI.[;
A3: diff(cos,x) = -sin.x by SIN_COS:72;
0 < sin.x by A2,Th23;
then 0-sin.x < 0 by REAL_2:105;
hence diff(cos,x) < 0 by A3,XCMPLX_1:150;
end;
hence thesis by A1,Th21,ROLLE:10;
end;
theorem Th38:
cos is_increasing_on ].PI,2*PI.[
proof
A1: cos is_differentiable_on ].PI,2*PI.[
proof
].PI,2*PI.[ is open by RCOMP_1:25;
hence cos is_differentiable_on ].PI,2*PI.[ by FDIFF_1:34,SIN_COS:72;
end;
for x be Real st x in ].PI,2*PI.[ holds diff(cos,x) > 0
proof
let x be Real;
assume A2: x in ].PI,2*PI.[;
A3: diff(cos,x) = -sin.x by SIN_COS:72;
0 > sin.x by A2,Th25;
then 0-sin.x > 0 by SQUARE_1:11;
hence diff(cos,x) > 0 by A3,XCMPLX_1:150;
end;
hence thesis by A1,Th21,ROLLE:9;
end;
theorem
sin is_increasing_on [.-PI/2,PI/2.]
proof
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 [.-PI/2,PI/2.] & r1 in dom sin &
r2 in [.-PI/2,PI/2.] & r2 in dom sin by A1,A2,XBOOLE_0:def 3;
then A5: -PI/2 <= r1 & r1 <= PI/2 & -PI/2 <= r2 & r2 <= PI/2 by TOPREAL5:1;
set r3 = (r1+r2)/2;
abs(sin r3 ) <= 1 by SIN_COS:30;
then abs(sin.r3 ) <= 1 by SIN_COS:def 21;
then A6: sin.r3 >= -1 & sin.r3 <= 1 by ABSVALUE:12;
abs(sin r2 ) <= 1 by SIN_COS:30;
then abs(sin.r2 ) <= 1 by SIN_COS:def 21;
then A7: sin.r2 >= -1 by ABSVALUE:12;
A8: r1 < r3 & r3 < r2 by A3,TOPREAL3:3;
then -PI/2 < r3 & r3 < PI/2 by A5,AXIOMS:22;
then r3 in ].-PI/2,PI/2.[ & r3 in dom sin by JORDAN6:45,SIN_COS:27;
then A9: r3 in ].-PI/2,PI/2.[ /\ dom sin by XBOOLE_0:def 3;
now per cases by A5,REAL_1:def 5;
suppose A10: -PI/2 < r1;
then A11: -PI/2 < r2 by A3,AXIOMS:22;
now per cases by A5,REAL_1:def 5;
suppose A12: r2 < PI/2;
then r1 < PI/2 by A3,AXIOMS:22;
then r1 in ].-PI/2,PI/2.[ & r2 in ].-PI/2,PI/2.[
by A10,A11,A12,JORDAN6:45;
then r1 in ].-PI/2,PI/2.[ /\ dom sin & r2 in ].-PI/2,PI/2.[
/\ dom sin by A4,XBOOLE_0:def 3;
hence sin.r2 > sin.r1 by A3,Th35,RFUNCT_2:def 2;
suppose A13: r2 = PI/2;
then r1 in ].-PI/2,PI/2.[ by A3,A10,JORDAN6:45;
then r1 in ].-PI/2,PI/2.[ /\ dom sin by A4,XBOOLE_0:def 3;
then A14: sin.r3 > sin.r1 by A8,A9,Th35,RFUNCT_2:def 2;
assume sin.r2 <= sin.r1;
hence contradiction by A6,A13,A14,AXIOMS:22,SIN_COS:81;
end;
hence sin.r2 > sin.r1;
suppose A15: -PI/2 = r1;
now per cases by A5,REAL_1:def 5;
suppose r2 < PI/2;
then r2 in ].-PI/2,PI/2.[ by A3,A15,JORDAN6:45;
then r2 in ].-PI/2,PI/2.[ /\ dom sin by A4,XBOOLE_0:def 3;
then A16: sin.r2 > sin.r3 by A8,A9,Th35,RFUNCT_2:def 2;
assume sin.r2 <= sin.r1;
then sin.r2 <= -1 by A15,SIN_COS:33,81;
hence contradiction by A6,A7,A16,AXIOMS:21;
suppose r2 = PI/2;
then sin.r2 = 1 & sin.r1 = -1 by A15,SIN_COS:33,81;
hence sin.r2 > sin.r1;
end;
hence sin.r2 > sin.r1;
end;
hence sin.r2 > sin.r1;
end;
theorem
sin is_decreasing_on [.PI/2,3/2*PI.]
proof
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 [.PI/2,3/2*PI.] & r1 in dom sin &
r2 in [.PI/2,3/2*PI.] & r2 in dom sin by A1,A2,XBOOLE_0:def 3;
then A5: PI/2 <= r1 & r1 <= 3/2*PI & PI/2 <= r2 & r2 <= 3/2*PI by TOPREAL5:
1;
abs(sin r1 ) <= 1 by SIN_COS:30;
then abs(sin.r1 ) <= 1 by SIN_COS:def 21;
then A6: sin.r1 >= -1 by ABSVALUE:12;
set r3 = (r1+r2)/2;
abs(sin r3 ) <= 1 by SIN_COS:30;
then abs(sin.r3 ) <= 1 by SIN_COS:def 21;
then A7: sin.r3 >= -1 & sin.r3 <= 1 by ABSVALUE:12;
abs(sin r2 ) <= 1 by SIN_COS:30;
then abs(sin.r2 ) <= 1 by SIN_COS:def 21;
then A8: sin.r2 <= 1 by ABSVALUE:12;
A9: r1 < r3 & r3 < r2 by A3,TOPREAL3:3;
then PI/2 < r3 & r3 < 3/2*PI by A5,AXIOMS:22;
then r3 in ].PI/2,3/2*PI.[ & r3 in dom sin by JORDAN6:45,SIN_COS:27;
then A10: r3 in ].PI/2,3/2*PI.[ /\ dom sin by XBOOLE_0:def 3;
now per cases by A5,REAL_1:def 5;
suppose A11: PI/2 < r1;
then A12: PI/2 < r2 by A3,AXIOMS:22;
now per cases by A5,REAL_1:def 5;
suppose A13: r2 < 3/2*PI;
then r1 < 3/2*PI by A3,AXIOMS:22;
then r1 in ].PI/2,3/2*PI.[ & r2 in
].PI/2,3/2*PI.[ by A11,A12,A13,JORDAN6:45;
then r1 in ].PI/2,3/2*PI.[ /\ dom sin &
r2 in ].PI/2,3/2*PI.[ /\ dom sin by A4,XBOOLE_0:def 3;
hence sin.r2 < sin.r1 by A3,Th36,RFUNCT_2:def 3;
suppose A14: r2 = 3/2*PI;
then r1 in ].PI/2,3/2*PI.[ by A3,A11,JORDAN6:45;
then r1 in ].PI/2,3/2*PI.[ /\ dom sin by A4,XBOOLE_0:def 3;
then A15: sin.r3 < sin.r1 by A9,A10,Th36,RFUNCT_2:def 3;
assume sin.r2 >= sin.r1;
hence contradiction by A6,A7,A14,A15,Th20,AXIOMS:21,SIN_COS:81;
end;
hence sin.r2 < sin.r1;
suppose A16: PI/2 = r1;
now per cases by A5,REAL_1:def 5;
suppose r2 < 3/2*PI;
then r2 in ].PI/2,3/2*PI.[ by A3,A16,JORDAN6:45;
then r2 in ].PI/2,3/2*PI.[ /\ dom sin by A4,XBOOLE_0:def 3;
then A17: sin.r2 < sin.r3 by A9,A10,Th36,RFUNCT_2:def 3;
assume sin.r2 >= sin.r1;
hence contradiction by A7,A8,A16,A17,AXIOMS:21,SIN_COS:81;
suppose r2 = 3/2*PI;
hence sin.r2 < sin.r1 by A16,Th20,SIN_COS:81;
end;
hence sin.r2 < sin.r1;
end;
hence sin.r2 < sin.r1;
end;
theorem Th41:
cos is_decreasing_on [.0,PI.]
proof
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 [.0,PI.] & r1 in dom cos & r2 in [.0,PI.] & r2 in dom cos
by A1,A2,XBOOLE_0:def 3;
then A5: 0 <= r1 & r1 <= PI & 0 <= r2 & r2 <= PI by TOPREAL5:1;
abs(cos r1) <= 1 by SIN_COS:30;
then abs(cos.r1) <= 1 by SIN_COS:def 23;
then A6: cos.r1 >= -1 by ABSVALUE:12;
set r3 = (r1+r2)/2;
abs(cos r3) <= 1 by SIN_COS:30;
then abs(cos.r3) <= 1 by SIN_COS:def 23;
then A7: cos.r3 >= -1 & cos.r3 <= 1 by ABSVALUE:12;
abs(cos r2) <= 1 by SIN_COS:30;
then abs(cos.r2) <= 1 by SIN_COS:def 23;
then A8: cos.r2 <= 1 by ABSVALUE:12;
A9: r1 < r3 & r3 < r2 by A3,TOPREAL3:3;
then 0 < r3 & r3 < PI by A5,AXIOMS:22;
then r3 in ].0,PI.[ & r3 in dom cos by JORDAN6:45,SIN_COS:27;
then A10: r3 in ].0,PI.[ /\ dom cos by XBOOLE_0:def 3;
now per cases by A4,TOPREAL5:1;
suppose A11: 0 < r1;
then A12: 0 < r2 by A3,AXIOMS:22;
now per cases by A5,REAL_1:def 5;
suppose A13: r2 < PI;
then r1 < PI by A3,AXIOMS:22;
then r1 in ].0,PI.[ & r2 in ].0,PI.[ by A11,A12,A13,JORDAN6:45;
then r1 in ].0,PI.[ /\ dom cos & r2 in ].0,PI.[ /\ dom cos
by A4,XBOOLE_0:def 3;
hence cos.r2 < cos.r1 by A3,Th37,RFUNCT_2:def 3;
suppose A14: r2 = PI;
then r1 in ].0,PI.[ by A3,A11,JORDAN6:45;
then r1 in ].0,PI.[ /\ dom cos by A4,XBOOLE_0:def 3;
then A15: cos.r3 < cos.r1 by A9,A10,Th37,RFUNCT_2:def 3;
assume cos.r2 >= cos.r1;
hence contradiction by A6,A7,A14,A15,AXIOMS:21,SIN_COS:81;
end;
hence cos.r2 < cos.r1;
suppose A16: 0 = r1;
now per cases by A5,REAL_1:def 5;
suppose r2 < PI;
then r2 in ].0,PI.[ by A3,A16,JORDAN6:45;
then r2 in ].0,PI.[ /\ dom cos by A4,XBOOLE_0:def 3;
then A17: cos.r2 < cos.r3 by A9,A10,Th37,RFUNCT_2:def 3;
assume cos.r2 >= cos.r1;
hence contradiction by A7,A8,A16,A17,AXIOMS:21,SIN_COS:33;
suppose r2 = PI;
hence cos.r2 < cos.r1 by A16,SIN_COS:33,81;
end;
hence cos.r2 < cos.r1;
end;
hence cos.r2 < cos.r1;
end;
theorem Th42:
cos is_increasing_on [.PI,2*PI.]
proof
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 [.PI,2*PI.] & r1 in dom cos & r2 in [.PI,2*PI.] & r2 in
dom cos by A1,A2,XBOOLE_0:def 3;
then A5: PI <= r1 & r1 <= 2*PI & PI <= r2 & r2 <= 2*PI by TOPREAL5:1;
set r3 = (r1+r2)/2;
abs(cos r3 ) <= 1 by SIN_COS:30;
then abs(cos.r3 ) <= 1 by SIN_COS:def 23;
then A6: cos.r3 >= -1 & cos.r3 <= 1 by ABSVALUE:12;
abs(cos r2 ) <= 1 by SIN_COS:30;
then abs(cos.r2 ) <= 1 by SIN_COS:def 23;
then A7: cos.r2 >= -1 by ABSVALUE:12;
A8: r1 < r3 & r3 < r2 by A3,TOPREAL3:3;
then PI < r3 & r3 < 2*PI by A5,AXIOMS:22;
then r3 in ].PI,2*PI.[ & r3 in dom cos by JORDAN6:45,SIN_COS:27;
then A9: r3 in ].PI,2*PI.[ /\ dom cos by XBOOLE_0:def 3;
now per cases by A5,REAL_1:def 5;
suppose A10: PI < r1;
then A11: PI < r2 by A3,AXIOMS:22;
now per cases by A5,REAL_1:def 5;
suppose A12: r2 < 2*PI;
then r1 < 2*PI by A3,AXIOMS:22;
then r1 in ].PI,2*PI.[ & r2 in ].PI,2*PI.[ by A10,A11,A12,JORDAN6:45;
then r1 in ].PI,2*PI.[ /\ dom cos & r2 in ].PI,2*PI.[ /\ dom cos
by A4,XBOOLE_0:def 3;
hence cos.r2 > cos.r1 by A3,Th38,RFUNCT_2:def 2;
suppose A13: r2 = 2*PI;
then r1 in ].PI,2*PI.[ by A3,A10,JORDAN6:45;
then r1 in ].PI,2*PI.[ /\ dom cos by A4,XBOOLE_0:def 3;
then A14: cos.r3 > cos.r1 by A8,A9,Th38,RFUNCT_2:def 2;
assume cos.r2 <= cos.r1;
hence contradiction by A6,A13,A14,AXIOMS:22,SIN_COS:81;
end;
hence cos.r2 > cos.r1;
suppose A15: PI = r1;
now per cases by A5,REAL_1:def 5;
suppose r2 < 2*PI;
then r2 in ].PI,2*PI.[ by A3,A15,JORDAN6:45;
then r2 in ].PI,2*PI.[ /\ dom cos by A4,XBOOLE_0:def 3;
then A16: cos.r2 > cos.r3 by A8,A9,Th38,RFUNCT_2:def 2;
assume cos.r2 <= cos.r1;
hence contradiction by A6,A7,A15,A16,AXIOMS:21,SIN_COS:81;
suppose r2 = 2*PI;
hence cos.r2 > cos.r1 by A15,SIN_COS:81;
end;
hence cos.r2 > cos.r1;
end;
hence cos.r2 > cos.r1;
end;
theorem Th43:
sin is_continuous_on REAL &
for x,y be real number holds
sin is_continuous_on [.x,y.] & sin is_continuous_on ].x,y.[
proof
thus A1: sin is_continuous_on REAL by FDIFF_1:33,SIN_COS:73;
let x,y be real number;
thus thesis by A1,FCONT_1:17;
end;
theorem Th44:
cos is_continuous_on REAL &
for x,y be real number holds
cos is_continuous_on [.x,y.] & cos is_continuous_on ].x,y.[
proof
thus A1: cos is_continuous_on REAL by FDIFF_1:33,SIN_COS:72;
let x,y be real number;
thus thesis by A1,FCONT_1:17;
end;
theorem Th45:
sin.x in [.-1,1 .] & cos.x in [.-1,1 .]
proof
abs(sin x) <= 1 & abs(cos x) <= 1 by SIN_COS:30;
then abs(sin.x) <= 1 & abs(cos.x) <= 1 by SIN_COS:def 21,def 23;
then -1 <= sin.x & sin.x <= 1 & -1 <= cos.x & cos.x <= 1 by ABSVALUE:12;
hence thesis by TOPREAL5:1;
end;
theorem
rng sin = [.-1,1 .]
proof
now let y be set;
thus y in [.-1,1 .] implies ex x be set st x in dom sin & y = sin.x
proof
assume A1: y in [.-1,1 .];
then reconsider y1=y as Real;
A2: sin is_continuous_on [.-PI/2,PI/2 .] by Th43;
y1 in [.-1,1 .] \/ [.1,sin.(-PI/2).] by A1,XBOOLE_0:def 2;
then y1 in [.sin.(-PI/2),sin.(PI/2).] \/ [.sin.(PI/2),sin.(-PI/2).]
by SIN_COS:33,81;
then consider x be Real such that
x in [.-PI/2,PI/2 .] and
A3: y1 = sin.x by A2,Th21,FCONT_2:16;
take x;
x in REAL;
hence x in dom sin & y = sin.x by A3,SIN_COS:def 20;
end;
thus (ex x be set st x in dom sin & y = sin.x) implies y in [.-1,1 .]
proof
given x be set such that
A4: x in dom sin and
A5: y = sin.x;
reconsider x1=x as Real by A4,SIN_COS:def 20;
y = sin.x1 by A5;
hence y in [.-1,1 .] by Th45;
end;
end;
hence thesis by FUNCT_1:def 5;
end;
theorem
rng cos = [.-1,1 .]
proof
now let y be set;
thus y in [.-1,1 .] implies ex x be set st x in dom cos & y = cos.x
proof
assume A1: y in [.-1,1 .];
then reconsider y1=y as Real;
A2: cos is_continuous_on [.0,PI.] by Th44;
y1 in [.cos.0,cos.PI.] \/ [.cos.PI,cos.0 .]
by A1,SIN_COS:33,81,XBOOLE_0:def 2;
then consider x be Real such that
x in [.0,PI.] and
A3: y1 = cos.x by A2,Th21,FCONT_2:16;
take x;
x in REAL;
hence x in dom cos & y = cos.x by A3,SIN_COS:def 22;
end;
thus (ex x be set st x in dom cos & y = cos.x) implies y in [.-1,1 .]
proof
given x be set such that
A4: x in dom cos and
A5: y = cos.x;
reconsider x1=x as Real by A4,SIN_COS:def 22;
y = cos.x1 by A5;
hence y in [.-1,1 .] by Th45;
end;
end;
hence thesis by FUNCT_1:def 5;
end;
theorem
rng (sin|[.-PI/2,PI/2.]) = [.-1,1 .]
proof
set sin1 = sin|[.-PI/2,PI/2.];
now let y be set;
thus y in [.-1,1 .] implies ex x be set st x in dom sin1 & y = sin1.x
proof
assume A1: y in [.-1,1 .];
then reconsider y1=y as Real;
sin is_continuous_on [.-PI/2,PI/2 .] by Th43;
then A2: sin1 is_continuous_on [.-PI/2,PI/2 .] by FCONT_1:16;
-PI/2 in [.-PI/2,PI/2.] & PI/2 in [.-PI/2,PI/2.] by Th21,TOPREAL5:1;
then sin1.(PI/2) = sin.(PI/2) & sin1.(-PI/2) = sin.(-PI/2)
by FUNCT_1:72;
then y1 in [.sin1.(-PI/2),sin1.(PI/2).] by A1,SIN_COS:33,81;
then y1 in [.sin1.(-PI/2),sin1.(PI/2).]\/[.sin1.(PI/2),sin1.(-PI/2).]
by XBOOLE_0:def 2;
then consider x be Real such that
A3: x in [.-PI/2,PI/2 .] and
A4: y1 = sin1.x by A2,Th21,FCONT_2:16;
take x;
x in REAL /\ [.-PI/2,PI/2 .] by A3,XBOOLE_0:def 3;
then x in dom sin /\ [.-PI/2,PI/2 .] by SIN_COS:def 20;
hence x in dom sin1 & y = sin1.x by A4,FUNCT_1:68;
end;
thus (ex x be set st x in dom sin1 & y = sin1.x) implies y in [.-1,1 .]
proof
given x be set such that
A5: x in dom sin1 and
A6: y = sin1.x;
dom sin1 c= dom sin by FUNCT_1:76;
then reconsider x1=x as Real by A5,SIN_COS:def 20;
y = sin.x1 by A5,A6,FUNCT_1:70;
hence y in [.-1,1 .] by Th45;
end;
end;
hence thesis by FUNCT_1:def 5;
end;
theorem
rng (sin|[.PI/2,3/2*PI.]) = [.-1,1 .]
proof
set sin1 = sin|[.PI/2,3/2*PI.];
now let y be set;
thus y in [.-1,1 .] implies ex x be set st x in dom sin1 & y = sin1.x
proof
assume A1: y in [.-1,1 .];
then reconsider y1=y as Real;
sin is_continuous_on [.PI/2,3/2*PI.] by Th43;
then A2: sin1 is_continuous_on [.PI/2,3/2*PI.] by FCONT_1:16;
PI/2 in [.PI/2,3/2*PI.] & 3/2*PI in [.PI/2,3/2*PI.] by Th21,TOPREAL5:1;
then sin1.(PI/2) = sin.(PI/2) & sin1.(3/2*PI) = sin.(3/2*PI)
by FUNCT_1:72;
then y1 in [.sin1.(PI/2),sin1.(3/2*PI).] \/
[.sin1.(3/2*PI),sin1.(PI/2).] by A1,Th20,SIN_COS:81,XBOOLE_0:def 2;
then consider x be Real such that
A3: x in [.PI/2,3/2*PI.] and
A4: y1 = sin1.x by A2,Th21,FCONT_2:16;
take x;
x in REAL /\ [.PI/2,3/2*PI.] by A3,XBOOLE_0:def 3;
then x in dom sin /\ [.PI/2,3/2*PI.] by SIN_COS:def 20;
hence x in dom sin1 & y = sin1.x by A4,FUNCT_1:68;
end;
thus (ex x be set st x in dom sin1 & y = sin1.x) implies y in [.-1,1 .]
proof
given x be set such that
A5: x in dom sin1 and
A6: y = sin1.x;
dom sin1 c= dom sin by FUNCT_1:76;
then reconsider x1=x as Real by A5,SIN_COS:def 20;
y = sin.x1 by A5,A6,FUNCT_1:70;
hence y in [.-1,1 .] by Th45;
end;
end;
hence thesis by FUNCT_1:def 5;
end;
theorem Th50:
rng (cos|[.0,PI.]) = [.-1,1 .]
proof
set cos1 = cos|[.0,PI.];
now let y be set;
thus y in [.-1,1 .] implies ex x be set st x in dom cos1 & y = cos1.x
proof
assume A1: y in [.-1,1 .];
then reconsider y1=y as Real;
cos is_continuous_on [.0,PI.] by Th44;
then A2: cos1 is_continuous_on [.0,PI.] by FCONT_1:16;
0 in [.0,PI.] & PI in [.0,PI.] by Th21,TOPREAL5:1;
then cos1.0 = cos.0 & cos1.PI = cos.PI by FUNCT_1:72;
then y1 in [.cos1.0,cos1.PI.] \/ [.cos1.PI,cos1.0 .]
by A1,SIN_COS:33,81,XBOOLE_0:def 2;
then consider x be Real such that
A3: x in [.0,PI.] and
A4: y1 = cos1.x by A2,Th21,FCONT_2:16;
take x;
x in REAL /\ [.0,PI.] by A3,XBOOLE_0:def 3;
then x in dom cos /\ [.0,PI.] by SIN_COS:def 22;
hence x in dom cos1 & y = cos1.x by A4,FUNCT_1:68;
end;
thus (ex x be set st x in dom cos1 & y = cos1.x) implies y in [.-1,1 .]
proof
given x be set such that
A5: x in dom cos1 and
A6: y = cos1.x;
dom cos1 c= dom cos by FUNCT_1:76;
then reconsider x1=x as Real by A5,SIN_COS:def 22;
y = cos.x1 by A5,A6,FUNCT_1:70;
hence y in [.-1,1 .] by Th45;
end;
end;
hence thesis by FUNCT_1:def 5;
end;
theorem Th51:
rng (cos|[.PI,2*PI.]) = [.-1,1 .]
proof
set cos1 = cos|[.PI,2*PI.];
now let y be set;
thus y in [.-1,1 .] implies ex x be set st x in dom cos1 & y = cos1.x
proof
assume A1: y in [.-1,1 .];
then reconsider y1=y as Real;
cos is_continuous_on [.PI,2*PI.] by Th44;
then A2: cos1 is_continuous_on [.PI,2*PI.] by FCONT_1:16;
PI in [.PI,2*PI.] & 2*PI in [.PI,2*PI.] by Th21,TOPREAL5:1;
then cos1.PI = cos.PI & cos1.(2*PI) = cos.(2*PI) by FUNCT_1:72;
then y1 in [.cos1.PI,cos1.(2*PI).] \/ [.cos1.(2*PI),cos1.PI.]
by A1,SIN_COS:81,XBOOLE_0:def 2;
then consider x be Real such that
A3: x in [.PI,2*PI.] and
A4: y1 = cos1.x by A2,Th21,FCONT_2:16;
take x;
x in REAL /\ [.PI,2*PI.] by A3,XBOOLE_0:def 3;
then x in dom cos /\ [.PI,2*PI.] by SIN_COS:def 22;
hence x in dom cos1 & y = cos1.x by A4,FUNCT_1:68;
end;
thus (ex x be set st x in dom cos1 & y = cos1.x) implies y in [.-1,1 .]
proof
given x be set such that
A5: x in dom cos1 and
A6: y = cos1.x;
dom cos1 c= dom cos by FUNCT_1:76;
then reconsider x1=x as Real by A5,SIN_COS:def 22;
y = cos.x1 by A5,A6,FUNCT_1:70;
hence y in [.-1,1 .] by Th45;
end;
end;
hence thesis by FUNCT_1:def 5;
end;
begin :: Argument of Complex Number
definition
let z be Element of F_Complex;
func Arg z -> Real means :Def1:
z = [**|.z.|*cos it,|.z.|*sin it**] & 0 <= it & it < 2*PI
if z <> 0.F_Complex
otherwise it = 0;
existence
proof
thus z <> 0.F_Complex implies ex r be Real st
z = [**|.z.|*cos r,|.z.|*sin r**] & 0 <= r & r < 2*PI
proof
assume z <> 0.F_Complex;
then A1: |.z.| <> 0 by COMPLFLD:94;
A2: |.z.| >= 0 by COMPLFLD:95;
Re z <= |.z.| by HAHNBAN1:18;
then A3: Re z/|.z.| <= 1 by A1,A2,REAL_2:117;
reconsider z1=z as Element of COMPLEX by COMPLFLD:def 1;
now per cases;
suppose A4: Im z >= 0;
set 0PI = [.0,PI.];
reconsider cos1 = cos|0PI as PartFunc of 0PI,REAL by PARTFUN1:43;
reconsider cos1 as one-to-one PartFunc of 0PI,REAL by Th41,RFUNCT_2:82;
now per cases;
suppose Re z/|.z.| in dom (cos1");
then cos1".(Re z/|.z.|) in 0PI by PARTFUN1:27;
hence cos1".(Re z/|.z.|) is real number by XREAL_0:def 1;
suppose not Re z/|.z.| in dom (cos1");
hence cos1".(Re z/|.z.|) is real number by FUNCT_1:def 4;
end;
then reconsider r = cos1".(Re z/|.z.|) as Real by XREAL_0:def 1;
take r;
Re z >= -|.z.| by Th5;
then -1 <= Re z/|.z.| by A1,A2,REAL_2:117;
then A5: Re z/|.z.| in rng cos1 by A3,Th50,TOPREAL5:1;
then Re z/|.z.| in dom (cos1") by FUNCT_1:55;
then r in rng (cos1") by FUNCT_1:def 5;
then r in dom cos1 by FUNCT_1:55;
then A6: r in [.0,PI.] by RELAT_1:86;
A7: cos r = cos.r by SIN_COS:def 23
.= cos1.r by A6,FUNCT_1:72
.= Re z/|.z.| by A5,FUNCT_1:57;
then A8: Re z = |.z.|*cos r by A1,XCMPLX_1:88;
A9: |.z.|^2 = (Re z)^2 + (Im z)^2 by Th7;
A10: |.z.|^2 <> 0 by A1,SQUARE_1:73;
0 <= r & r <= PI by A6,TOPREAL5:1;
then (0 = r or 0 < r) & (r = PI or r < PI) by REAL_1:def 5;
then r = 0 or r = PI or r in ].0,PI.[ by JORDAN6:45;
then A11: sin.r >= 0 by Th23,SIN_COS:33,81;
(cos.r)^2 + (sin.r)^2 = 1 by SIN_COS:31;
then (sin.r)^2 = 1 - (cos.r)^2 by XCMPLX_1:26
.= 1 - (Re z/|.z.|)^2 by A7,SIN_COS:def 23
.= 1 - (Re z)^2/|.z.|^2 by SQUARE_1:69
.= |.z.|^2/|.z.|^2 - (Re z)^2/|.z.|^2 by A10,XCMPLX_1:60
.= (|.z.|^2 - (Re z)^2)/|.z.|^2 by XCMPLX_1:121
.= (Im z)^2/|.z.|^2 by A9,XCMPLX_1:26
.= ((Im z)/|.z.|)^2 by SQUARE_1:69;
then sin.r = sqrt((Im z)/|.z.|)^2 by A11,SQUARE_1:89
.= abs((Im z)/|.z.|) by SQUARE_1:91
.= abs(Im z)/abs |.z.| by ABSVALUE:16
.= abs(Im z)/|.z.| by HAHNBAN1:12;
then abs(Im z) = |.z.|*sin.r by A1,XCMPLX_1:88;
then A12: Im z = |.z.|*sin.r by A4,ABSVALUE:def 1
.= |.z.|*sin r by SIN_COS:def 21;
z1 = [*Re z1,Im z1*] by COMPLEX1:8
.= [*Re z,Im z1*] by HAHNBAN1:def 3
.= [*Re z,Im z*] by HAHNBAN1:def 4;
hence z = [**|.z.|*cos r,|.z.|*sin r**] by A8,A12,HAHNBAN1:def 1;
thus 0 <= r by A6,TOPREAL5:1;
r <= PI by A6,TOPREAL5:1;
hence r < 2*PI by Th21,AXIOMS:22;
suppose A13: Im z < 0;
now per cases;
suppose Re z <> |.z.|;
then A14: Re z/|.z.| <> 1 by XCMPLX_1:58;
set 0PI = [.PI,2*PI.];
reconsider cos1 = cos|0PI as PartFunc of 0PI,REAL by PARTFUN1:43;
reconsider cos1 as one-to-one PartFunc of 0PI,REAL
by Th42,RFUNCT_2:82;
now per cases;
suppose Re z/|.z.| in dom (cos1");
then cos1".(Re z/|.z.|) in 0PI by PARTFUN1:27;
hence cos1".(Re z/|.z.|) is real number by XREAL_0:def 1;
suppose not Re z/|.z.| in dom (cos1");
hence cos1".(Re z/|.z.|) is real number by CARD_1:51,FUNCT_1:def 4;
end;
then reconsider r = cos1".(Re z/|.z.|) as Real by XREAL_0:def 1;
take r;
Re z >= -|.z.| by Th5;
then -1 <= Re z/|.z.| by A1,A2,REAL_2:117;
then A15: Re z/|.z.| in rng cos1 by A3,Th51,TOPREAL5:1;
then A16: Re z/|.z.| in dom (cos1") by FUNCT_1:55;
then r in rng (cos1") by FUNCT_1:def 5;
then r in dom cos1 by FUNCT_1:55;
then A17: r in [.PI,2*PI.] by RELAT_1:86;
A18: cos r = cos.r by SIN_COS:def 23
.= cos1.r by A17,FUNCT_1:72
.= Re z/|.z.| by A15,FUNCT_1:57;
then A19: Re z = |.z.|*cos r by A1,XCMPLX_1:88;
A20: |.z.|^2 = (Re z)^2 + (Im z)^2 by Th7;
A21: |.z.|^2 <> 0 by A1,SQUARE_1:73;
PI <= r & r <= 2*PI by A17,TOPREAL5:1;
then (PI = r or PI < r) & (r = 2*PI or r < 2*PI) by REAL_1:def 5;
then r = PI or r = 2*PI or r in ].PI,2*PI.[ by JORDAN6:45;
then A22: sin.r <= 0 by Th25,SIN_COS:81;
(cos.r)^2 + (sin.r)^2 = 1 by SIN_COS:31;
then (sin.r)^2 = 1 - (cos.r)^2 by XCMPLX_1:26
.= 1 - (Re z/|.z.|)^2 by A18,SIN_COS:def 23
.= 1 - (Re z)^2/|.z.|^2 by SQUARE_1:69
.= |.z.|^2/|.z.|^2 - (Re z)^2/|.z.|^2 by A21,XCMPLX_1:60
.= (|.z.|^2 - (Re z)^2)/|.z.|^2 by XCMPLX_1:121
.= (Im z)^2/|.z.|^2 by A20,XCMPLX_1:26
.= ((Im z)/|.z.|)^2 by SQUARE_1:69;
then -sin.r = sqrt((Im z)/|.z.|)^2 by A22,SQUARE_1:90
.= abs((Im z)/|.z.|) by SQUARE_1:91
.= abs(Im z)/abs |.z.| by ABSVALUE:16
.= abs(Im z)/|.z.| by HAHNBAN1:12;
then sin.r = -(abs(Im z)/|.z.|);
then sin.r = (-abs(Im z))/|.z.| by XCMPLX_1:188;
then -abs(Im z) = |.z.|*sin.r by A1,XCMPLX_1:88;
then A23: --Im z = |.z.|*sin.r by A13,ABSVALUE:def 1
.= |.z.|*sin r by SIN_COS:def 21;
z1 = [*Re z1,Im z1*] by COMPLEX1:8
.= [*Re z,Im z1*] by HAHNBAN1:def 3
.= [*Re z,Im z*] by HAHNBAN1:def 4;
hence z = [**|.z.|*cos r,|.z.|*sin r**] by A19,A23,HAHNBAN1:def 1;
PI <= r by A17,TOPREAL5:1;
hence 0 <= r by Th21,AXIOMS:22;
A24: r <> 2*PI
proof
A25: dom cos = REAL by SIN_COS:def 22;
A26: cos1" is one-to-one by FUNCT_1:62;
1 in rng cos1 by Th51,TOPREAL5:1;
then A27: 1 in dom (cos1") by FUNCT_1:55;
assume A28: r = 2*PI;
A29: 2*PI in [.PI,2*PI.] by Th21,TOPREAL5:1;
then A30: 2*PI in dom cos1 by A25,RELAT_1:86;
cos1.(2*PI) = 1 by A29,FUNCT_1:72,SIN_COS:81;
then cos1".1 = 2*PI by A30,FUNCT_1:54;
hence contradiction by A14,A16,A26,A27,A28,FUNCT_1:def 8;
end;
r <= 2*PI by A17,TOPREAL5:1;
hence r < 2*PI by A24,REAL_1:def 5;
suppose A31: Re z = |.z.|;
then (Re z)^2 = (Re z)^2 + (Im z)^2 by Th7;
then (Re z)^2 - (Re z)^2 = (Im z)^2 by XCMPLX_1:26;
then (Im z)^2 = 0 by XCMPLX_1:14;
then A32: Im z = 0 by SQUARE_1:73;
consider z2 be Element of COMPLEX such that
A33: z = z2 and
A34: Re z = Re z2 by HAHNBAN1:def 3;
consider z3 be Element of COMPLEX such that
A35: z = z3 and
A36: Im z = Im z3 by HAHNBAN1:def 4;
A37: z = [*Re z2,Im z3*] by A33,A35,COMPLEX1:8;
reconsider r=0 as Real;
take r;
thus z = [**|.z.|*cos r,|.z.|*sin r**]
by A31,A32,A34,A36,A37,HAHNBAN1:def 1,SIN_COS:34;
thus 0 <= r;
thus r < 2*PI by Th21;
end;
hence thesis;
end;
hence thesis;
end;
thus thesis;
end;
uniqueness
proof
z <> 0.F_Complex implies for x,y be Real st
z = [**|.z.|*cos x,|.z.|*sin x**] & 0 <= x & x < 2*PI &
z = [**|.z.|*cos y,|.z.|*sin y**] & 0 <= y & y < 2*PI holds x = y
proof
assume z <> 0.F_Complex;
then A38: |.z.| <> 0 by COMPLFLD:94;
let x,y be Real;
assume that
A39: z = [**|.z.|*cos x,|.z.|*sin x**] and
A40: 0 <= x and
A41: x < 2*PI and
A42: z = [**|.z.|*cos y,|.z.|*sin y**] and
A43: 0 <= y and
A44: y < 2*PI;
[*|.z.|*cos x,|.z.|*sin x*] = [**|.z.|*cos y,|.z.|*sin y**]
by A39,A42,HAHNBAN1:def 1
.= [*|.z.|*cos y,|.z.|*sin y*] by HAHNBAN1:def 1;
then |.z.|*cos x = |.z.|*cos y & |.z.|*sin x = |.z.|*sin y by ARYTM_0:12
;
then cos x = cos y & sin x = sin y by A38,XCMPLX_1:5;
then A45: cos x = cos y & sin x = sin.y by SIN_COS:def 21;
then cos x = cos.y & sin.x = sin.y by SIN_COS:def 21,def 23;
then A46: cos.x = cos.y & sin.x = sin.y by SIN_COS:def 23;
A47: dom cos = REAL by SIN_COS:def 22;
now per cases;
suppose x <= PI & y <= PI;
then x in [.0,PI.] & y in [.0,PI.] by A40,A43,TOPREAL5:1;
then A48: x in [.0,PI.] /\ dom cos & y in [.0,PI.] /\ dom cos
by A47,XBOOLE_0:def 3;
assume x <> y;
then x < y or y < x by AXIOMS:21;
hence contradiction by A46,A48,Th41,RFUNCT_2:def 3;
suppose x > PI & y > PI;
then x in [.PI,2*PI.] & y in [.PI,2*PI.] by A41,A44,TOPREAL5:1;
then A49: x in [.PI,2*PI.] /\ dom cos & y in [.PI,2*PI.] /\ dom cos
by A47,XBOOLE_0:def 3
;
assume x <> y;
then x < y or y < x by AXIOMS:21;
hence contradiction by A46,A49,Th42,RFUNCT_2:def 2;
suppose x <= PI & y > PI;
then x in [.0,PI.] & y in ].PI,2*PI.[ by A40,A44,JORDAN6:45,TOPREAL5:1;
then sin.x >= 0 & sin.y < 0 by Th24,Th25;
hence x = y by A45,SIN_COS:def 21;
suppose y <= PI & x > PI;
then y in [.0,PI.] & x in ].PI,2*PI.[ by A41,A43,JORDAN6:45,TOPREAL5:1;
then sin.y >= 0 & sin.x < 0 by Th24,Th25;
hence x = y by A45,SIN_COS:def 21;
end;
hence x = y;
end;
hence thesis;
end;
consistency;
end;
theorem Th52:
for z be Element of F_Complex holds
0 <= Arg z & Arg z < 2*PI
proof
let z be Element of F_Complex;
0 <= Arg z & Arg z < 2*PI or z = 0.F_Complex by Def1;
hence thesis by Def1,Th21;
end;
theorem Th53:
for x be Real st x >= 0 holds
Arg [**x,0**] = 0
proof
let x be Real;
assume A1: x >= 0;
A2: 0 <= Arg [**x,0**] & Arg [**x,0**] < 2*PI by Th52;
per cases by A1;
suppose A3: x > -0;
then [*x,0*] <> 0.F_Complex by ARYTM_0:12,L0,COMPLFLD:9;
then A4: [**x,0**] <> 0.F_Complex by HAHNBAN1:def 1;
then A5: |. [**x,0**] .| <> 0 by COMPLFLD:94;
[**x,0**] = [**|. [**x,0**] .|*cos Arg [**x,0**],
|. [**x,0**] .|*sin Arg [**x,0**]**] by A4,Def1;
then A6: |. [**x,0**] .|*cos Arg [**x,0**] = x &
|. [**x,0**] .|*sin Arg [**x,0**] = 0 by Th8;
then sin Arg [**x,0**] = 0 by A5,XCMPLX_1:6;
then Arg [**x,0**] = 0 or |. [**x,0**] .|*-1 = x
by A2,A6,Th33,SIN_COS:82;
then Arg [**x,0**] = 0 or -|. [**x,0**] .| = x by XCMPLX_1:180;
then Arg [**x,0**] = 0 or |. [**x,0**] .| < 0 by A3,REAL_1:50;
hence Arg [**x,0**] = 0 by COMPLFLD:95;
suppose x = 0;
then [**x,0**] = 0.F_Complex by L0,COMPLFLD:9,HAHNBAN1:def 1
;
hence thesis by Def1;
end;
theorem Th54:
for x be Real st x < 0 holds
Arg [**x,0**] = PI
proof
let x be Real;
assume A1: x < 0;
A2: 0 <= Arg [**x,0**] & Arg [**x,0**] < 2*PI by Th52;
[*x,0*] <> 0.F_Complex by A1,ARYTM_0:12,L0,COMPLFLD:9;
then A3: [**x,0**] <> 0.F_Complex by HAHNBAN1:def 1;
then A4: |. [**x,0**] .| <> 0 by COMPLFLD:94;
[**x,0**] = [**|. [**x,0**] .|*cos Arg [**x,0**],
|. [**x,0**] .|*sin Arg [**x,0**]**] by A3,Def1;
then A5: |. [**x,0**] .|*cos Arg [**x,0**] = x &
|. [**x,0**] .|*sin Arg [**x,0**] = 0 by Th8;
then sin Arg [**x,0**] = 0 by A4,XCMPLX_1:6;
then Arg [**x,0**] = PI or |. [**x,0**] .|*1 = x by A2,A5,Th33,SIN_COS:34;
hence thesis by A1,COMPLFLD:95;
end;
theorem Th55:
for x be Real st x > 0 holds
Arg [**0,x**] = PI/2
proof
let x be Real;
assume A1: x > 0;
then A2: x > -0;
A3: 0 <= Arg [**0,x**] & Arg [**0,x**] < 2*PI by Th52;
[*0,x*] <> 0.F_Complex by A1,ARYTM_0:12,L0,COMPLFLD:9;
then A4: [**0,x**] <> 0.F_Complex by HAHNBAN1:def 1;
then A5: |. [**0,x**] .| <> 0 by COMPLFLD:94;
[**0,x**] = [**|. [**0,x**] .|*cos Arg [**0,x**],
|. [**0,x**] .|*sin Arg [**0,x**]**] by A4,Def1;
then A6: |. [**0,x**] .|*cos Arg [**0,x**] = 0 &
|. [**0,x**] .|*sin Arg [**0,x**] = x by Th8;
then cos Arg [**0,x**] = 0 by A5,XCMPLX_1:6;
then Arg [**0,x**] = PI/2 or |. [**0,x**] .|*-1 = x
by A3,A6,Th20,Th34,SIN_COS:82;
then Arg [**0,x**] = PI/2 or -|. [**0,x**] .| = x by XCMPLX_1:180;
then Arg [**0,x**] = PI/2 or |. [**0,x**] .| < 0 by A2,REAL_1:50;
hence thesis by COMPLFLD:95;
end;
theorem Th56:
for x be Real st x < 0 holds
Arg [**0,x**] = 3/2*PI
proof
let x be Real;
assume A1: x < 0;
A2: 0 <= Arg [**0,x**] & Arg [**0,x**] < 2*PI by Th52;
[*0,x*] <> 0.F_Complex by A1,ARYTM_0:12,L0,COMPLFLD:9;
then A3: [**0,x**] <> 0.F_Complex by HAHNBAN1:def 1;
then A4: |. [**0,x**] .| <> 0 by COMPLFLD:94;
[**0,x**] = [**|. [**0,x**] .|*cos Arg [**0,x**],
|. [**0,x**] .|*sin Arg [**0,x**]**] by A3,Def1;
then A5: |. [**0,x**] .|*cos Arg [**0,x**] = 0 &
|. [**0,x**] .|*sin Arg [**0,x**] = x by Th8;
then cos Arg [**0,x**] = 0 by A4,XCMPLX_1:6;
then Arg [**0,x**] = 3/2*PI or |. [**0,x**] .|*1 = x
by A2,A5,Th34,SIN_COS:82;
hence thesis by A1,COMPLFLD:95;
end;
theorem
Arg 1_(F_Complex) = 0
proof
1_(F_Complex) = [**1,0**] by L1,COMPLFLD:10,HAHNBAN1:def 1;
hence thesis by Th53;
end;
theorem
Arg i_FC = PI/2 by Th55,HAHNBAN1:6;
theorem Th59:
for z be Element of F_Complex holds
Arg z in ].0,PI/2.[ iff Re z > 0 & Im z > 0
proof
let z be Element of F_Complex;
thus Arg z in ].0,PI/2.[ implies Re z > 0 & Im z > 0
proof
assume A1: Arg z in ].0,PI/2.[;
then A2: Arg z > 0 & Arg z < PI/2 by JORDAN6:45;
then A3: z <> 0.F_Complex by Def1;
then z = [**|.z.|*cos Arg z,|.z.|*sin Arg z**] by Def1;
then A4: Re z = |.z.|*cos Arg z & Im z = |.z.|*sin Arg z by HAHNBAN1:15;
A5: |.z.| > 0 by A3,COMPLFLD:96;
cos Arg z > 0 by A1,SIN_COS:86;
hence Re z > 0 by A4,A5,SQUARE_1:21;
Arg z < PI by A2,Th21,AXIOMS:22;
then Arg z in ].0,PI.[ by A2,JORDAN6:45;
then sin.Arg z > 0 by Th23;
then sin Arg z > 0 by SIN_COS:def 21;
hence Im z > 0 by A4,A5,SQUARE_1:21;
end;
assume that
A6: Re z > 0 and
A7: Im z > 0;
z = [**Re z,Im z**] by Th9;
then A8: z <> 0.F_Complex by A6,Th8,Th10;
then A9: |.z.| > 0 by COMPLFLD:96;
A10: 0 <= Arg z & Arg z < 2*PI by Th52;
z = [**|.z.|*cos Arg z,|.z.|*sin Arg z**] by A8,Def1;
then |.z.|*cos Arg z > 0 & |.z.|*sin Arg z > 0 by A6,A7,HAHNBAN1:15;
then cos Arg z > 0 & sin Arg z > 0 by A9,SQUARE_1:23;
then A11: cos.Arg z > 0 & sin.Arg z > 0 by SIN_COS:def 21,def 23;
then not Arg z in [.PI,2*PI.] & not Arg z in [.PI/2,3/2*PI.] by Th26,Th30;
then A12: PI/2 > Arg z or PI > Arg z & 3/2*PI < Arg z by A10,TOPREAL5:1;
Arg z > 0 by A10,A11,REAL_1:def 5,SIN_COS:33;
hence thesis by A12,Th21,AXIOMS:22,JORDAN6:45;
end;
theorem Th60:
for z be Element of F_Complex holds
Arg z in ].PI/2,PI.[ iff Re z < 0 & Im z > 0
proof
let z be Element of F_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 A2: Arg z > PI/2 & Arg z < PI by JORDAN6:45;
then A3: z <> 0.F_Complex by Def1,Th21;
then z = [**|.z.|*cos Arg z,|.z.|*sin Arg z**] by Def1;
then A4: Re z = |.z.|*cos Arg z & Im z = |.z.|*sin Arg z by HAHNBAN1:15;
A5: |.z.| > 0 by A3,COMPLFLD:96;
PI/2 < Arg z & Arg z < PI by A1,JORDAN6:45;
then PI/2 < Arg z & Arg z < 3/2*PI by Th21,AXIOMS:22;
then Arg z in ].PI/2,3/2*PI.[ by JORDAN6:45;
then cos.Arg z < 0 by Th29;
then cos Arg z < 0 by SIN_COS:def 23;
hence Re z < 0 by A4,A5,SQUARE_1:24;
Arg z > 0 by A2,Th21,AXIOMS:22;
then Arg z in ].0,PI.[ by A2,JORDAN6:45;
then sin.Arg z > 0 by Th23;
then sin Arg z > 0 by SIN_COS:def 21;
hence Im z > 0 by A4,A5,SQUARE_1:21;
end;
assume that
A6: Re z < 0 and
A7: Im z > 0;
z = [**Re z,Im z**] by Th9;
then A8: z <> 0.F_Complex by A6,Th8,Th10;
then A9: |.z.| > 0 by COMPLFLD:96;
A10: 0 <= Arg z & Arg z < 2*PI by Th52;
z = [**|.z.|*cos Arg z,|.z.|*sin Arg z**] by A8,Def1;
then |.z.|*cos Arg z < 0 & |.z.|*sin Arg z > 0 by A6,A7,HAHNBAN1:15;
then cos Arg z < 0 & sin Arg z > 0 by A9,SQUARE_1:19,23;
then cos.Arg z < 0 & sin.Arg z > 0 by SIN_COS:def 21,def 23;
then not Arg z in [.PI,2*PI.] & not Arg z in [.-PI/2,PI/2.] by Th26,Th28;
then Arg z < PI & (Arg z < -PI/2 or Arg z > PI/2) by A10,TOPREAL5:1;
hence thesis by A10,Th21,AXIOMS:22,JORDAN6:45;
end;
theorem Th61:
for z be Element of F_Complex holds
Arg z in ].PI,3/2*PI.[ iff Re z < 0 & Im z < 0
proof
let z be Element of F_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 A2: Arg z > PI & Arg z < 3/2*PI by JORDAN6:45;
then A3: z <> 0.F_Complex by Def1,Th21;
then z = [**|.z.|*cos Arg z,|.z.|*sin Arg z**] by Def1;
then A4: Re z = |.z.|*cos Arg z & Im z = |.z.|*sin Arg z by HAHNBAN1:15;
A5: |.z.| > 0 by A3,COMPLFLD:96;
PI < Arg z & Arg z < 3/2*PI by A1,JORDAN6:45;
then PI/2 < Arg z & Arg z < 3/2*PI by Th21,AXIOMS:22;
then Arg z in ].PI/2,3/2*PI.[ by JORDAN6:45;
then cos.Arg z < 0 by Th29;
then cos Arg z < 0 by SIN_COS:def 23;
hence Re z < 0 by A4,A5,SQUARE_1:24;
Arg z < 2*PI by A2,Th21,AXIOMS:22;
then Arg z in ].PI,2*PI.[ by A2,JORDAN6:45;
then sin.Arg z < 0 by Th25;
then sin Arg z < 0 by SIN_COS:def 21;
hence Im z < 0 by A4,A5,SQUARE_1:24;
end;
assume that
A6: Re z < 0 and
A7: Im z < 0;
z = [**Re z,Im z**] by Th9;
then A8: z <> 0.F_Complex by A6,Th8,Th10;
then A9: |.z.| > 0 by COMPLFLD:96;
A10: 0 <= Arg z & Arg z < 2*PI by Th52;
z = [**|.z.|*cos Arg z,|.z.|*sin Arg z**] by A8,Def1;
then |.z.|*cos Arg z < 0 & |.z.|*sin Arg z < 0 by A6,A7,HAHNBAN1:15;
then cos Arg z < 0 & sin Arg z < 0 by A9,SQUARE_1:19;
then cos.Arg z < 0 & sin.Arg z < 0 by SIN_COS:def 21,def 23;
then not Arg z in [.0,PI.] & not Arg z in [.-PI/2,PI/2.] &
not Arg z in [.3/2*PI,2*PI.] by Th24,Th28,Th32;
then Arg z > PI & (Arg z < -PI/2 or Arg z > PI/2) & Arg z < 3/2*PI
by A10,
TOPREAL5:1;
hence thesis by JORDAN6:45;
end;
theorem Th62:
for z be Element of F_Complex holds
Arg z in ].3/2*PI,2*PI.[ iff Re z > 0 & Im z < 0
proof
let z be Element of F_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 > 3/2*PI & Arg z < 2*PI by JORDAN6:45;
then A3: z <> 0.F_Complex by Def1,Th21;
then z = [**|.z.|*cos Arg z,|.z.|*sin Arg z**] by Def1;
then A4: Re z = |.z.|*cos Arg z & Im z = |.z.|*sin Arg z by HAHNBAN1:15;
A5: |.z.| > 0 by A3,COMPLFLD:96;
cos.Arg z > 0 by A1,Th31;
then cos Arg z > 0 by SIN_COS:def 23;
hence Re z > 0 by A4,A5,SQUARE_1:21;
Arg z > PI by A2,Th21,AXIOMS:22;
then Arg z in ].PI,2*PI.[ by A2,JORDAN6:45;
then sin.Arg z < 0 by Th25;
then sin Arg z < 0 by SIN_COS:def 21;
hence Im z < 0 by A4,A5,SQUARE_1:24;
end;
assume that
A6: Re z > 0 and
A7: Im z < 0;
z = [**Re z,Im z**] by Th9;
then A8: z <> 0.F_Complex by A6,Th8,Th10;
then A9: |.z.| > 0 by COMPLFLD:96;
A10: 0 <= Arg z & Arg z < 2*PI by Th52;
z = [**|.z.|*cos Arg z,|.z.|*sin Arg z**] by A8,Def1;
then |.z.|*cos Arg z > 0 & |.z.|*sin Arg z < 0 by A6,A7,HAHNBAN1:15;
then cos Arg z > 0 & sin Arg z < 0 by A9,SQUARE_1:19,23;
then cos.Arg z > 0 & sin.Arg z < 0 by SIN_COS:def 21,def 23;
then not Arg z in [.0,PI.] & not Arg z in [.PI/2,3/2*PI.] by Th24,Th30;
then Arg z > PI & (Arg z < PI/2 or Arg z > 3/2*PI) by A10,TOPREAL5:1;
hence thesis by A10,Th21,AXIOMS:22,JORDAN6:45;
end;
theorem Th63:
for z be Element of F_Complex st Im z > 0 holds
sin Arg z > 0
proof
let z be Element of F_Complex;
assume A1: Im z > 0;
Re z < 0 or Re z = 0 or Re z > 0;
then Re z < 0 or Re z > 0 or z = [**0,Im z**] by Th9;
then Arg z in ].PI/2,PI.[ or Arg z in ].0,PI/2.[ or Arg z = PI/2
by A1,Th55,Th59,Th60;
then PI/2 < Arg z & Arg z < PI or 0 < Arg z & Arg z < PI/2 or
Arg z = PI/2 by JORDAN6:45;
then 0 < Arg z & Arg z < PI by Th21,AXIOMS:22;
then Arg z in ].0,PI.[ by JORDAN6:45;
then sin.Arg z > 0 by Th23;
hence thesis by SIN_COS:def 21;
end;
theorem Th64:
for z be Element of F_Complex st Im z < 0 holds
sin Arg z < 0
proof
let z be Element of F_Complex;
assume A1: Im z < 0;
Re z < 0 or Re z = 0 or Re z > 0;
then Re z < 0 or Re z > 0 or z = [**0,Im z**] by Th9;
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,Th56,Th61,Th62;
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 JORDAN6:45;
then PI < Arg z & Arg z < 2*PI by Th21,AXIOMS:22;
then Arg z in ].PI,2*PI.[ by JORDAN6:45;
then sin.Arg z < 0 by Th25;
hence thesis by SIN_COS:def 21;
end;
theorem
for z be Element of F_Complex st Im z >= 0 holds
sin Arg z >= 0
proof
let z be Element of F_Complex;
assume Im z >= 0;
then Im z > 0 or Im z = 0;
then sin Arg z > 0 or z = [**Re z,0**] & (Re z >= 0 or Re z < 0)
by Th9,Th63;
hence thesis by Th53,Th54,SIN_COS:34,82;
end;
theorem
for z be Element of F_Complex st Im z <= 0 holds
sin Arg z <= 0
proof
let z be Element of F_Complex;
assume Im z <= 0;
then Im z < 0 or Im z = 0;
then sin Arg z < 0 or z = [**Re z,0**] & (Re z >= 0 or Re z < 0)
by Th9,Th64;
hence thesis by Th53,Th54,SIN_COS:34,82;
end;
theorem Th67:
for z be Element of F_Complex st Re z > 0 holds
cos Arg z > 0
proof
let z be Element of F_Complex;
assume A1: Re z > 0;
Im z < 0 or Im z = 0 or Im z > 0;
then Im z < 0 or Im z > 0 or z = [**Re z,0**] by Th9;
then Arg z in ].0,PI/2.[ or Arg z in ].3/2*PI,2*PI.[ or Arg z = 0
by A1,Th53,Th59,Th62;
then cos.Arg z > 0 by Th31,SIN_COS:33,85;
hence thesis by SIN_COS:def 23;
end;
theorem Th68:
for z be Element of F_Complex st Re z < 0 holds
cos Arg z < 0
proof
let z be Element of F_Complex;
assume A1: Re z < 0;
Im z < 0 or Im z = 0 or Im z > 0;
then Im z < 0 or Im z > 0 or z = [**Re z,0**] by Th9;
then Arg z in ].PI/2,PI.[ or Arg z in ].PI,3/2*PI.[ or Arg z = PI
by A1,Th54,Th60,Th61;
then PI/2 < Arg z & Arg z < PI or PI < Arg z & Arg z < 3/2*PI or
Arg z = PI by JORDAN6:45;
then PI/2 < Arg z & Arg z < 3/2*PI by Th21,AXIOMS:22;
then Arg z in ].PI/2,3/2*PI.[ by JORDAN6:45;
then cos.Arg z < 0 by Th29;
hence thesis by SIN_COS:def 23;
end;
theorem
for z be Element of F_Complex st Re z >= 0 holds
cos Arg z >= 0
proof
let z be Element of F_Complex;
assume Re z >= 0;
then Re z > 0 or Re z = 0;
then cos Arg z > 0 or z = [**0,Im z**] & (Im z > 0 or Im z < 0 or Im z = 0
)
by Th9,Th67;
then cos Arg z > 0 or Arg z = PI/2 or Arg z = 3/2*PI or Arg z = 0
by Def1,Th10,Th55,Th56;
hence thesis by Th20,SIN_COS:34,82;
end;
theorem
for z be Element of F_Complex st Re z <= 0 &
z <> 0.F_Complex holds
cos Arg z <= 0
proof
let z be Element of F_Complex;
assume that
A1: Re z <= 0 and
A2: z <> 0.F_Complex;
Re z < 0 or Re z = 0 by A1;
then cos Arg z < 0 or z = [**0,Im z**] & (Im z >= 0 or Im z < 0)
by Th9,Th68;
then cos Arg z < 0 or z = [**0,Im z**] & (Im z > 0 or Im z < 0)
by A2,Th10,REAL_1:def 5;
hence thesis by Th20,Th55,Th56,SIN_COS:82;
end;
theorem Th71:
for n be Nat holds
(power F_Complex).([**cos x,sin x**],n) = [**cos (n*x),sin (n*x)**]
proof
defpred P[Nat] means
(power F_Complex).([**cos x,sin x**],$1) = [**cos ($1*x),sin ($1*x)**];
(power F_Complex).([**cos x,sin x**],0) = 1.F_Complex by GROUP_1:def 7
.= [*1,0*] by L1,COMPLFLD:10,POLYNOM2:3
.= [**cos (0*x),sin (0*x)**] by HAHNBAN1:def 1,SIN_COS:34;
then A1: P[0];
A2: now let n be Nat;
assume P[n];
then (power F_Complex).([**cos x,sin x**],n+1) =
[**cos(n*x),sin(n*x)**]*[**cos x,sin x**] by GROUP_1:def 7
.= [**cos(n*x)*cos x - sin(n*x)*sin x,cos(n*x)*sin x+cos x*sin(n*x)**]
by HAHNBAN1:11
.= [**cos(n*x+x),cos(n*x)*sin x+cos x*sin(n*x)**] by SIN_COS:80
.= [**cos(n*x+1*x),sin(n*x+1*x)**] by SIN_COS:80
.= [**cos((n+1)*x),sin(n*x+1*x)**] by XCMPLX_1:8
.= [**cos((n+1)*x),sin((n+1)*x)**] by XCMPLX_1:8;
hence P[n+1];
end;
thus for n be Nat holds P[n] from Ind(A1,A2);
end;
theorem
for z be Element of F_Complex
for n be Nat st z <> 0.F_Complex or n <> 0 holds
(power F_Complex).(z,n) =
[**(|.z.| to_power n)*cos (n*Arg z),(|.z.| to_power n)*sin (n*Arg z)**]
proof
let z be Element of F_Complex;
let n be Nat;
assume A1: z <> 0.F_Complex or n <> 0;
per cases by A1,NAT_1:18;
suppose A2: z <> 0.F_Complex;
then A3: |.z.| > 0 by COMPLFLD:96;
thus (power F_Complex).(z,n) =
(power F_Complex).([**|.z.|*cos Arg z-0*sin Arg z,
|.z.|*sin Arg z+cos Arg z*0**],n) by A2,Def1
.= (power F_Complex).([**|.z.|,0**]*[**cos Arg z,sin Arg z**],n)
by HAHNBAN1:11
.= (power F_Complex).([**|.z.|,0**],n)*
(power F_Complex).([**cos Arg z,sin Arg z**],n) by Th15
.= (power F_Complex).([**|.z.|,0**],n)*
[**cos (n*Arg z),sin (n*Arg z)**] by Th71
.= [**|.z.| to_power n,0**]*[**cos (n*Arg z),sin (n*Arg z)**]
by A3,Th16
.= [**(|.z.| to_power n)*cos(n*Arg z)-0*sin (n*Arg z),
(|.z.| to_power n)*sin(n*Arg z)+0*cos(n*Arg z)**] by HAHNBAN1:11
.= [**(|.z.| to_power n)*cos(n*Arg z),
(|.z.| to_power n)*sin(n*Arg z)**];
suppose A4: z = 0.F_Complex & n > 0;
hence (power F_Complex).(z,n) = [**0*cos(n*Arg z),0*sin(n*Arg z)**]
by Th10,Th14
.= [**0*cos(n*Arg z),(|.z.| to_power n)*sin(n*Arg z)**]
by A4,Lm1,COMPLFLD:93,POWER:def 2
.= [**(|.z.| to_power n)*cos(n*Arg z),(|.z.| to_power n)*sin(n*Arg z)**]
by A4,Lm1,COMPLFLD:93,POWER:def 2;
end;
theorem Th73:
for n,k be Nat st n <> 0 holds
(power F_Complex).([**cos((x+2*PI*k)/n),sin((x+2*PI*k)/n)**],n) =
[**cos x,sin x**]
proof
let n,k be Nat;
assume A1: n <> 0;
thus (power F_Complex).([**cos((x+2*PI*k)/n),sin((x+2*PI*k)/n)**],n) =
[**cos(n*((x+2*PI*k)/n)),sin(n*((x+2*PI*k)/n))**] by Th71
.= [**cos(x+2*PI*k),sin(n*((x+2*PI*k)/n))**] by A1,XCMPLX_1:88
.= [**cos(x+2*PI*k),sin(x+2*PI*k)**] by A1,XCMPLX_1:88
.= [**cos.(x+2*PI*k),sin(x+2*PI*k)**] by SIN_COS:def 23
.= [**cos.(x+2*PI*k),sin.(x+2*PI*k)**] by SIN_COS:def 21
.= [**cos.(x+2*PI*k),sin.x**] by SIN_COS2:10
.= [**cos.x,sin.x**] by SIN_COS2:11
.= [**cos.x,sin x**] by SIN_COS:def 21
.= [**cos x,sin x**] by SIN_COS:def 23;
end;
theorem Th74:
for z be Element of F_Complex
for n,k be Nat st n <> 0 holds
z = (power F_Complex).([**(n-root |.z.|)*cos((Arg z+2*PI*k)/n),
(n-root |.z.|)*sin((Arg z+2*PI*k)/n)**],n)
proof
let z be Element of F_Complex;
let n,k be Nat;
assume A1: n <> 0;
then A2: n > 0 by NAT_1:19;
then A3: n >= 0+1 by NAT_1:38;
per cases;
suppose A4: z <> 0.F_Complex;
then A5: |.z.| > 0 by COMPLFLD:96;
then n-root |.z.| = n -Root |.z.| by A3,POWER:def 1;
then A6: n-root |.z.| > 0 by A3,A5,PREPOWER:def 3;
thus (power F_Complex).([**(n-root |.z.|)*cos((Arg z+2*PI*k)/n),
(n-root |.z.|)*sin((Arg z+2*PI*k)/n)**],n) =
(power F_Complex).([**(n-root |.z.|)*cos((Arg z+2*PI*k)/n)-
0*sin((Arg z+2*PI*k)/n),(n-root |.z.|)*sin((Arg z+2*PI*k)/n)+
0*cos((Arg z+2*PI*k)/n)**],n)
.= (power F_Complex).([**n-root |.z.|,0**]*
[**cos((Arg z+2*PI*k)/n),sin((Arg z+2*PI*k)/n)**],n) by HAHNBAN1:11
.= (power F_Complex).([**n-root |.z.|,0**],n)*(power F_Complex).
([**cos((Arg z+2*PI*k)/n),sin((Arg z+2*PI*k)/n)**],n) by Th15
.= (power F_Complex).([**n-root |.z.|,0**],n)*[**cos Arg z,sin Arg z**]
by A1,Th73
.= [**(n-root |.z.|) to_power n,0**]*[**cos Arg z,sin Arg z**]
by A6,Th16
.= [**|.z.|,0**]*[**cos Arg z,sin Arg z**] by A1,A5,Th17
.= [**|.z.|*cos Arg z-0*sin Arg z,|.z.|*sin Arg z+0*cos Arg z**]
by HAHNBAN1:11
.= z by A4,Def1;
suppose A7: z = 0.F_Complex;
then |.z.| = 0 by COMPLFLD:9,93,def 1;
hence (power F_Complex).([**(n-root |.z.|)*cos((Arg z+2*PI*k)/n),
(n-root |.z.|)*sin((Arg z+2*PI*k)/n)**],n) =
(power F_Complex).([**0*cos((Arg z+2*PI*k)/n),
(n-root 0)*sin((Arg z+2*PI*k)/n)**],n) by A3,POWER:6
.= (power F_Complex).([**0,0*sin((Arg z+2*PI*k)/n)**],n) by A3,POWER:6
.= z by A2,A7,Th10,Th14;
end;
definition
let x be Element of F_Complex;
let n be non empty Nat;
mode CRoot of n,x -> Element of F_Complex means :Def2:
(power F_Complex).(it,n) = x;
existence
proof
take [**(n-root |.x.|)*cos((Arg x+2*PI*0)/n),
(n-root |.x.|)*sin((Arg x+2*PI*0)/n)**];
thus thesis by Th74;
end;
end;
theorem
for x be Element of F_Complex
for n be non empty 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)**] is CRoot of n,x
proof
let x be Element of F_Complex;
let n be non empty Nat;
let k be Nat;
(power F_Complex).([**(n-root |.x.|)*cos((Arg x+2*PI*k)/n),
(n-root |.x.|)*sin((Arg x+2*PI*k)/n)**],n) = x by Th74;
hence thesis by Def2;
end;
theorem
for x be Element of F_Complex
for v be CRoot of 1,x holds
v = x
proof
let x be Element of F_Complex;
let v be CRoot of 1,x;
(power F_Complex).(v,1) = x by Def2;
hence v = x by Th12;
end;
theorem
for n be non empty Nat
for v be CRoot of n,0.F_Complex holds
v = 0.F_Complex
proof
let n be non empty Nat;
let v be CRoot of n,0.F_Complex;
defpred P[Nat] means (power F_Complex).(v,$1) = 0.F_Complex;
A1: ex n be non empty Nat st P[n]
proof
take n;
thus thesis by Def2;
end;
A2: now let k be non empty Nat;
assume that
A3: k <> 1 and
A4: P[k];
consider t be Nat such that
A5: k = t+1 by NAT_1:22;
k >= 1 by RLVECT_1:99;
then t+1 > 0+1 by A3,A5,REAL_1:def 5;
then A6: t > 0 by AXIOMS:24;
reconsider t as non empty Nat by A3,A5,CARD_1:51;
take t;
thus t < k by A5,NAT_1:38;
(power F_Complex).(v,k) = (power F_Complex).(v,t)*v by A5,GROUP_1:def 7;
then (power F_Complex).(v,t) = 0.F_Complex or v = 0.F_Complex
by A4,VECTSP_1:44;
hence P[t] by A6,Th14;
end;
P[1] from Regr_without_0(A1,A2);
hence thesis by Th12;
end;
theorem
for n be non empty Nat
for x be Element of F_Complex
for v be CRoot of n,x st v = 0.F_Complex holds
x = 0.F_Complex
proof
let n be non empty Nat;
let x be Element of F_Complex;
let v be CRoot of n,x;
A1: n >= 0 & n <> 0 by NAT_1:18;
assume v = 0.F_Complex;
then (power F_Complex).(0.F_Complex,n) = x by Def2;
hence thesis by A1,Th14;
end;