:: by Robert Milewski

::

:: Received July 21, 2000

:: Copyright (c) 2000-2012 Association of Mizar Users

begin

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 :: COMPTRIG:5

theorem Th6: :: COMPTRIG:6

for a, b, c, x being real number holds

( not x in ].a,c.[ or x in ].a,b.[ or x = b or x in ].b,c.[ )

( not x in ].a,c.[ or x in ].a,b.[ or x = b or x in ].b,c.[ )

proof end;

begin

definition

let z be complex number ;

( ( z <> 0 implies ex b_{1} being Real st

( z = (|.z.| * (cos b_{1})) + ((|.z.| * (sin b_{1})) * <i>) & 0 <= b_{1} & b_{1} < 2 * PI ) ) & ( not z <> 0 implies ex b_{1} being Real st b_{1} = 0 ) )

for b_{1}, b_{2} being Real holds

( ( z <> 0 & z = (|.z.| * (cos b_{1})) + ((|.z.| * (sin b_{1})) * <i>) & 0 <= b_{1} & b_{1} < 2 * PI & z = (|.z.| * (cos b_{2})) + ((|.z.| * (sin b_{2})) * <i>) & 0 <= b_{2} & b_{2} < 2 * PI implies b_{1} = b_{2} ) & ( not z <> 0 & b_{1} = 0 & b_{2} = 0 implies b_{1} = b_{2} ) )

for b_{1} being Real holds verum
;

end;
func Arg z -> Real means :Def1: :: COMPTRIG:def 1

( z = (|.z.| * (cos it)) + ((|.z.| * (sin it)) * <i>) & 0 <= it & it < 2 * PI ) if z <> 0

otherwise it = 0 ;

existence ( z = (|.z.| * (cos it)) + ((|.z.| * (sin it)) * <i>) & 0 <= it & it < 2 * PI ) if z <> 0

otherwise it = 0 ;

( ( z <> 0 implies ex b

( z = (|.z.| * (cos b

proof end;

uniqueness for b

( ( z <> 0 & z = (|.z.| * (cos b

proof end;

consistency for b

:: deftheorem Def1 defines Arg COMPTRIG:def 1 :

for z being complex number

for b_{2} being Real holds

( ( z <> 0 implies ( b_{2} = Arg z iff ( z = (|.z.| * (cos b_{2})) + ((|.z.| * (sin b_{2})) * <i>) & 0 <= b_{2} & b_{2} < 2 * PI ) ) ) & ( not z <> 0 implies ( b_{2} = Arg z iff b_{2} = 0 ) ) );

for z being complex number

for b

( ( z <> 0 implies ( b

theorem Th44: :: COMPTRIG:44

for z being complex number holds

( Arg z in ].((3 / 2) * PI),(2 * PI).[ iff ( Re z > 0 & Im z < 0 ) )

( Arg z in ].((3 / 2) * PI),(2 * PI).[ iff ( Re z > 0 & Im z < 0 ) )

proof end;

theorem Th53: :: COMPTRIG:53

for x being real number

for n being Nat holds ((cos x) + ((sin x) * <i>)) |^ n = (cos (n * x)) + ((sin (n * x)) * <i>)

for n being Nat holds ((cos x) + ((sin x) * <i>)) |^ n = (cos (n * x)) + ((sin (n * x)) * <i>)

proof end;

theorem :: COMPTRIG:54

for z being Element of COMPLEX

for n being Nat st ( z <> 0 or n <> 0 ) holds

z |^ n = ((|.z.| |^ n) * (cos (n * (Arg z)))) + (((|.z.| |^ n) * (sin (n * (Arg z)))) * <i>)

for n being Nat st ( z <> 0 or n <> 0 ) holds

z |^ n = ((|.z.| |^ n) * (cos (n * (Arg z)))) + (((|.z.| |^ n) * (sin (n * (Arg z)))) * <i>)

proof end;

theorem Th55: :: COMPTRIG:55

for x being Real

for n, k being Nat st n <> 0 holds

((cos ((x + ((2 * PI) * k)) / n)) + ((sin ((x + ((2 * PI) * k)) / n)) * <i>)) |^ n = (cos x) + ((sin x) * <i>)

for n, k being 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 end;

theorem Th56: :: COMPTRIG:56

for z being complex number

for n, k being 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

for n, k being 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 end;

definition

let x be complex number ;

let n be non empty Nat;

existence

ex b_{1} being complex number st b_{1} |^ n = x

end;
let n be non empty Nat;

existence

ex b

proof end;

:: deftheorem Def2 defines CRoot COMPTRIG:def 2 :

for x being complex number

for n being non empty Nat

for b_{3} being complex number holds

( b_{3} is CRoot of n,x iff b_{3} |^ n = x );

for x being complex number

for n being non empty Nat

for b

( b

theorem :: COMPTRIG:57

for x being Element of COMPLEX

for n being non empty Nat

for k being 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

for n being non empty Nat

for k being 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 end;

theorem :: COMPTRIG:60

for n being non empty Nat

for x being Element of COMPLEX

for v being CRoot of n,x st v = 0 holds

x = 0

for x being Element of COMPLEX

for v being CRoot of n,x st v = 0 holds

x = 0

proof end;