:: by Yuguang Yang and Yasunari Shidama

::

:: Received October 22, 1998

:: Copyright (c) 1998-2017 Association of Mizar Users

:: Some definitions and properties of complex sequence

definition

let m, k be natural Number ;

correctness

coherence

( ( m <= k implies 1 is Element of COMPLEX ) & ( not m <= k implies 0 is Element of COMPLEX ) );

consistency

for b_{1} being Element of COMPLEX holds verum;

end;
correctness

coherence

( ( m <= k implies 1 is Element of COMPLEX ) & ( not m <= k implies 0 is Element of COMPLEX ) );

consistency

for b

proof end;

:: deftheorem Def1 defines CHK SIN_COS:def 1 :

for m, k being natural Number holds

( ( m <= k implies CHK (m,k) = 1 ) & ( not m <= k implies CHK (m,k) = 0 ) );

for m, k being natural Number holds

( ( m <= k implies CHK (m,k) = 1 ) & ( not m <= k implies CHK (m,k) = 0 ) );

registration
end;

1 in NAT

;

then reconsider jj = 1 as Element of REAL by NUMBERS:19;

definition

ex b_{1} being Real_Sequence st

( b_{1} . 0 = 1 & ( for n being Nat holds b_{1} . (n + 1) = (b_{1} . n) * (n + 1) ) )

for b_{1}, b_{2} being Real_Sequence st b_{1} . 0 = 1 & ( for n being Nat holds b_{1} . (n + 1) = (b_{1} . n) * (n + 1) ) & b_{2} . 0 = 1 & ( for n being Nat holds b_{2} . (n + 1) = (b_{2} . n) * (n + 1) ) holds

b_{1} = b_{2}
end;

func Prod_real_n -> Real_Sequence means :Def2: :: SIN_COS:def 2

( it . 0 = 1 & ( for n being Nat holds it . (n + 1) = (it . n) * (n + 1) ) );

existence ( it . 0 = 1 & ( for n being Nat holds it . (n + 1) = (it . n) * (n + 1) ) );

ex b

