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

begin

scheme :: COMPTRIG:sch 1
Regrwithout0{ P₁[ Nat] } :

P₁[1]

provided

A1: ex k being non empty Nat st P₁[k] and
A2: for k being non empty Nat st k <> 1 & P₁[k] holds
ex n being non empty Nat st
( n < k & P₁[n] )

proof end;

theorem :: COMPTRIG:1

canceled;

theorem :: COMPTRIG:2

canceled;

theorem Th3: :: COMPTRIG:3

for z being complex number holds Re z >= - |.z.|

proof end;

theorem :: COMPTRIG:4

for z being complex number holds Im z >= - |.z.|

proof end;

theorem :: COMPTRIG:5

canceled;

theorem :: COMPTRIG:6

canceled;

theorem Th7: :: COMPTRIG:7

for z being complex number holds |.z.| ^2 = ((Re z) ^2) + ((Im z) ^2)

proof end;

theorem :: COMPTRIG:8

canceled;

theorem :: COMPTRIG:9

canceled;

theorem :: COMPTRIG:10

canceled;

theorem :: COMPTRIG:11

canceled;

theorem :: COMPTRIG:12

canceled;

theorem :: COMPTRIG:13

canceled;

theorem :: COMPTRIG:14

canceled;

theorem :: COMPTRIG:15

canceled;

theorem :: COMPTRIG:16

canceled;

theorem Th17: :: COMPTRIG:17

for x being real number
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;

begin

theorem :: COMPTRIG:18

canceled;

theorem :: COMPTRIG:19

canceled;

theorem :: COMPTRIG:20

canceled;

PI in ].0,4.[
by SIN_COS:def 32;

then Lm1: 0 < PI
by XXREAL_1:4;

then Lm2: 0 + (PI / 2) < (PI / 2) + (PI / 2)
by XREAL_1:8;

Lm3: 0 + PI < PI + PI
by Lm1, XREAL_1:8;

Lm4: 0 + (PI / 2) < PI + (PI / 2)
by Lm1, XREAL_1:8;

Lm5: (PI / 2) + (PI / 2) < PI + (PI / 2)
by Lm2, XREAL_1:8;

((3 / 2) * PI) + (PI / 2) = 2 * PI
;

then Lm6: (3 / 2) * PI < 2 * PI
by Lm5, XREAL_1:8;

Lm7: 0 < (3 / 2) * PI
by Lm1;

theorem :: COMPTRIG:21

( 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:8;

theorem Th22: :: COMPTRIG:22

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

proof end;

theorem Th23: :: COMPTRIG:23

for x being real number st x in ].0,PI.[ holds
sin . x > 0

proof end;

theorem Th24: :: COMPTRIG:24

for x being real number st x in [.0,PI.] holds
sin . x >= 0

proof end;

theorem Th25: :: COMPTRIG:25

for x being real number st x in ].PI,(2 * PI).[ holds
sin . x < 0

proof end;

theorem Th26: :: COMPTRIG:26

for x being real number st x in [.PI,(2 * PI).] holds
sin . x <= 0

proof end;

theorem Th27: :: COMPTRIG:27

for x being real number st x in ].(- (PI / 2)),(PI / 2).[ holds
cos . x > 0

proof end;

theorem Th28: :: COMPTRIG:28

for x being real number st x in [.(- (PI / 2)),(PI / 2).] holds
cos . x >= 0

proof end;

theorem Th29: :: COMPTRIG:29

for x being real number st x in ].(PI / 2),((3 / 2) * PI).[ holds
cos . x < 0

proof end;

theorem Th30: :: COMPTRIG:30

for x being real number st x in [.(PI / 2),((3 / 2) * PI).] holds
cos . x <= 0

proof end;

theorem Th31: :: COMPTRIG:31

for x being real number st x in ].((3 / 2) * PI),(2 * PI).[ holds
cos . x > 0

proof end;

theorem Th32: :: COMPTRIG:32

for x being real number st x in [.((3 / 2) * PI),(2 * PI).] holds
cos . x >= 0

proof end;

theorem Th33: :: COMPTRIG:33

for x being real number st 0 <= x & x < 2 * PI & sin x = 0 & not x = 0 holds
x = PI

proof end;

theorem Th34: :: COMPTRIG:34

for x being real number st 0 <= x & x < 2 * PI & cos x = 0 & not x = PI / 2 holds
x = (3 / 2) * PI

proof end;

theorem Th35: :: COMPTRIG:35

sin | ].(- (PI / 2)),(PI / 2).[ is increasing

proof end;

theorem Th36: :: COMPTRIG:36

sin | ].(PI / 2),((3 / 2) * PI).[ is decreasing

proof end;

theorem Th37: :: COMPTRIG:37

cos | ].0,PI.[ is decreasing

proof end;

theorem Th38: :: COMPTRIG:38

cos | ].PI,(2 * PI).[ is increasing

proof end;

theorem :: COMPTRIG:39

sin | [.(- (PI / 2)),(PI / 2).] is increasing

proof end;

theorem :: COMPTRIG:40

sin | [.(PI / 2),((3 / 2) * PI).] is decreasing

proof end;

theorem Th41: :: COMPTRIG:41

cos | [.0,PI.] is decreasing

proof end;

theorem Th42: :: COMPTRIG:42

cos | [.PI,(2 * PI).] is increasing

proof end;

theorem :: COMPTRIG:43

canceled;

theorem :: COMPTRIG:44

canceled;

theorem Th45: :: COMPTRIG:45

for x being real number holds
( sin . x in [.(- 1),1.] & cos . x in [.(- 1),1.] )

proof end;

theorem :: COMPTRIG:46

rng sin = [.(- 1),1.]

proof end;

theorem :: COMPTRIG:47

rng cos = [.(- 1),1.]

proof end;

theorem :: COMPTRIG:48

rng (sin | [.(- (PI / 2)),(PI / 2).]) = [.(- 1),1.]

proof end;

theorem :: COMPTRIG:49

rng (sin | [.(PI / 2),((3 / 2) * PI).]) = [.(- 1),1.]

proof end;

theorem Th50: :: COMPTRIG:50

rng (cos | [.0,PI.]) = [.(- 1),1.]

proof end;

theorem Th51: :: COMPTRIG:51

rng (cos | [.PI,(2 * PI).]) = [.(- 1),1.]

proof end;

begin

definition

let z be complex number ;
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 b₁ being Real st
( z = (|.z.| * (cos b₁)) + ((|.z.| * (sin b₁)) * <i>) & 0 <= b₁ & b₁ < 2 * PI ) ) & ( not z <> 0 implies ex b₁ being Real st b₁ = 0 ) )

