SIN_COS: Trigonometric Functions and Existence of Circle Ratio

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

begin

definition

let m, k be Element of NAT ;
canceled;
func CHK (m,k) -> Element of COMPLEX equals :Def2: :: SIN_COS:def 2
1 if m <= k
otherwise 0 ;
correctness

proof end;

end;

:: deftheorem SIN_COS:def 1 :

:: deftheorem Def2 defines CHK SIN_COS:def 2 :

registration

let m, k be Element of NAT ;
cluster CHK (m,k) -> real ;
coherence by Def2;

end;

scheme :: SIN_COS:sch 1
ExComplexCASE{ F₁( 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 = F₁(k,n) ) & ( n > k implies seq . n = 0 ) )

proof end;

scheme :: SIN_COS:sch 2
ExRealCASE{ F₁( 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 = F₁(k,n) ) & ( n > k implies rseq . n = 0 ) )

proof end;

definition

let x be Element of COMPLEX ;
let c be complex number ;
:: original: *
redefine func x * c -> Element of COMPLEX ;
coherence by XCMPLX_0:def 2;

end;

definition

canceled;
canceled;
func Prod_real_n -> Real_Sequence means :Def5: :: SIN_COS:def 5
( it . 0 = 1 & ( for n being Element of NAT holds it . (n + 1) = (it . n) * (n + 1) ) );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem SIN_COS:def 3 :

:: deftheorem SIN_COS:def 4 :

:: deftheorem Def5 defines Prod_real_n SIN_COS:def 5 :

definition

canceled;
let n be Nat;
redefine func n ! equals :: SIN_COS:def 7
Prod_real_n . n;
compatibility

proof end;

end;

:: deftheorem SIN_COS:def 6 :

:: deftheorem defines ! SIN_COS:def 7 :

definition