( b

proof end;

uniqueness for b

b

proof end;

:: deftheorem Def2 defines Prod_real_n SIN_COS:def 2 :

for b_{1} being Real_Sequence holds

( b_{1} = Prod_real_n iff ( b_{1} . 0 = 1 & ( for n being Nat holds b_{1} . (n + 1) = (b_{1} . n) * (n + 1) ) ) );

for b

( b

definition

let n be Nat;

compatibility

for b_{1} being set holds

( b_{1} = n ! iff b_{1} = Prod_real_n . n )

end;
compatibility

for b

( b

proof end;

definition

let z be Complex;

deffunc H_{1}( Nat) -> set = (z |^ $1) / ($1 !);

ex b_{1} being Complex_Sequence st

for n being Nat holds b_{1} . n = (z |^ n) / (n !)

for b_{1}, b_{2} being Complex_Sequence st ( for n being Nat holds b_{1} . n = (z |^ n) / (n !) ) & ( for n being Nat holds b_{2} . n = (z |^ n) / (n !) ) holds

b_{1} = b_{2}

end;
deffunc H

func z ExpSeq -> Complex_Sequence means :Def4: :: SIN_COS:def 4

for n being Nat holds it . n = (z |^ n) / (n !);

existence for n being Nat holds it . n = (z |^ n) / (n !);

ex b

for n being Nat holds b

proof end;

uniqueness for b

b

proof end;

:: deftheorem Def4 defines ExpSeq SIN_COS:def 4 :

for z being Complex

for b_{2} being Complex_Sequence holds

( b_{2} = z ExpSeq iff for n being Nat holds b_{2} . n = (z |^ n) / (n !) );

for z being Complex

for b

( b

definition

let a be Real;

deffunc H_{1}( Nat) -> set = (a |^ $1) / ($1 !);

ex b_{1} being Real_Sequence st

for n being Nat holds b_{1} . n = (a |^ n) / (n !)

for b_{1}, b_{2} being Real_Sequence st ( for n being Nat holds b_{1} . n = (a |^ n) / (n !) ) & ( for n being Nat holds b_{2} . n = (a |^ n) / (n !) ) holds

b_{1} = b_{2}

end;
deffunc H

func a rExpSeq -> Real_Sequence means :Def5: :: SIN_COS:def 5

for n being Nat holds it . n = (a |^ n) / (n !);

existence for n being Nat holds it . n = (a |^ n) / (n !);

ex b

for n being Nat holds b

proof end;

uniqueness for b

b

proof end;

:: deftheorem Def5 defines rExpSeq SIN_COS:def 5 :

for a being Real

for b_{2} being Real_Sequence holds

( b_{2} = a rExpSeq iff for n being Nat holds b_{2} . n = (a |^ n) / (n !) );

for a being Real

for b

( b

theorem Th2: :: SIN_COS:2

for k, m being Nat holds

( ( 0 < k implies ((k -' 1) !) * k = k ! ) & ( k <= m implies ((m -' k) !) * ((m + 1) - k) = ((m + 1) -' k) ! ) )

( ( 0 < k implies ((k -' 1) !) * k = k ! ) & ( k <= m implies ((m -' k) !) * ((m + 1) - k) = ((m + 1) -' k) ! ) )

proof end;

definition

let n be Nat;

ex b_{1} being Complex_Sequence st

for k being Nat holds

( ( k <= n implies b_{1} . k = (n !) / ((k !) * ((n -' k) !)) ) & ( k > n implies b_{1} . k = 0 ) )

for b_{1}, b_{2} being Complex_Sequence st ( for k being Nat holds

( ( k <= n implies b_{1} . k = (n !) / ((k !) * ((n -' k) !)) ) & ( k > n implies b_{1} . k = 0 ) ) ) & ( for k being Nat holds

( ( k <= n implies b_{2} . k = (n !) / ((k !) * ((n -' k) !)) ) & ( k > n implies b_{2} . k = 0 ) ) ) holds

b_{1} = b_{2}

end;
func Coef n -> Complex_Sequence means :Def6: :: SIN_COS:def 6

for k being Nat holds

( ( k <= n implies it . k = (n !) / ((k !) * ((n -' k) !)) ) & ( k > n implies it . k = 0 ) );

existence for k being Nat holds

( ( k <= n implies it . k = (n !) / ((k !) * ((n -' k) !)) ) & ( k > n implies it . k = 0 ) );

ex b

for k being Nat holds

( ( k <= n implies b

proof end;

uniqueness for b

( ( k <= n implies b

( ( k <= n implies b

b

proof end;

:: deftheorem Def6 defines Coef SIN_COS:def 6 :

for n being Nat

for b_{2} being Complex_Sequence holds

( b_{2} = Coef n iff for k being Nat holds

( ( k <= n implies b_{2} . k = (n !) / ((k !) * ((n -' k) !)) ) & ( k > n implies b_{2} . k = 0 ) ) );

for n being Nat

for b

( b

( ( k <= n implies b

definition

let n be Nat;

ex b_{1} being Complex_Sequence st

for k being Nat holds

( ( k <= n implies b_{1} . k = 1r / ((k !) * ((n -' k) !)) ) & ( k > n implies b_{1} . k = 0 ) )

for b_{1}, b_{2} being Complex_Sequence st ( for k being Nat holds

( ( k <= n implies b_{1} . k = 1r / ((k !) * ((n -' k) !)) ) & ( k > n implies b_{1} . k = 0 ) ) ) & ( for k being Nat holds

( ( k <= n implies b_{2} . k = 1r / ((k !) * ((n -' k) !)) ) & ( k > n implies b_{2} . k = 0 ) ) ) holds

b_{1} = b_{2}

end;
func Coef_e n -> Complex_Sequence means :Def7: :: SIN_COS:def 7

for k being Nat holds

( ( k <= n implies it . k = 1r / ((k !) * ((n -' k) !)) ) & ( k > n implies it . k = 0 ) );

existence for k being Nat holds

( ( k <= n implies it . k = 1r / ((k !) * ((n -' k) !)) ) & ( k > n implies it . k = 0 ) );

ex b

for k being Nat holds

( ( k <= n implies b

proof end;

uniqueness for b

( ( k <= n implies b

( ( k <= n implies b

b

proof end;

:: deftheorem Def7 defines Coef_e SIN_COS:def 7 :

for n being Nat

for b_{2} being Complex_Sequence holds

( b_{2} = Coef_e n iff for k being Nat holds

( ( k <= n implies b_{2} . k = 1r / ((k !) * ((n -' k) !)) ) & ( k > n implies b_{2} . k = 0 ) ) );

for n being Nat

for b

( b

( ( k <= n implies b

definition

let seq be Complex_Sequence;

ex b_{1} being Complex_Sequence st

( b_{1} . 0 = 0 & ( for k being Nat holds b_{1} . (k + 1) = seq . k ) )

for b_{1}, b_{2} being Complex_Sequence st b_{1} . 0 = 0 & ( for k being Nat holds b_{1} . (k + 1) = seq . k ) & b_{2} . 0 = 0 & ( for k being Nat holds b_{2} . (k + 1) = seq . k ) holds

b_{1} = b_{2}

end;
func Shift seq -> Complex_Sequence means :Def8: :: SIN_COS:def 8

( it . 0 = 0 & ( for k being Nat holds it . (k + 1) = seq . k ) );

existence ( it . 0 = 0 & ( for k being Nat holds it . (k + 1) = seq . k ) );

ex b

( b

proof end;

uniqueness for b

b

proof end;

:: deftheorem Def8 defines Shift SIN_COS:def 8 :

for seq, b_{2} being Complex_Sequence holds

( b_{2} = Shift seq iff ( b_{2} . 0 = 0 & ( for k being Nat holds b_{2} . (k + 1) = seq . k ) ) );

for seq, b

( b

definition

let n be Nat;

let z, w be Complex;

ex b_{1} being Complex_Sequence st

for k being Nat holds

( ( k <= n implies b_{1} . k = (((Coef n) . k) * (z |^ k)) * (w |^ (n -' k)) ) & ( n < k implies b_{1} . k = 0 ) )

for b_{1}, b_{2} being Complex_Sequence st ( for k being Nat holds

( ( k <= n implies b_{1} . k = (((Coef n) . k) * (z |^ k)) * (w |^ (n -' k)) ) & ( n < k implies b_{1} . k = 0 ) ) ) & ( for k being Nat holds

( ( k <= n implies b_{2} . k = (((Coef n) . k) * (z |^ k)) * (w |^ (n -' k)) ) & ( n < k implies b_{2} . k = 0 ) ) ) holds

b_{1} = b_{2}

end;
let z, w be Complex;

func Expan (n,z,w) -> Complex_Sequence means :Def9: :: SIN_COS:def 9

for k being Nat holds

( ( k <= n implies it . k = (((Coef n) . k) * (z |^ k)) * (w |^ (n -' k)) ) & ( n < k implies it . k = 0 ) );

existence for k being Nat holds

( ( k <= n implies it . k = (((Coef n) . k) * (z |^ k)) * (w |^ (n -' k)) ) & ( n < k implies it . k = 0 ) );

ex b

for k being Nat holds

( ( k <= n implies b

proof end;

uniqueness for b

( ( k <= n implies b

( ( k <= n implies b

b

proof end;

:: deftheorem Def9 defines Expan SIN_COS:def 9 :

for n being Nat

for z, w being Complex

for b_{4} being Complex_Sequence holds

( b_{4} = Expan (n,z,w) iff for k being Nat holds

( ( k <= n implies b_{4} . k = (((Coef n) . k) * (z |^ k)) * (w |^ (n -' k)) ) & ( n < k implies b_{4} . k = 0 ) ) );

for n being Nat

for z, w being Complex

for b

( b

( ( k <= n implies b

definition

let n be Nat;

let z, w be Complex;

ex b_{1} being Complex_Sequence st

for k being Nat holds

( ( k <= n implies b_{1} . k = (((Coef_e n) . k) * (z |^ k)) * (w |^ (n -' k)) ) & ( n < k implies b_{1} . k = 0 ) )

for b_{1}, b_{2} being Complex_Sequence st ( for k being Nat holds

( ( k <= n implies b_{1} . k = (((Coef_e n) . k) * (z |^ k)) * (w |^ (n -' k)) ) & ( n < k implies b_{1} . k = 0 ) ) ) & ( for k being Nat holds

( ( k <= n implies b_{2} . k = (((Coef_e n) . k) * (z |^ k)) * (w |^ (n -' k)) ) & ( n < k implies b_{2} . k = 0 ) ) ) holds

b_{1} = b_{2}

end;
let z, w be Complex;

func Expan_e (n,z,w) -> Complex_Sequence means :Def10: :: SIN_COS:def 10

for k being Nat holds

( ( k <= n implies it . k = (((Coef_e n) . k) * (z |^ k)) * (w |^ (n -' k)) ) & ( n < k implies it . k = 0 ) );

existence for k being Nat holds

( ( k <= n implies it . k = (((Coef_e n) . k) * (z |^ k)) * (w |^ (n -' k)) ) & ( n < k implies it . k = 0 ) );

ex b

for k being Nat holds

( ( k <= n implies b

proof end;

uniqueness for b

( ( k <= n implies b

( ( k <= n implies b

b

proof end;

:: deftheorem Def10 defines Expan_e SIN_COS:def 10 :

for n being Nat

for z, w being Complex

for b_{4} being Complex_Sequence holds

( b_{4} = Expan_e (n,z,w) iff for k being Nat holds

( ( k <= n implies b_{4} . k = (((Coef_e n) . k) * (z |^ k)) * (w |^ (n -' k)) ) & ( n < k implies b_{4} . k = 0 ) ) );

for n being Nat

for z, w being Complex

for b

( b

( ( k <= n implies b

definition

let n be Nat;

let z, w be Complex;

ex b_{1} being Complex_Sequence st

for k being Nat holds

( ( k <= n implies b_{1} . k = ((z ExpSeq) . k) * ((Partial_Sums (w ExpSeq)) . (n -' k)) ) & ( n < k implies b_{1} . k = 0 ) )

for b_{1}, b_{2} being Complex_Sequence st ( for k being Nat holds

( ( k <= n implies b_{1} . k = ((z ExpSeq) . k) * ((Partial_Sums (w ExpSeq)) . (n -' k)) ) & ( n < k implies b_{1} . k = 0 ) ) ) & ( for k being Nat holds

( ( k <= n implies b_{2} . k = ((z ExpSeq) . k) * ((Partial_Sums (w ExpSeq)) . (n -' k)) ) & ( n < k implies b_{2} . k = 0 ) ) ) holds

b_{1} = b_{2}

end;
let z, w be Complex;

func Alfa (n,z,w) -> Complex_Sequence means :Def11: :: SIN_COS:def 11

for k being Nat holds

( ( k <= n implies it . k = ((z ExpSeq) . k) * ((Partial_Sums (w ExpSeq)) . (n -' k)) ) & ( n < k implies it . k = 0 ) );

existence for k being Nat holds

( ( k <= n implies it . k = ((z ExpSeq) . k) * ((Partial_Sums (w ExpSeq)) . (n -' k)) ) & ( n < k implies it . k = 0 ) );

ex b

for k being Nat holds

( ( k <= n implies b

proof end;

uniqueness for b

( ( k <= n implies b

( ( k <= n implies b

b

proof end;

:: deftheorem Def11 defines Alfa SIN_COS:def 11 :

for n being Nat

for z, w being Complex

for b_{4} being Complex_Sequence holds

( b_{4} = Alfa (n,z,w) iff for k being Nat holds

( ( k <= n implies b_{4} . k = ((z ExpSeq) . k) * ((Partial_Sums (w ExpSeq)) . (n -' k)) ) & ( n < k implies b_{4} . k = 0 ) ) );

for n being Nat

for z, w being Complex

for b

( b

( ( k <= n implies b

definition

let a, b be Real;

let n be Nat;

ex b_{1} being Real_Sequence st

for k being Nat holds

( ( k <= n implies b_{1} . k = ((a rExpSeq) . k) * (((Partial_Sums (b rExpSeq)) . n) - ((Partial_Sums (b rExpSeq)) . (n -' k))) ) & ( n < k implies b_{1} . k = 0 ) )

for b_{1}, b_{2} being Real_Sequence st ( for k being Nat holds

( ( k <= n implies b_{1} . k = ((a rExpSeq) . k) * (((Partial_Sums (b rExpSeq)) . n) - ((Partial_Sums (b rExpSeq)) . (n -' k))) ) & ( n < k implies b_{1} . k = 0 ) ) ) & ( for k being Nat holds

( ( k <= n implies b_{2} . k = ((a rExpSeq) . k) * (((Partial_Sums (b rExpSeq)) . n) - ((Partial_Sums (b rExpSeq)) . (n -' k))) ) & ( n < k implies b_{2} . k = 0 ) ) ) holds

b_{1} = b_{2}

end;
let n be Nat;

func Conj (n,a,b) -> Real_Sequence means :: SIN_COS:def 12

for k being 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 for k being 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 ) );

ex b

for k being Nat holds

( ( k <= n implies b

proof end;

uniqueness for b

( ( k <= n implies b

( ( k <= n implies b

b

proof end;

:: deftheorem defines Conj SIN_COS:def 12 :

for a, b being Real

for n being Nat

for b_{4} being Real_Sequence holds

( b_{4} = Conj (n,a,b) iff for k being Nat holds

( ( k <= n implies b_{4} . k = ((a rExpSeq) . k) * (((Partial_Sums (b rExpSeq)) . n) - ((Partial_Sums (b rExpSeq)) . (n -' k))) ) & ( n < k implies b_{4} . k = 0 ) ) );

for a, b being Real

for n being Nat

for b

( b

( ( k <= n implies b

definition

let z, w be Complex;

let n be Nat;

ex b_{1} being Complex_Sequence st

for k being Nat holds

( ( k <= n implies b_{1} . k = ((z ExpSeq) . k) * (((Partial_Sums (w ExpSeq)) . n) - ((Partial_Sums (w ExpSeq)) . (n -' k))) ) & ( n < k implies b_{1} . k = 0 ) )

for b_{1}, b_{2} being Complex_Sequence st ( for k being Nat holds

( ( k <= n implies b_{1} . k = ((z ExpSeq) . k) * (((Partial_Sums (w ExpSeq)) . n) - ((Partial_Sums (w ExpSeq)) . (n -' k))) ) & ( n < k implies b_{1} . k = 0 ) ) ) & ( for k being Nat holds

( ( k <= n implies b_{2} . k = ((z ExpSeq) . k) * (((Partial_Sums (w ExpSeq)) . n) - ((Partial_Sums (w ExpSeq)) . (n -' k))) ) & ( n < k implies b_{2} . k = 0 ) ) ) holds

b_{1} = b_{2}

end;
let n be Nat;

func Conj (n,z,w) -> Complex_Sequence means :Def13: :: SIN_COS:def 13

for k being 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 for k being 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 ) );

ex b

for k being Nat holds

( ( k <= n implies b

proof end;

uniqueness for b

( ( k <= n implies b

( ( k <= n implies b

b

proof end;

:: deftheorem Def13 defines Conj SIN_COS:def 13 :

for z, w being Complex

for n being Nat

for b_{4} being Complex_Sequence holds

( b_{4} = Conj (n,z,w) iff for k being Nat holds

( ( k <= n implies b_{4} . k = ((z ExpSeq) . k) * (((Partial_Sums (w ExpSeq)) . n) - ((Partial_Sums (w ExpSeq)) . (n -' k))) ) & ( n < k implies b_{4} . k = 0 ) ) );

for z, w being Complex

for n being Nat

for b

( b

( ( k <= n implies b

Lm1: for p1, p2, g1, g2 being Real holds

( (p1 + (g1 * <i>)) * (p2 + (g2 * <i>)) = ((p1 * p2) - (g1 * g2)) + (((p1 * g2) + (p2 * g1)) * <i>) & (p2 + (g2 * <i>)) *' = p2 + ((- g2) * <i>) )

proof end;

theorem Th3: :: SIN_COS:3

for n being Nat

for z being Complex holds

( (z ExpSeq) . (n + 1) = (((z ExpSeq) . n) * z) / ((n + 1) + (0 * <i>)) & (z ExpSeq) . 0 = 1 & |.((z ExpSeq) . n).| = (|.z.| rExpSeq) . n )

for z being Complex holds

( (z ExpSeq) . (n + 1) = (((z ExpSeq) . n) * z) / ((n + 1) + (0 * <i>)) & (z ExpSeq) . 0 = 1 & |.((z ExpSeq) . n).| = (|.z.| rExpSeq) . n )

proof end;

theorem Th5: :: SIN_COS:5

for k being Nat

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

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

proof end;

theorem Th8: :: SIN_COS:8

for w, z being Complex

for n being Nat holds ((z + w) |^ n) / (n !) = (Partial_Sums (Expan_e (n,z,w))) . n

for n being Nat holds ((z + w) |^ n) / (n !) = (Partial_Sums (Expan_e (n,z,w))) . n

proof end;

theorem Th11: :: SIN_COS:11

for w, z being Complex

for k, l being Nat st l <= k holds

(Alfa ((k + 1),z,w)) . l = ((Alfa (k,z,w)) . l) + ((Expan_e ((k + 1),z,w)) . l)

for k, l being 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 Th12: :: SIN_COS:12

for w, z being Complex

for k being 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)

for k being 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 w, z being Complex

for n being Nat holds (Partial_Sums ((z + w) ExpSeq)) . n = (Partial_Sums (Alfa (n,z,w))) . n

for n being Nat holds (Partial_Sums ((z + w) ExpSeq)) . n = (Partial_Sums (Alfa (n,z,w))) . n

proof end;

theorem Th15: :: SIN_COS:15

for w, z being Complex

for k being 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

for k being 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 Th16: :: SIN_COS:16

for z being Complex

for k being Nat holds

( |.((Partial_Sums (z ExpSeq)) . k).| <= (Partial_Sums (|.z.| rExpSeq)) . k & (Partial_Sums (|.z.| rExpSeq)) . k <= Sum (|.z.| rExpSeq) & |.((Partial_Sums (z ExpSeq)) . k).| <= Sum (|.z.| rExpSeq) )

for k being Nat holds

( |.((Partial_Sums (z ExpSeq)) . k).| <= (Partial_Sums (|.z.| rExpSeq)) . k & (Partial_Sums (|.z.| rExpSeq)) . k <= Sum (|.z.| rExpSeq) & |.((Partial_Sums (z ExpSeq)) . k).| <= Sum (|.z.| rExpSeq) )

proof end;

theorem Th19: :: SIN_COS:19

for z being Complex

for m, n being Nat holds

( |.((Partial_Sums (|.z.| rExpSeq)) . n).| = (Partial_Sums (|.z.| rExpSeq)) . n & ( n <= m implies |.(((Partial_Sums (|.z.| rExpSeq)) . m) - ((Partial_Sums (|.z.| rExpSeq)) . n)).| = ((Partial_Sums (|.z.| rExpSeq)) . m) - ((Partial_Sums (|.z.| rExpSeq)) . n) ) )

for m, n being Nat holds

( |.((Partial_Sums (|.z.| rExpSeq)) . n).| = (Partial_Sums (|.z.| rExpSeq)) . n & ( n <= m implies |.(((Partial_Sums (|.z.| rExpSeq)) . m) - ((Partial_Sums (|.z.| rExpSeq)) . n)).| = ((Partial_Sums (|.z.| rExpSeq)) . m) - ((Partial_Sums (|.z.| rExpSeq)) . n) ) )

proof end;

theorem Th20: :: SIN_COS:20

for w, z being Complex

for k, n being Nat holds |.((Partial_Sums |.(Conj (k,z,w)).|) . n).| = (Partial_Sums |.(Conj (k,z,w)).|) . n

for k, n being Nat holds |.((Partial_Sums |.(Conj (k,z,w)).|) . n).| = (Partial_Sums |.(Conj (k,z,w)).|) . n

proof end;

theorem Th21: :: SIN_COS:21

for w, z being Complex

for p being Real st p > 0 holds

ex n being Nat st

for k being Nat st n <= k holds

|.((Partial_Sums |.(Conj (k,z,w)).|) . k).| < p

for p being Real st p > 0 holds

ex n being Nat st

for k being Nat st n <= k holds

|.((Partial_Sums |.(Conj (k,z,w)).|) . k).| < p

proof end;

theorem Th22: :: SIN_COS:22

for w, z being Complex

for seq being Complex_Sequence st ( for k being Nat holds seq . k = (Partial_Sums (Conj (k,z,w))) . k ) holds

( seq is convergent & lim seq = 0 )

for seq being Complex_Sequence st ( for k being 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 holds (Sum (z ExpSeq)) * (Sum (w ExpSeq)) = Sum ((z + w) ExpSeq)

proof end;

definition

ex b_{1} being Function of COMPLEX,COMPLEX st

for z being Complex holds b_{1} . z = Sum (z ExpSeq)

for b_{1}, b_{2} being Function of COMPLEX,COMPLEX st ( for z being Complex holds b_{1} . z = Sum (z ExpSeq) ) & ( for z being Complex holds b_{2} . z = Sum (z ExpSeq) ) holds

b_{1} = b_{2}
end;

func exp -> Function of COMPLEX,COMPLEX means :Def14: :: SIN_COS:def 14

for z being Complex holds it . z = Sum (z ExpSeq);

existence for z being Complex holds it . z = Sum (z ExpSeq);

ex b

for z being Complex holds b

proof end;

uniqueness for b

b

proof end;

:: deftheorem Def14 defines exp SIN_COS:def 14 :

for b_{1} being Function of COMPLEX,COMPLEX holds

( b_{1} = exp iff for z being Complex holds b_{1} . z = Sum (z ExpSeq) );

for b

( b

definition

let z be Complex;

:: original: exp

redefine func exp z -> Element of COMPLEX ;

coherence

exp z is Element of COMPLEX by XCMPLX_0:def 2;

end;
:: original: exp

redefine func exp z -> Element of COMPLEX ;

coherence

exp z is Element of COMPLEX by XCMPLX_0:def 2;

definition

ex b_{1} being Function of REAL,REAL st

for d being Real holds b_{1} . d = Im (Sum ((d * <i>) ExpSeq))

for b_{1}, b_{2} being Function of REAL,REAL st ( for d being Real holds b_{1} . d = Im (Sum ((d * <i>) ExpSeq)) ) & ( for d being Real holds b_{2} . d = Im (Sum ((d * <i>) ExpSeq)) ) holds

b_{1} = b_{2}
end;

func sin -> Function of REAL,REAL means :Def16: :: SIN_COS:def 16

for d being Real holds it . d = Im (Sum ((d * <i>) ExpSeq));

existence for d being Real holds it . d = Im (Sum ((d * <i>) ExpSeq));

ex b

for d being Real holds b

proof end;

uniqueness for b

b

proof end;

:: deftheorem Def16 defines sin SIN_COS:def 16 :

for b_{1} being Function of REAL,REAL holds

( b_{1} = sin iff for d being Real holds b_{1} . d = Im (Sum ((d * <i>) ExpSeq)) );

for b

( b

definition

ex b_{1} being Function of REAL,REAL st

for d being Real holds b_{1} . d = Re (Sum ((d * <i>) ExpSeq))

for b_{1}, b_{2} being Function of REAL,REAL st ( for d being Real holds b_{1} . d = Re (Sum ((d * <i>) ExpSeq)) ) & ( for d being Real holds b_{2} . d = Re (Sum ((d * <i>) ExpSeq)) ) holds

b_{1} = b_{2}
end;

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 for d being Real holds it . d = Re (Sum ((d * <i>) ExpSeq));

ex b

for d being Real holds b

proof end;

uniqueness for b

b

proof end;

:: deftheorem Def18 defines cos SIN_COS:def 18 :

for b_{1} being Function of REAL,REAL holds

( b_{1} = cos iff for d being Real holds b_{1} . d = Re (Sum ((d * <i>) ExpSeq)) );

for b

( b

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

proof end;

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

proof end;

Lm5: for th, th1 being Real st th = th1 holds

( |.(Sum ((th * <i>) ExpSeq)).| = 1 & |.(sin . th1).| <= 1 & |.(cos . th1).| <= 1 )

proof end;

theorem :: SIN_COS:27

for th being Real holds

( |.(exp (th * <i>)).| = 1 & ( for th being Real holds

( |.(sin th).| <= 1 & |.(cos th).| <= 1 ) ) )

( |.(exp (th * <i>)).| = 1 & ( for th being Real holds

( |.(sin th).| <= 1 & |.(cos th).| <= 1 ) ) )

proof end;

theorem Th28: :: SIN_COS:28

for th being Real holds

( ((cos . th) ^2) + ((sin . th) ^2) = 1 & ((cos . th) * (cos . th)) + ((sin . th) * (sin . th)) = 1 )

( ((cos . th) ^2) + ((sin . th) ^2) = 1 & ((cos . th) * (cos . th)) + ((sin . th) * (sin . th)) = 1 )

proof end;

theorem :: SIN_COS:29

theorem Th30: :: SIN_COS:30

for th being Real holds

( cos . 0 = 1 & sin . 0 = 0 & cos . (- th) = cos . th & sin . (- th) = - (sin . th) )

( cos . 0 = 1 & sin . 0 = 0 & cos . (- th) = cos . th & sin . (- th) = - (sin . th) )

proof end;

theorem :: SIN_COS:31

definition

let th be Real;

deffunc H_{1}( Nat) -> set = (((- 1) |^ $1) * (th |^ ((2 * $1) + 1))) / (((2 * $1) + 1) !);

ex b_{1} being Real_Sequence st

for n being Nat holds b_{1} . n = (((- 1) |^ n) * (th |^ ((2 * n) + 1))) / (((2 * n) + 1) !)

for b_{1}, b_{2} being Real_Sequence st ( for n being Nat holds b_{1} . n = (((- 1) |^ n) * (th |^ ((2 * n) + 1))) / (((2 * n) + 1) !) ) & ( for n being Nat holds b_{2} . n = (((- 1) |^ n) * (th |^ ((2 * n) + 1))) / (((2 * n) + 1) !) ) holds

b_{1} = b_{2}
_{2}( Nat) -> set = (((- 1) |^ $1) * (th |^ (2 * $1))) / ((2 * $1) !);

ex b_{1} being Real_Sequence st

for n being Nat holds b_{1} . n = (((- 1) |^ n) * (th |^ (2 * n))) / ((2 * n) !)

for b_{1}, b_{2} being Real_Sequence st ( for n being Nat holds b_{1} . n = (((- 1) |^ n) * (th |^ (2 * n))) / ((2 * n) !) ) & ( for n being Nat holds b_{2} . n = (((- 1) |^ n) * (th |^ (2 * n))) / ((2 * n) !) ) holds

b_{1} = b_{2}

end;
deffunc H

func th P_sin -> Real_Sequence means :Def20: :: SIN_COS:def 20

for n being Nat holds it . n = (((- 1) |^ n) * (th |^ ((2 * n) + 1))) / (((2 * n) + 1) !);

existence for n being Nat holds it . n = (((- 1) |^ n) * (th |^ ((2 * n) + 1))) / (((2 * n) + 1) !);

ex b

for n being Nat holds b

proof end;

uniqueness for b

b

proof end;

deffunc H
func th P_cos -> Real_Sequence means :Def21: :: SIN_COS:def 21

for n being Nat holds it . n = (((- 1) |^ n) * (th |^ (2 * n))) / ((2 * n) !);

existence for n being Nat holds it . n = (((- 1) |^ n) * (th |^ (2 * n))) / ((2 * n) !);

ex b

for n being Nat holds b

proof end;

uniqueness for b

b

proof end;

:: deftheorem Def20 defines P_sin SIN_COS:def 20 :

for th being Real

for b_{2} being Real_Sequence holds

( b_{2} = th P_sin iff for n being Nat holds b_{2} . n = (((- 1) |^ n) * (th |^ ((2 * n) + 1))) / (((2 * n) + 1) !) );

for th being Real

for b

( b

:: deftheorem Def21 defines P_cos SIN_COS:def 21 :

for th being Real

for b_{2} being Real_Sequence holds

( b_{2} = th P_cos iff for n being Nat holds b_{2} . n = (((- 1) |^ n) * (th |^ (2 * n))) / ((2 * n) !) );

for th being Real

for b

( b

theorem Th32: :: SIN_COS:32

for z being Complex

for k being Nat holds

( z |^ (2 * k) = (z |^ k) |^ 2 & z |^ (2 * k) = (z |^ 2) |^ k )

for k being Nat holds

( z |^ (2 * k) = (z |^ k) |^ 2 & z |^ (2 * k) = (z |^ 2) |^ k )

proof end;

theorem Th33: :: SIN_COS:33

for k being Nat

for th being Real holds

( (th * <i>) |^ (2 * k) = ((- 1) |^ k) * (th |^ (2 * k)) & (th * <i>) |^ ((2 * k) + 1) = (((- 1) |^ k) * (th |^ ((2 * k) + 1))) * <i> )

for th being Real holds

( (th * <i>) |^ (2 * k) = ((- 1) |^ k) * (th |^ (2 * k)) & (th * <i>) |^ ((2 * k) + 1) = (((- 1) |^ k) * (th |^ ((2 * k) + 1))) * <i> )

proof end;

::$CT

theorem Th34: :: SIN_COS:35

for n being Nat

for th being Real holds

( (Partial_Sums (th P_sin)) . n = (Partial_Sums (Im ((th * <i>) ExpSeq))) . ((2 * n) + 1) & (Partial_Sums (th P_cos)) . n = (Partial_Sums (Re ((th * <i>) ExpSeq))) . (2 * n) )

for th being Real holds

( (Partial_Sums (th P_sin)) . n = (Partial_Sums (Im ((th * <i>) ExpSeq))) . ((2 * n) + 1) & (Partial_Sums (th P_cos)) . n = (Partial_Sums (Re ((th * <i>) ExpSeq))) . (2 * n) )

proof end;

theorem Th35: :: SIN_COS:36

for th being Real holds

( Partial_Sums (th P_sin) is convergent & Sum (th P_sin) = Im (Sum ((th * <i>) ExpSeq)) & Partial_Sums (th P_cos) is convergent & Sum (th P_cos) = Re (Sum ((th * <i>) ExpSeq)) )

( Partial_Sums (th P_sin) is convergent & Sum (th P_sin) = Im (Sum ((th * <i>) ExpSeq)) & Partial_Sums (th P_cos) is convergent & Sum (th P_cos) = Re (Sum ((th * <i>) ExpSeq)) )

proof end;

theorem :: SIN_COS:38

for p, th being Real

for rseq being Real_Sequence st rseq is convergent & lim rseq = th & ( for n being Nat holds rseq . n >= p ) holds

th >= p by PREPOWER:1;

for rseq being Real_Sequence st rseq is convergent & lim rseq = th & ( for n being Nat holds rseq . n >= p ) holds

th >= p by PREPOWER:1;

deffunc H

consider bq being Real_Sequence such that

Lm6: for n being Nat holds bq . n = H

bq is increasing sequence of NAT

proof end;

then reconsider bq = bq as increasing sequence of NAT ;

Lm7: for n being Nat

for th, th1, th2, th3 being Real holds

( th |^ (2 * n) = (th |^ n) |^ 2 & (- 1) |^ (2 * n) = 1 & (- 1) |^ ((2 * n) + 1) = - 1 )

proof end;

::$CT

Lm8: for n being Nat

for z being Complex 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;

definition

ex b_{1} being Function of REAL,REAL st

for d being Real holds b_{1} . d = Sum (d rExpSeq)

for b_{1}, b_{2} being Function of REAL,REAL st ( for d being Real holds b_{1} . d = Sum (d rExpSeq) ) & ( for d being Real holds b_{2} . d = Sum (d rExpSeq) ) holds

b_{1} = b_{2}
end;

func exp_R -> Function of REAL,REAL means :Def22: :: SIN_COS:def 22

for d being Real holds it . d = Sum (d rExpSeq);

existence for d being Real holds it . d = Sum (d rExpSeq);

ex b

for d being Real holds b

proof end;

uniqueness for b

b

proof end;

:: deftheorem Def22 defines exp_R SIN_COS:def 22 :

for b_{1} being Function of REAL,REAL holds

( b_{1} = exp_R iff for d being Real holds b_{1} . d = Sum (d rExpSeq) );

for b

( b

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

proof end;

Lm11: exp_R . 0 = 1

proof end;

definition

let z be Complex;

deffunc H_{2}( Nat) -> set = (z |^ ($1 + 1)) / (($1 + 2) !);

ex b_{1} being Complex_Sequence st

for n being Nat holds b_{1} . n = (z |^ (n + 1)) / ((n + 2) !)

for b_{1}, b_{2} being Complex_Sequence st ( for n being Nat holds b_{1} . n = (z |^ (n + 1)) / ((n + 2) !) ) & ( for n being Nat holds b_{2} . n = (z |^ (n + 1)) / ((n + 2) !) ) holds

b_{1} = b_{2}
_{3}( Nat) -> set = (z |^ $1) / (($1 + 2) !);

ex b_{1} being Complex_Sequence st

for n being Nat holds b_{1} . n = (z |^ n) / ((n + 2) !)

for b_{1}, b_{2} being Complex_Sequence st ( for n being Nat holds b_{1} . n = (z |^ n) / ((n + 2) !) ) & ( for n being Nat holds b_{2} . n = (z |^ n) / ((n + 2) !) ) holds

b_{1} = b_{2}

end;
deffunc H

func z P_dt -> Complex_Sequence means :Def24: :: SIN_COS:def 24

for n being Nat holds it . n = (z |^ (n + 1)) / ((n + 2) !);

existence for n being Nat holds it . n = (z |^ (n + 1)) / ((n + 2) !);

ex b

for n being Nat holds b

proof end;

uniqueness for b

b

proof end;

deffunc H
func z P_t -> Complex_Sequence means :: SIN_COS:def 25

for n being Nat holds it . n = (z |^ n) / ((n + 2) !);

existence for n being Nat holds it . n = (z |^ n) / ((n + 2) !);

ex b

for n being Nat holds b

proof end;

uniqueness for b

b

proof end;

:: deftheorem Def24 defines P_dt SIN_COS:def 24 :

for z being Complex

for b_{2} being Complex_Sequence holds

( b_{2} = z P_dt iff for n being Nat holds b_{2} . n = (z |^ (n + 1)) / ((n + 2) !) );

for z being Complex

for b

( b

:: deftheorem defines P_t SIN_COS:def 25 :

for z being Complex

for b_{2} being Complex_Sequence holds

( b_{2} = z P_t iff for n being Nat holds b_{2} . n = (z |^ n) / ((n + 2) !) );

for z being Complex

for b

( b

Lm12: for p being Real

for z being Complex holds

( Re ((p * <i>) * z) = - (p * (Im z)) & Im ((p * <i>) * z) = p * (Re z) & Re (p * z) = p * (Re z) & Im (p * z) = p * (Im z) )

proof end;

Lm13: for p being Real

for z being Complex st p > 0 holds

( Re (z / (p * <i>)) = (Im z) / p & Im (z / (p * <i>)) = - ((Re z) / p) & |.(z / p).| = |.z.| / p )

proof end;

theorem Th57: :: SIN_COS:58

for p being Real st p > 0 holds

ex q being Real st

( q > 0 & ( for z being Complex st |.z.| < q holds

|.(Sum (z P_dt)).| < p ) )

ex q being Real st

( q > 0 & ( for z being Complex st |.z.| < q holds

|.(Sum (z P_dt)).| < p ) )

proof end;

theorem Th58: :: SIN_COS:59

for z, z1 being Complex holds (Sum ((z1 + z) ExpSeq)) - (Sum (z1 ExpSeq)) = ((Sum (z1 ExpSeq)) * z) + ((z * (Sum (z P_dt))) * (Sum (z1 ExpSeq)))

proof end;

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

proof end;

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

proof end;

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

proof end;

definition
end;

Lm14: ( dom (tan | [.0,1.]) = [.0,1.] & ( for th being Real 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 st th in ].0,1.[ holds

diff (tan,th) > 0 ) )

proof end;

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

proof end;

definition

existence

ex b_{1} being Real st

( tan . (b_{1} / 4) = 1 & b_{1} in ].0,4.[ )

for b_{1}, b_{2} being Real st tan . (b_{1} / 4) = 1 & b_{1} in ].0,4.[ & tan . (b_{2} / 4) = 1 & b_{2} in ].0,4.[ holds

b_{1} = b_{2}

end;
ex b

( tan . (b

proof end;

uniqueness for b

b

proof end;

:: deftheorem Def28 defines PI SIN_COS:def 28 :

for b_{1} being Real holds

( b_{1} = PI iff ( tan . (b_{1} / 4) = 1 & b_{1} in ].0,4.[ ) );

for b

( b

theorem Th73: :: SIN_COS:74

for th1, th2 being Real holds

( sin . (th1 + th2) = ((sin . th1) * (cos . th2)) + ((cos . th1) * (sin . th2)) & cos . (th1 + th2) = ((cos . th1) * (cos . th2)) - ((sin . th1) * (sin . th2)) )

( 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:75

theorem Th75: :: SIN_COS:76

( 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:77

theorem Th77: :: SIN_COS:78

for th being Real 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) )

( 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:79

Lm17: for th being Real st th in [.0,1.] holds

sin . th >= 0

proof end;

:: from COMPLEX2, 2006.03,06, A.T.

registration

coherence

sin is continuous

cos is continuous

exp_R is continuous

end;
sin is continuous

proof end;

coherence cos is continuous

proof end;

coherence exp_R is continuous

proof end;