:: Trigonometric Form of Complex Numbers
:: by Robert Milewski
::
:: Received July 21, 2000
:: Copyright (c) 2000-2012 Association of Mizar Users


begin

scheme :: COMPTRIG:sch 1
Regrwithout0{ P1[ Nat] } :
 P1[1]
provided
A1: ex k being non empty Nat st P1[k] and
A2: for k being non empty Nat st k <> 1 &amp; P1[k] holds
ex n being non empty Nat st
( n < k &amp; P1[n] )
proofend;

theorem Th1: :: COMPTRIG:1
for z being complex number holds Re z >= - |.z.|
proofend;

theorem :: COMPTRIG:2
for z being complex number holds Im z >= - |.z.|
proofend;

theorem Th3: :: COMPTRIG:3
for z being complex number holds |.z.| ^2 = ((Re z) ^2) + ((Im z) ^2)
proofend;

theorem Th4: :: COMPTRIG:4
for x being real number
for n being Nat st x >= 0 &amp; n <> 0 holds
(n -root x) |^ n = x
proofend;

registration
cluster PI  ->  non negative ;
coherence
 not PI is negative
proofend;
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 :: COMPTRIG:5
( 0 < PI / 2 &amp; PI / 2 < PI &amp; 0 < PI &amp; - (PI / 2) < PI / 2 &amp; PI < 2 * PI &amp; PI / 2 < (3 / 2) * PI &amp; - (PI / 2) < 0 &amp; 0 < 2 * PI &amp; PI < (3 / 2) * PI &amp; (3 / 2) * PI < 2 * PI &amp; 0 < (3 / 2) * PI ) by Lm2, Lm3, Lm4, XREAL_1:6;

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.[ )
proofend;

