:: SIN_COS semantic presentation

definition

let c₁, c₂ be Nat;
canceled;
func CHK c₁,c₂ -> Element of COMPLEX equals :Def2: :: SIN_COS:def 2
1 if a₁ <= a₂
otherwise 0;
correctness by COMPLEX1:def 6, COMPLEX1:def 7;

end;

:: deftheorem Def1 SIN_COS:def 1 :

:: deftheorem Def2 defines CHK SIN_COS:def 2 :

registration

let c₁, c₂ be Nat;
cluster CHK a₁,a₂ -> real ;
coherence

proof end;

end;

scheme :: SIN_COS:sch 1
s1{ F₁( Nat, Nat) -> Element of COMPLEX } :

for b₁ being Nat ex b₂ being Complex_Sequence st
for b₃ being Nat holds
( ( b₃ <= b₁ implies b₂ . b₃ = F₁(b₁,b₃) ) & ( b₃ > b₁ implies b₂ . b₃ = 0 ) )

proof end;

scheme :: SIN_COS:sch 2
s2{ F₁( Nat, Nat) -> real number } :

for b₁ being Nat ex b₂ being Real_Sequence st
for b₃ being Nat holds
( ( b₃ <= b₁ implies b₂ . b₃ = F₁(b₁,b₃) ) & ( b₃ > b₁ implies b₂ . b₃ = 0 ) )

proof end;

definition

canceled;
func Prod_complex_n -> Complex_Sequence means :Def4: :: SIN_COS:def 4
( a₁ . 0 = 1 & ( for b₁ being Nat holds a₁ . (b₁ + 1) = (a₁ . b₁) * (b₁ + 1) ) );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def3 SIN_COS:def 3 :

:: deftheorem Def4 defines Prod_complex_n SIN_COS:def 4 :

definition

func Prod_real_n -> Real_Sequence means :Def5: :: SIN_COS:def 5
( a₁ . 0 = 1 & ( for b₁ being Nat holds a₁ . (b₁ + 1) = (a₁ . b₁) * (b₁ + 1) ) );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def5 defines Prod_real_n SIN_COS:def 5 :

definition

let c₁ be Nat;
func c₁ !c -> Element of COMPLEX equals :: SIN_COS:def 6
Prod_complex_n . a₁;
coherence ;

end;

:: deftheorem Def6 defines !c SIN_COS:def 6 :

definition

let c₁ be Nat;
redefine func ! as c₁ ! -> Real equals :: SIN_COS:def 7
Prod_real_n . a₁;
coherence by XREAL_0:def 1;
compatibility

proof end;

end;

:: deftheorem Def7 defines ! SIN_COS:def 7 :

definition

