:: COMPTRIG semantic presentation

Lemma1: for b₁ being complex number st |.b₁.| = 0 holds
b₁ = 0
by COMPLEX1:131;

Lemma2: for b₁ being complex number holds
( b₁ <> 0 iff 0 < |.b₁.| )
by COMPLEX1:133;

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

Lemma4: for b₁, b₂ being Real holds [*b₁,b₂*] = b₁ + (b₂ * )
by COMPLEX1:27;

Lemma5: for b₁, b₂ being Real holds [**b₁,b₂**] = b₁ + (b₂ * )
by HAHNBAN1:def 1;

Lemma6: for b₁ being complex number holds b₁ = (Re b₁) + ((Im b₁) * )
by COMPLEX1:29;

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

P₁[1]

provided

E7: ex b₁ being non empty Nat st P₁[b₁] and
E8: for b₁ being non empty Nat st b₁ <> 1 & P₁[b₁] holds
ex b₂ being non empty Nat st
( b₂ < b₁ & P₁[b₂] )

proof end;

theorem Th1: :: COMPTRIG:1

canceled;

theorem Th2: :: COMPTRIG:2

canceled;

theorem Th3: :: COMPTRIG:3

for b₁ being complex number holds Re b₁ >= - |.b₁.|

proof end;

theorem Th4: :: COMPTRIG:4

for b₁ being complex number holds Im b₁ >= - |.b₁.|

proof end;

theorem Th5: :: COMPTRIG:5

canceled;

theorem Th6: :: COMPTRIG:6

canceled;

theorem Th7: :: COMPTRIG:7

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

proof end;

theorem Th8: :: COMPTRIG:8

for b₁, b₂, b₃, b₄ being Real st [**b₁,b₂**] = [**b₃,b₄**] holds
( b₁ = b₃ & b₂ = b₄ )

proof end;

theorem Th9: :: COMPTRIG:9

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

proof end;

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

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

theorem Th10: :: COMPTRIG:10

canceled;

theorem Th11: :: COMPTRIG:11

canceled;

theorem Th12: :: COMPTRIG:12

for b₁ being non empty unital HGrStr
for b₂ being Element of b₁ holds (power b₁) . b₂,1 = b₂

proof end;

theorem Th13: :: COMPTRIG:13

for b₁ being non empty unital HGrStr
for b₂ being Element of b₁ holds (power b₁) . b₂,2 = b₂ * b₂

proof end;

theorem Th14: :: COMPTRIG:14

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

proof end;

theorem Th15: :: COMPTRIG:15

for b₁ being non empty unital associative commutative HGrStr
for b₂, b₃ being Element of b₁
for b₄ being Nat holds (power b₁) . (b₂ * b₃),b₄ = ((power b₁) . b₂,b₄) * ((power b₁) . b₃,b₄)

proof end;

theorem Th16: :: COMPTRIG:16

for b₁ being Real st b₁ > 0 holds
for b₂ being Nat holds (power F_Complex ) . [**b₁,0**],b₂ = [**(b₁ to_power b₂),0**]

proof end;

theorem Th17: :: COMPTRIG:17

for b₁ being real number
for b₂ being Nat st b₁ >= 0 & b₂ <> 0 holds
(b₂ -root b₁) to_power b₂ = b₁

proof end;

theorem Th18: :: COMPTRIG:18

canceled;

theorem Th19: :: 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 b₁, b₂, b₃, b₄ being real number holds
( not b₄ in ].b₁,b₃.[ or b₄ in ].b₁,b₂.[ or b₄ = b₂ or b₄ in ].b₂,b₃.[ )

proof end;

theorem Th23: :: COMPTRIG:23

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

proof end;

theorem Th24: :: COMPTRIG:24

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

proof end;

theorem Th25: :: COMPTRIG:25

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

proof end;

theorem Th26: :: COMPTRIG:26

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

proof end;

theorem Th27: :: COMPTRIG:27

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

proof end;

theorem Th28: :: COMPTRIG:28

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

proof end;

theorem Th29: :: COMPTRIG:29

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

proof end;

theorem Th30: :: COMPTRIG:30

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

proof end;

theorem Th31: :: COMPTRIG:31

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

proof end;

theorem Th32: :: COMPTRIG:32

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

proof end;

theorem Th33: :: COMPTRIG:33

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

proof end;

theorem Th34: :: COMPTRIG:34

for b₁ being real number st 0 <= b₁ & b₁ < 2 * PI & cos b₁ = 0 & not b₁ = PI / 2 holds
b₁ = (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 Th39: :: COMPTRIG:39

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

proof end;

theorem Th40: :: 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 b₁, b₂ being real number holds
( sin is_continuous_on [.b₁,b₂.] & sin is_continuous_on ].b₁,b₂.[ ) ) )

proof end;

theorem Th44: :: COMPTRIG:44

( cos is_continuous_on REAL & ( for b₁, b₂ being real number holds
( cos is_continuous_on [.b₁,b₂.] & cos is_continuous_on ].b₁,b₂.[ ) ) )

proof end;