let z be complex number ;
deffunc H₁( Element of NAT ) -> Element of COMPLEX = (z #N $1) / ($1 !);
func z ExpSeq -> Complex_Sequence means :Def8: :: SIN_COS:def 8
for n being Element of NAT holds it . n = (z #N n) / (n !);
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def8 defines ExpSeq SIN_COS:def 8 :

definition

let a be real number ;
deffunc H₁( Element of NAT ) -> Element of REAL = (a |^ $1) / ($1 !);
func a rExpSeq -> Real_Sequence means :Def9: :: SIN_COS:def 9
for n being Element of NAT holds it . n = (a |^ n) / (n !);
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def9 defines rExpSeq SIN_COS:def 9 :

theorem Th1: :: SIN_COS:1

for n being Element of NAT holds
( 0 ! = 1 & n ! <> 0 & (n + 1) ! = (n !) * (n + 1) ) by Def5;

theorem :: SIN_COS:2

canceled;

theorem Th3: :: SIN_COS:3

for k, m being Element of NAT holds
( ( 0 < k implies ((k -' 1) !) * k = k ! ) & ( k <= m implies ((m -' k) !) * ((m + 1) - k) = ((m + 1) -' k) ! ) )

proof end;

definition

let n be Element of NAT ;
func Coef n -> Complex_Sequence means :Def10: :: SIN_COS:def 10
for k being Element of NAT holds
( ( k <= n implies it . k = (n !) / ((k !) * ((n -' k) !)) ) & ( k > n implies it . k = 0 ) );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def10 defines Coef SIN_COS:def 10 :

definition

let n be Element of NAT ;
func Coef_e n -> Complex_Sequence means :Def11: :: SIN_COS:def 11
for k being Element of NAT holds
( ( k <= n implies it . k = 1r / ((k !) * ((n -' k) !)) ) & ( k > n implies it . k = 0 ) );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def11 defines Coef_e SIN_COS:def 11 :

definition

let seq be Complex_Sequence;
func Shift seq -> Complex_Sequence means :Def12: :: SIN_COS:def 12
( it . 0 = 0 & ( for k being Element of NAT holds it . (k + 1) = seq . k ) );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def12 defines Shift SIN_COS:def 12 :

definition

let n be Element of NAT ;
let z, w be Element of COMPLEX ;
func Expan (n,z,w) -> Complex_Sequence means :Def13: :: SIN_COS:def 13
for k being Element of NAT holds
( ( k <= n implies it . k = (((Coef n) . k) * (z |^ k)) * (w |^ (n -' k)) ) & ( n < k implies it . k = 0 ) );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def13 defines Expan SIN_COS:def 13 :

definition

let n be Element of NAT ;
let z, w be Element of COMPLEX ;
func Expan_e (n,z,w) -> Complex_Sequence means :Def14: :: SIN_COS:def 14
for k being Element of NAT holds
( ( k <= n implies it . k = (((Coef_e n) . k) * (z |^ k)) * (w |^ (n -' k)) ) & ( n < k implies it . k = 0 ) );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def14 defines Expan_e SIN_COS:def 14 :

definition

let n be Element of NAT ;
let z, w be Element of COMPLEX ;
func Alfa (n,z,w) -> Complex_Sequence means :Def15: :: SIN_COS:def 15
for k being Element of NAT holds
( ( k <= n implies it . k = ((z ExpSeq) . k) * ((Partial_Sums (w ExpSeq)) . (n -' k)) ) & ( n < k implies it . k = 0 ) );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def15 defines Alfa SIN_COS:def 15 :

definition

let a, b be real number ;
let n be Element of NAT ;
func Conj (n,a,b) -> Real_Sequence means :: SIN_COS:def 16
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))) ) & ( n < k implies it . k = 0 ) );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem defines Conj SIN_COS:def 16 :

definition

let z, w be Element of COMPLEX ;
let n be Element of NAT ;
func Conj (n,z,w) -> Complex_Sequence means :Def17: :: SIN_COS:def 17
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))) ) & ( n < k implies it . k = 0 ) );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def17 defines Conj SIN_COS:def 17 :

Lm1: for p1, p2, g1, g2 being Element of REAL holds
( (p1 + (g1 * )) * (p2 + (g2 * )) = ((p1 * p2) - (g1 * g2)) + (((p1 * g2) + (p2 * g1)) * ) & (p2 + (g2 * )) *' = p2 + ((- g2) * ) )

proof end;

theorem Th4: :: SIN_COS:4

for n being Element of NAT
for z being complex number holds
( (z ExpSeq) . (n + 1) = (((z ExpSeq) . n) * z) / ((n + 1) + (0 * )) & (z ExpSeq) . 0 = 1 & |.((z ExpSeq) . n).| = (|.z.| rExpSeq) . n )

proof end;

theorem Th5: :: SIN_COS:5

for k being Element of NAT
for seq being Complex_Sequence st 0 < k holds
(Shift seq) . k = seq . (k -' 1)

proof end;

theorem Th6: :: SIN_COS:6

for k being Element of NAT
for seq being Complex_Sequence holds (Partial_Sums seq) . k = ((Partial_Sums (Shift seq)) . k) + (seq . k)

proof end;

theorem Th7: :: SIN_COS:7

for z, w being Element of COMPLEX
for n being Element of NAT holds (z + w) |^ n = (Partial_Sums (Expan (n,z,w))) . n

proof end;

theorem Th8: :: SIN_COS:8

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

proof end;

theorem Th9: :: SIN_COS:9

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

proof end;

theorem Th10: :: SIN_COS:10

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

proof end;

registration

let z be complex number ;
cluster z ExpSeq -> absolutely_summable ;
coherence

proof end;

end;

theorem Th11: :: SIN_COS:11

for z, w being Element of COMPLEX holds
( (z ExpSeq) . 0 = 1 & (Expan (0,z,w)) . 0 = 1 )

proof end;

theorem Th12: :: SIN_COS:12

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)

proof end;

theorem Th13: :: SIN_COS:13

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)

proof end;

theorem Th14: :: SIN_COS:14

for z, w being Element of COMPLEX
for k being Element of NAT holds (z ExpSeq) . k = (Expan_e (k,z,w)) . k

proof end;

theorem Th15: :: SIN_COS:15

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

proof end;

theorem Th16: :: SIN_COS:16

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

proof end;

theorem Th17: :: SIN_COS:17

proof end;

theorem Th18: :: SIN_COS:18

for z being Element of COMPLEX holds 1 <= Sum (|.z.| rExpSeq)

proof end;

theorem Th19: :: SIN_COS:19

for z being Element of COMPLEX
for n being Element of NAT holds 0 <= (|.z.| rExpSeq) . n

proof end;

theorem Th20: :: SIN_COS:20

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 & ( n <= m implies abs (((Partial_Sums (|.z.| rExpSeq)) . m) - ((Partial_Sums (|.z.| rExpSeq)) . n)) = ((Partial_Sums (|.z.| rExpSeq)) . m) - ((Partial_Sums (|.z.| rExpSeq)) . n) ) )

proof end;

theorem Th21: :: SIN_COS:21

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

proof end;

theorem Th22: :: SIN_COS:22

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

proof end;

theorem Th23: :: SIN_COS:23

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 & lim seq = 0 )

proof end;

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

proof end;

begin

definition

func exp -> Function of COMPLEX,COMPLEX means :Def18: :: SIN_COS:def 18
for z being complex number holds it . z = Sum (z ExpSeq);
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def18 defines exp SIN_COS:def 18 :

definition

let z be complex number ;
func exp z -> complex number equals :: SIN_COS:def 19
exp . z;
coherence ;

end;

:: deftheorem defines exp SIN_COS:def 19 :

definition

let z be complex number ;
:: original: exp
redefine func exp z -> Element of COMPLEX ;
coherence by XCMPLX_0:def 2;

end;

theorem :: SIN_COS:24

for z1, z2 being complex number holds exp (z1 + z2) = (exp z1) * (exp z2)

proof end;

begin

definition

func sin -> Function of REAL,REAL means :Def20: :: SIN_COS:def 20
for d being Element of REAL holds it . d = Im (Sum ((d * ) ExpSeq));
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def20 defines sin SIN_COS:def 20 :

definition

let th be real number ;
func sin th -> set equals :: SIN_COS:def 21
sin . th;
coherence ;

end;

:: deftheorem defines sin SIN_COS:def 21 :

registration

let th be real number ;
cluster sin th -> real ;
coherence ;

end;

definition

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

end;

definition

func cos -> Function of REAL,REAL means :Def22: :: SIN_COS:def 22
for d being Real holds it . d = Re (Sum ((d * ) ExpSeq));
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def22 defines cos SIN_COS:def 22 :

definition

let th be real number ;
func cos th -> set equals :: SIN_COS:def 23
cos . th;
coherence ;

end;

:: deftheorem defines cos SIN_COS:def 23 :

registration

let th be real number ;
cluster cos th -> real ;
coherence ;

end;

definition

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

end;

theorem :: SIN_COS:25

canceled;

theorem :: SIN_COS:26

canceled;

theorem Th27: :: SIN_COS:27

( dom sin = REAL & dom cos = REAL ) by FUNCT_2:def 1;

Lm3: for th being Real holds Sum ((th * ) ExpSeq) = (cos . th) + ((sin . th) * )

proof end;

theorem :: SIN_COS:28

for th being Real holds exp (th * ) = (cos th) + ((sin th) * )

proof end;

Lm4: for th being Real holds (Sum ((th * ) ExpSeq)) *' = Sum ((- (th * )) ExpSeq)

proof end;

theorem :: SIN_COS:29

for th being Real holds (exp (th * )) *' = exp (- (th * ))

proof end;

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

proof end;

theorem :: SIN_COS:30

for th being Real holds
( |.(exp (th * )).| = 1 & ( for th being real number holds
( abs (sin th) <= 1 & abs (cos th) <= 1 ) ) )

proof end;

theorem Th31: :: SIN_COS:31

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

proof end;

theorem :: SIN_COS:32

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

theorem Th33: :: SIN_COS:33

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

proof end;

theorem :: SIN_COS:34

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

definition

let th be real number ;
deffunc H₁( Element of NAT ) -> Element of REAL = (((- 1) |^ $1) * (th |^ ((2 * $1) + 1))) / (((2 * $1) + 1) !);
func th P_sin -> Real_Sequence means :Def24: :: SIN_COS:def 24
for n being Element of NAT holds it . n = (((- 1) |^ n) * (th |^ ((2 * n) + 1))) / (((2 * n) + 1) !);
existence

proof end;

uniqueness

proof end;

deffunc H₂( Element of NAT ) -> Element of REAL = (((- 1) |^ $1) * (th |^ (2 * $1))) / ((2 * $1) !);
func th P_cos -> Real_Sequence means :Def25: :: SIN_COS:def 25
for n being Element of NAT holds it . n = (((- 1) |^ n) * (th |^ (2 * n))) / ((2 * n) !);
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 :

theorem Th35: :: SIN_COS:35

for z being complex number
for k being Element of NAT holds
( z |^ (2 * k) = (z |^ k) |^ 2 & z |^ (2 * k) = (z |^ 2) |^ k )

proof end;

theorem Th36: :: SIN_COS:36

for k being Element of NAT
for th being Real holds
( (th * ) |^ (2 * k) = ((- 1) |^ k) * (th |^ (2 * k)) & (th * ) |^ ((2 * k) + 1) = (((- 1) |^ k) * (th |^ ((2 * k) + 1))) * )

proof end;

theorem :: SIN_COS:37

for n being Element of NAT holds n ! = n ! ;

theorem Th38: :: SIN_COS:38

for n being Element of NAT
for th being Real holds
( (Partial_Sums (th P_sin)) . n = (Partial_Sums (Im ((th * ) ExpSeq))) . ((2 * n) + 1) & (Partial_Sums (th P_cos)) . n = (Partial_Sums (Re ((th * ) ExpSeq))) . (2 * n) )

proof end;

theorem Th39: :: SIN_COS:39

for th being Real holds
( Partial_Sums (th P_sin) is convergent & Sum (th P_sin) = Im (Sum ((th * ) ExpSeq)) & Partial_Sums (th P_cos) is convergent & Sum (th P_cos) = Re (Sum ((th * ) ExpSeq)) )

proof end;

theorem Th40: :: SIN_COS:40

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

proof end;

theorem :: SIN_COS:41

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

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

consider bq being Real_Sequence such that
Lm6: for n being Element of NAT holds bq . n = H₁(n) from SEQ_1:sch 1();

bq is increasing sequence of NAT

proof end;

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 & (- 1) |^ (2 * n) = 1 & (- 1) |^ ((2 * n) + 1) = - 1 )

proof end;

theorem Th42: :: SIN_COS:42

for n, k being Element of NAT st n <= k holds
n ! <= k !

proof end;

theorem Th43: :: SIN_COS:43

for n, k being Element of NAT
for th being real number st 0 <= th & th <= 1 & n <= k holds
th |^ k <= th |^ n

proof end;

theorem :: SIN_COS:44

canceled;

theorem :: SIN_COS:45

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

theorem Th46: :: SIN_COS:46

for p being real number holds Im (Sum (p 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 th being Real holds th rExpSeq = Re (th ExpSeq)

proof end;

theorem Th49: :: SIN_COS:49

for th being Real holds
( th rExpSeq is summable & Sum (th rExpSeq) = Re (Sum (th ExpSeq)) )

proof end;

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

proof end;

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

proof end;

theorem Th50: :: SIN_COS:50

for p, q being real number holds Sum ((p + q) rExpSeq) = (Sum (p rExpSeq)) * (Sum (q rExpSeq))

proof end;

definition

func exp_R -> Function of REAL,REAL means :Def26: :: SIN_COS:def 26
for d being real number holds it . d = Sum (d rExpSeq);
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def26 defines exp_R SIN_COS:def 26 :

definition

let th be real number ;
func exp_R th -> set equals :: SIN_COS:def 27
exp_R . th;
coherence ;

end;

:: deftheorem defines exp_R SIN_COS:def 27 :

registration

let th be real number ;
cluster exp_R th -> real ;
coherence ;

end;

definition

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

end;

theorem Th51: :: SIN_COS:51

dom exp_R = REAL by FUNCT_2:def 1;

theorem :: SIN_COS:52

canceled;

theorem Th53: :: SIN_COS:53

for th being Real holds exp_R . th = Re (Sum (th ExpSeq))

proof end;

theorem :: SIN_COS:54

for th being Real holds exp th = exp_R th

proof end;

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

proof end;

theorem :: SIN_COS:55

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

Lm11: exp_R . 0 = 1

proof end;

theorem :: SIN_COS:56

exp_R 0 = 1 by Lm11;

theorem Th57: :: SIN_COS:57

for th being real number st th > 0 holds
exp_R . th >= 1

proof end;

theorem Th58: :: SIN_COS:58

for th being real number st th < 0 holds
( 0 < exp_R . th & exp_R . th <= 1 )

proof end;

theorem Th59: :: SIN_COS:59

for th being real number holds exp_R . th > 0

proof end;

theorem :: SIN_COS:60

for th being real number holds exp_R th > 0 by Th59;

begin

definition

let z be complex number ;
deffunc H₂( Element of NAT ) -> Element of COMPLEX = (z #N ($1 + 1)) / (($1 + 2) !);
func z P_dt -> Complex_Sequence means :Def28: :: SIN_COS:def 28
for n being Element of NAT holds it . n = (z |^ (n + 1)) / ((n + 2) !);
existence

proof end;

uniqueness

proof end;

deffunc H₃( Element of NAT ) -> Element of COMPLEX = (z #N $1) / (($1 + 2) !);
func z P_t -> Complex_Sequence means :: SIN_COS:def 29
for n being Element of NAT holds it . n = (z #N n) / ((n + 2) !);
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def28 defines P_dt SIN_COS:def 28 :

:: deftheorem defines P_t SIN_COS:def 29 :

Lm12: for p being Real
for z being complex number holds
( Re ((p * ) * z) = - (p * (Im z)) & Im ((p * ) * z) = p * (Re z) & Re (p * z) = p * (Re z) & Im (p * z) = p * (Im z) )

proof end;

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

proof end;

theorem Th61: :: SIN_COS:61

for z being complex number holds z P_dt is absolutely_summable

proof end;

theorem Th62: :: SIN_COS:62

for z being complex number holds z * (Sum (z P_dt)) = ((Sum (z ExpSeq)) - 1r) - z

proof end;

theorem Th63: :: SIN_COS:63

for p being real number st p > 0 holds
ex q being Real st
( q > 0 & ( for z being complex number st |.z.| < q holds
|.(Sum (z P_dt)).| < p ) )

proof end;

theorem Th64: :: SIN_COS:64

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

proof end;

theorem Th65: :: SIN_COS:65

for p, q being Real holds (cos . (p + q)) - (cos . p) = (- (q * (sin . p))) - (q * (Im ((Sum ((q * ) P_dt)) * ((cos . p) + ((sin . p) * )))))

proof end;

theorem Th66: :: SIN_COS:66

for p, q being Real holds (sin . (p + q)) - (sin . p) = (q * (cos . p)) + (q * (Re ((Sum ((q * ) P_dt)) * ((cos . p) + ((sin . p) * )))))

proof end;

theorem Th67: :: SIN_COS:67

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

proof end;

theorem Th68: :: SIN_COS:68

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

proof end;

theorem Th69: :: SIN_COS:69

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

proof end;

theorem Th70: :: SIN_COS:70

for p being real number holds
( exp_R is_differentiable_in p & diff (exp_R,p) = exp_R . p )

proof end;

theorem Th71: :: SIN_COS:71

for th being real number holds
( exp_R is_differentiable_on REAL & diff (exp_R,th) = exp_R . th )

proof end;

theorem Th72: :: SIN_COS:72

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

proof end;

theorem Th73: :: SIN_COS:73

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

proof end;

theorem Th74: :: SIN_COS:74

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

proof end;

definition

func tan -> PartFunc of REAL,REAL equals :: SIN_COS:def 30
sin / cos;
coherence ;
func cot -> PartFunc of REAL,REAL equals :: SIN_COS:def 31
cos / sin;
coherence ;

end;

:: deftheorem defines tan SIN_COS:def 30 :

:: deftheorem defines cot SIN_COS:def 31 :

theorem Th75: :: SIN_COS:75

( [.0,1.] c= dom tan & ].0,1.[ c= dom tan )

proof end;

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

proof end;

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

proof end;

theorem Th76: :: SIN_COS:76

tan | [.0,1.] is continuous

proof end;

theorem Th77: :: SIN_COS:77

for th1, th2 being real number st th1 in ].0,1.[ & th2 in ].0,1.[ & tan . th1 = tan . th2 holds
th1 = th2

proof end;

Lm16: ( tan . 0 = 0 & tan . 1 > 1 )

proof end;

begin

definition

func PI -> real number means :Def32: :: SIN_COS:def 32
( tan . (it / 4) = 1 & it in ].0,4.[ );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def32 defines PI SIN_COS:def 32 :

definition

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

end;

theorem Th78: :: SIN_COS:78

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

proof end;

begin

theorem Th79: :: SIN_COS:79

for th1, th2 being real number holds
( sin . (th1 + th2) = ((sin . th1) * (cos . th2)) + ((cos . th1) * (sin . th2)) & cos . (th1 + th2) = ((cos . th1) * (cos . th2)) - ((sin . th1) * (sin . th2)) )

proof end;

theorem :: SIN_COS:80

for th1, th2 being real number holds
( sin (th1 + th2) = ((sin th1) * (cos th2)) + ((cos th1) * (sin th2)) & cos (th1 + th2) = ((cos th1) * (cos th2)) - ((sin th1) * (sin th2)) ) 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 :: 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 th being real number holds
( sin . (th + (2 * PI)) = sin . th & cos . (th + (2 * PI)) = cos . th & sin . ((PI / 2) - th) = cos . th & cos . ((PI / 2) - th) = sin . th & sin . ((PI / 2) + th) = cos . th & cos . ((PI / 2) + th) = - (sin . th) & sin . (PI + th) = - (sin . th) & cos . (PI + th) = - (cos . th) )

proof end;

theorem :: SIN_COS:84

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