proof end;

uniqueness
for b₁, b₂ being Real holds
( ( z <> 0 & z = (|.z.| * (cos b₁)) + ((|.z.| * (sin b₁)) * <i>) & 0 <= b₁ & b₁ < 2 * PI & z = (|.z.| * (cos b₂)) + ((|.z.| * (sin b₂)) * <i>) & 0 <= b₂ & b₂ < 2 * PI implies b₁ = b₂ ) & ( not z <> 0 & b₁ = 0 & b₂ = 0 implies b₁ = b₂ ) )

proof end;

consistency
for b₁ being Real holds verum ;

end;

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

theorem Th52: :: COMPTRIG:52

for z being complex number holds
( 0 <= Arg z & Arg z < 2 * PI )

proof end;

theorem Th53: :: COMPTRIG:53

for x being Real st x >= 0 holds
Arg x = 0

proof end;

theorem Th54: :: COMPTRIG:54

for x being Real st x < 0 holds
Arg x = PI

proof end;

theorem Th55: :: COMPTRIG:55

for x being Real st x > 0 holds
Arg (x * <i>) = PI / 2

proof end;

theorem Th56: :: COMPTRIG:56

for x being Real st x < 0 holds
Arg (x * <i>) = (3 / 2) * PI

proof end;

theorem :: COMPTRIG:57

Arg 1 = 0 by Th53;

theorem :: COMPTRIG:58

Arg <i> = PI / 2

proof end;

theorem Th59: :: COMPTRIG:59

for z being complex number holds
( Arg z in ].0,(PI / 2).[ iff ( Re z > 0 & Im z > 0 ) )

proof end;

theorem Th60: :: COMPTRIG:60

for z being complex number holds
( Arg z in ].(PI / 2),PI.[ iff ( Re z < 0 & Im z > 0 ) )

proof end;

theorem Th61: :: COMPTRIG:61

for z being complex number holds
( Arg z in ].PI,((3 / 2) * PI).[ iff ( Re z < 0 & Im z < 0 ) )

proof end;

theorem Th62: :: COMPTRIG:62

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

proof end;

theorem Th63: :: COMPTRIG:63

for z being complex number st Im z > 0 holds
sin (Arg z) > 0

proof end;

theorem Th64: :: COMPTRIG:64

for z being complex number st Im z < 0 holds
sin (Arg z) < 0

proof end;

theorem :: COMPTRIG:65

for z being complex number st Im z >= 0 holds
sin (Arg z) >= 0

proof end;

theorem :: COMPTRIG:66

for z being complex number st Im z <= 0 holds
sin (Arg z) <= 0

proof end;

theorem Th67: :: COMPTRIG:67

for z being complex number st Re z > 0 holds
cos (Arg z) > 0

proof end;

theorem Th68: :: COMPTRIG:68

for z being complex number st Re z < 0 holds
cos (Arg z) < 0

proof end;

theorem :: COMPTRIG:69

for z being complex number st Re z >= 0 holds
cos (Arg z) >= 0

proof end;

theorem :: COMPTRIG:70

for z being complex number st Re z <= 0 & z <> 0 holds
cos (Arg z) <= 0

proof end;

theorem Th71: :: COMPTRIG:71

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

proof end;

theorem :: COMPTRIG:72

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 Th73: :: COMPTRIG:73

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 Th74: :: COMPTRIG:74

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

proof end;

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 b₁ being complex number st b₁ |^ n = x

proof end;

end;

:: deftheorem Def2 defines CRoot COMPTRIG:def 2 :
for x being complex number
for n being non empty Nat
for b₃ being complex number holds
( b₃ is CRoot of n,x iff b₃ |^ n = x );

theorem :: COMPTRIG:75

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

proof end;

theorem :: COMPTRIG:76

for x being Element of COMPLEX
for v being CRoot of 1,x holds v = x

proof end;

theorem :: COMPTRIG:77

for n being non empty Nat
for v being CRoot of n, 0 holds v = 0

proof end;

theorem :: COMPTRIG:78

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

proof end;

theorem :: COMPTRIG:79

for a being real number st 0 <= a & a < 2 * PI & cos a = 1 holds
a = 0

proof end;

theorem :: COMPTRIG:80

for z being complex number holds z = (|.z.| * (cos (Arg z))) + ((|.z.| * (sin (Arg z))) * <i>)

proof end;