:: Trigonometric Functions and Existence of Circle Ratio
:: by Yuguang Yang and Yasunari Shidama
::
:: Received October 22, 1998
:: Copyright (c) 1998-2012 Association of Mizar Users


begin

:: Some definitions and properties of complex sequence
definition
let m, k be Element of NAT ;
func CHK (m,k) ->  Element of COMPLEX  equals :Def1: :: SIN_COS:def 1
1 if m <= k
otherwise  0 ;
correctness
coherence
( ( m <= k implies 1 is Element of COMPLEX ) &amp; ( not m <= k implies 0 is Element of COMPLEX ) );
consistency
for b1 being Element of COMPLEX holds verum;
proofend;
end;

:: deftheorem Def1 defines CHK SIN_COS:def_1_:_
 for m, k being Element of NAT holds
( ( m <= k implies CHK (m,k) = 1 ) &amp; ( not m <= k implies CHK (m,k) = 0 ) );

registration
let m, k be Element of NAT ;
cluster CHK (m,k) ->  real ;
coherence
 CHK (m,k) is real by Def1;
end;

scheme :: SIN_COS:sch 1
ExComplexCASE{ F1( Nat, Nat) ->  complex number } :
 for k being Element of NAT ex seq being Complex_Sequence st
for n being Element of NAT holds
( ( n <= k implies seq . n = F1(k,n) ) &amp; ( n > k implies seq . n = 0 ) )
proofend;

scheme :: SIN_COS:sch 2
ExRealCASE{ F1( Nat, Nat) ->  real number } :
 for k being Element of NAT ex rseq being Real_Sequence st
for n being Element of NAT holds
( ( n <= k implies rseq . n = F1(k,n) ) &amp; ( n > k implies rseq . n = 0 ) )
proofend;

definition
func Prod_real_n  ->  Real_Sequence means :Def2: :: SIN_COS:def 2
( it . 0 = 1 &amp; ( for n being Element of NAT holds it . (n + 1) = (it . n) * (n + 1) ) );
existence
 ex b1 being Real_Sequence st
( b1 . 0 = 1 &amp; ( for n being Element of NAT holds b1 . (n + 1) = (b1 . n) * (n + 1) ) )
proofend;
uniqueness
 for b1, b2 being Real_Sequence st b1 . 0 = 1 &amp; ( for n being Element of NAT holds b1 . (n + 1) = (b1 . n) * (n + 1) ) &amp; b2 . 0 = 1 &amp; ( for n being Element of NAT holds b2 . (n + 1) = (b2 . n) * (n + 1) ) holds
b1 = b2
proofend;
end;

:: deftheorem Def2 defines Prod_real_n SIN_COS:def_2_:_
 for b1 being Real_Sequence holds
( b1 = Prod_real_n iff ( b1 . 0 = 1 &amp; ( for n being Element of NAT holds b1 . (n + 1) = (b1 . n) * (n + 1) ) ) );

definition
let n be Nat;
redefine func n !  equals :: SIN_COS:def 3
Prod_real_n . n;
compatibility
 for b1 being Element of REAL holds
( b1 = n ! iff b1 = Prod_real_n . n )
proofend;
end;

:: deftheorem  defines ! SIN_COS:def_3_:_
 for n being Nat holds n ! = Prod_real_n . n;