theorem Th7: :: COMPTRIG:7
for x being real number st x in ].0,PI.[ holds
sin . x > 0
proofend;

theorem Th8: :: COMPTRIG:8
for x being real number st x in [.0,PI.] holds
sin . x >= 0
proofend;

theorem Th9: :: COMPTRIG:9
for x being real number st x in ].PI,(2 * PI).[ holds
sin . x < 0
proofend;

theorem Th10: :: COMPTRIG:10
for x being real number st x in [.PI,(2 * PI).] holds
sin . x <= 0
proofend;

theorem Th11: :: COMPTRIG:11
for x being real number st x in ].(- (PI / 2)),(PI / 2).[ holds
cos . x > 0
proofend;

theorem Th12: :: COMPTRIG:12
for x being real number st x in [.(- (PI / 2)),(PI / 2).] holds
cos . x >= 0
proofend;

theorem Th13: :: COMPTRIG:13
for x being real number st x in ].(PI / 2),((3 / 2) * PI).[ holds
cos . x < 0
proofend;

theorem Th14: :: COMPTRIG:14
for x being real number st x in [.(PI / 2),((3 / 2) * PI).] holds
cos . x <= 0
proofend;

theorem Th15: :: COMPTRIG:15
for x being real number st x in ].((3 / 2) * PI),(2 * PI).[ holds
cos . x > 0
proofend;

theorem Th16: :: COMPTRIG:16
for x being real number st x in [.((3 / 2) * PI),(2 * PI).] holds
cos . x >= 0
proofend;

theorem Th17: :: COMPTRIG:17
for x being real number st 0 <= x &amp; x < 2 * PI &amp; sin x = 0 &amp; not x = 0 holds
x = PI
proofend;

theorem Th18: :: COMPTRIG:18
for x being real number st 0 <= x &amp; x < 2 * PI &amp; cos x = 0 &amp; not x = PI / 2 holds
x = (3 / 2) * PI
proofend;

theorem Th19: :: COMPTRIG:19
sin | ].(- (PI / 2)),(PI / 2).[ is increasing
proofend;

theorem Th20: :: COMPTRIG:20
sin | ].(PI / 2),((3 / 2) * PI).[ is decreasing
proofend;

theorem Th21: :: COMPTRIG:21
cos | ].0,PI.[ is decreasing
proofend;

theorem Th22: :: COMPTRIG:22
cos | ].PI,(2 * PI).[ is increasing
proofend;

theorem :: COMPTRIG:23
sin | [.(- (PI / 2)),(PI / 2).] is increasing
proofend;

theorem :: COMPTRIG:24
sin | [.(PI / 2),((3 / 2) * PI).] is decreasing
proofend;

theorem Th25: :: COMPTRIG:25
cos | [.0,PI.] is decreasing
proofend;

theorem Th26: :: COMPTRIG:26
cos | [.PI,(2 * PI).] is increasing
proofend;

theorem Th27: :: COMPTRIG:27
for x being real number holds
( sin . x in [.(- 1),1.] &amp; cos . x in [.(- 1),1.] )
proofend;

theorem :: COMPTRIG:28
rng sin = [.(- 1),1.]
proofend;

theorem :: COMPTRIG:29
rng cos = [.(- 1),1.]
proofend;

theorem :: COMPTRIG:30
rng (sin | [.(- (PI / 2)),(PI / 2).]) = [.(- 1),1.]
proofend;

theorem :: COMPTRIG:31
rng (sin | [.(PI / 2),((3 / 2) * PI).]) = [.(- 1),1.]
proofend;

theorem Th32: :: COMPTRIG:32
rng (cos | [.0,PI.]) = [.(- 1),1.]
proofend;

theorem Th33: :: COMPTRIG:33
rng (cos | [.PI,(2 * PI).]) = [.(- 1),1.]
proofend;

begin

definition
let z be complex number ;
func Arg z ->  Real means :Def1: :: COMPTRIG:def 1
( z = (|.z.| * (cos it)) + ((|.z.| * (sin it)) * <i>) &amp; 0 <= it &amp; it < 2 * PI ) if z <> 0
otherwise it = 0 ;
existence
 ( ( z <> 0 implies ex b1 being Real st
( z = (|.z.| * (cos b1)) + ((|.z.| * (sin b1)) * <i>) &amp; 0 <= b1 &amp; b1 < 2 * PI ) ) &amp; ( not z <> 0 implies ex b1 being Real st b1 = 0 ) )
proofend;
uniqueness
 for b1, b2 being Real holds
( ( z <> 0 &amp; z = (|.z.| * (cos b1)) + ((|.z.| * (sin b1)) * <i>) &amp; 0 <= b1 &amp; b1 < 2 * PI &amp; z = (|.z.| * (cos b2)) + ((|.z.| * (sin b2)) * <i>) &amp; 0 <= b2 &amp; b2 < 2 * PI implies b1 = b2 ) &amp; ( not z <> 0 &amp; b1 = 0 &amp; b2 = 0 implies b1 = b2 ) )
proofend;
consistency
 for b1 being Real holds verum ;
end;

:: deftheorem Def1 defines Arg COMPTRIG:def_1_:_
 for z being complex number
for b2 being Real holds
( ( z <> 0 implies ( b2 = Arg z iff ( z = (|.z.| * (cos b2)) + ((|.z.| * (sin b2)) * <i>) &amp; 0 <= b2 &amp; b2 < 2 * PI ) ) ) &amp; ( not z <> 0 implies ( b2 = Arg z iff b2 = 0 ) ) );

theorem Th34: :: COMPTRIG:34
for z being complex number holds
( 0 <= Arg z &amp; Arg z < 2 * PI )
proofend;

theorem Th35: :: COMPTRIG:35
for x being Real st x >= 0 holds
Arg x = 0
proofend;

theorem Th36: :: COMPTRIG:36
for x being Real st x < 0 holds
Arg x = PI
proofend;

theorem Th37: :: COMPTRIG:37
for x being Real st x > 0 holds
Arg (x * <i>) = PI / 2
proofend;

theorem Th38: :: COMPTRIG:38
for x being Real st x < 0 holds
Arg (x * <i>) = (3 / 2) * PI
proofend;

theorem :: COMPTRIG:39
Arg 1 = 0 by Th35;

theorem :: COMPTRIG:40
Arg <i> = PI / 2
proofend;

theorem Th41: :: COMPTRIG:41
for z being complex number holds
( Arg z in ].0,(PI / 2).[ iff ( Re z > 0 &amp; Im z > 0 ) )
proofend;

theorem Th42: :: COMPTRIG:42
for z being complex number holds
( Arg z in ].(PI / 2),PI.[ iff ( Re z < 0 &amp; Im z > 0 ) )
proofend;

theorem Th43: :: COMPTRIG:43
for z being complex number holds
( Arg z in ].PI,((3 / 2) * PI).[ iff ( Re z < 0 &amp; Im z < 0 ) )
proofend;

theorem Th44: :: COMPTRIG:44
for z being complex number holds
( Arg z in ].((3 / 2) * PI),(2 * PI).[ iff ( Re z > 0 &amp; Im z < 0 ) )
proofend;

theorem Th45: :: COMPTRIG:45
for z being complex number st Im z > 0 holds
sin (Arg z) > 0
proofend;

theorem Th46: :: COMPTRIG:46
for z being complex number st Im z < 0 holds
sin (Arg z) < 0
proofend;

theorem :: COMPTRIG:47
for z being complex number st Im z >= 0 holds
sin (Arg z) >= 0
proofend;

theorem :: COMPTRIG:48
for z being complex number st Im z <= 0 holds
sin (Arg z) <= 0
proofend;

theorem Th49: :: COMPTRIG:49
for z being complex number st Re z > 0 holds
cos (Arg z) > 0
proofend;

theorem Th50: :: COMPTRIG:50
for z being complex number st Re z < 0 holds
cos (Arg z) < 0
proofend;

theorem :: COMPTRIG:51
for z being complex number st Re z >= 0 holds
cos (Arg z) >= 0
proofend;

theorem :: COMPTRIG:52
for z being complex number st Re z <= 0 &amp; z <> 0 holds
cos (Arg z) <= 0
proofend;

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>)
proofend;

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>)
proofend;

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>)
proofend;

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
proofend;

definition
let x be complex number ;
let n be non empty Nat;
mode CRoot of n,x ->  complex number  means :Def2: :: COMPTRIG:def 2
it |^ n = x;
existence
 ex b1 being complex number st b1 |^ n = x
proofend;
end;

:: deftheorem Def2 defines CRoot COMPTRIG:def_2_:_
 for x being complex number
for n being non empty Nat
for b3 being complex number holds
( b3 is CRoot of n,x iff b3 |^ n = x );

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
proofend;

theorem :: COMPTRIG:58
for x being Element of COMPLEX
for v being CRoot of 1,x holds v = x
proofend;

theorem :: COMPTRIG:59
for n being non empty Nat
for v being CRoot of n, 0 holds v = 0
proofend;

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
proofend;

theorem :: COMPTRIG:61
for a being real number st 0 <= a &amp; a < 2 * PI &amp; cos a = 1 holds
a = 0
proofend;

theorem :: COMPTRIG:62
for z being complex number holds z = (|.z.| * (cos (Arg z))) + ((|.z.| * (sin (Arg z))) * <i>)
proofend;