let c₁ be Element of COMPLEX ;
deffunc H₁( Nat) -> Element of COMPLEX = (c₁ #N a₁) / (a₁ !c );
func c₁ ExpSeq -> Complex_Sequence means :Def8: :: SIN_COS:def 8
for b₁ being Nat holds a₂ . b₁ = (a₁ #N b₁) / (b₁ !c );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def8 defines ExpSeq SIN_COS:def 8 :

definition

let c₁ be real number ;
deffunc H₁( Nat) -> set = (c₁ |^ a₁) / (a₁ ! );
func c₁ ExpSeq -> Real_Sequence means :Def9: :: SIN_COS:def 9
for b₁ being Nat holds a₂ . b₁ = (a₁ |^ b₁) / (b₁ ! );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def9 defines ExpSeq SIN_COS:def 9 :

theorem Th1: :: SIN_COS:1

for b₁ being Nat holds
( 0 !c = 1 & b₁ !c <> 0 & (b₁ + 1) !c = (b₁ !c ) * (b₁ + 1) )

proof end;

theorem Th2: :: SIN_COS:2

for b₁ being Nat holds
( b₁ ! <> 0 & (b₁ + 1) ! = (b₁ ! ) * (b₁ + 1) ) by NEWTON:21, NEWTON:23;

theorem Th3: :: SIN_COS:3

( ( for b₁ being Nat st 0 < b₁ holds
((b₁ -' 1) !c ) * b₁ = b₁ !c ) & ( for b₁, b₂ being Nat st b₂ <= b₁ holds
((b₁ -' b₂) !c ) * ((b₁ + 1) - b₂) = ((b₁ + 1) -' b₂) !c ) )

proof end;

definition

let c₁ be Nat;
func Coef c₁ -> Complex_Sequence means :Def10: :: SIN_COS:def 10
for b₁ being Nat holds
( ( b₁ <= a₁ implies a₂ . b₁ = (a₁ !c ) / ((b₁ !c ) * ((a₁ -' b₁) !c )) ) & ( b₁ > a₁ implies a₂ . b₁ = 0 ) );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def10 defines Coef SIN_COS:def 10 :

definition

let c₁ be Nat;
func Coef_e c₁ -> Complex_Sequence means :Def11: :: SIN_COS:def 11
for b₁ being Nat holds
( ( b₁ <= a₁ implies a₂ . b₁ = 1r / ((b₁ !c ) * ((a₁ -' b₁) !c )) ) & ( b₁ > a₁ implies a₂ . b₁ = 0 ) );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def11 defines Coef_e SIN_COS:def 11 :

definition

let c₁ be Complex_Sequence;
func Sift c₁ -> Complex_Sequence means :Def12: :: SIN_COS:def 12
( a₂ . 0 = 0 & ( for b₁ being Nat holds a₂ . (b₁ + 1) = a₁ . b₁ ) );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def12 defines Sift SIN_COS:def 12 :

definition

let c₁ be Nat;
let c₂, c₃ be Element of COMPLEX ;
func Expan c₁,c₂,c₃ -> Complex_Sequence means :Def13: :: SIN_COS:def 13
for b₁ being Nat holds
( ( b₁ <= a₁ implies a₄ . b₁ = (((Coef a₁) . b₁) * (a₂ #N b₁)) * (a₃ #N (a₁ -' b₁)) ) & ( a₁ < b₁ implies a₄ . b₁ = 0 ) );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def13 defines Expan SIN_COS:def 13 :

definition

let c₁ be Nat;
let c₂, c₃ be Element of COMPLEX ;
func Expan_e c₁,c₂,c₃ -> Complex_Sequence means :Def14: :: SIN_COS:def 14
for b₁ being Nat holds
( ( b₁ <= a₁ implies a₄ . b₁ = (((Coef_e a₁) . b₁) * (a₂ #N b₁)) * (a₃ #N (a₁ -' b₁)) ) & ( a₁ < b₁ implies a₄ . b₁ = 0 ) );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def14 defines Expan_e SIN_COS:def 14 :

definition

let c₁ be Nat;
let c₂, c₃ be Element of COMPLEX ;
func Alfa c₁,c₂,c₃ -> Complex_Sequence means :Def15: :: SIN_COS:def 15
for b₁ being Nat holds
( ( b₁ <= a₁ implies a₄ . b₁ = ((a₂ ExpSeq ) . b₁) * ((Partial_Sums (a₃ ExpSeq )) . (a₁ -' b₁)) ) & ( a₁ < b₁ implies a₄ . b₁ = 0 ) );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def15 defines Alfa SIN_COS:def 15 :

definition

let c₁, c₂ be real number ;
let c₃ be Nat;
func Conj c₃,c₁,c₂ -> Real_Sequence means :: SIN_COS:def 16
for b₁ being Nat holds
( ( b₁ <= a₃ implies a₄ . b₁ = ((a₁ ExpSeq ) . b₁) * (((Partial_Sums (a₂ ExpSeq )) . a₃) - ((Partial_Sums (a₂ ExpSeq )) . (a₃ -' b₁))) ) & ( a₃ < b₁ implies a₄ . b₁ = 0 ) );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def16 defines Conj SIN_COS:def 16 :

definition

let c₁, c₂ be Element of COMPLEX ;
let c₃ be Nat;
func Conj c₃,c₁,c₂ -> Complex_Sequence means :Def17: :: SIN_COS:def 17
for b₁ being Nat holds
( ( b₁ <= a₃ implies a₄ . b₁ = ((a₁ ExpSeq ) . b₁) * (((Partial_Sums (a₂ ExpSeq )) . a₃) - ((Partial_Sums (a₂ ExpSeq )) . (a₃ -' b₁))) ) & ( a₃ < b₁ implies a₄ . b₁ = 0 ) );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def17 defines Conj SIN_COS:def 17 :

Lemma15: for b₁, b₂, b₃, b₄ being Element of REAL holds
( (b₁ + (b₃ * )) * (b₂ + (b₄ * )) = ((b₁ * b₂) - (b₃ * b₄)) + (((b₁ * b₄) + (b₂ * b₃)) * ) & (b₂ + (b₄ * )) *' = b₂ + ((- b₄) * ) )

proof end;

theorem Th4: :: SIN_COS:4

for b₁ being Element of COMPLEX
for b₂ being Nat holds
( (b₁ ExpSeq ) . (b₂ + 1) = (((b₁ ExpSeq ) . b₂) * b₁) / ((b₂ + 1) + (0 * )) & (b₁ ExpSeq ) . 0 = 1 & |.((b₁ ExpSeq ) . b₂).| = (|.b₁.| ExpSeq ) . b₂ )

proof end;

theorem Th5: :: SIN_COS:5

for b₁ being Nat
for b₂ being Complex_Sequence st 0 < b₁ holds
(Sift b₂) . b₁ = b₂ . (b₁ -' 1)

proof end;

theorem Th6: :: SIN_COS:6

for b₁ being Nat
for b₂ being Complex_Sequence holds (Partial_Sums b₂) . b₁ = ((Partial_Sums (Sift b₂)) . b₁) + (b₂ . b₁)

proof end;

theorem Th7: :: SIN_COS:7

for b₁, b₂ being Element of COMPLEX
for b₃ being Nat holds (b₁ + b₂) #N b₃ = (Partial_Sums (Expan b₃,b₁,b₂)) . b₃

proof end;

theorem Th8: :: SIN_COS:8

for b₁, b₂ being Element of COMPLEX
for b₃ being Nat holds Expan_e b₃,b₁,b₂ = (1r / (b₃ !c )) (#) (Expan b₃,b₁,b₂)

proof end;

theorem Th9: :: SIN_COS:9

for b₁, b₂ being Element of COMPLEX
for b₃ being Nat holds ((b₁ + b₂) #N b₃) / (b₃ !c ) = (Partial_Sums (Expan_e b₃,b₁,b₂)) . b₃

proof end;

theorem Th10: :: SIN_COS:10

( 0c ExpSeq is absolutely_summable & Sum (0c ExpSeq ) = 1r )

proof end;

registration

let c₁ be Element of COMPLEX ;
cluster a₁ ExpSeq -> absolutely_summable ;
coherence

proof end;

end;

theorem Th11: :: SIN_COS:11

for b₁, b₂ being Element of COMPLEX holds
( (b₁ ExpSeq ) . 0 = 1 & (Expan 0,b₁,b₂) . 0 = 1 )

proof end;

theorem Th12: :: SIN_COS:12

for b₁, b₂ being Element of COMPLEX
for b₃, b₄ being Nat st b₃ <= b₄ holds
(Alfa (b₄ + 1),b₁,b₂) . b₃ = ((Alfa b₄,b₁,b₂) . b₃) + ((Expan_e (b₄ + 1),b₁,b₂) . b₃)

proof end;

theorem Th13: :: SIN_COS:13

for b₁, b₂ being Element of COMPLEX
for b₃ being Nat holds (Partial_Sums (Alfa (b₃ + 1),b₁,b₂)) . b₃ = ((Partial_Sums (Alfa b₃,b₁,b₂)) . b₃) + ((Partial_Sums (Expan_e (b₃ + 1),b₁,b₂)) . b₃)

proof end;

theorem Th14: :: SIN_COS:14

for b₁, b₂ being Element of COMPLEX
for b₃ being Nat holds (b₁ ExpSeq ) . b₃ = (Expan_e b₃,b₁,b₂) . b₃

proof end;

theorem Th15: :: SIN_COS:15

for b₁, b₂ being Element of COMPLEX
for b₃ being Nat holds (Partial_Sums ((b₁ + b₂) ExpSeq )) . b₃ = (Partial_Sums (Alfa b₃,b₁,b₂)) . b₃

proof end;

theorem Th16: :: SIN_COS:16

for b₁, b₂ being Element of COMPLEX
for b₃ being Nat holds (((Partial_Sums (b₁ ExpSeq )) . b₃) * ((Partial_Sums (b₂ ExpSeq )) . b₃)) - ((Partial_Sums ((b₁ + b₂) ExpSeq )) . b₃) = (Partial_Sums (Conj b₃,b₁,b₂)) . b₃

proof end;

theorem Th17: :: SIN_COS:17

proof end;

theorem Th18: :: SIN_COS:18

for b₁ being Element of COMPLEX holds 1 <= Sum (|.b₁.| ExpSeq )

proof end;

theorem Th19: :: SIN_COS:19

for b₁ being Element of COMPLEX
for b₂ being Nat holds 0 <= (|.b₁.| ExpSeq ) . b₂

proof end;

theorem Th20: :: SIN_COS:20

for b₁ being Element of COMPLEX
for b₂, b₃ being Nat holds
( abs ((Partial_Sums (|.b₁.| ExpSeq )) . b₂) = (Partial_Sums (|.b₁.| ExpSeq )) . b₂ & ( b₂ <= b₃ implies abs (((Partial_Sums (|.b₁.| ExpSeq )) . b₃) - ((Partial_Sums (|.b₁.| ExpSeq )) . b₂)) = ((Partial_Sums (|.b₁.| ExpSeq )) . b₃) - ((Partial_Sums (|.b₁.| ExpSeq )) . b₂) ) )

proof end;

theorem Th21: :: SIN_COS:21

for b₁, b₂ being Element of COMPLEX
for b₃, b₄ being Nat holds abs ((Partial_Sums |.(Conj b₃,b₁,b₂).|) . b₄) = (Partial_Sums |.(Conj b₃,b₁,b₂).|) . b₄

proof end;

theorem Th22: :: SIN_COS:22

for b₁, b₂ being Element of COMPLEX
for b₃ being real number st b₃ > 0 holds
ex b₄ being Nat st
for b₅ being Nat st b₄ <= b₅ holds
abs ((Partial_Sums |.(Conj b₅,b₁,b₂).|) . b₅) < b₃

proof end;

theorem Th23: :: SIN_COS:23

for b₁, b₂ being Element of COMPLEX
for b₃ being Complex_Sequence st ( for b₄ being Nat holds b₃ . b₄ = (Partial_Sums (Conj b₄,b₁,b₂)) . b₄ ) holds
( b₃ is convergent & lim b₃ = 0 )

proof end;

Lemma36: for b₁, b₂ being Element of COMPLEX holds (Sum (b₁ ExpSeq )) * (Sum (b₂ ExpSeq )) = Sum ((b₁ + b₂) ExpSeq )

proof end;

definition

func exp -> PartFunc of COMPLEX , COMPLEX means :Def18: :: SIN_COS:def 18
( dom a₁ = COMPLEX & ( for b₁ being Element of COMPLEX holds a₁ . b₁ = Sum (b₁ ExpSeq ) ) );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def18 defines exp SIN_COS:def 18 :

definition

let c₁ be Element of COMPLEX ;
func exp c₁ -> Element of COMPLEX equals :: SIN_COS:def 19
exp . a₁;
correctness

proof end;

end;

:: deftheorem Def19 defines exp SIN_COS:def 19 :

Lemma38: for b₁ being Element of COMPLEX holds exp b₁ = Sum (b₁ ExpSeq )
by Def18;

theorem Th24: :: SIN_COS:24

for b₁, b₂ being Element of COMPLEX holds exp (b₁ + b₂) = (exp b₁) * (exp b₂)

proof end;

definition

func sin -> PartFunc of REAL , REAL means :Def20: :: SIN_COS:def 20
( dom a₁ = REAL & ( for b₁ being Element of REAL holds a₁ . b₁ = Im (Sum ([*0,b₁*] ExpSeq )) ) );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def20 defines sin SIN_COS:def 20 :

definition

let c₁ be real number ;
func sin c₁ -> set equals :: SIN_COS:def 21
sin . a₁;
correctness ;

end;

:: deftheorem Def21 defines sin SIN_COS:def 21 :

registration

let c₁ be real number ;
cluster sin a₁ -> real ;
correctness ;

end;

definition

let c₁ be Real;
redefine func sin as sin c₁ -> Real;
correctness ;

end;

theorem Th25: :: SIN_COS:25

sin is Function of REAL , REAL

proof end;

definition

func cos -> PartFunc of REAL , REAL means :Def22: :: SIN_COS:def 22
( dom a₁ = REAL & ( for b₁ being Real holds a₁ . b₁ = Re (Sum ([*0,b₁*] ExpSeq )) ) );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def22 defines cos SIN_COS:def 22 :

definition

let c₁ be real number ;
func cos c₁ -> set equals :: SIN_COS:def 23
cos . a₁;
correctness ;

end;

:: deftheorem Def23 defines cos SIN_COS:def 23 :

registration

let c₁ be real number ;
cluster cos a₁ -> real ;
correctness ;

end;

definition

let c₁ be Real;
redefine func cos as cos c₁ -> Real;
correctness ;

end;

theorem Th26: :: SIN_COS:26

cos is Function of REAL , REAL

proof end;

theorem Th27: :: SIN_COS:27

( dom sin = REAL & dom cos = REAL ) by Def20, Def22;

Lemma42: for b₁ being Real holds Sum ([*0,b₁*] ExpSeq ) = (cos . b₁) + ((sin . b₁) * )

proof end;

theorem Th28: :: SIN_COS:28

for b₁ being Real holds exp [*0,b₁*] = (cos b₁) + ((sin b₁) * )

proof end;

Lemma43: for b₁ being Real holds (Sum ([*0,b₁*] ExpSeq )) *' = Sum ((- [*0,b₁*]) ExpSeq )

proof end;

theorem Th29: :: SIN_COS:29

for b₁ being Real holds (exp [*0,b₁*]) *' = exp (- [*0,b₁*])

proof end;

Lemma44: for b₁ being Real
for b₂ being real number st b₁ = b₂ holds
( |.(Sum ([*0,b₁*] ExpSeq )).| = 1 & abs (sin . b₂) <= 1 & abs (cos . b₂) <= 1 )

proof end;

theorem Th30: :: SIN_COS:30

for b₁ being Real holds
( |.(exp [*0,b₁*]).| = 1 & ( for b₂ being real number holds
( abs (sin b₂) <= 1 & abs (cos b₂) <= 1 ) ) )

proof end;

theorem Th31: :: SIN_COS:31

for b₁ being real number holds
( ((cos . b₁) ^2 ) + ((sin . b₁) ^2 ) = 1 & ((cos . b₁) * (cos . b₁)) + ((sin . b₁) * (sin . b₁)) = 1 )

proof end;

theorem Th32: :: SIN_COS:32

for b₁ being real number holds
( ((cos b₁) ^2 ) + ((sin b₁) ^2 ) = 1 & ((cos b₁) * (cos b₁)) + ((sin b₁) * (sin b₁)) = 1 ) by Th31;

Lemma46: 0c = [*0,0*]
by ARYTM_0:def 7;

theorem Th33: :: SIN_COS:33

for b₁ being real number holds
( cos . 0 = 1 & sin . 0 = 0 & cos . (- b₁) = cos . b₁ & sin . (- b₁) = - (sin . b₁) )

proof end;

theorem Th34: :: SIN_COS:34

for b₁ being real number holds
( cos 0 = 1 & sin 0 = 0 & cos (- b₁) = cos b₁ & sin (- b₁) = - (sin b₁) ) by Th33;

definition

let c₁ be real number ;
deffunc H₁( Nat) -> set = (((- 1) |^ a₁) * (c₁ |^ ((2 * a₁) + 1))) / (((2 * a₁) + 1) ! );
func c₁ P_sin -> Real_Sequence means :Def24: :: SIN_COS:def 24
for b₁ being Nat holds a₂ . b₁ = (((- 1) |^ b₁) * (a₁ |^ ((2 * b₁) + 1))) / (((2 * b₁) + 1) ! );
existence

proof end;

uniqueness

proof end;

deffunc H₂( Nat) -> set = (((- 1) |^ a₁) * (c₁ |^ (2 * a₁))) / ((2 * a₁) ! );
func c₁ P_cos -> Real_Sequence means :Def25: :: SIN_COS:def 25
for b₁ being Nat holds a₂ . b₁ = (((- 1) |^ b₁) * (a₁ |^ (2 * b₁))) / ((2 * b₁) ! );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def24 defines P_sin SIN_COS:def 24 :

:: deftheorem Def25 defines P_cos SIN_COS:def 25 :

Lemma50: for b₁, b₂, b₃ being Real st b₃ <> 0 holds
( [*b₁,b₂*] / [*b₃,0*] = [*(b₁ / b₃),(b₂ / b₃)*] & [*b₁,b₂*] / [*0,b₃*] = [*(b₂ / b₃),(- (b₁ / b₃))*] )

proof end;

Lemma51: for b₁, b₂, b₃ being Real holds
( [*b₁,b₂*] * [*b₃,0*] = [*(b₁ * b₃),(b₂ * b₃)*] & [*b₁,b₂*] * [*0,b₃*] = [*(- (b₂ * b₃)),(b₁ * b₃)*] )

proof end;

theorem Th35: :: SIN_COS:35

for b₁ being Element of COMPLEX
for b₂ being Nat holds
( b₁ #N (2 * b₂) = (b₁ #N b₂) #N 2 & b₁ #N (2 * b₂) = (b₁ #N 2) #N b₂ )

proof end;

Lemma53: 1r = [*1,0*]
by ARYTM_0:def 7, COMPLEX1:def 7;

theorem Th36: :: SIN_COS:36

for b₁ being Nat
for b₂ being Real holds
( [*0,b₂*] #N (2 * b₁) = [*(((- 1) |^ b₁) * (b₂ |^ (2 * b₁))),0*] & [*0,b₂*] #N ((2 * b₁) + 1) = [*0,(((- 1) |^ b₁) * (b₂ |^ ((2 * b₁) + 1)))*] )

proof end;

theorem Th37: :: SIN_COS:37

for b₁ being Nat holds b₁ !c = [*(b₁ ! ),0*]

proof end;

theorem Th38: :: SIN_COS:38

for b₁ being Nat
for b₂ being Real holds
( (Partial_Sums (b₂ P_sin )) . b₁ = (Partial_Sums (Im ([*0,b₂*] ExpSeq ))) . ((2 * b₁) + 1) & (Partial_Sums (b₂ P_cos )) . b₁ = (Partial_Sums (Re ([*0,b₂*] ExpSeq ))) . (2 * b₁) )

proof end;

theorem Th39: :: SIN_COS:39

for b₁ being Real holds
( Partial_Sums (b₁ P_sin ) is convergent & Sum (b₁ P_sin ) = Im (Sum ([*0,b₁*] ExpSeq )) & Partial_Sums (b₁ P_cos ) is convergent & Sum (b₁ P_cos ) = Re (Sum ([*0,b₁*] ExpSeq )) )

proof end;

theorem Th40: :: SIN_COS:40

for b₁ being real number holds
( cos . b₁ = Sum (b₁ P_cos ) & sin . b₁ = Sum (b₁ P_sin ) )

proof end;

theorem Th41: :: SIN_COS:41

for b₁, b₂ being real number
for b₃ being Real_Sequence st b₃ is convergent & lim b₃ = b₂ & ( for b₄ being Nat holds b₃ . b₄ >= b₁ ) holds
b₂ >= b₁

proof end;

deffunc H₁( Real) -> Element of REAL = (2 * a₁) + 1;

consider c₁ being Real_Sequence such that
Lemma60: for b₁ being Nat holds c₁ . b₁ = H₁(b₁) from SEQ_1:sch 1();

c₁ is increasing Seq_of_Nat

proof end;

then reconsider c₂ = c₁ as increasing Seq_of_Nat ;

Lemma61: for b₁ being Nat
for b₂, b₃, b₄, b₅ being real number holds
( b₂ |^ 0 = 1 & b₂ |^ (2 * b₁) = (b₂ |^ b₁) |^ 2 & b₂ |^ 1 = b₂ & b₂ |^ 2 = b₂ * b₂ & (- 1) |^ (2 * b₁) = 1 & (- 1) |^ ((2 * b₁) + 1) = - 1 )

proof end;

Lemma62: for b₁, b₂, b₃, b₄ being Real holds
( [*b₁,b₂*] + [*b₃,b₄*] = [*(b₁ + b₃),(b₂ + b₄)*] & (5 / 6) ^2 = 25 / 36 )

proof end;

theorem Th42: :: SIN_COS:42

for b₁, b₂, b₃ being Nat st b₁ < b₂ holds
( b₃ ! > 0 & b₁ ! <= b₂ ! )

proof end;

theorem Th43: :: SIN_COS:43

for b₁ being real number
for b₂, b₃ being Nat st 0 <= b₁ & b₁ <= 1 & b₂ <= b₃ holds
b₁ |^ b₃ <= b₁ |^ b₂

proof end;

theorem Th44: :: SIN_COS:44

for b₁ being Nat
for b₂ being Real holds [*b₂,0*] #N b₁ = [*(b₂ |^ b₁),0*]

proof end;

theorem Th45: :: SIN_COS:45

for b₁ being Nat
for b₂ being Real holds ([*b₂,0*] #N b₁) / (b₁ !c ) = [*((b₂ |^ b₁) / (b₁ ! )),0*]

proof end;

theorem Th46: :: SIN_COS:46

for b₁ being Real holds Im (Sum ([*b₁,0*] ExpSeq )) = 0

proof end;

theorem Th47: :: SIN_COS:47

( cos . 1 > 0 & sin . 1 > 0 & cos . 1 < sin . 1 )

proof end;

theorem Th48: :: SIN_COS:48

for b₁ being Real holds b₁ ExpSeq = Re ([*b₁,0*] ExpSeq )

proof end;

theorem Th49: :: SIN_COS:49

for b₁ being Real holds
( b₁ ExpSeq is summable & Sum (b₁ ExpSeq ) = Re (Sum ([*b₁,0*] ExpSeq )) )

proof end;

Lemma71: for b₁ being Element of COMPLEX
for b₂ being Nat holds
( b₁ * (b₁ #N b₂) = b₁ #N (b₂ + 1) & (b₁ ExpSeq ) . 1 = b₁ & (b₁ ExpSeq ) . 0 = 1r & b₁ #N 1 = b₁ & |.(b₁ #N b₂).| = |.b₁.| |^ b₂ )

proof end;

Lemma72: for b₁ being Real holds Sum ([*b₁,0*] ExpSeq ) = [*(Sum (b₁ ExpSeq )),0*]

proof end;

theorem Th50: :: SIN_COS:50

for b₁, b₂ being real number holds Sum ((b₁ + b₂) ExpSeq ) = (Sum (b₁ ExpSeq )) * (Sum (b₂ ExpSeq ))

proof end;

definition

func exp -> PartFunc of REAL , REAL means :Def26: :: SIN_COS:def 26
( dom a₁ = REAL & ( for b₁ being real number holds a₁ . b₁ = Sum (b₁ ExpSeq ) ) );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def26 defines exp SIN_COS:def 26 :

definition

let c₃ be real number ;
func exp c₁ -> set equals :: SIN_COS:def 27
exp . a₁;
correctness ;

end;

:: deftheorem Def27 defines exp SIN_COS:def 27 :

registration

let c₃ be real number ;
cluster exp a₁ -> real ;
correctness ;

end;

definition

let c₃ be Real;
redefine func exp as exp c₁ -> Real;
correctness ;

end;

theorem Th51: :: SIN_COS:51

dom exp = REAL by Def26;

theorem Th52: :: SIN_COS:52

canceled;

theorem Th53: :: SIN_COS:53

for b₁ being Real holds exp . b₁ = Re (Sum ([*b₁,0*] ExpSeq ))

proof end;

theorem Th54: :: SIN_COS:54

for b₁ being Real holds exp [*b₁,0*] = [*(exp b₁),0*]

proof end;

Lemma77: for b₁, b₂ being real number holds exp . (b₁ + b₂) = (exp . b₁) * (exp . b₂)

proof end;

theorem Th55: :: SIN_COS:55

for b₁, b₂ being real number holds exp (b₁ + b₂) = (exp b₁) * (exp b₂) by Lemma77;

Lemma78: exp . 0 = 1

proof end;

theorem Th56: :: SIN_COS:56

exp 0 = 1 by Lemma78;

theorem Th57: :: SIN_COS:57

for b₁ being real number st b₁ > 0 holds
exp . b₁ >= 1

proof end;

theorem Th58: :: SIN_COS:58

for b₁ being real number st b₁ < 0 holds
( 0 < exp . b₁ & exp . b₁ <= 1 )

proof end;

theorem Th59: :: SIN_COS:59

for b₁ being real number holds exp . b₁ > 0

proof end;

theorem Th60: :: SIN_COS:60

for b₁ being real number holds exp b₁ > 0 by Th59;

definition

let c₃ be Element of COMPLEX ;
deffunc H₂( Nat) -> Element of COMPLEX = (c₃ #N (a₁ + 1)) / ((a₁ + 2) !c );
func c₁ P_dt -> Complex_Sequence means :Def28: :: SIN_COS:def 28
for b₁ being Nat holds a₂ . b₁ = (a₁ #N (b₁ + 1)) / ((b₁ + 2) !c );
existence

proof end;

uniqueness

proof end;

deffunc H₃( Nat) -> Element of COMPLEX = (c₃ #N a₁) / ((a₁ + 2) !c );
func c₁ P_t -> Complex_Sequence means :: SIN_COS:def 29
for b₁ being Nat holds a₂ . b₁ = (a₁ #N b₁) / ((b₁ + 2) !c );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def28 defines P_dt SIN_COS:def 28 :

:: deftheorem Def29 defines P_t SIN_COS:def 29 :

Lemma83: for b₁ being Element of COMPLEX
for b₂ being Real holds
( Re ([*0,b₂*] * b₁) = - (b₂ * (Im b₁)) & Im ([*0,b₂*] * b₁) = b₂ * (Re b₁) & Re ([*b₂,0*] * b₁) = b₂ * (Re b₁) & Im ([*b₂,0*] * b₁) = b₂ * (Im b₁) )

proof end;

Lemma84: for b₁ being Element of COMPLEX
for b₂ being Real st b₂ > 0 holds
( Re (b₁ / [*0,b₂*]) = (Im b₁) / b₂ & Im (b₁ / [*0,b₂*]) = - ((Re b₁) / b₂) & |.(b₁ / [*b₂,0*]).| = |.b₁.| / b₂ )

proof end;

theorem Th61: :: SIN_COS:61

for b₁ being Element of COMPLEX holds b₁ P_dt is absolutely_summable

proof end;

theorem Th62: :: SIN_COS:62

for b₁ being Element of COMPLEX holds b₁ * (Sum (b₁ P_dt )) = ((Sum (b₁ ExpSeq )) - 1r ) - b₁

proof end;

theorem Th63: :: SIN_COS:63

for b₁ being real number st b₁ > 0 holds
ex b₂ being Real st
( b₂ > 0 & ( for b₃ being Element of COMPLEX st |.b₃.| < b₂ holds
|.(Sum (b₃ P_dt )).| < b₁ ) )

proof end;

theorem Th64: :: SIN_COS:64

for b₁, b₂ being Element of COMPLEX holds (Sum ((b₂ + b₁) ExpSeq )) - (Sum (b₂ ExpSeq )) = ((Sum (b₂ ExpSeq )) * b₁) + ((b₁ * (Sum (b₁ P_dt ))) * (Sum (b₂ ExpSeq )))

proof end;

theorem Th65: :: SIN_COS:65

for b₁, b₂ being Real holds (cos . (b₁ + b₂)) - (cos . b₁) = (- (b₂ * (sin . b₁))) - (b₂ * (Im ((Sum ([*0,b₂*] P_dt )) * [*(cos . b₁),(sin . b₁)*])))

proof end;

theorem Th66: :: SIN_COS:66

for b₁, b₂ being Real holds (sin . (b₁ + b₂)) - (sin . b₁) = (b₂ * (cos . b₁)) + (b₂ * (Re ((Sum ([*0,b₂*] P_dt )) * [*(cos . b₁),(sin . b₁)*])))

proof end;

theorem Th67: :: SIN_COS:67

for b₁, b₂ being Real holds (exp . (b₁ + b₂)) - (exp . b₁) = (b₂ * (exp . b₁)) + ((b₂ * (exp . b₁)) * (Re (Sum ([*b₂,0*] P_dt ))))

proof end;

theorem Th68: :: SIN_COS:68

for b₁ being real number holds
( cos is_differentiable_in b₁ & diff cos ,b₁ = - (sin . b₁) )

proof end;

theorem Th69: :: SIN_COS:69

for b₁ being real number holds
( sin is_differentiable_in b₁ & diff sin ,b₁ = cos . b₁ )

proof end;

theorem Th70: :: SIN_COS:70

for b₁ being real number holds
( exp is_differentiable_in b₁ & diff exp ,b₁ = exp . b₁ )

proof end;

theorem Th71: :: SIN_COS:71

( exp is_differentiable_on REAL & ( for b₁ being real number st b₁ in REAL holds
diff exp ,b₁ = exp . b₁ ) )

proof end;

theorem Th72: :: SIN_COS:72

( cos is_differentiable_on REAL & ( for b₁ being real number st b₁ in REAL holds
diff cos ,b₁ = - (sin . b₁) ) )

proof end;

theorem Th73: :: SIN_COS:73

for b₁ being real number holds
( sin is_differentiable_on REAL & diff sin ,b₁ = cos . b₁ )

proof end;

theorem Th74: :: SIN_COS:74

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

proof end;

theorem Th75: :: SIN_COS:75

( [.0,1.] c= dom (sin / cos ) & ].0,1.[ c= dom (sin / cos ) )

proof end;

Lemma99: ( dom ((sin / cos ) | [.0,1.]) = [.0,1.] & ( for b₁ being real number st b₁ in [.0,1.] holds
((sin / cos ) | [.0,1.]) . b₁ = (sin / cos ) . b₁ ) )

proof end;

Lemma100: ( sin / cos is_differentiable_on ].0,1.[ & ( for b₁ being real number st b₁ in ].0,1.[ holds
diff (sin / cos ),b₁ > 0 ) )

proof end;

theorem Th76: :: SIN_COS:76

sin / cos is_continuous_on [.0,1.]

proof end;

theorem Th77: :: SIN_COS:77

for b₁, b₂ being real number st b₁ in ].0,1.[ & b₂ in ].0,1.[ & (sin / cos ) . b₁ = (sin / cos ) . b₂ holds
b₁ = b₂

proof end;

Lemma103: ( (sin / cos ) . 0 = 0 & (sin / cos ) . 1 > 1 )

proof end;

definition

func PI -> real number means :Def30: :: SIN_COS:def 30
( (sin / cos ) . (a₁ / 4) = 1 & a₁ in ].0,4.[ );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def30 defines PI SIN_COS:def 30 :

definition

redefine func PI as PI -> Real;
coherence by XREAL_0:def 1;

end;

theorem Th78: :: SIN_COS:78

sin . (PI / 4) = cos . (PI / 4)

proof end;

theorem Th79: :: SIN_COS:79

for b₁, b₂ being real number holds
( sin . (b₁ + b₂) = ((sin . b₁) * (cos . b₂)) + ((cos . b₁) * (sin . b₂)) & cos . (b₁ + b₂) = ((cos . b₁) * (cos . b₂)) - ((sin . b₁) * (sin . b₂)) )

proof end;

theorem Th80: :: SIN_COS:80

for b₁, b₂ being real number holds
( sin (b₁ + b₂) = ((sin b₁) * (cos b₂)) + ((cos b₁) * (sin b₂)) & cos (b₁ + b₂) = ((cos b₁) * (cos b₂)) - ((sin b₁) * (sin b₂)) ) by Th79;

theorem Th81: :: SIN_COS:81

( cos . (PI / 2) = 0 & sin . (PI / 2) = 1 & cos . PI = - 1 & sin . PI = 0 & cos . (PI + (PI / 2)) = 0 & sin . (PI + (PI / 2)) = - 1 & cos . (2 * PI ) = 1 & sin . (2 * PI ) = 0 )

proof end;

theorem Th82: :: SIN_COS:82

( cos (PI / 2) = 0 & sin (PI / 2) = 1 & cos PI = - 1 & sin PI = 0 & cos (PI + (PI / 2)) = 0 & sin (PI + (PI / 2)) = - 1 & cos (2 * PI ) = 1 & sin (2 * PI ) = 0 ) by Th81;

theorem Th83: :: SIN_COS:83

for b₁ being real number holds
( sin . (b₁ + (2 * PI )) = sin . b₁ & cos . (b₁ + (2 * PI )) = cos . b₁ & sin . ((PI / 2) - b₁) = cos . b₁ & cos . ((PI / 2) - b₁) = sin . b₁ & sin . ((PI / 2) + b₁) = cos . b₁ & cos . ((PI / 2) + b₁) = - (sin . b₁) & sin . (PI + b₁) = - (sin . b₁) & cos . (PI + b₁) = - (cos . b₁) )

proof end;

theorem Th84: :: SIN_COS:84

for b₁ being real number holds
( sin (b₁ + (2 * PI )) = sin b₁ & cos (b₁ + (2 * PI )) = cos b₁ & sin ((PI / 2) - b₁) = cos b₁ & cos ((PI / 2) - b₁) = sin b₁ & sin ((PI / 2) + b₁) = cos b₁ & cos ((PI / 2) + b₁) = - (sin b₁) & sin (PI + b₁) = - (sin b₁) & cos (PI + b₁) = - (cos b₁) ) by Th83;

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

proof end;

theorem Th85: :: SIN_COS:85

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

proof end;

theorem Th86: :: SIN_COS:86

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