definition
let z be complex number ;
deffunc H1( Element of NAT ) ->  Element of COMPLEX = (z #N $1) / ($1 !);
funcz ExpSeq  ->  Complex_Sequence means :Def4: :: SIN_COS:def 4
 for n being Element of NAT holds it . n = (z #N n) / (n !);
existence
 ex b1 being Complex_Sequence st
for n being Element of NAT holds b1 . n = (z #N n) / (n !)
proofend;
uniqueness
 for b1, b2 being Complex_Sequence st ( for n being Element of NAT holds b1 . n = (z #N n) / (n !) ) &amp; ( for n being Element of NAT holds b2 . n = (z #N n) / (n !) ) holds
b1 = b2
proofend;
end;

:: deftheorem Def4 defines ExpSeq SIN_COS:def_4_:_
 for z being complex number
for b2 being Complex_Sequence holds
( b2 = z ExpSeq iff for n being Element of NAT holds b2 . n = (z #N n) / (n !) );

definition
let a be real number ;
deffunc H1( Element of NAT ) ->  Element of REAL = (a |^ $1) / ($1 !);
funca rExpSeq  ->  Real_Sequence means :Def5: :: SIN_COS:def 5
 for n being Element of NAT holds it . n = (a |^ n) / (n !);
existence
 ex b1 being Real_Sequence st
for n being Element of NAT holds b1 . n = (a |^ n) / (n !)
proofend;
uniqueness
 for b1, b2 being Real_Sequence st ( for n being Element of NAT holds b1 . n = (a |^ n) / (n !) ) &amp; ( for n being Element of NAT holds b2 . n = (a |^ n) / (n !) ) holds
b1 = b2
proofend;
end;

:: deftheorem Def5 defines rExpSeq SIN_COS:def_5_:_
 for a being real number
for b2 being Real_Sequence holds
( b2 = a rExpSeq iff for n being Element of NAT holds b2 . n = (a |^ n) / (n !) );

theorem Th1: :: SIN_COS:1
for n being Element of NAT holds
( 0 ! = 1 &amp; n ! <> 0 &amp; (n + 1) ! = (n !) * (n + 1) ) by Def2;

theorem Th2: :: SIN_COS:2
for k, m being Element of NAT holds
( ( 0 < k implies ((k -' 1) !) * k = k ! ) &amp; ( k <= m implies ((m -' k) !) * ((m + 1) - k) = ((m + 1) -' k) ! ) )
proofend;

definition
let n be Element of NAT ;
func Coef n ->  Complex_Sequence means :Def6: :: SIN_COS:def 6
 for k being Element of NAT holds
( ( k <= n implies it . k = (n !) / ((k !) * ((n -' k) !)) ) &amp; ( k > n implies it . k = 0 ) );
existence
 ex b1 being Complex_Sequence st
for k being Element of NAT holds
( ( k <= n implies b1 . k = (n !) / ((k !) * ((n -' k) !)) ) &amp; ( k > n implies b1 . k = 0 ) )
proofend;
uniqueness
 for b1, b2 being Complex_Sequence st ( for k being Element of NAT holds
( ( k <= n implies b1 . k = (n !) / ((k !) * ((n -' k) !)) ) &amp; ( k > n implies b1 . k = 0 ) ) ) &amp; ( for k being Element of NAT holds
( ( k <= n implies b2 . k = (n !) / ((k !) * ((n -' k) !)) ) &amp; ( k > n implies b2 . k = 0 ) ) ) holds
b1 = b2
proofend;
end;

:: deftheorem Def6 defines Coef SIN_COS:def_6_:_
 for n being Element of NAT
for b2 being Complex_Sequence holds
( b2 = Coef n iff for k being Element of NAT holds
( ( k <= n implies b2 . k = (n !) / ((k !) * ((n -' k) !)) ) &amp; ( k > n implies b2 . k = 0 ) ) );

definition
let n be Element of NAT ;
func Coef_e n ->  Complex_Sequence means :Def7: :: SIN_COS:def 7
 for k being Element of NAT holds
( ( k <= n implies it . k = 1r / ((k !) * ((n -' k) !)) ) &amp; ( k > n implies it . k = 0 ) );
existence
 ex b1 being Complex_Sequence st
for k being Element of NAT holds
( ( k <= n implies b1 . k = 1r / ((k !) * ((n -' k) !)) ) &amp; ( k > n implies b1 . k = 0 ) )
proofend;
uniqueness
 for b1, b2 being Complex_Sequence st ( for k being Element of NAT holds
( ( k <= n implies b1 . k = 1r / ((k !) * ((n -' k) !)) ) &amp; ( k > n implies b1 . k = 0 ) ) ) &amp; ( for k being Element of NAT holds
( ( k <= n implies b2 . k = 1r / ((k !) * ((n -' k) !)) ) &amp; ( k > n implies b2 . k = 0 ) ) ) holds
b1 = b2
proofend;
end;

:: deftheorem Def7 defines Coef_e SIN_COS:def_7_:_
 for n being Element of NAT
for b2 being Complex_Sequence holds
( b2 = Coef_e n iff for k being Element of NAT holds
( ( k <= n implies b2 . k = 1r / ((k !) * ((n -' k) !)) ) &amp; ( k > n implies b2 . k = 0 ) ) );

definition
let seq be Complex_Sequence;
func Shift seq ->  Complex_Sequence means :Def8: :: SIN_COS:def 8
( it . 0 = 0 &amp; ( for k being Element of NAT holds it . (k + 1) = seq . k ) );
existence
 ex b1 being Complex_Sequence st
( b1 . 0 = 0 &amp; ( for k being Element of NAT holds b1 . (k + 1) = seq . k ) )
proofend;
uniqueness
 for b1, b2 being Complex_Sequence st b1 . 0 = 0 &amp; ( for k being Element of NAT holds b1 . (k + 1) = seq . k ) &amp; b2 . 0 = 0 &amp; ( for k being Element of NAT holds b2 . (k + 1) = seq . k ) holds
b1 = b2
proofend;
end;

:: deftheorem Def8 defines Shift SIN_COS:def_8_:_
 for seq, b2 being Complex_Sequence holds
( b2 = Shift seq iff ( b2 . 0 = 0 &amp; ( for k being Element of NAT holds b2 . (k + 1) = seq . k ) ) );

definition
let n be Element of NAT ;
let z, w be Element of COMPLEX ;
func Expan (n,z,w) ->  Complex_Sequence means :Def9: :: SIN_COS:def 9
 for k being Element of NAT holds
( ( k <= n implies it . k = (((Coef n) . k) * (z |^ k)) * (w |^ (n -' k)) ) &amp; ( n < k implies it . k = 0 ) );
existence
 ex b1 being Complex_Sequence st
for k being Element of NAT holds
( ( k <= n implies b1 . k = (((Coef n) . k) * (z |^ k)) * (w |^ (n -' k)) ) &amp; ( n < k implies b1 . k = 0 ) )
proofend;
uniqueness
 for b1, b2 being Complex_Sequence st ( for k being Element of NAT holds
( ( k <= n implies b1 . k = (((Coef n) . k) * (z |^ k)) * (w |^ (n -' k)) ) &amp; ( n < k implies b1 . k = 0 ) ) ) &amp; ( for k being Element of NAT holds
( ( k <= n implies b2 . k = (((Coef n) . k) * (z |^ k)) * (w |^ (n -' k)) ) &amp; ( n < k implies b2 . k = 0 ) ) ) holds
b1 = b2
proofend;
end;

:: deftheorem Def9 defines Expan SIN_COS:def_9_:_
 for n being Element of NAT
for z, w being Element of COMPLEX
for b4 being Complex_Sequence holds
( b4 = Expan (n,z,w) iff for k being Element of NAT holds
( ( k <= n implies b4 . k = (((Coef n) . k) * (z |^ k)) * (w |^ (n -' k)) ) &amp; ( n < k implies b4 . k = 0 ) ) );

definition
let n be Element of NAT ;
let z, w be Element of COMPLEX ;
func Expan_e (n,z,w) ->  Complex_Sequence means :Def10: :: SIN_COS:def 10
 for k being Element of NAT holds
( ( k <= n implies it . k = (((Coef_e n) . k) * (z |^ k)) * (w |^ (n -' k)) ) &amp; ( n < k implies it . k = 0 ) );
existence
 ex b1 being Complex_Sequence st
for k being Element of NAT holds
( ( k <= n implies b1 . k = (((Coef_e n) . k) * (z |^ k)) * (w |^ (n -' k)) ) &amp; ( n < k implies b1 . k = 0 ) )
proofend;
uniqueness
 for b1, b2 being Complex_Sequence st ( for k being Element of NAT holds
( ( k <= n implies b1 . k = (((Coef_e n) . k) * (z |^ k)) * (w |^ (n -' k)) ) &amp; ( n < k implies b1 . k = 0 ) ) ) &amp; ( for k being Element of NAT holds
( ( k <= n implies b2 . k = (((Coef_e n) . k) * (z |^ k)) * (w |^ (n -' k)) ) &amp; ( n < k implies b2 . k = 0 ) ) ) holds
b1 = b2
proofend;
end;

:: deftheorem Def10 defines Expan_e SIN_COS:def_10_:_
 for n being Element of NAT
for z, w being Element of COMPLEX
for b4 being Complex_Sequence holds
( b4 = Expan_e (n,z,w) iff for k being Element of NAT holds
( ( k <= n implies b4 . k = (((Coef_e n) . k) * (z |^ k)) * (w |^ (n -' k)) ) &amp; ( n < k implies b4 . k = 0 ) ) );

definition
let n be Element of NAT ;
let z, w be Element of COMPLEX ;
func Alfa (n,z,w) ->  Complex_Sequence means :Def11: :: SIN_COS:def 11
 for k being Element of NAT holds
( ( k <= n implies it . k = ((z ExpSeq) . k) * ((Partial_Sums (w ExpSeq)) . (n -' k)) ) &amp; ( n < k implies it . k = 0 ) );
existence
 ex b1 being Complex_Sequence st
for k being Element of NAT holds
( ( k <= n implies b1 . k = ((z ExpSeq) . k) * ((Partial_Sums (w ExpSeq)) . (n -' k)) ) &amp; ( n < k implies b1 . k = 0 ) )
proofend;
uniqueness
 for b1, b2 being Complex_Sequence st ( for k being Element of NAT holds
( ( k <= n implies b1 . k = ((z ExpSeq) . k) * ((Partial_Sums (w ExpSeq)) . (n -' k)) ) &amp; ( n < k implies b1 . k = 0 ) ) ) &amp; ( for k being Element of NAT holds
( ( k <= n implies b2 . k = ((z ExpSeq) . k) * ((Partial_Sums (w ExpSeq)) . (n -' k)) ) &amp; ( n < k implies b2 . k = 0 ) ) ) holds
b1 = b2
proofend;
end;

:: deftheorem Def11 defines Alfa SIN_COS:def_11_:_
 for n being Element of NAT
for z, w being Element of COMPLEX
for b4 being Complex_Sequence holds
( b4 = Alfa (n,z,w) iff for k being Element of NAT holds
( ( k <= n implies b4 . k = ((z ExpSeq) . k) * ((Partial_Sums (w ExpSeq)) . (n -' k)) ) &amp; ( n < k implies b4 . k = 0 ) ) );

definition
let a, b be real number ;
let n be Element of NAT ;
func Conj (n,a,b) ->  Real_Sequence means :: SIN_COS:def 12
 for k being Element of NAT holds
( ( k <= n implies it . k = ((a rExpSeq) . k) * (((Partial_Sums (b rExpSeq)) . n) - ((Partial_Sums (b rExpSeq)) . (n -' k))) ) &amp; ( n < k implies it . k = 0 ) );
existence
 ex b1 being Real_Sequence st
for k being Element of NAT holds
( ( k <= n implies b1 . k = ((a rExpSeq) . k) * (((Partial_Sums (b rExpSeq)) . n) - ((Partial_Sums (b rExpSeq)) . (n -' k))) ) &amp; ( n < k implies b1 . k = 0 ) )
proofend;
uniqueness
 for b1, b2 being Real_Sequence st ( for k being Element of NAT holds
( ( k <= n implies b1 . k = ((a rExpSeq) . k) * (((Partial_Sums (b rExpSeq)) . n) - ((Partial_Sums (b rExpSeq)) . (n -' k))) ) &amp; ( n < k implies b1 . k = 0 ) ) ) &amp; ( for k being Element of NAT holds
( ( k <= n implies b2 . k = ((a rExpSeq) . k) * (((Partial_Sums (b rExpSeq)) . n) - ((Partial_Sums (b rExpSeq)) . (n -' k))) ) &amp; ( n < k implies b2 . k = 0 ) ) ) holds
b1 = b2
proofend;
end;

:: deftheorem  defines Conj SIN_COS:def_12_:_
 for a, b being real number
for n being Element of NAT
for b4 being Real_Sequence holds
( b4 = Conj (n,a,b) iff for k being Element of NAT holds
( ( k <= n implies b4 . k = ((a rExpSeq) . k) * (((Partial_Sums (b rExpSeq)) . n) - ((Partial_Sums (b rExpSeq)) . (n -' k))) ) &amp; ( n < k implies b4 . k = 0 ) ) );

definition
let z, w be Element of COMPLEX ;
let n be Element of NAT ;
func Conj (n,z,w) ->  Complex_Sequence means :Def13: :: SIN_COS:def 13
 for k being Element of NAT holds
( ( k <= n implies it . k = ((z ExpSeq) . k) * (((Partial_Sums (w ExpSeq)) . n) - ((Partial_Sums (w ExpSeq)) . (n -' k))) ) &amp; ( n < k implies it . k = 0 ) );
existence
 ex b1 being Complex_Sequence st
for k being Element of NAT holds
( ( k <= n implies b1 . k = ((z ExpSeq) . k) * (((Partial_Sums (w ExpSeq)) . n) - ((Partial_Sums (w ExpSeq)) . (n -' k))) ) &amp; ( n < k implies b1 . k = 0 ) )
proofend;
uniqueness
 for b1, b2 being Complex_Sequence st ( for k being Element of NAT holds
( ( k <= n implies b1 . k = ((z ExpSeq) . k) * (((Partial_Sums (w ExpSeq)) . n) - ((Partial_Sums (w ExpSeq)) . (n -' k))) ) &amp; ( n < k implies b1 . k = 0 ) ) ) &amp; ( for k being Element of NAT holds
( ( k <= n implies b2 . k = ((z ExpSeq) . k) * (((Partial_Sums (w ExpSeq)) . n) - ((Partial_Sums (w ExpSeq)) . (n -' k))) ) &amp; ( n < k implies b2 . k = 0 ) ) ) holds
b1 = b2
proofend;
end;

:: deftheorem Def13 defines Conj SIN_COS:def_13_:_
 for z, w being Element of COMPLEX
for n being Element of NAT
for b4 being Complex_Sequence holds
( b4 = Conj (n,z,w) iff for k being Element of NAT holds
( ( k <= n implies b4 . k = ((z ExpSeq) . k) * (((Partial_Sums (w ExpSeq)) . n) - ((Partial_Sums (w ExpSeq)) . (n -' k))) ) &amp; ( n < k implies b4 . k = 0 ) ) );

Lm1:  for p1, p2, g1, g2 being Element of REAL holds
( (p1 + (g1 * <i>)) * (p2 + (g2 * <i>)) = ((p1 * p2) - (g1 * g2)) + (((p1 * g2) + (p2 * g1)) * <i>) &amp; (p2 + (g2 * <i>)) *' = p2 + ((- g2) * <i>) )
proofend;

theorem Th3: :: SIN_COS:3
for n being Element of NAT
for z being complex number holds
( (z ExpSeq) . (n + 1) = (((z ExpSeq) . n) * z) / ((n + 1) + (0 * <i>)) &amp; (z ExpSeq) . 0 = 1 &amp; |.((z ExpSeq) . n).| = (|.z.| rExpSeq) . n )
proofend;

theorem Th4: :: SIN_COS:4
for k being Element of NAT
for seq being Complex_Sequence st 0 < k holds
(Shift seq) . k = seq . (k -' 1)
proofend;

theorem Th5: :: SIN_COS:5
for k being Element of NAT
for seq being Complex_Sequence holds (Partial_Sums seq) . k = ((Partial_Sums (Shift seq)) . k) + (seq . k)
proofend;

theorem Th6: :: SIN_COS:6
for z, w being Element of COMPLEX
for n being Element of NAT holds (z + w) |^ n = (Partial_Sums (Expan (n,z,w))) . n
proofend;

theorem Th7: :: SIN_COS:7
for z, w being Element of COMPLEX
for n being Element of NAT holds Expan_e (n,z,w) = (1r / (n !)) (#) (Expan (n,z,w))
proofend;

theorem Th8: :: SIN_COS:8
for z, w being Element of COMPLEX
for n being Element of NAT holds ((z + w) |^ n) / (n !) = (Partial_Sums (Expan_e (n,z,w))) . n
proofend;

theorem Th9: :: SIN_COS:9
( 0c ExpSeq is absolutely_summable &amp; Sum (0c ExpSeq) = 1r )
proofend;

registration
let z be complex number ;
clusterz ExpSeq  ->  absolutely_summable ;
coherence
 z ExpSeq is absolutely_summable
proofend;
end;

theorem Th10: :: SIN_COS:10
for z, w being Element of COMPLEX holds
( (z ExpSeq) . 0 = 1 &amp; (Expan (0,z,w)) . 0 = 1 )
proofend;

theorem Th11: :: SIN_COS:11
for z, w being Element of COMPLEX
for l, k being Element of NAT st l <= k holds
(Alfa ((k + 1),z,w)) . l = ((Alfa (k,z,w)) . l) + ((Expan_e ((k + 1),z,w)) . l)
proofend;

theorem Th12: :: SIN_COS:12
for z, w being Element of COMPLEX
for k being Element of NAT holds (Partial_Sums (Alfa ((k + 1),z,w))) . k = ((Partial_Sums (Alfa (k,z,w))) . k) + ((Partial_Sums (Expan_e ((k + 1),z,w))) . k)
proofend;

theorem Th13: :: SIN_COS:13
for z, w being Element of COMPLEX
for k being Element of NAT holds (z ExpSeq) . k = (Expan_e (k,z,w)) . k
proofend;

theorem Th14: :: SIN_COS:14
for z, w being Element of COMPLEX
for n being Element of NAT holds (Partial_Sums ((z + w) ExpSeq)) . n = (Partial_Sums (Alfa (n,z,w))) . n
proofend;

theorem Th15: :: SIN_COS:15
for z, w being Element of COMPLEX
for k being Element of NAT holds (((Partial_Sums (z ExpSeq)) . k) * ((Partial_Sums (w ExpSeq)) . k)) - ((Partial_Sums ((z + w) ExpSeq)) . k) = (Partial_Sums (Conj (k,z,w))) . k
proofend;

theorem Th16: :: SIN_COS:16
for z being Element of COMPLEX
for k being Element of NAT holds
( |.((Partial_Sums (z ExpSeq)) . k).| <= (Partial_Sums (|.z.| rExpSeq)) . k &amp; (Partial_Sums (|.z.| rExpSeq)) . k <= Sum (|.z.| rExpSeq) &amp; |.((Partial_Sums (z ExpSeq)) . k).| <= Sum (|.z.| rExpSeq) )
proofend;

theorem Th17: :: SIN_COS:17
for z being Element of COMPLEX holds 1 <= Sum (|.z.| rExpSeq)
proofend;

theorem Th18: :: SIN_COS:18
for z being Element of COMPLEX
for n being Element of NAT holds 0 <= (|.z.| rExpSeq) . n
proofend;

theorem Th19: :: SIN_COS:19
for z being Element of COMPLEX
for n, m being Element of NAT holds
( abs ((Partial_Sums (|.z.| rExpSeq)) . n) = (Partial_Sums (|.z.| rExpSeq)) . n &amp; ( n <= m implies abs (((Partial_Sums (|.z.| rExpSeq)) . m) - ((Partial_Sums (|.z.| rExpSeq)) . n)) = ((Partial_Sums (|.z.| rExpSeq)) . m) - ((Partial_Sums (|.z.| rExpSeq)) . n) ) )
proofend;

theorem Th20: :: SIN_COS:20
for z, w being Element of COMPLEX
for k, n being Element of NAT holds abs ((Partial_Sums |.(Conj (k,z,w)).|) . n) = (Partial_Sums |.(Conj (k,z,w)).|) . n
proofend;

theorem Th21: :: SIN_COS:21
for z, w being Element of COMPLEX
for p being real number st p > 0 holds
ex n being Element of NAT st
for k being Element of NAT st n <= k holds
abs ((Partial_Sums |.(Conj (k,z,w)).|) . k) < p
proofend;

theorem Th22: :: SIN_COS:22
for z, w being Element of COMPLEX
for seq being Complex_Sequence st ( for k being Element of NAT holds seq . k = (Partial_Sums (Conj (k,z,w))) . k ) holds
( seq is convergent &amp; lim seq = 0 )
proofend;

Lm2:  for z, w being complex number holds (Sum (z ExpSeq)) * (Sum (w ExpSeq)) = Sum ((z + w) ExpSeq)
proofend;

begin

definition
func exp  ->  Function of COMPLEX,COMPLEX means :Def14: :: SIN_COS:def 14
 for z being complex number holds it . z = Sum (z ExpSeq);
existence
 ex b1 being Function of COMPLEX,COMPLEX st
for z being complex number holds b1 . z = Sum (z ExpSeq)
proofend;
uniqueness
 for b1, b2 being Function of COMPLEX,COMPLEX st ( for z being complex number holds b1 . z = Sum (z ExpSeq) ) &amp; ( for z being complex number holds b2 . z = Sum (z ExpSeq) ) holds
b1 = b2
proofend;
end;

:: deftheorem Def14 defines exp SIN_COS:def_14_:_
 for b1 being Function of COMPLEX,COMPLEX holds
( b1 = exp iff for z being complex number holds b1 . z = Sum (z ExpSeq) );

definition
let z be complex number ;
func exp z ->  complex number  equals :: SIN_COS:def 15
exp . z;
coherence
 exp . z is complex number ;
end;

:: deftheorem  defines exp SIN_COS:def_15_:_
 for z being complex number holds exp z = exp . z;

definition
let z be complex number ;
:: original:exp
redefine func exp z ->  Element of COMPLEX ;
coherence
 exp z is Element of COMPLEX by XCMPLX_0:def_2;
end;

theorem :: SIN_COS:23
for z1, z2 being complex number holds exp (z1 + z2) = (exp z1) * (exp z2)
proofend;

begin

definition
func sin  ->  Function of REAL,REAL means :Def16: :: SIN_COS:def 16
 for d being Element of REAL holds it . d = Im (Sum ((d * <i>) ExpSeq));
existence
 ex b1 being Function of REAL,REAL st
for d being Element of REAL holds b1 . d = Im (Sum ((d * <i>) ExpSeq))
proofend;
uniqueness
 for b1, b2 being Function of REAL,REAL st ( for d being Element of REAL holds b1 . d = Im (Sum ((d * <i>) ExpSeq)) ) &amp; ( for d being Element of REAL holds b2 . d = Im (Sum ((d * <i>) ExpSeq)) ) holds
b1 = b2
proofend;
end;

:: deftheorem Def16 defines sin SIN_COS:def_16_:_
 for b1 being Function of REAL,REAL holds
( b1 = sin iff for d being Element of REAL holds b1 . d = Im (Sum ((d * <i>) ExpSeq)) );

definition
let th be real number ;
func sin th ->  set  equals :: SIN_COS:def 17
sin . th;
coherence
 sin . th is set ;
end;

:: deftheorem  defines sin SIN_COS:def_17_:_
 for th being real number holds sin th = sin . th;

registration
let th be real number ;
cluster sin th ->  real ;
coherence
 sin th is real ;
end;

definition
let th be Real;
:: original:sin
redefine func sin th ->  Real;
coherence
 sin th is Real ;
end;

definition
func cos  ->  Function of REAL,REAL means :Def18: :: SIN_COS:def 18
 for d being Real holds it . d = Re (Sum ((d * <i>) ExpSeq));
existence
 ex b1 being Function of REAL,REAL st
for d being Real holds b1 . d = Re (Sum ((d * <i>) ExpSeq))
proofend;
uniqueness
 for b1, b2 being Function of REAL,REAL st ( for d being Real holds b1 . d = Re (Sum ((d * <i>) ExpSeq)) ) &amp; ( for d being Real holds b2 . d = Re (Sum ((d * <i>) ExpSeq)) ) holds
b1 = b2
proofend;
end;

:: deftheorem Def18 defines cos SIN_COS:def_18_:_
 for b1 being Function of REAL,REAL holds
( b1 = cos iff for d being Real holds b1 . d = Re (Sum ((d * <i>) ExpSeq)) );

definition
let th be real number ;
func cos th ->  set  equals :: SIN_COS:def 19
cos . th;
coherence
 cos . th is set ;
end;

:: deftheorem  defines cos SIN_COS:def_19_:_
 for th being real number holds cos th = cos . th;

registration
let th be real number ;
cluster cos th ->  real ;
coherence
 cos th is real ;
end;

definition
let th be Real;
:: original:cos
redefine func cos th ->  Real;
coherence
 cos th is Real ;
end;

theorem Th24: :: SIN_COS:24
( dom sin = REAL &amp; dom cos = REAL ) by FUNCT_2:def_1;

Lm3:  for th being Real holds Sum ((th * <i>) ExpSeq) = (cos . th) + ((sin . th) * <i>)
proofend;

theorem :: SIN_COS:25
for th being Real holds exp (th * <i>) = (cos th) + ((sin th) * <i>)
proofend;

Lm4:  for th being Real holds (Sum ((th * <i>) ExpSeq)) *' = Sum ((- (th * <i>)) ExpSeq)
proofend;

theorem :: SIN_COS:26
for th being Real holds (exp (th * <i>)) *' = exp (- (th * <i>))
proofend;

Lm5:  for th being Real
for th1 being real number st th = th1 holds
( |.(Sum ((th * <i>) ExpSeq)).| = 1 &amp; abs (sin . th1) <= 1 &amp; abs (cos . th1) <= 1 )
proofend;

theorem :: SIN_COS:27
for th being Real holds
( |.(exp (th * <i>)).| = 1 &amp; ( for th being real number holds
( abs (sin th) <= 1 &amp; abs (cos th) <= 1 ) ) )
proofend;

theorem Th28: :: SIN_COS:28
for th being real number holds
( ((cos . th) ^2) + ((sin . th) ^2) = 1 &amp; ((cos . th) * (cos . th)) + ((sin . th) * (sin . th)) = 1 )
proofend;

theorem :: SIN_COS:29
for th being real number holds
( ((cos th) ^2) + ((sin th) ^2) = 1 &amp; ((cos th) * (cos th)) + ((sin th) * (sin th)) = 1 ) by Th28;

theorem Th30: :: SIN_COS:30
for th being real number holds
( cos . 0 = 1 &amp; sin . 0 = 0 &amp; cos . (- th) = cos . th &amp; sin . (- th) = - (sin . th) )
proofend;

theorem :: SIN_COS:31
for th being real number holds
( cos 0 = 1 &amp; sin 0 = 0 &amp; cos (- th) = cos th &amp; sin (- th) = - (sin th) ) by Th30;

definition
let th be real number ;
deffunc H1( Element of NAT ) ->  Element of REAL = (((- 1) |^ $1) * (th |^ ((2 * $1) + 1))) / (((2 * $1) + 1) !);
functh P_sin  ->  Real_Sequence means :Def20: :: SIN_COS:def 20
 for n being Element of NAT holds it . n = (((- 1) |^ n) * (th |^ ((2 * n) + 1))) / (((2 * n) + 1) !);
existence
 ex b1 being Real_Sequence st
for n being Element of NAT holds b1 . n = (((- 1) |^ n) * (th |^ ((2 * n) + 1))) / (((2 * n) + 1) !)
proofend;
uniqueness
 for b1, b2 being Real_Sequence st ( for n being Element of NAT holds b1 . n = (((- 1) |^ n) * (th |^ ((2 * n) + 1))) / (((2 * n) + 1) !) ) &amp; ( for n being Element of NAT holds b2 . n = (((- 1) |^ n) * (th |^ ((2 * n) + 1))) / (((2 * n) + 1) !) ) holds
b1 = b2
proofend;
deffunc H2( Element of NAT ) ->  Element of REAL = (((- 1) |^ $1) * (th |^ (2 * $1))) / ((2 * $1) !);
functh P_cos  ->  Real_Sequence means :Def21: :: SIN_COS:def 21
 for n being Element of NAT holds it . n = (((- 1) |^ n) * (th |^ (2 * n))) / ((2 * n) !);
existence
 ex b1 being Real_Sequence st
for n being Element of NAT holds b1 . n = (((- 1) |^ n) * (th |^ (2 * n))) / ((2 * n) !)
proofend;
uniqueness
 for b1, b2 being Real_Sequence st ( for n being Element of NAT holds b1 . n = (((- 1) |^ n) * (th |^ (2 * n))) / ((2 * n) !) ) &amp; ( for n being Element of NAT holds b2 . n = (((- 1) |^ n) * (th |^ (2 * n))) / ((2 * n) !) ) holds
b1 = b2
proofend;
end;

:: deftheorem Def20 defines P_sin SIN_COS:def_20_:_
 for th being real number
for b2 being Real_Sequence holds
( b2 = th P_sin iff for n being Element of NAT holds b2 . n = (((- 1) |^ n) * (th |^ ((2 * n) + 1))) / (((2 * n) + 1) !) );

:: deftheorem Def21 defines P_cos SIN_COS:def_21_:_
 for th being real number
for b2 being Real_Sequence holds
( b2 = th P_cos iff for n being Element of NAT holds b2 . n = (((- 1) |^ n) * (th |^ (2 * n))) / ((2 * n) !) );

theorem Th32: :: SIN_COS:32
for z being complex number
for k being Element of NAT holds
( z |^ (2 * k) = (z |^ k) |^ 2 &amp; z |^ (2 * k) = (z |^ 2) |^ k )
proofend;

theorem Th33: :: SIN_COS:33
for k being Element of NAT
for th being Real holds
( (th * <i>) |^ (2 * k) = ((- 1) |^ k) * (th |^ (2 * k)) &amp; (th * <i>) |^ ((2 * k) + 1) = (((- 1) |^ k) * (th |^ ((2 * k) + 1))) * <i> )
proofend;

theorem :: SIN_COS:34
for n being Element of NAT holds n ! = n ! ;

theorem Th35: :: SIN_COS:35
for n being Element of NAT
for th being Real holds
( (Partial_Sums (th P_sin)) . n = (Partial_Sums (Im ((th * <i>) ExpSeq))) . ((2 * n) + 1) &amp; (Partial_Sums (th P_cos)) . n = (Partial_Sums (Re ((th * <i>) ExpSeq))) . (2 * n) )
proofend;

theorem Th36: :: SIN_COS:36
for th being Real holds
( Partial_Sums (th P_sin) is convergent &amp; Sum (th P_sin) = Im (Sum ((th * <i>) ExpSeq)) &amp; Partial_Sums (th P_cos) is convergent &amp; Sum (th P_cos) = Re (Sum ((th * <i>) ExpSeq)) )
proofend;

theorem Th37: :: SIN_COS:37
for th being real number holds
( cos . th = Sum (th P_cos) &amp; sin . th = Sum (th P_sin) )
proofend;

theorem :: SIN_COS:38
for p, th being real number
for rseq being Real_Sequence st rseq is convergent &amp; lim rseq = th &amp; ( for n being Element of NAT holds rseq . n >= p ) holds
th >= p by PREPOWER:1;

deffunc H1( Real) ->  Element of REAL = (2 * $1) + 1;

consider bq being Real_Sequence such that
Lm6:  for n being Element of NAT holds bq . n = H1(n) from SEQ_1:sch_1();

 bq is increasing sequence of NAT
proofend;

then reconsider bq = bq as increasing sequence of NAT ;

Lm7:  for n being Element of NAT
for th, th1, th2, th3 being real number holds
( th |^ (2 * n) = (th |^ n) |^ 2 &amp; (- 1) |^ (2 * n) = 1 &amp; (- 1) |^ ((2 * n) + 1) = - 1 )
proofend;

theorem Th39: :: SIN_COS:39
for n, k being Element of NAT st n <= k holds
n ! <= k !
proofend;

theorem Th40: :: SIN_COS:40
for n, k being Element of NAT
for th being real number st 0 <= th &amp; th <= 1 &amp; n <= k holds
th |^ k <= th |^ n
proofend;

theorem :: SIN_COS:41
for n being Element of NAT
for th being Real holds (th |^ n) / (n !) = (th |^ n) / (n !) ;

theorem Th42: :: SIN_COS:42
for p being real number holds Im (Sum (p ExpSeq)) = 0
proofend;

theorem Th43: :: SIN_COS:43
( cos . 1 > 0 &amp; sin . 1 > 0 &amp; cos . 1 < sin . 1 )
proofend;

theorem Th44: :: SIN_COS:44
for th being Real holds th rExpSeq = Re (th ExpSeq)
proofend;

theorem Th45: :: SIN_COS:45
for th being Real holds
( th rExpSeq is summable &amp; Sum (th rExpSeq) = Re (Sum (th ExpSeq)) )
proofend;

Lm8:  for n being Element of NAT
for z being complex number holds
( (z ExpSeq) . 1 = z &amp; (z ExpSeq) . 0 = 1r &amp; |.(z |^ n).| = |.z.| |^ n )
proofend;

Lm9:  for th being Real holds Sum (th ExpSeq) = Sum (th rExpSeq)
proofend;

theorem Th46: :: SIN_COS:46
for p, q being real number holds Sum ((p + q) rExpSeq) = (Sum (p rExpSeq)) * (Sum (q rExpSeq))
proofend;

definition
func exp_R  ->  Function of REAL,REAL means :Def22: :: SIN_COS:def 22
 for d being real number holds it . d = Sum (d rExpSeq);
existence
 ex b1 being Function of REAL,REAL st
for d being real number holds b1 . d = Sum (d rExpSeq)
proofend;
uniqueness
 for b1, b2 being Function of REAL,REAL st ( for d being real number holds b1 . d = Sum (d rExpSeq) ) &amp; ( for d being real number holds b2 . d = Sum (d rExpSeq) ) holds
b1 = b2
proofend;
end;

:: deftheorem Def22 defines exp_R SIN_COS:def_22_:_
 for b1 being Function of REAL,REAL holds
( b1 = exp_R iff for d being real number holds b1 . d = Sum (d rExpSeq) );

definition
let th be real number ;
func exp_R th ->  set  equals :: SIN_COS:def 23
exp_R . th;
coherence
 exp_R . th is set ;
end;

:: deftheorem  defines exp_R SIN_COS:def_23_:_
 for th being real number holds exp_R th = exp_R . th;

registration
let th be real number ;
cluster exp_R th ->  real ;
coherence
 exp_R th is real ;
end;

definition
let th be Real;
:: original:exp_R
redefine func exp_R th ->  Real;
coherence
 exp_R th is Real ;
end;

theorem Th47: :: SIN_COS:47
dom exp_R = REAL by FUNCT_2:def_1;

theorem Th48: :: SIN_COS:48
for th being Real holds exp_R . th = Re (Sum (th ExpSeq))
proofend;

theorem :: SIN_COS:49
for th being Real holds exp th = exp_R th
proofend;

Lm10:  for p, q being real number holds exp_R . (p + q) = (exp_R . p) * (exp_R . q)
proofend;

theorem :: SIN_COS:50
for p, q being real number holds exp_R (p + q) = (exp_R p) * (exp_R q) by Lm10;

Lm11:  exp_R . 0 = 1
proofend;

theorem :: SIN_COS:51
exp_R 0 = 1 by Lm11;

theorem Th52: :: SIN_COS:52
for th being real number st th > 0 holds
exp_R . th >= 1
proofend;

theorem Th53: :: SIN_COS:53
for th being real number st th < 0 holds
( 0 < exp_R . th &amp; exp_R . th <= 1 )
proofend;

theorem Th54: :: SIN_COS:54
for th being real number holds exp_R . th > 0
proofend;

theorem :: SIN_COS:55
for th being real number holds exp_R th > 0 by Th54;

begin

definition
let z be complex number ;
deffunc H2( Element of NAT ) ->  Element of COMPLEX = (z #N ($1 + 1)) / (($1 + 2) !);
funcz P_dt  ->  Complex_Sequence means :Def24: :: SIN_COS:def 24
 for n being Element of NAT holds it . n = (z |^ (n + 1)) / ((n + 2) !);
existence
 ex b1 being Complex_Sequence st
for n being Element of NAT holds b1 . n = (z |^ (n + 1)) / ((n + 2) !)
proofend;
uniqueness
 for b1, b2 being Complex_Sequence st ( for n being Element of NAT holds b1 . n = (z |^ (n + 1)) / ((n + 2) !) ) &amp; ( for n being Element of NAT holds b2 . n = (z |^ (n + 1)) / ((n + 2) !) ) holds
b1 = b2
proofend;
deffunc H3( Element of NAT ) ->  Element of COMPLEX = (z #N $1) / (($1 + 2) !);
funcz P_t  ->  Complex_Sequence means :: SIN_COS:def 25
 for n being Element of NAT holds it . n = (z #N n) / ((n + 2) !);
existence
 ex b1 being Complex_Sequence st
for n being Element of NAT holds b1 . n = (z #N n) / ((n + 2) !)
proofend;
uniqueness
 for b1, b2 being Complex_Sequence st ( for n being Element of NAT holds b1 . n = (z #N n) / ((n + 2) !) ) &amp; ( for n being Element of NAT holds b2 . n = (z #N n) / ((n + 2) !) ) holds
b1 = b2
proofend;
end;

:: deftheorem Def24 defines P_dt SIN_COS:def_24_:_
 for z being complex number
for b2 being Complex_Sequence holds
( b2 = z P_dt iff for n being Element of NAT holds b2 . n = (z |^ (n + 1)) / ((n + 2) !) );

:: deftheorem  defines P_t SIN_COS:def_25_:_
 for z being complex number
for b2 being Complex_Sequence holds
( b2 = z P_t iff for n being Element of NAT holds b2 . n = (z #N n) / ((n + 2) !) );

Lm12:  for p being Real
for z being complex number holds
( Re ((p * <i>) * z) = - (p * (Im z)) &amp; Im ((p * <i>) * z) = p * (Re z) &amp; Re (p * z) = p * (Re z) &amp; Im (p * z) = p * (Im z) )
proofend;

Lm13:  for p being real number
for z being complex number st p > 0 holds
( Re (z / (p * <i>)) = (Im z) / p &amp; Im (z / (p * <i>)) = - ((Re z) / p) &amp; |.(z / p).| = |.z.| / p )
proofend;

theorem Th56: :: SIN_COS:56
for z being complex number holds z P_dt is absolutely_summable
proofend;

theorem Th57: :: SIN_COS:57
for z being complex number holds z * (Sum (z P_dt)) = ((Sum (z ExpSeq)) - 1r) - z
proofend;

theorem Th58: :: SIN_COS:58
for p being real number st p > 0 holds
ex q being Real st
( q > 0 &amp; ( for z being complex number st |.z.| < q holds
|.(Sum (z P_dt)).| < p ) )
proofend;

theorem Th59: :: SIN_COS:59
for z, z1 being complex number holds (Sum ((z1 + z) ExpSeq)) - (Sum (z1 ExpSeq)) = ((Sum (z1 ExpSeq)) * z) + ((z * (Sum (z P_dt))) * (Sum (z1 ExpSeq)))
proofend;

theorem Th60: :: SIN_COS:60
for p, q being Real holds (cos . (p + q)) - (cos . p) = (- (q * (sin . p))) - (q * (Im ((Sum ((q * <i>) P_dt)) * ((cos . p) + ((sin . p) * <i>)))))
proofend;

theorem Th61: :: SIN_COS:61
for p, q being Real holds (sin . (p + q)) - (sin . p) = (q * (cos . p)) + (q * (Re ((Sum ((q * <i>) P_dt)) * ((cos . p) + ((sin . p) * <i>)))))
proofend;

theorem Th62: :: SIN_COS:62
for p, q being Real holds (exp_R . (p + q)) - (exp_R . p) = (q * (exp_R . p)) + ((q * (exp_R . p)) * (Re (Sum (q P_dt))))
proofend;

theorem Th63: :: SIN_COS:63
for p being real number holds
( cos is_differentiable_in p &amp; diff (cos,p) = - (sin . p) )
proofend;

theorem Th64: :: SIN_COS:64
for p being real number holds
( sin is_differentiable_in p &amp; diff (sin,p) = cos . p )
proofend;

theorem Th65: :: SIN_COS:65
for p being real number holds
( exp_R is_differentiable_in p &amp; diff (exp_R,p) = exp_R . p )
proofend;

theorem Th66: :: SIN_COS:66
for th being real number holds
( exp_R is_differentiable_on REAL &amp; diff (exp_R,th) = exp_R . th )
proofend;

theorem Th67: :: SIN_COS:67
for th being real number holds
( cos is_differentiable_on REAL &amp; diff (cos,th) = - (sin . th) )
proofend;

theorem Th68: :: SIN_COS:68
for th being real number holds
( sin is_differentiable_on REAL &amp; diff (sin,th) = cos . th )
proofend;

theorem Th69: :: SIN_COS:69
for th being real number st th in [.0,1.] holds
( 0 < cos . th &amp; cos . th >= 1 / 2 )
proofend;

definition
func tan  ->  PartFunc of REAL,REAL equals :: SIN_COS:def 26
sin / cos;
coherence
 sin / cos is PartFunc of REAL,REAL ;
func cot  ->  PartFunc of REAL,REAL equals :: SIN_COS:def 27
cos / sin;
coherence
 cos / sin is PartFunc of REAL,REAL ;
end;

:: deftheorem  defines tan SIN_COS:def_26_:_
 tan = sin / cos;

:: deftheorem  defines cot SIN_COS:def_27_:_
 cot = cos / sin;

theorem Th70: :: SIN_COS:70
( [.0,1.] c= dom tan &amp; ].0,1.[ c= dom tan )
proofend;

Lm14:  ( dom (tan | [.0,1.]) = [.0,1.] &amp; ( for th being real number st th in [.0,1.] holds
(tan | [.0,1.]) . th = tan . th ) )
proofend;

Lm15:  ( tan is_differentiable_on ].0,1.[ &amp; ( for th being real number st th in ].0,1.[ holds
diff (tan,th) > 0 ) )
proofend;

theorem Th71: :: SIN_COS:71
tan | [.0,1.] is continuous
proofend;

theorem Th72: :: SIN_COS:72
for th1, th2 being real number st th1 in ].0,1.[ &amp; th2 in ].0,1.[ &amp; tan . th1 = tan . th2 holds
th1 = th2
proofend;

Lm16:  ( tan . 0 = 0 &amp; tan . 1 > 1 )
proofend;

begin

definition
func PI  ->  real number  means :Def28: :: SIN_COS:def 28
( tan . (it / 4) = 1 &amp; it in ].0,4.[ );
existence
 ex b1 being real number st
( tan . (b1 / 4) = 1 &amp; b1 in ].0,4.[ )
proofend;
uniqueness
 for b1, b2 being real number st tan . (b1 / 4) = 1 &amp; b1 in ].0,4.[ &amp; tan . (b2 / 4) = 1 &amp; b2 in ].0,4.[ holds
b1 = b2
proofend;
end;

:: deftheorem Def28 defines PI SIN_COS:def_28_:_
 for b1 being real number holds
( b1 = PI iff ( tan . (b1 / 4) = 1 &amp; b1 in ].0,4.[ ) );

definition
:: original:PI
redefine func PI  ->  Real;
coherence
 PI is Real by XREAL_0:def_1;
end;

theorem Th73: :: SIN_COS:73
sin . (PI / 4) = cos . (PI / 4)
proofend;

begin

theorem Th74: :: SIN_COS:74
for th1, th2 being real number holds
( sin . (th1 + th2) = ((sin . th1) * (cos . th2)) + ((cos . th1) * (sin . th2)) &amp; cos . (th1 + th2) = ((cos . th1) * (cos . th2)) - ((sin . th1) * (sin . th2)) )
proofend;

theorem :: SIN_COS:75
for th1, th2 being real number holds
( sin (th1 + th2) = ((sin th1) * (cos th2)) + ((cos th1) * (sin th2)) &amp; cos (th1 + th2) = ((cos th1) * (cos th2)) - ((sin th1) * (sin th2)) ) by Th74;

theorem Th76: :: SIN_COS:76
( cos . (PI / 2) = 0 &amp; sin . (PI / 2) = 1 &amp; cos . PI = - 1 &amp; sin . PI = 0 &amp; cos . (PI + (PI / 2)) = 0 &amp; sin . (PI + (PI / 2)) = - 1 &amp; cos . (2 * PI) = 1 &amp; sin . (2 * PI) = 0 )
proofend;

theorem :: SIN_COS:77
( cos (PI / 2) = 0 &amp; sin (PI / 2) = 1 &amp; cos PI = - 1 &amp; sin PI = 0 &amp; cos (PI + (PI / 2)) = 0 &amp; sin (PI + (PI / 2)) = - 1 &amp; cos (2 * PI) = 1 &amp; sin (2 * PI) = 0 ) by Th76;

theorem Th78: :: SIN_COS:78
for th being real number holds
( sin . (th + (2 * PI)) = sin . th &amp; cos . (th + (2 * PI)) = cos . th &amp; sin . ((PI / 2) - th) = cos . th &amp; cos . ((PI / 2) - th) = sin . th &amp; sin . ((PI / 2) + th) = cos . th &amp; cos . ((PI / 2) + th) = - (sin . th) &amp; sin . (PI + th) = - (sin . th) &amp; cos . (PI + th) = - (cos . th) )
proofend;

theorem :: SIN_COS:79
for th being real number holds
( sin (th + (2 * PI)) = sin th &amp; cos (th + (2 * PI)) = cos th &amp; sin ((PI / 2) - th) = cos th &amp; cos ((PI / 2) - th) = sin th &amp; sin ((PI / 2) + th) = cos th &amp; cos ((PI / 2) + th) = - (sin th) &amp; sin (PI + th) = - (sin th) &amp; cos (PI + th) = - (cos th) ) by Th78;

Lm17:  for th being real number st th in [.0,1.] holds
sin . th >= 0
proofend;

theorem Th80: :: SIN_COS:80
for th being real number st th in ].0,(PI / 2).[ holds
cos . th > 0
proofend;

theorem :: SIN_COS:81
for th being real number st th in ].0,(PI / 2).[ holds
cos th > 0 by Th80;

begin

:: from COMPLEX2, 2006.03,06, A.T.
theorem :: SIN_COS:82
for a, b being real number holds sin (a - b) = ((sin a) * (cos b)) - ((cos a) * (sin b))
proofend;

theorem :: SIN_COS:83
for a, b being real number holds cos (a - b) = ((cos a) * (cos b)) + ((sin a) * (sin b))
proofend;

registration
cluster sin  ->  continuous ;
coherence
 sin is continuous
proofend;
cluster cos  ->  continuous ;
coherence
 cos is continuous
proofend;
cluster exp_R  ->  continuous ;
coherence
 exp_R is continuous
proofend;
end;