theorem Th45: :: COMPTRIG:45

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

proof end;

theorem Th46: :: COMPTRIG:46

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

proof end;

theorem Th47: :: COMPTRIG:47

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

proof end;

theorem Th48: :: COMPTRIG:48

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

proof end;

theorem Th49: :: 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 c₁ be complex number ;
func Arg c₁ -> Real means :Def1: :: COMPTRIG:def 1
( a₁ = (|.a₁.| * (cos a₂)) + ((|.a₁.| * (sin a₂)) * ) & 0 <= a₂ & a₂ < 2 * PI ) if a₁ <> 0
otherwise a₂ = 0;
existence

proof end;

uniqueness

proof end;

consistency ;

end;

:: deftheorem Def1 defines Arg COMPTRIG:def 1 :

theorem Th52: :: COMPTRIG:52

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

proof end;

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

proof end;

theorem Th53: :: COMPTRIG:53

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

proof end;

theorem Th54: :: COMPTRIG:54

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

proof end;

theorem Th55: :: COMPTRIG:55

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

proof end;

theorem Th56: :: COMPTRIG:56

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

proof end;

theorem Th57: :: COMPTRIG:57

Arg (1. F_Complex ) = 0

proof end;

theorem Th58: :: COMPTRIG:58

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

theorem Th59: :: COMPTRIG:59

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

proof end;

theorem Th60: :: COMPTRIG:60

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

proof end;

theorem Th61: :: COMPTRIG:61

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

proof end;

theorem Th62: :: COMPTRIG:62

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

proof end;

theorem Th63: :: COMPTRIG:63

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

proof end;

theorem Th64: :: COMPTRIG:64

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

proof end;

theorem Th65: :: COMPTRIG:65

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

proof end;

theorem Th66: :: COMPTRIG:66

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

proof end;

theorem Th67: :: COMPTRIG:67

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

proof end;

theorem Th68: :: COMPTRIG:68

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

proof end;

theorem Th69: :: COMPTRIG:69

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

proof end;

theorem Th70: :: COMPTRIG:70

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

proof end;

theorem Th71: :: COMPTRIG:71

for b₁ being Real
for b₂ being Nat holds (power F_Complex ) . [**(cos b₁),(sin b₁)**],b₂ = [**(cos (b₂ * b₁)),(sin (b₂ * b₁))**]

proof end;

theorem Th72: :: COMPTRIG:72

for b₁ being Element of F_Complex
for b₂ being Nat st ( b₁ <> 0. F_Complex or b₂ <> 0 ) holds
(power F_Complex ) . b₁,b₂ = [**((|.b₁.| to_power b₂) * (cos (b₂ * (Arg b₁)))),((|.b₁.| to_power b₂) * (sin (b₂ * (Arg b₁))))**]

proof end;

theorem Th73: :: COMPTRIG:73

for b₁ being Real
for b₂, b₃ being Nat st b₂ <> 0 holds
(power F_Complex ) . [**(cos ((b₁ + ((2 * PI ) * b₃)) / b₂)),(sin ((b₁ + ((2 * PI ) * b₃)) / b₂))**],b₂ = [**(cos b₁),(sin b₁)**]

proof end;

theorem Th74: :: COMPTRIG:74

for b₁ being Element of F_Complex
for b₂, b₃ being Nat st b₂ <> 0 holds
b₁ = (power F_Complex ) . [**((b₂ -root |.b₁.|) * (cos (((Arg b₁) + ((2 * PI ) * b₃)) / b₂))),((b₂ -root |.b₁.|) * (sin (((Arg b₁) + ((2 * PI ) * b₃)) / b₂)))**],b₂

proof end;

definition

let c₁ be Element of F_Complex ;
let c₂ be non empty Nat;
mode CRoot of c₂,c₁ -> Element of F_Complex means :Def2: :: COMPTRIG:def 2
(power F_Complex ) . a₃,a₂ = a₁;
existence

proof end;

end;

:: deftheorem Def2 defines CRoot COMPTRIG:def 2 :

theorem Th75: :: COMPTRIG:75

for b₁ being Element of F_Complex
for b₂ being non empty Nat
for b₃ being Nat holds [**((b₂ -root |.b₁.|) * (cos (((Arg b₁) + ((2 * PI ) * b₃)) / b₂))),((b₂ -root |.b₁.|) * (sin (((Arg b₁) + ((2 * PI ) * b₃)) / b₂)))**] is CRoot of b₂,b₁

proof end;

theorem Th76: :: COMPTRIG:76

for b₁ being Element of F_Complex
for b₂ being CRoot of 1,b₁ holds b₂ = b₁

proof end;

theorem Th77: :: COMPTRIG:77

for b₁ being non empty Nat
for b₂ being CRoot of b₁, 0. F_Complex holds b₂ = 0. F_Complex

proof end;

theorem Th78: :: COMPTRIG:78

for b₁ being non empty Nat
for b₂ being Element of F_Complex
for b₃ being CRoot of b₁,b₂ st b₃ = 0. F_Complex holds
b₂ = 0. F_Complex

proof end;