:: COMPTRIG semantic presentation

Lm1: for z being complex number st |.z.| = 0 holds
z = 0
by COMPLEX1:131;

Lm2: for z being complex number holds
( z <> 0 iff 0 < |.z.| )
by COMPLEX1:133;

Lm3: 0. F_Complex = 0
by COMPLFLD:9;

Lm4: for x, y being Real holds [*x,y*] = x + (y * )
by COMPLEX1:27;

Lm5: for x, y being Real holds [**x,y**] = x + (y * )
by HAHNBAN1:def 1;

Lm6: for z being complex number holds z = (Re z) + ((Im z) * )
by COMPLEX1:29;

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 Th8: :: COMPTRIG:8

for x1, x2, y1, y2 being Real st [**x1,x2**] = [**y1,y2**] holds
( x1 = y1 & x2 = y2 )

proof end;

theorem Th9: :: COMPTRIG:9

for z being complex number holds z = [**(Re z),(Im z)**]

proof end;

Lm7: 0 + (0 * ) = [**0,0**]
by HAHNBAN1:def 1;

Lm8: 0. F_Complex = the Zero of F_Complex
by RLVECT_1:def 2;

theorem :: COMPTRIG:10

canceled;

theorem :: COMPTRIG:11

canceled;

theorem Th12: :: COMPTRIG:12

for L being non empty unital HGrStr
for x being Element of L holds (power L) . x,1 = x

proof end;

theorem :: COMPTRIG:13

for L being non empty unital HGrStr
for x being Element of L holds (power L) . x,2 = x * x

proof end;

theorem Th14: :: COMPTRIG:14

for L being non empty add-associative right_zeroed right_complementable unital right-distributive doubleLoopStr
for n being Nat st n > 0 holds
(power L) . (0. L),n = 0. L

proof end;

theorem Th15: :: COMPTRIG:15

for L being non empty unital associative commutative HGrStr
for x, y being Element of L
for n being Nat holds (power L) . (x * y),n = ((power L) . x,n) * ((power L) . y,n)

proof end;

theorem Th16: :: COMPTRIG:16

for x being Real st x > 0 holds
for n being Nat holds (power F_Complex ) . [**x,0**],n = [**(x to_power n),0**]

proof end;

theorem Th17: :: COMPTRIG:17

for x being real number
for n being Nat st x >= 0 & n <> 0 holds
(n -root x) to_power n = x

proof end;

theorem :: COMPTRIG:18

canceled;

theorem :: COMPTRIG:19

canceled;

theorem Th20: :: COMPTRIG:20

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

theorem Th21: :: 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 )

proof end;

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 is_increasing_on ].(- (PI / 2)),(PI / 2).[

proof end;

theorem Th36: :: COMPTRIG:36

sin is_decreasing_on ].(PI / 2),((3 / 2) * PI ).[

proof end;

theorem Th37: :: COMPTRIG:37

cos is_decreasing_on ].0,PI .[

proof end;

theorem Th38: :: COMPTRIG:38

cos is_increasing_on ].PI ,(2 * PI ).[

proof end;

theorem :: COMPTRIG:39

sin is_increasing_on [.(- (PI / 2)),(PI / 2).]

proof end;

theorem :: COMPTRIG:40

sin is_decreasing_on [.(PI / 2),((3 / 2) * PI ).]

proof end;

theorem Th41: :: COMPTRIG:41

cos is_decreasing_on [.0,PI .]

proof end;

theorem Th42: :: COMPTRIG:42

cos is_increasing_on [.PI ,(2 * PI ).]

proof end;

theorem Th43: :: COMPTRIG:43

( sin is_continuous_on REAL & ( for x, y being real number holds
( sin is_continuous_on [.x,y.] & sin is_continuous_on ].x,y.[ ) ) )

proof end;

theorem Th44: :: COMPTRIG:44

( cos is_continuous_on REAL & ( for x, y being real number holds
( cos is_continuous_on [.x,y.] & cos is_continuous_on ].x,y.[ ) ) )

proof end;

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;

definition

let z be complex number ;
func Arg z -> Real means :Def1: :: COMPTRIG:def 1
( z = (|.z.| * (cos it)) + ((|.z.| * (sin it)) * ) & 0 <= it & it < 2 * PI ) if z <> 0
otherwise it = 0;
existence

proof end;

uniqueness

proof end;

consistency ;

end;

:: deftheorem Def1 defines Arg COMPTRIG:def 1 :

theorem Th52: :: COMPTRIG:52

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

proof end;

Lm9: for z being complex number st z <> 0 holds
z = [**(|.z.| * (cos (Arg z))),(|.z.| * (sin (Arg z)))**]

proof end;

theorem Th53: :: COMPTRIG:53

for x being Real st x >= 0 holds
Arg [**x,0**] = 0

proof end;

theorem Th54: :: COMPTRIG:54

for x being Real st x < 0 holds
Arg [**x,0**] = PI

proof end;

theorem Th55: :: COMPTRIG:55

for x being Real st x > 0 holds
Arg [**0,x**] = PI / 2

proof end;

theorem Th56: :: COMPTRIG:56

for x being Real st x < 0 holds
Arg [**0,x**] = (3 / 2) * PI

proof end;

theorem :: COMPTRIG:57

Arg (1. F_Complex ) = 0

proof end;

theorem :: COMPTRIG:58

Arg i_FC = PI / 2 by Th55, HAHNBAN1:6;

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
for n being Nat holds (power F_Complex ) . [**(cos x),(sin x)**],n = [**(cos (n * x)),(sin (n * x))**]

proof end;

theorem :: COMPTRIG:72

for z being Element of F_Complex
for n being 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 end;

theorem Th73: :: COMPTRIG:73

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

theorem Th74: :: COMPTRIG:74

for z being Element of F_Complex
for n, k being 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 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: :: COMPTRIG:def 2
(power F_Complex ) . it,n = x;
existence

proof end;

end;

:: deftheorem Def2 defines CRoot COMPTRIG:def 2 :

theorem :: COMPTRIG:75

for x being Element of F_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)))**] is CRoot of n,x

proof end;

theorem :: COMPTRIG:76

for x being Element of F_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. F_Complex holds v = 0. F_Complex

proof end;

theorem :: COMPTRIG:78

for n being non empty Nat
for x being Element of F_Complex
for v being CRoot of n,x st v = 0. F_Complex holds
x = 0. F_Complex

proof end;