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


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

theorem Th1: :: COMPTRIG:1
for z being Complex holds Re z >= - |.z.|
proof end;

theorem :: COMPTRIG:2
for z being Complex holds Im z >= - |.z.|
proof end;

theorem Th3: :: COMPTRIG:3
for z being Complex holds |.z.| ^2 = ((Re z) ^2) + ((Im z) ^2)
proof end;

theorem Th4: :: COMPTRIG:4
for x being Real
for n being Nat st x >= 0 & n <> 0 holds
(n -root x) |^ n = x
proof end;

registration
cluster PI -> non negative ;
coherence
not PI is negative
proof end;
end;

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 & 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: :: COMPTRIG:6
for a, b, c, x being Real holds
( not x in ].a,c.[ or x in ].a,b.[ or x = b or x in ].b,c.[ )
proof end;

theorem Th7: :: COMPTRIG:7
for x being Real st x in ].0,PI.[ holds
sin . x > 0
proof end;

theorem Th8: :: COMPTRIG:8
for x being Real st x in [.0,PI.] holds
sin . x >= 0
proof end;

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

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

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

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

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

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

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

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

theorem Th17: :: COMPTRIG:17
for x being Real st 0 <= x & x < 2 * PI & sin x = 0 & not x = 0 holds
x = PI
proof end;

theorem Th18: :: COMPTRIG:18
for x being Real st 0 <= x & x < 2 * PI & cos x = 0 & not x = PI / 2 holds
x = (3 / 2) * PI
proof end;

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

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

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

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

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

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

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

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

theorem Th27: :: COMPTRIG:27
for x being Real holds
( sin . x in [.(- 1),1.] & cos . x in [.(- 1),1.] )
proof end;

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

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

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

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

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

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

definition
let z be Complex;
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 <> 0 implies ex b1 being Real st
( z = (|.z.| * (cos b1)) + ((|.z.| * (sin b1)) * <i>) & 0 <= b1 & b1 < 2 * PI ) ) & ( not z <> 0 implies ex b1 being Real st b1 = 0 ) )
proof end;
uniqueness
for b1, b2 being Real holds
( ( z <> 0 & z = (|.z.| * (cos b1)) + ((|.z.| * (sin b1)) * <i>) & 0 <= b1 & b1 < 2 * PI & z = (|.z.| * (cos b2)) + ((|.z.| * (sin b2)) * <i>) & 0 <= b2 & b2 < 2 * PI implies b1 = b2 ) & ( not z <> 0 & b1 = 0 & b2 = 0 implies b1 = b2 ) )
proof end;
consistency
for b1 being Real holds verum ;
end;

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

theorem Th34: :: COMPTRIG:34
for z being Complex holds
( 0 <= Arg z & Arg z < 2 * PI )
proof end;

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

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

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

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

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

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

theorem Th41: :: COMPTRIG:41
for z being Complex holds
( Arg z in ].0,(PI / 2).[ iff ( Re z > 0 & Im z > 0 ) )
proof end;

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

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

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

theorem Th45: :: COMPTRIG:45
for z being Complex st Im z > 0 holds
sin (Arg z) > 0
proof end;

theorem Th46: :: COMPTRIG:46
for z being Complex st Im z < 0 holds
sin (Arg z) < 0
proof end;

theorem :: COMPTRIG:47
for z being Complex st Im z >= 0 holds
sin (Arg z) >= 0
proof end;

theorem :: COMPTRIG:48
for z being Complex st Im z <= 0 holds
sin (Arg z) <= 0
proof end;

theorem Th49: :: COMPTRIG:49
for z being Complex st Re z > 0 holds
cos (Arg z) > 0
proof end;

theorem Th50: :: COMPTRIG:50
for z being Complex st Re z < 0 holds
cos (Arg z) < 0
proof end;

theorem :: COMPTRIG:51
for z being Complex st Re z >= 0 holds
cos (Arg z) >= 0
proof end;

theorem :: COMPTRIG:52
for z being Complex st Re z <= 0 & z <> 0 holds
cos (Arg z) <= 0
proof end;

theorem Th53: :: COMPTRIG:53
for x being Real
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>)
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>)
proof end;

theorem Th56: :: COMPTRIG:56
for z being Complex
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;
let n be non zero Nat;
mode CRoot of n,x -> Complex means :Def2: :: COMPTRIG:def 2
it |^ n = x;
existence
ex b1 being Complex st b1 |^ n = x
proof end;
end;

:: deftheorem Def2 defines CRoot COMPTRIG:def 2 :
for x being Complex
for n being non zero Nat
for b3 being Complex holds
( b3 is CRoot of n,x iff b3 |^ n = x );

theorem :: COMPTRIG:57
for x being Element of COMPLEX
for n being non zero 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:58
for x being Element of COMPLEX
for v being CRoot of 1,x holds v = x
proof end;

theorem :: COMPTRIG:59
for n being non zero Nat
for v being CRoot of n, 0 holds v = 0
proof end;

theorem :: COMPTRIG:60
for n being non zero Nat
for x being Element of COMPLEX
for v being CRoot of n,x st v = 0 holds
x = 0
proof end;

theorem :: COMPTRIG:61
for a being Real st 0 <= a & a < 2 * PI & cos a = 1 holds
a = 0
proof end;

theorem :: COMPTRIG:62
for z being Complex holds z = (|.z.| * (cos (Arg z))) + ((|.z.| * (sin (Arg z))) * <i>)
proof end;