:: Trigonometric Functions and Existence of Circle Ratio
::  by Yuguang Yang and Yasunari Shidama
::
:: Received October 22, 1998
:: Copyright (c) 1998-2021 Association of Mizar Users
::           (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.

environ

 vocabularies NUMBERS, REAL_1, XREAL_0, SUBSET_1, COMSEQ_1, SEQ_1, FDIFF_1,
      XXREAL_0, CARD_1, COMPLEX1, FUNCT_1, RELAT_1, XCMPLX_0, ARYTM_3, NAT_1,
      REALSET1, NEWTON, ARYTM_1, VALUED_1, SERIES_1, PREPOWER, CARD_3, SEQ_2,
      ORDINAL2, SQUARE_1, VALUED_0, XXREAL_2, FUNCT_2, TARSKI, RCOMP_1,
      XXREAL_1, PARTFUN1, XBOOLE_0, FCONT_1, SIN_COS, FUNCT_7, ORDINAL1;
 notations TARSKI, XBOOLE_0, SUBSET_1, ORDINAL1, NUMBERS, XXREAL_0, XREAL_0,
      ABIAN, XCMPLX_0, COMPLEX1, REAL_1, RELAT_1, FUNCT_1, RELSET_1, FCONT_1,
      FUNCT_2, VALUED_1, SEQ_1, SEQ_2, FDIFF_1, SERIES_1, NAT_1, NEWTON,
      SQUARE_1, PARTFUN1, VALUED_0, RCOMP_1, NAT_D, RFUNCT_1, COMSEQ_1,
      COMSEQ_2, COMSEQ_3, PREPOWER;
 constructors PARTFUN1, FUNCT_4, ARYTM_0, REAL_1, SQUARE_1, NAT_1, RCOMP_1,
      RFUNCT_1, COMSEQ_2, RFUNCT_2, FCONT_1, FDIFF_1, PREPOWER, COMSEQ_3,
      NAT_D, RECDEF_1, SEQM_3, SERIES_1, SEQ_2, VALUED_1, RELSET_1, ABIAN,
      BINOP_2, RVSUM_1, XXREAL_2, NUMBERS;
 registrations XBOOLE_0, ORDINAL1, RELSET_1, FUNCT_2, NUMBERS, XCMPLX_0,
      XXREAL_0, XREAL_0, SQUARE_1, NAT_1, MEMBERED, RCOMP_1, COMSEQ_2, FDIFF_1,
      NEWTON, COMSEQ_3, VALUED_0, VALUED_1, SEQ_4, FCONT_3, ABIAN, SEQ_2,
      INT_1;
 requirements REAL, NUMERALS, SUBSET, BOOLE, ARITHM;


begin

reserve q,th,r for Real,
  a,b,p for Real,
  w,z for Complex,
  k,l,m,n,n1,n2 for Nat,
  seq,seq1,seq2,cq1 for Complex_Sequence,
  rseq,rseq1,rseq2 for Real_Sequence,
  rr for set,
  hy1 for 0-convergent non-zero Real_Sequence;

:: Some definitions and properties of complex sequence

definition
  let m,k be natural Number;
  func CHK(m,k) -> Element of COMPLEX equals
:: SIN_COS:def 1

  1 if m <= k otherwise 0;
end;

registration
  let m,k be natural Number;
  cluster CHK(m,k) -> real;
end;

scheme :: SIN_COS:sch 1
 ExComplexCASE{F(Nat,Nat)->Complex}:
  for k holds ex seq st for n holds (n <= k implies seq.n=F(k,n)) &
  (n > k implies seq.n=0);

scheme :: SIN_COS:sch 2
 ExRealCASE{F(Nat,Nat)->Real}: for k holds
  ex rseq st for n holds (n <= k implies rseq.n=F(k,n)) &
  (n > k implies rseq.n=0);

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

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

definition
  let n be Nat;
  redefine func n! equals
:: SIN_COS:def 3
  Prod_real_n.n;
end;

definition
  let z be Complex;
  func z ExpSeq -> Complex_Sequence means
:: SIN_COS:def 4

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

definition
  let a be Real;
  func a rExpSeq -> Real_Sequence means
:: SIN_COS:def 5

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

theorem :: SIN_COS:1
  0! = 1 & n! <> 0 & (n+1)! = n! * (n+1);

theorem :: SIN_COS:2
  (0 < k implies ((k-'1)! ) * k = k!) &
  (k <= m implies ((m-'k)!) * (m+1-k) = (m+1-'k)!);

definition
  let n be Nat;
  func Coef(n) -> Complex_Sequence means
:: SIN_COS:def 6

  for k be Nat holds
  (k <= n implies it.k = n! /( (k! ) * ((n-'k)! ))) &
  (k > n implies it.k = 0);
end;

definition
  let n be Nat;
  func Coef_e(n) -> Complex_Sequence means
:: SIN_COS:def 7

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

definition
  let seq;
  func Shift seq -> Complex_Sequence means
:: SIN_COS:def 8

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

definition
  let n;
  let z,w be Complex;
  func Expan(n,z,w) -> Complex_Sequence means
:: SIN_COS:def 9

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

definition
  let n;
  let z,w be Complex;
  func Expan_e(n,z,w) -> Complex_Sequence means
:: SIN_COS:def 10

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

definition
  let n;
  let z,w be Complex;
  func Alfa(n,z,w) -> Complex_Sequence means
:: SIN_COS:def 11

  for k be Nat holds ( k <= n implies
  it.k= (z ExpSeq).k * Partial_Sums(w ExpSeq).(n-'k) ) &
  ( n < k implies it.k=0);
end;

definition
  let a,b be Real;
  let n be Nat;
  func Conj(n,a,b) -> Real_Sequence means
:: SIN_COS:def 12
  for k be 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);
end;

definition
  let z, w be Complex;
  let n be Nat;
  func Conj(n,z,w) -> Complex_Sequence means
:: SIN_COS:def 13

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

theorem :: SIN_COS:3
  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;

theorem :: SIN_COS:4
  0 < k implies (Shift(seq)).k=seq.(k-'1);

theorem :: SIN_COS:5
  Partial_Sums(seq).k=Partial_Sums(Shift(seq)).k+seq.k;

theorem :: SIN_COS:6
  (z+w) |^ n = Partial_Sums(Expan(n,z,w)).n;

theorem :: SIN_COS:7
  Expan_e(n,z,w)=(1r/(n! )) (#) Expan(n,z,w);

theorem :: SIN_COS:8
  ((z+w) |^ n) / (n!) = Partial_Sums(Expan_e(n,z,w)).n;

theorem :: SIN_COS:9
  ((0c qua Complex) ExpSeq is absolutely_summable)
  & Sum((0c qua Complex) ExpSeq)=1r;

registration
  let z be Complex;
  cluster z ExpSeq -> absolutely_summable;
end;

theorem :: SIN_COS:10
  (z ExpSeq).0 = 1 & Expan(0,z,w).0 = 1;

theorem :: SIN_COS:11
  l <= k implies (Alfa(k+1,z,w)).l = (Alfa(k,z,w)).l + Expan_e(k+1,z,w).l;

theorem :: SIN_COS:12
  Partial_Sums((Alfa(k+1,z,w))).k = (Partial_Sums(( Alfa(k,z,w)))).k
  + (Partial_Sums(( Expan_e(k+1,z,w) ))).k;

theorem :: SIN_COS:13
  (z ExpSeq).k=(Expan_e(k,z,w)).k;

theorem :: SIN_COS:14
  Partial_Sums((z+w) ExpSeq).n = Partial_Sums(Alfa(n,z,w)).n;

theorem :: SIN_COS:15
  Partial_Sums(z ExpSeq).k * Partial_Sums(w ExpSeq).k
  -Partial_Sums((z+w) ExpSeq).k = Partial_Sums(Conj(k,z,w)).k;

theorem :: SIN_COS:16
  |. 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);

theorem :: SIN_COS:17
  1 <= Sum(|.z.| rExpSeq);

theorem :: SIN_COS:18
  0 <= (|. z .| rExpSeq).n;

theorem :: SIN_COS:19
  |.(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);

theorem :: SIN_COS:20
  |.Partial_Sums(|.Conj(k,z,w).|).n.|=Partial_Sums(|.Conj(k,z,w).|).n;

theorem :: SIN_COS:21
  for p being Real st p>0 ex n st for k st n <= k
  holds |.Partial_Sums(|.Conj(k,z,w).|).k.| < p;

theorem :: SIN_COS:22
  (for k holds seq.k=Partial_Sums((Conj(k,z,w))).k) implies
  seq is convergent & lim seq = 0;

begin :: Definition of Exponential Function on Complex

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

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

definition
  let z be Complex;
  func exp z -> Complex equals
:: SIN_COS:def 15
  exp.z;
end;

definition
  let z be Complex;
  redefine func exp z -> Element of COMPLEX;
end;

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

begin :: Definition of Sinus, Cosine, and Exponential Function on REAL

reserve d for Real;

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

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

definition
  let th be Real;
  func sin th -> number equals
:: SIN_COS:def 17
  sin.th;
end;

registration
  let th be Real;
  cluster sin th -> real;
end;

definition
  func cos -> Function of REAL, REAL means
:: SIN_COS:def 18

  for d holds it.d = Re(Sum(d*<i> ExpSeq));
end;

definition
  let th be Real;
  func cos th -> number equals
:: SIN_COS:def 19
  cos.th;
end;

registration
  let th be Real;
  cluster cos th -> real;
end;

theorem :: SIN_COS:24
  dom(sin)=REAL & dom(cos)=REAL;

theorem :: SIN_COS:25
  exp(th*<i>)=cos(th)+(sin th)*<i>;

theorem :: SIN_COS:26
  (exp((th*<i>)))*'=exp(-(th*<i>));

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

reserve th,th1,th2 for Real;

theorem :: SIN_COS:28
  (cos.th)^2+(sin.th)^2=1 & (cos.th)*(cos.th)+(sin.th)*(sin.th)=1;

theorem :: SIN_COS:29
  (cos(th))^2+(sin(th))^2=1 &
  (cos(th))*(cos(th))+(sin(th))*(sin(th))=1;

theorem :: SIN_COS:30
  cos.0=1 & sin.0=0 & cos.(-th)=cos.th & sin.(-th)=-sin.th;

theorem :: SIN_COS:31
  cos(0)=1 & sin(0)=0 & cos(-th)=cos(th) & sin(-th)=-sin(th);

definition
  let th be Real;
  func th P_sin -> Real_Sequence means
:: SIN_COS:def 20

  for n holds it.n = (-1)|^ n * (th)|^ (2*n+1)/((2*n+1)!);
  func th P_cos -> Real_Sequence means
:: SIN_COS:def 21

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

theorem :: SIN_COS:32
  for z being Complex,
  k holds z|^ (2*k) = (z|^ k)|^ 2& z|^ (2*k)= (z|^ 2)|^ k;

theorem :: SIN_COS:33
  for th holds (th*<i>) |^ (2*k)=(-1)|^ k* (th |^ (2*k))
  & (th*<i>) |^ (2*k+1)=(-1)|^ k* (th |^ (2*k+1))*<i>;

::$CT

theorem :: SIN_COS:35
  for th 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);

theorem :: SIN_COS:36
  for th 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));

theorem :: SIN_COS:37
  cos.th=Sum(th P_cos) & sin.th=Sum(th P_sin);

theorem :: SIN_COS:38
  for p,th,rseq st rseq is convergent &
  lim(rseq)=th & (for n holds rseq.n >= p) holds th >= p;

theorem :: SIN_COS:39
  n <= k implies n! <= k!;

theorem :: SIN_COS:40
  0<=th & th <=1 & n<=k implies th |^ k <= th |^ n;

::$CT

theorem :: SIN_COS:42
  for p being Real holds Im(Sum(p ExpSeq))=0;

theorem :: SIN_COS:43
  cos.1>0 & sin.1>0 & cos.1<sin.1;

theorem :: SIN_COS:44
  for th holds th rExpSeq=Re(th ExpSeq);

theorem :: SIN_COS:45
  for th holds th rExpSeq is summable &
  Sum(th rExpSeq)=Re(Sum(th ExpSeq));

theorem :: SIN_COS:46
  for p,q being Real holds
  Sum((p+q) rExpSeq) = (Sum(p rExpSeq))*(Sum(q rExpSeq));

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

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

definition
  let th be Real;
  func exp_R th -> number equals
:: SIN_COS:def 23
  exp_R.th;
end;

registration
  let th be Real;
  cluster exp_R th -> real;
end;

theorem :: SIN_COS:47
  dom(exp_R)=REAL;

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

theorem :: SIN_COS:49
  for th holds exp th=exp_R th;

theorem :: SIN_COS:50
  for p,q being Real holds exp_R(p+q) = exp_R(p) * exp_R(q);

theorem :: SIN_COS:51
  exp_R(0) =1;

theorem :: SIN_COS:52
  th > 0 implies exp_R.th >=1;

theorem :: SIN_COS:53
  th < 0 implies 0<exp_R.th & exp_R.th <=1;

theorem :: SIN_COS:54
  exp_R.th>0;

theorem :: SIN_COS:55
  exp_R(th)>0;

begin :: Differential of sin, cos, and Exponential Function

definition
  let z be Complex;
  func z P_dt -> Complex_Sequence means
:: SIN_COS:def 24

  for n holds it.n = (z|^(n+1))/((n+2)!);
  func z P_t -> Complex_Sequence means
:: SIN_COS:def 25
  for n holds it.n = (z|^(n))/((n+2)!);
end;

theorem :: SIN_COS:56
  for z being Complex holds z P_dt is absolutely_summable;

theorem :: SIN_COS:57
  for z being Complex holds z*(Sum(z P_dt))=(Sum(z ExpSeq))-1r-z;

theorem :: SIN_COS:58
  for p st p>0 holds ex q st q>0 &
  for z being Complex st |.z.|<q holds |.(Sum(z P_dt)).|<p;

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

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

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

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

theorem :: SIN_COS:63
  cos is_differentiable_in p & diff(cos,p)=-sin.p;

theorem :: SIN_COS:64
  sin is_differentiable_in p & diff(sin,p)=cos.p;

theorem :: SIN_COS:65
  exp_R is_differentiable_in p & diff(exp_R,p)=exp_R.p;

theorem :: SIN_COS:66
  exp_R is_differentiable_on REAL & diff(exp_R,th)=exp_R.th;

theorem :: SIN_COS:67
  cos is_differentiable_on REAL & diff(cos,th)=-sin.th;

theorem :: SIN_COS:68
  sin is_differentiable_on REAL & diff(sin,th)=cos.th;

theorem :: SIN_COS:69
  th in [.0,1 .] implies 0<cos.th & cos.th>=1/2;

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

theorem :: SIN_COS:70
  [.0,1 .] c= dom tan & ].0,1 .[ c= dom tan;

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

theorem :: SIN_COS:72
  th1 in ].0,1 .[ & th2 in ].0,1 .[ & tan.th1=tan.th2 implies th1=th2;

begin :: Existence of Circle Ratio

definition
  func PI -> Real means
:: SIN_COS:def 28

  tan.(it/4) = 1 & it in ]. 0, 4 .[;
end;

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

begin :: Formulas of sin and cos

theorem :: SIN_COS:74
  sin.(th1+th2)=(sin.(th1)) *(cos.(th2))+(cos.(th1)) * (sin.(th2)) &
  cos.(th1+th2)=(cos.(th1)) *(cos.(th2))-(sin.(th1)) * (sin.(th2));

theorem :: SIN_COS:75
  sin(th1+th2)=(sin(th1)) *(cos(th2))+(cos(th1)) * (sin(th2)) &
  cos(th1+th2)=(cos(th1)) *(cos(th2))-(sin(th1)) * (sin(th2));

theorem :: 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;

theorem :: SIN_COS:77
  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;

theorem :: SIN_COS:78
  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;

theorem :: SIN_COS:79
  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);

theorem :: SIN_COS:80
  th in ].0,PI/2.[ implies cos.th > 0;

theorem :: SIN_COS:81
  th in ].0,PI/2.[ implies cos(th) > 0;

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

theorem :: SIN_COS:82
  sin(a-b) = sin(a)*cos(b)-cos(a)*sin(b);

theorem :: SIN_COS:83
  cos(a-b) = cos(a)*cos(b)+sin(a)*sin(b);

registration
  cluster sin -> continuous;
  cluster cos -> continuous;
  cluster exp_R -> continuous;
end;